let Al be QC-alphabet ; :: thesis: for PHI being Consistent Subset of (CQC-WFF Al) holds PHI \/ (Example_Formulae_of Al) is Consistent Subset of (CQC-WFF (FCEx Al))
let PHI be Consistent Subset of (CQC-WFF Al); :: thesis: PHI \/ (Example_Formulae_of Al) is Consistent Subset of (CQC-WFF (FCEx Al))
reconsider Al2 = FCEx Al as Al -expanding QC-alphabet ;
for s being object st s in CQC-WFF Al holds
s in CQC-WFF Al2

proof

let s be object ; :: thesis: ( s in CQC-WFF Al implies s in CQC-WFF Al2 )
assume s in CQC-WFF Al ; :: thesis: s in CQC-WFF Al2
then reconsider s = s as Element of CQC-WFF Al ;
s is Element of CQC-WFF Al2 by QC_TRANS:7;
hence s in CQC-WFF Al2 ; :: thesis: verum

end;

then A1: CQC-WFF Al c= CQC-WFF Al2 ;
then ( PHI c= CQC-WFF Al2 & Example_Formulae_of Al c= CQC-WFF Al2 ) ;
then reconsider B = PHI \/ (Example_Formulae_of Al) as Subset of (CQC-WFF Al2) by XBOOLE_1:8;
B is Consistent

proof

assume B is Inconsistent ; :: thesis: contradiction
then consider CHI2 being Subset of (CQC-WFF Al2) such that
A2: ( CHI2 c= B & CHI2 is finite & CHI2 is Inconsistent ) by HENMODEL:7;
reconsider CHI2 = CHI2 as finite Subset of (CQC-WFF Al2) by A2;
consider Al1 being countable QC-alphabet such that
A3: ( CHI2 is finite Subset of (CQC-WFF Al1) & Al2 is Al1 -expanding ) by QC_TRANS:20;
reconsider Al2 = Al2 as Al1 -expanding QC-alphabet by A3;
consider CHI1 being Subset of (CQC-WFF Al1) such that
A4: CHI1 = CHI2 by A3;
reconsider CHI1 = CHI1 as finite Subset of (CQC-WFF Al1) by A4;
set PHI1 = CHI1 /\ PHI;
( CHI1 /\ PHI c= CHI1 & CHI1 c= CQC-WFF Al1 ) by XBOOLE_1:18;
then reconsider PHI1 = CHI1 /\ PHI as Subset of (CQC-WFF Al1) by XBOOLE_1:1;
reconsider Al2 = Al2 as Al -expanding QC-alphabet ;
PHI is Subset of (CQC-WFF Al2) by A1, XBOOLE_1:1;
then consider PHIp being Subset of (CQC-WFF Al2) such that
A5: PHIp = PHI ;
set PHI2 = CHI2 /\ PHIp;
reconsider PHI2 = CHI2 /\ PHIp as Subset of (CQC-WFF Al2) ;
PHI1 is Consistent

proof

reconsider Al2 = Al2 as Al1 -expanding QC-alphabet ;
PHI is Al2 -Consistent by QC_TRANS:23;
then ( PHIp is Consistent & PHI2 c= PHIp ) by A5, QC_TRANS:def 2, XBOOLE_1:18;
then ( PHI2 is Consistent & PHI2 = PHI1 ) by A4, A5, QC_TRANS:22;
then PHI2 is Al1 -Consistent by QC_TRANS:18;
hence PHI1 is Consistent by A4, A5, QC_TRANS:def 2; :: thesis: verum

end;

then reconsider PHI1 = PHI1 as Consistent Subset of (CQC-WFF Al1) ;
still_not-bound_in PHI1 is finite ;
then consider CZ being Consistent Subset of (CQC-WFF Al1), JH being Henkin_interpretation of CZ such that
A6: JH, valH Al1 |= PHI1 by GOEDELCP:34;
consider A2 being non empty set , J2 being interpretation of Al2,A2, v2 being Element of Valuations_in (Al2,A2) such that
A7: J2,v2 |= PHI2 by A4, A5, A6, QC_TRANS:21;
set Ex2 = CHI2 /\ (Example_Formulae_of Al);
reconsider Ex2 = CHI2 /\ (Example_Formulae_of Al) as Subset of (CQC-WFF Al2) ;
A8: CHI2 = CHI2 /\ (PHIp \/ (Example_Formulae_of Al)) by A2, A5, XBOOLE_1:28
.= PHI2 \/ Ex2 by XBOOLE_1:23 ;
ex A being non empty set ex J being interpretation of Al2,A ex v being Element of Valuations_in (Al2,A) st J,v |= PHI2 \/ Ex2

proof

defpred S₁[ set ] means ex A being non empty set ex J being interpretation of Al2,A ex v being Element of Valuations_in (Al2,A) ex Ex3 being Subset of (CQC-WFF Al2) st
( Ex3 = $1 & J,v |= PHI2 \/ Ex3 );
A9: Ex2 is finite ;
J2,v2 |= PHI2 \/ ({} (CQC-WFF Al2)) by A7;
then A10: S₁[ {} ] ;
A11: for b, B being set st b in Ex2 & B c= Ex2 & S₁[B] holds
S₁[B \/ {b}]

proof

let b, B be set ; :: thesis: ( b in Ex2 & B c= Ex2 & S₁[B] implies S₁[B \/ {b}] )
assume A12: ( b in Ex2 & B c= Ex2 & S₁[B] ) ; :: thesis: S₁[B \/ {b}]
reconsider B = B as Subset of (CQC-WFF Al2) by A12;
consider A being non empty set , J being interpretation of Al2,A, v being Element of Valuations_in (Al2,A) such that
A13: J,v |= PHI2 \/ B by A12;
Ex2 c= Example_Formulae_of Al by XBOOLE_1:18;
then b in Example_Formulae_of Al by A12;
then consider p being Element of CQC-WFF Al, x being bound_QC-variable of Al such that
A14: b = Example_Formula_of (p,x) ;
set fc = Example_of (p,x);
set x2 = Al2 -Cast x;
set p2 = Al2 -Cast p;
reconsider fc = Example_of (p,x), x2 = Al2 -Cast x as bound_QC-variable of Al2 ;
reconsider p2 = Al2 -Cast p as Element of CQC-WFF Al2 ;
reconsider b = b as Element of CQC-WFF Al2 by A14;
A15: ( J,v |= b implies S₁[B \/ {b}] )

proof

assume A16: J,v |= b ; :: thesis: S₁[B \/ {b}]
for q2 being Element of CQC-WFF Al2 st q2 in PHI2 \/ (B \/ {b}) holds
J,v |= q2

proof

let q2 be Element of CQC-WFF Al2; :: thesis: ( q2 in PHI2 \/ (B \/ {b}) implies J,v |= q2 )
assume q2 in PHI2 \/ (B \/ {b}) ; :: thesis: J,v |= q2
then q2 in (PHI2 \/ B) \/ {b} by XBOOLE_1:4;
then A17: ( q2 in PHI2 \/ B or q2 in {b} ) by XBOOLE_0:def 3;

per cases ( q2 in PHI2 \/ B or not q2 in PHI2 \/ B ) ;

suppose q2 in PHI2 \/ B ; :: thesis: J,v |= q2

hence J,v |= q2 by A13, CALCUL_1:def 11; :: thesis: verum

end;

suppose not q2 in PHI2 \/ B ; :: thesis: J,v |= q2

hence J,v |= q2 by A16, A17, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence S₁[B \/ {b}] by CALCUL_1:def 11; :: thesis: verum

end;

per cases ( not J,v |= Ex (x2,p2) or J,v |= Ex (x2,p2) ) ;

suppose not J,v |= Ex (x2,p2) ; :: thesis: S₁[B \/ {b}]

then J,v |= 'not' (Ex (x2,p2)) by VALUAT_1:17;
hence S₁[B \/ {b}] by A14, A15, Th8; :: thesis: verum

end;

suppose J,v |= Ex (x2,p2) ; :: thesis: S₁[B \/ {b}]

then consider a being Element of A such that
A18: J,v . (x2 | a) |= p2 by GOEDELCP:9;
reconsider vp = v . (fc | a) as Element of Valuations_in (Al2,A) ;
A19: for p2 being Element of CQC-WFF Al2 st p2 is Element of CQC-WFF Al holds
v | (still_not-bound_in p2) = vp | (still_not-bound_in p2)

proof

let p2 be Element of CQC-WFF Al2; :: thesis: ( p2 is Element of CQC-WFF Al implies v | (still_not-bound_in p2) = vp | (still_not-bound_in p2) )
assume p2 is Element of CQC-WFF Al ; :: thesis: v | (still_not-bound_in p2) = vp | (still_not-bound_in p2)
then consider pp being Element of CQC-WFF Al such that
A20: pp = p2 ;
not [ the free_symbol of Al,[x,p]] in QC-symbols Al by Def2;
then not [4,[ the free_symbol of Al,[x,p]]] in [:{4},(QC-symbols Al):] by ZFMISC_1:87;
then not fc in bound_QC-variables Al by QC_LANG1:def 4;
then not fc in still_not-bound_in pp ;
then not fc in still_not-bound_in (Al2 -Cast pp) by QC_TRANS:12;
then not fc in still_not-bound_in p2 by A20, QC_TRANS:def 3;
hence v | (still_not-bound_in p2) = vp | (still_not-bound_in p2) by CALCUL_1:26; :: thesis: verum

end;

p2 = p by QC_TRANS:def 3;
then v | (still_not-bound_in p2) = vp | (still_not-bound_in p2) by A19;
then (v . (x2 | a)) | (still_not-bound_in p2) = (vp . (x2 | a)) | (still_not-bound_in p2) by SUBLEMMA:64;
then ( J,vp . (x2 | a) |= p2 & vp . fc = a ) by A18, SUBLEMMA:49, SUBLEMMA:68;
then A21: J,vp |= p2 . (x2,fc) by CALCUL_1:24;
for q2 being Element of CQC-WFF Al2 st q2 in PHI2 \/ (B \/ {b}) holds
J,vp |= q2

proof

let q2 be Element of CQC-WFF Al2; :: thesis: ( q2 in PHI2 \/ (B \/ {b}) implies J,vp |= q2 )
assume q2 in PHI2 \/ (B \/ {b}) ; :: thesis: J,vp |= q2
then q2 in (PHI2 \/ B) \/ {b} by XBOOLE_1:4;
then A22: ( q2 in PHI2 \/ B or q2 in {b} ) by XBOOLE_0:def 3;

per cases ( q2 in PHI2 or q2 in B or ( not q2 in PHI2 & not q2 in B ) ) ;

suppose A23: q2 in PHI2 ; :: thesis: J,vp |= q2

then A24: q2 in PHI2 \/ B by XBOOLE_0:def 3;
( PHI2 c= PHI & PHI c= CQC-WFF Al ) by A5, XBOOLE_1:18;
then PHI2 c= CQC-WFF Al ;
then ( v | (still_not-bound_in q2) = vp | (still_not-bound_in q2) & J,v |= q2 ) by A13, A19, A23, A24, CALCUL_1:def 11;
hence J,vp |= q2 by SUBLEMMA:68; :: thesis: verum

end;

suppose A25: q2 in B ; :: thesis: J,vp |= q2

B c= Example_Formulae_of Al by A12, XBOOLE_1:18;
then q2 in Example_Formulae_of Al by A25;
then consider r being Element of CQC-WFF Al, y being bound_QC-variable of Al such that
A26: q2 = Example_Formula_of (r,y) ;
set fcr = Example_of (r,y);
set y2 = Al2 -Cast y;
set r2 = Al2 -Cast r;
reconsider fcr = Example_of (r,y), y2 = Al2 -Cast y as bound_QC-variable of Al2 ;
reconsider r2 = Al2 -Cast r as Element of CQC-WFF Al2 ;

per cases ( fcr = fc or not fcr = fc ) ;

suppose fcr = fc ; :: thesis: J,vp |= q2

then [ the free_symbol of Al,[x,p]] = [ the free_symbol of Al,[y,r]] by XTUPLE_0:1;
then [x,p] = [y,r] by XTUPLE_0:1;
then ( r = p & x = y ) by XTUPLE_0:1;
hence J,vp |= q2 by A21, A26, Th8; :: thesis: verum

end;

suppose A27: not fcr = fc ; :: thesis: J,vp |= q2

A28: q2 in PHI2 \/ B by A25, XBOOLE_0:def 3;

per cases ( J,v |= 'not' (Ex (y2,r2)) or not J,v |= 'not' (Ex (y2,r2)) ) ;

suppose A29: J,v |= 'not' (Ex (y2,r2)) ; :: thesis: J,vp |= q2

set fml = 'not' (Ex (y2,r2));
'not' (Ex (y,r)) = Al2 -Cast ('not' (Ex (y,r))) by QC_TRANS:def 3
.= 'not' (Al2 -Cast (Ex (y,r))) by QC_TRANS:8
.= 'not' (Ex (y2,r2)) by Th7 ;
then ( v | (still_not-bound_in ('not' (Ex (y2,r2)))) = vp | (still_not-bound_in ('not' (Ex (y2,r2)))) & J,v |= 'not' (Ex (y2,r2)) ) by A19, A29;
then J,vp |= 'not' (Ex (y2,r2)) by SUBLEMMA:68;
hence J,vp |= q2 by A26, Th8; :: thesis: verum

end;

suppose not J,v |= 'not' (Ex (y2,r2)) ; :: thesis: J,vp |= q2

then J,v |= r2 . (y2,fcr) by A13, A26, A28, Th8, CALCUL_1:def 11;
then consider a2 being Element of A such that
A30: ( v . fcr = a2 & J,v . (y2 | a2) |= r2 ) by CALCUL_1:24;
A31: vp . fcr = a2 by A27, A30, SUBLEMMA:48;
not [ the free_symbol of Al,[x,p]] in QC-symbols Al by Def2;
then not [4,[ the free_symbol of Al,[x,p]]] in [:{4},(QC-symbols Al):] by ZFMISC_1:87;
then not fc in bound_QC-variables Al by QC_LANG1:def 4;
then not fc in still_not-bound_in r ;
then not fc in still_not-bound_in r2 by QC_TRANS:12;
then (v . (fc | a)) | (still_not-bound_in r2) = v | (still_not-bound_in r2) by CALCUL_1:26;
then (vp . (y2 | a2)) | (still_not-bound_in r2) = (v . (y2 | a2)) | (still_not-bound_in r2) by SUBLEMMA:64;
then J,vp . (y2 | a2) |= r2 by A30, SUBLEMMA:68;
then J,vp |= r2 . (y2,fcr) by A31, CALCUL_1:24;
hence J,vp |= q2 by A26, Th8; :: thesis: verum

end;

end;

end;

end;

end;

suppose ( not q2 in PHI2 & not q2 in B ) ; :: thesis: J,vp |= q2

then q2 = b by A22, TARSKI:def 1, XBOOLE_0:def 3;
hence J,vp |= q2 by A14, A21, Th8; :: thesis: verum

end;

end;

end;

hence S₁[B \/ {b}] by CALCUL_1:def 11; :: thesis: verum

end;

end;

end;

S₁[Ex2] from FINSET_1:sch 2(A9, A10, A11);
hence ex A being non empty set ex J being interpretation of Al2,A ex v being Element of Valuations_in (Al2,A) st J,v |= PHI2 \/ Ex2 ; :: thesis: verum

end;

hence contradiction by A2, A8, HENMODEL:12; :: thesis: verum

end;

hence PHI \/ (Example_Formulae_of Al) is Consistent Subset of (CQC-WFF (FCEx Al)) ; :: thesis: verum