let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for X being Subset of (CQC-WFF Al) st p is_formal_provable_from X holds
X |= p

let p be Element of CQC-WFF Al; :: thesis: for X being Subset of (CQC-WFF Al) st p is_formal_provable_from X holds
X |= p

let X be Subset of (CQC-WFF Al); :: thesis: ( p is_formal_provable_from X implies X |= p )
assume p is_formal_provable_from X ; :: thesis: X |= p
then consider f being FinSequence of CQC-WFF Al such that
A1: rng (Ant f) c= X and
A2: Suc f = p and
A3: |- f ;
consider PR being FinSequence of such that
A4: PR is a_proof and
A5: f = (PR . (len PR)) `1 by A3;
PR <> {} by A4;
then A6: 1 <= len PR by FINSEQ_1:20;
defpred S1[ Nat] means ( \$1 <= len PR implies for m being Nat st 1 <= m & m <= \$1 holds
ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) );
A7: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; :: thesis: S1[k + 1]
assume A9: k + 1 <= len PR ; :: thesis: for m being Nat st 1 <= m & m <= k + 1 holds
ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g )

A10: k <= k + 1 by NAT_1:11;
let m be Nat; :: thesis: ( 1 <= m & m <= k + 1 implies ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) )

assume that
A11: 1 <= m and
A12: m <= k + 1 ; :: thesis: ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g )

A13: m <= len PR by ;
A14: now :: thesis: ( m = k + 1 implies ex g being object st
( g = (PR . m) `1 & ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) ) )
assume A15: m = k + 1 ; :: thesis: ex g being object st
( g = (PR . m) `1 & ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) )

take g = (PR . m) `1 ; :: thesis: ( g = (PR . m) `1 & ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) )

thus g = (PR . m) `1 ; :: thesis: ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g )

reconsider g = (PR . m) `1 as FinSequence of CQC-WFF Al by ;
A16: PR,m is_a_correct_step by A4, A11, A13;
now :: thesis: Ant g |= Suc g
not not (PR . m) `2 = 0 & ... & not (PR . m) `2 = 9 by ;
per cases ) `2 = 0 or (PR . m) `2 = 1 or (PR . m) `2 = 2 or (PR . m) `2 = 3 or (PR . m) `2 = 4 or (PR . m) `2 = 5 or (PR . m) `2 = 6 or (PR . m) `2 = 7 or (PR . m) `2 = 8 or (PR . m) `2 = 9 ) ;
suppose (PR . m) `2 = 0 ; :: thesis: Ant g |= Suc g
then ex f being FinSequence of CQC-WFF Al st
( Suc f is_tail_of Ant f & (PR . m) `1 = f ) by ;
hence Ant g |= Suc g by Th15; :: thesis: verum
end;
suppose (PR . m) `2 = 2 ; :: thesis: Ant g |= Suc g
then consider i being Nat, f, f1 being FinSequence of CQC-WFF Al such that
A17: 1 <= i and
A18: i < m and
A19: ( Ant f is_Subsequence_of Ant f1 & Suc f = Suc f1 & (PR . i) `1 = f & (PR . m) `1 = f1 ) by ;
i <= k by ;
then ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by ;
hence Ant g |= Suc g by ; :: thesis: verum
end;
suppose (PR . m) `2 = 3 ; :: thesis: Ant g |= Suc g
then consider i, j being Nat, f, f1 being FinSequence of CQC-WFF Al such that
A20: 1 <= i and
A21: i < m and
A22: 1 <= j and
A23: j < i and
A24: ( len f > 1 & len f1 > 1 & Ant (Ant f) = Ant (Ant f1) & 'not' (Suc (Ant f)) = Suc (Ant f1) & Suc f = Suc f1 & f = (PR . j) `1 & f1 = (PR . i) `1 ) and
A25: (Ant (Ant f)) ^ <*(Suc f)*> = (PR . m) `1 by ;
A26: ( Ant g = Ant (Ant f) & Suc g = Suc f ) by ;
A27: i <= k by ;
then j <= k by ;
then A28: ex h1 being FinSequence of CQC-WFF Al st
( h1 = (PR . j) `1 & Ant h1 |= Suc h1 ) by ;
ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by ;
hence Ant g |= Suc g by ; :: thesis: verum
end;
suppose (PR . m) `2 = 4 ; :: thesis: Ant g |= Suc g
then consider i, j being Nat, f, f1 being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al such that
A29: 1 <= i and
A30: i < m and
A31: 1 <= j and
A32: j < i and
A33: ( len f > 1 & Ant f = Ant f1 & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc f1 & f = (PR . j) `1 & f1 = (PR . i) `1 ) and
A34: (Ant (Ant f)) ^ <*p*> = (PR . m) `1 by ;
A35: ( Ant g = Ant (Ant f) & Suc g = p ) by ;
A36: i <= k by ;
then j <= k by ;
then A37: ex h1 being FinSequence of CQC-WFF Al st
( h1 = (PR . j) `1 & Ant h1 |= Suc h1 ) by ;
ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by ;
hence Ant g |= Suc g by ; :: thesis: verum
end;
suppose (PR . m) `2 = 5 ; :: thesis: Ant g |= Suc g
then consider i, j being Nat, f, f1 being FinSequence of CQC-WFF Al such that
A38: 1 <= i and
A39: i < m and
A40: 1 <= j and
A41: j < i and
A42: ( Ant f = Ant f1 & f = (PR . j) `1 & f1 = (PR . i) `1 ) and
A43: (Ant f) ^ <*((Suc f) '&' (Suc f1))*> = (PR . m) `1 by ;
A44: ( Ant g = Ant f & Suc g = (Suc f) '&' (Suc f1) ) by ;
A45: i <= k by ;
then j <= k by ;
then A46: ex h1 being FinSequence of CQC-WFF Al st
( h1 = (PR . j) `1 & Ant h1 |= Suc h1 ) by ;
ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by ;
hence Ant g |= Suc g by ; :: thesis: verum
end;
suppose (PR . m) `2 = 6 ; :: thesis: Ant g |= Suc g
then consider i being Nat, f being FinSequence of CQC-WFF Al, p, q being Element of CQC-WFF Al such that
A47: 1 <= i and
A48: i < m and
A49: ( p '&' q = Suc f & f = (PR . i) `1 ) and
A50: (Ant f) ^ <*p*> = (PR . m) `1 by ;
i <= k by ;
then A51: ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by ;
( Ant g = Ant f & Suc g = p ) by ;
hence Ant g |= Suc g by ; :: thesis: verum
end;
suppose (PR . m) `2 = 7 ; :: thesis: Ant g |= Suc g
then consider i being Nat, f being FinSequence of CQC-WFF Al, p, q being Element of CQC-WFF Al such that
A52: 1 <= i and
A53: i < m and
A54: ( p '&' q = Suc f & f = (PR . i) `1 ) and
A55: (Ant f) ^ <*q*> = (PR . m) `1 by ;
i <= k by ;
then A56: ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by ;
( Ant g = Ant f & Suc g = q ) by ;
hence Ant g |= Suc g by ; :: thesis: verum
end;
suppose (PR . m) `2 = 8 ; :: thesis: Ant g |= Suc g
then consider i being Nat, f being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al, x, y being bound_QC-variable of Al such that
A57: 1 <= i and
A58: i < m and
A59: ( Suc f = All (x,p) & f = (PR . i) `1 ) and
A60: (Ant f) ^ <*(p . (x,y))*> = (PR . m) `1 by ;
i <= k by ;
then A61: ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by ;
( Ant g = Ant f & Suc g = p . (x,y) ) by ;
hence Ant g |= Suc g by ; :: thesis: verum
end;
suppose (PR . m) `2 = 9 ; :: thesis: Ant g |= Suc g
then consider i being Nat, f being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al, x, y being bound_QC-variable of Al such that
A62: 1 <= i and
A63: i < m and
A64: ( Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 ) and
A65: (Ant f) ^ <*(All (x,p))*> = (PR . m) `1 by ;
i <= k by ;
then A66: ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by ;
( Ant g = Ant f & Suc g = All (x,p) ) by ;
hence Ant g |= Suc g by ; :: thesis: verum
end;
end;
end;
hence ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) ; :: thesis: verum
end;
( m <= k implies ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) ) by ;
hence ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) by ; :: thesis: verum
end;
A67: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A67, A7);
then consider g being FinSequence of CQC-WFF Al such that
A68: g = (PR . (len PR)) `1 and
A69: Ant g |= Suc g by A6;
let A be non empty set ; :: according to CALCUL_1:def 12 :: thesis: for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= X holds
J,v |= p

let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A) st J,v |= X holds
J,v |= p

let v be Element of Valuations_in (Al,A); :: thesis: ( J,v |= X implies J,v |= p )
assume J,v |= X ; :: thesis: J,v |= p
then for p being Element of CQC-WFF Al st p in rng (Ant f) holds
J,v |= p by A1;
then J,v |= rng (Ant f) ;
then J,v |= Ant g by ;
hence J,v |= p by A2, A5, A68, A69; :: thesis: verum