let F be Subset of PL-WFF; :: thesis: for A being Element of PL-WFF holds
( F |- A iff ex G being Subset of PL-WFF st
( G c= F & G is finite & G |- A ) )
let A be Element of PL-WFF ; :: thesis: ( F |- A iff ex G being Subset of PL-WFF st
( G c= F & G is finite & G |- A ) )
hereby :: thesis: ( ex G being Subset of PL-WFF st
( G c= F & G is finite & G |- A ) implies F |- A )
assume F |- A ; :: thesis: ex G being Subset of PL-WFF st
( G c= F & G is finite & G |- A )
then consider f being FinSequence of PL-WFF such that
A1: ( f . (len f) = A & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds
prc f,F,i ) ) ;
deffunc H1( Nat) -> set = f . $1;
set w2 = { i where i is Element of NAT : ( 1 <= i & i <= len f ) } ;
set G = { H1(i) where i is Element of NAT : i in { i where i is Element of NAT : ( 1 <= i & i <= len f ) } } ;
F1: { i where i is Element of NAT : ( 1 <= i & i <= len f ) } c= Seg (len f)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { i where i is Element of NAT : ( 1 <= i & i <= len f ) } or x in Seg (len f) )
assume x in { i where i is Element of NAT : ( 1 <= i & i <= len f ) } ; :: thesis: x in Seg (len f)
then consider i being Element of NAT such that
F2: ( i = x & 1 <= i & i <= len f ) ;
reconsider i1 = i as Nat ;
thus x in Seg (len f) by F2; :: thesis: verum
end;
A8: { i where i is Element of NAT : ( 1 <= i & i <= len f ) } is finite by F1;
A4: { H1(i) where i is Element of NAT : i in { i where i is Element of NAT : ( 1 <= i & i <= len f ) } } c= PL-WFF
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H1(i) where i is Element of NAT : i in { i where i is Element of NAT : ( 1 <= i & i <= len f ) } } or x in PL-WFF )
assume x in { H1(i) where i is Element of NAT : i in { i where i is Element of NAT : ( 1 <= i & i <= len f ) } } ; :: thesis: x in PL-WFF
then consider i being Element of NAT such that
A6: ( x = H1(i) & i in { i where i is Element of NAT : ( 1 <= i & i <= len f ) } ) ;
consider j being Element of NAT such that
A9: ( j = i & 1 <= j & j <= len f ) by A6;
i in dom f by FINSEQ_3:25, A9;
then A7: x in rng f by A6, FUNCT_1:def 3;
rng f c= PL-WFF by FINSEQ_1:def 4;
hence x in PL-WFF by A7; :: thesis: verum
end;
{ H1(i) where i is Element of NAT : i in { i where i is Element of NAT : ( 1 <= i & i <= len f ) } } is finite from FRAENKEL:sch 21(A8);
then reconsider G = { H1(i) where i is Element of NAT : i in { i where i is Element of NAT : ( 1 <= i & i <= len f ) } } as finite Subset of PL-WFF by A4;
now :: thesis: for i being Nat st 1 <= i & i <= len f holds
prc f,F /\ G,i
let i be Nat; :: thesis: ( 1 <= i & i <= len f implies prc f,F /\ G,b1 )
assume A6: ( 1 <= i & i <= len f ) ; :: thesis: prc f,F /\ G,b1
then prc f,F,i by A1;
per cases then ( f . i in PL_axioms or f . i in F or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & f /. j,f /. k MP_rule f /. i ) ) ;
suppose f . i in PL_axioms ; :: thesis: prc f,F /\ G,b1
hence prc f,F /\ G,i ; :: thesis: verum
end;
suppose A5: f . i in F ; :: thesis: prc f,F /\ G,b1
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
i1 in { i where i is Element of NAT : ( 1 <= i & i <= len f ) } by A6;
then f . i in G ;
hence prc f,F /\ G,i by A5, XBOOLE_0:def 4; :: thesis: verum
end;
suppose ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & f /. j,f /. k MP_rule f /. i ) ; :: thesis: prc f,F /\ G,b1
hence prc f,F /\ G,i ; :: thesis: verum
end;
end;
end;
then F /\ G |- A by A1;
hence ex G being Subset of PL-WFF st
( G c= F & G is finite & G |- A ) by XBOOLE_1:17; :: thesis: verum
end;
given G being Subset of PL-WFF such that A1: ( G c= F & G is finite & G |- A ) ; :: thesis: F |- A
thus F |- A by A1, monmp; :: thesis: verum