let Al be QC-alphabet ; :: thesis: for Al2 being Al -expanding QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al2) st PHI is Subset of (CQC-WFF Al) holds
PHI is Al -Consistent
let Al2 be Al -expanding QC-alphabet ; :: thesis: for PHI being Consistent Subset of (CQC-WFF Al2) st PHI is Subset of (CQC-WFF Al) holds
PHI is Al -Consistent
let PHI be Consistent Subset of (CQC-WFF Al2); :: thesis: ( PHI is Subset of (CQC-WFF Al) implies PHI is Al -Consistent )
assume PHI is Subset of (CQC-WFF Al) ; :: thesis: PHI is Al -Consistent
for S being Subset of (CQC-WFF Al) st PHI = S holds
S is Consistent

proof

let S be Subset of (CQC-WFF Al); :: thesis: ( PHI = S implies S is Consistent )
assume A1: PHI = S ; :: thesis: S is Consistent
assume A2: S is Inconsistent ; :: thesis: contradiction
PHI |- 'not' (VERUM Al2)

proof

consider f being FinSequence of CQC-WFF Al such that
A3: ( rng f c= S & |- f ^ <*('not' (VERUM Al))*> ) by A2, GOEDELCP:24, HENMODEL:def 1;
set f2 = f;
for x being object st x in rng f holds
x in CQC-WFF Al2

proof

let x be object ; :: thesis: ( x in rng f implies x in CQC-WFF Al2 )
assume A4: x in rng f ; :: thesis: x in CQC-WFF Al2
x in PHI by A1, A3, A4;
hence x in CQC-WFF Al2 ; :: thesis: verum

end;

then reconsider f2 = f as FinSequence of CQC-WFF Al2 by FINSEQ_1:def 4, TARSKI:def 3;
consider PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] such that
A5: ( PR is a_proof & f ^ <*('not' (VERUM Al))*> = (PR . (len PR)) `1 ) by A3, CALCUL_1:def 9;
A6: ( PR <> {} & ( for n being Nat st 1 <= n & n <= len PR holds
PR,n is_a_correct_step ) ) by A5, CALCUL_1:def 8;
set PR2 = PR;
PR is FinSequence of [:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:]

proof

for p being object st p in CQC-WFF Al holds
p in CQC-WFF Al2

proof

let p be object ; :: thesis: ( p in CQC-WFF Al implies p in CQC-WFF Al2 )
assume p in CQC-WFF Al ; :: thesis: p in CQC-WFF Al2
then p is Element of CQC-WFF Al2 by Th7;
hence p in CQC-WFF Al2 ; :: thesis: verum

end;

then A7: ( CQC-WFF Al c= CQC-WFF Al2 & rng PR c= [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] ) ;
for x being object st x in set_of_CQC-WFF-seq Al holds
x in set_of_CQC-WFF-seq Al2

proof

let x be object ; :: thesis: ( x in set_of_CQC-WFF-seq Al implies x in set_of_CQC-WFF-seq Al2 )
assume x in set_of_CQC-WFF-seq Al ; :: thesis: x in set_of_CQC-WFF-seq Al2
then reconsider x = x as FinSequence of CQC-WFF Al by CALCUL_1:def 6;
rng x c= CQC-WFF Al2 by A7;
then x is FinSequence of CQC-WFF Al2 by FINSEQ_1:def 4;
hence x in set_of_CQC-WFF-seq Al2 by CALCUL_1:def 6; :: thesis: verum

end;

then set_of_CQC-WFF-seq Al c= set_of_CQC-WFF-seq Al2 ;
then [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] c= [:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:] by ZFMISC_1:95;
then rng PR c= [:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:] ;
hence PR is FinSequence of [:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:] by FINSEQ_1:def 4; :: thesis: verum

end;

then reconsider PR2 = PR as FinSequence of [:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:] ;
A8: PR2 is a_proof

proof

for n being Nat st 1 <= n & n <= len PR2 holds
PR2,n is_a_correct_step

proof

let n be Nat; :: thesis: ( 1 <= n & n <= len PR2 implies PR2,n is_a_correct_step )
assume A9: ( 1 <= n & n <= len PR2 ) ; :: thesis: PR2,n is_a_correct_step
A10: ( ( for i being Nat st 1 <= i & i < n holds
(PR2 . i) `1 in set_of_CQC-WFF-seq Al2 ) & (PR2 . n) `1 in set_of_CQC-WFF-seq Al2 )

proof

thus for i being Nat st 1 <= i & i < n holds
(PR2 . i) `1 in set_of_CQC-WFF-seq Al2 :: thesis: (PR2 . n) `1 in set_of_CQC-WFF-seq Al2

proof

let i be Nat; :: thesis: ( 1 <= i & i < n implies (PR2 . i) `1 in set_of_CQC-WFF-seq Al2 )
assume A11: ( 1 <= i & i < n ) ; :: thesis: (PR2 . i) `1 in set_of_CQC-WFF-seq Al2
set k = (len PR2) - n;
reconsider k = (len PR2) - n as Element of NAT by A9, NAT_1:21;
len PR2 = n + k ;
then A12: ( 1 <= i & i <= len PR2 ) by A11, NAT_1:12;
dom PR2 = Seg (len PR2) by FINSEQ_1:def 3;
then i in dom PR2 by A12, FINSEQ_1:1;
then PR2 . i in rng PR2 by FUNCT_1:def 3;
hence (PR2 . i) `1 in set_of_CQC-WFF-seq Al2 by MCART_1:10; :: thesis: verum

end;

dom PR2 = Seg (len PR2) by FINSEQ_1:def 3;
then n in dom PR2 by A9, FINSEQ_1:1;
then PR2 . n in rng PR2 by FUNCT_1:def 3;
hence (PR2 . n) `1 in set_of_CQC-WFF-seq Al2 by MCART_1:10; :: thesis: verum

end;

A13: PR,n is_a_correct_step by A5, CALCUL_1:def 8, A9;
not not (PR . n) `2 = 0 & ... & not (PR . n) `2 = 9 by CALCUL_1:31, A9;

per cases then ( (PR2 . n) `2 = 0 or (PR2 . n) `2 = 1 or (PR2 . n) `2 = 2 or (PR2 . n) `2 = 3 or (PR2 . n) `2 = 4 or (PR2 . n) `2 = 5 or (PR2 . n) `2 = 6 or (PR2 . n) `2 = 7 or (PR2 . n) `2 = 8 or (PR2 . n) `2 = 9 ) ;

suppose A14: (PR2 . n) `2 = 0 ; :: thesis: PR2,n is_a_correct_step

then consider g2 being FinSequence of CQC-WFF Al such that
A15: ( Suc g2 is_tail_of Ant g2 & (PR2 . n) `1 = g2 ) by A13, CALCUL_1:def 7;
g2 is FinSequence of CQC-WFF Al2 by A10, A15, CALCUL_1:def 6;
then consider g being FinSequence of CQC-WFF Al2 such that
A16: g = g2 ;
A17: ( Suc g = Suc g2 & Ant g = Ant g2 ) by A16, Th11;
thus PR2,n is_a_correct_step by A14, A15, A16, A17, CALCUL_1:def 7; :: thesis: verum

end;

suppose A18: (PR2 . n) `2 = 1 ; :: thesis: PR2,n is_a_correct_step

then consider g2 being FinSequence of CQC-WFF Al such that
A19: (PR . n) `1 = g2 ^ <*(VERUM Al)*> by A13, CALCUL_1:def 7;
g2 ^ <*(VERUM Al)*> is FinSequence of CQC-WFF Al2 by A10, A19, CALCUL_1:def 6;
then consider gp being FinSequence of CQC-WFF Al2 such that
A20: gp = g2 ^ <*(VERUM Al)*> ;
len gp <> 0 by A20;
then consider g being FinSequence of CQC-WFF Al2, v being Element of CQC-WFF Al2 such that
A21: gp = g ^ <*v*> by FINSEQ_2:19;
v = VERUM Al2 by A20, A21, FINSEQ_2:17;
hence PR2,n is_a_correct_step by A18, A19, A20, A21, CALCUL_1:def 7; :: thesis: verum

end;

suppose A22: (PR2 . n) `2 = 2 ; :: thesis: PR2,n is_a_correct_step

then consider i being Nat, g2, h2 being FinSequence of CQC-WFF Al such that
A23: ( 1 <= i & i < n & Ant g2 is_Subsequence_of Ant h2 & Suc g2 = Suc h2 & (PR2 . i) `1 = g2 & (PR2 . n) `1 = h2 ) by A13, CALCUL_1:def 7;
( g2 in set_of_CQC-WFF-seq Al2 & h2 in set_of_CQC-WFF-seq Al2 ) by A10, A23;
then ( h2 is FinSequence of CQC-WFF Al2 & g2 is FinSequence of CQC-WFF Al2 ) by CALCUL_1:def 6;
then consider g, h being FinSequence of CQC-WFF Al2 such that
A24: ( g = g2 & h = h2 ) ;
A25: Suc g = Suc g2 by A24, Th11
.= Suc h by A23, A24, Th11 ;
consider N being Subset of NAT such that
A26: Ant g2 c= Seq ((Ant h2) | N) by A23, CALCUL_1:def 4;
(Ant h2) | N = (Ant h) | N by A24, Th11;
then Ant g c= Seq ((Ant h) | N) by A24, A26, Th11;
then A27: Ant g is_Subsequence_of Ant h by CALCUL_1:def 4;
thus PR2,n is_a_correct_step by A22, A23, A24, A25, A27, CALCUL_1:def 7; :: thesis: verum

end;

suppose A28: (PR2 . n) `2 = 3 ; :: thesis: PR2,n is_a_correct_step

then consider i, j being Nat, g, h being FinSequence of CQC-WFF Al such that
A29: ( 1 <= i & i < n & 1 <= j & j < i & len g > 1 & len h > 1 & Ant (Ant g) = Ant (Ant h) & 'not' (Suc (Ant g)) = Suc (Ant h) & Suc g = Suc h & g = (PR2 . j) `1 & h = (PR2 . i) `1 & (Ant (Ant g)) ^ <*(Suc g)*> = (PR2 . n) `1 ) by A13, CALCUL_1:def 7;
( (PR2 . j) `1 = g & (PR2 . i) `1 = h & j < n ) by A29, XXREAL_0:2;
then ( g in set_of_CQC-WFF-seq Al2 & h in set_of_CQC-WFF-seq Al2 ) by A10, A29;
then ( h is FinSequence of CQC-WFF Al2 & g is FinSequence of CQC-WFF Al2 ) by CALCUL_1:def 6;
then consider g2, h2 being FinSequence of CQC-WFF Al2 such that
A30: ( g2 = g & h2 = h ) ;
A31: ( Ant g2 = Ant g & Ant h2 = Ant h ) by A30, Th11;
then A32: Ant (Ant g2) = Ant (Ant g) by Th11
.= Ant (Ant h2) by A29, A31, Th11 ;
A33: 'not' (Suc (Ant g2)) = 'not' (Al2 -Cast (Suc (Ant g))) by A31, Th11
.= Suc (Ant h2) by A29, A31, Th11 ;
A34: Suc g2 = Suc g by A30, Th11
.= Suc h2 by A29, A30, Th11 ;
A35: (PR2 . n) `1 = (Ant (Ant g)) ^ <*(Suc g2)*> by A29, A30, Th11
.= (Ant (Ant g2)) ^ <*(Suc g2)*> by A31, Th11 ;
thus PR2,n is_a_correct_step by A28, A29, A30, A32, A33, A34, A35, CALCUL_1:def 7; :: thesis: verum

end;

suppose A36: (PR2 . n) `2 = 4 ; :: thesis: PR2,n is_a_correct_step

then consider i, j being Nat, g, h being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al such that
A37: ( 1 <= i & i < n & 1 <= j & j < i & len g > 1 & Ant g = Ant h & Suc (Ant g) = 'not' p & 'not' (Suc g) = Suc h & g = (PR2 . j) `1 & h = (PR2 . i) `1 & (Ant (Ant g)) ^ <*p*> = (PR2 . n) `1 ) by A13, CALCUL_1:def 7;
( (PR2 . j) `1 = g & (PR2 . i) `1 = h & j < n ) by A37, XXREAL_0:2;
then ( g in set_of_CQC-WFF-seq Al2 & h in set_of_CQC-WFF-seq Al2 ) by A10, A37;
then ( h is FinSequence of CQC-WFF Al2 & g is FinSequence of CQC-WFF Al2 ) by CALCUL_1:def 6;
then consider g2, h2 being FinSequence of CQC-WFF Al2 such that
A38: ( g2 = g & h2 = h ) ;
A39: Ant g2 = Ant g by A38, Th11
.= Ant h2 by A37, A38, Th11 ;
Ant g2 = Ant g by A38, Th11;
then A40: Suc (Ant g2) = 'not' (Al2 -Cast p) by A37, Th11;
A41: 'not' (Suc g2) = 'not' (Al2 -Cast (Suc g)) by A38, Th11
.= Suc h2 by A37, A38, Th11 ;
Ant g2 = Ant g by A38, Th11;
then (Ant (Ant g2)) ^ <*(Al2 -Cast p)*> = (PR2 . n) `1 by Th11, A37;
hence PR2,n is_a_correct_step by A36, A37, A38, A39, A40, A41, CALCUL_1:def 7; :: thesis: verum

end;

suppose A42: (PR2 . n) `2 = 5 ; :: thesis: PR2,n is_a_correct_step

then consider i, j being Nat, g, h being FinSequence of CQC-WFF Al such that
A43: ( 1 <= i & i < n & 1 <= j & j < i & Ant g = Ant h & g = (PR2 . j) `1 & h = (PR2 . i) `1 & (Ant g) ^ <*((Suc g) '&' (Suc h))*> = (PR2 . n) `1 ) by A13, CALCUL_1:def 7;
( (PR2 . j) `1 = g & (PR2 . i) `1 = h & j < n ) by A43, XXREAL_0:2;
then ( g in set_of_CQC-WFF-seq Al2 & h in set_of_CQC-WFF-seq Al2 ) by A10, A43;
then ( h is FinSequence of CQC-WFF Al2 & g is FinSequence of CQC-WFF Al2 ) by CALCUL_1:def 6;
then consider g2, h2 being FinSequence of CQC-WFF Al2 such that
A44: ( g = g2 & h = h2 ) ;
( Al2 -Cast (Suc g) = Suc g2 & Al2 -Cast (Suc h) = Suc h2 ) by A44, Th11;
then A45: (Ant g2) ^ <*((Suc g2) '&' (Suc h2))*> = (PR2 . n) `1 by A43, A44, Th11;
Ant g2 = Ant g by A44, Th11
.= Ant h2 by A43, A44, Th11 ;
hence PR2,n is_a_correct_step by A42, A43, A44, A45, CALCUL_1:def 7; :: thesis: verum

end;

suppose A46: (PR2 . n) `2 = 6 ; :: thesis: PR2,n is_a_correct_step

then consider i being Nat, g being FinSequence of CQC-WFF Al, p, q being Element of CQC-WFF Al such that
A47: ( 1 <= i & i < n & p '&' q = Suc g & g = (PR2 . i) `1 & (Ant g) ^ <*p*> = (PR2 . n) `1 ) by A13, CALCUL_1:def 7;
g in set_of_CQC-WFF-seq Al2 by A10, A47;
then g is FinSequence of CQC-WFF Al2 by CALCUL_1:def 6;
then consider g2 being FinSequence of CQC-WFF Al2 such that
A48: g = g2 ;
A49: Suc g2 = (Al2 -Cast p) '&' (Al2 -Cast q) by A47, A48, Th11;
(Ant g2) ^ <*p*> = (PR2 . n) `1 by A47, A48, Th11;
hence PR2,n is_a_correct_step by A46, A47, A48, A49, CALCUL_1:def 7; :: thesis: verum

end;

suppose A50: (PR2 . n) `2 = 7 ; :: thesis: PR2,n is_a_correct_step

then consider i being Nat, g being FinSequence of CQC-WFF Al, p, q being Element of CQC-WFF Al such that
A51: ( 1 <= i & i < n & p '&' q = Suc g & g = (PR2 . i) `1 & (Ant g) ^ <*q*> = (PR2 . n) `1 ) by A13, CALCUL_1:def 7;
g in set_of_CQC-WFF-seq Al2 by A10, A51;
then g is FinSequence of CQC-WFF Al2 by CALCUL_1:def 6;
then reconsider g2 = g as FinSequence of CQC-WFF Al2 ;
A52: Suc g2 = (Al2 -Cast p) '&' (Al2 -Cast q) by A51, Th11;
(Ant g2) ^ <*(Al2 -Cast q)*> = (PR2 . n) `1 by A51, Th11;
hence PR2,n is_a_correct_step by A50, A51, A52, CALCUL_1:def 7; :: thesis: verum

end;

suppose A53: (PR2 . n) `2 = 8 ; :: thesis: PR2,n is_a_correct_step

then consider i being Nat, g being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al, x, y being bound_QC-variable of Al such that
A54: ( 1 <= i & i < n & Suc g = All (x,p) & g = (PR2 . i) `1 & (Ant g) ^ <*(p . (x,y))*> = (PR2 . n) `1 ) by A13, CALCUL_1:def 7;
g in set_of_CQC-WFF-seq Al2 by A10, A54;
then g is FinSequence of CQC-WFF Al2 by CALCUL_1:def 6;
then consider g2 being FinSequence of CQC-WFF Al2 such that
A55: g = g2 ;
( p is Element of CQC-WFF Al2 & x is bound_QC-variable of Al2 & y is bound_QC-variable of Al2 ) by Th4, Th7, TARSKI:def 3;
then consider q being Element of CQC-WFF Al2, a, b being bound_QC-variable of Al2 such that
A56: ( a = x & b = y & q = p ) ;
A57: (PR2 . n) `1 = (Ant g) ^ <*(q . (a,b))*> by A54, A56, Th17
.= (Ant g2) ^ <*(q . (a,b))*> by A55, Th11 ;
Suc g2 = All (a,q) by A54, A55, A56, Th11;
hence PR2,n is_a_correct_step by A53, A54, A55, A57, CALCUL_1:def 7; :: thesis: verum

end;

suppose A58: (PR2 . n) `2 = 9 ; :: thesis: PR2,n is_a_correct_step

then consider i being Nat, g being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al, x, y being bound_QC-variable of Al such that
A59: ( 1 <= i & i < n & Suc g = p . (x,y) & not y in still_not-bound_in (Ant g) & not y in still_not-bound_in (All (x,p)) & g = (PR2 . i) `1 & (Ant g) ^ <*(All (x,p))*> = (PR2 . n) `1 ) by A13, CALCUL_1:def 7;
g in set_of_CQC-WFF-seq Al2 by A10, A59;
then g is FinSequence of CQC-WFF Al2 by CALCUL_1:def 6;
then consider g2 being FinSequence of CQC-WFF Al2 such that
A60: g = g2 ;
( p is Element of CQC-WFF Al2 & x is bound_QC-variable of Al2 & y is bound_QC-variable of Al2 ) by Th4, Th7, TARSKI:def 3;
then consider q being Element of CQC-WFF Al2, a, b being bound_QC-variable of Al2 such that
A61: ( q = p & a = x & b = y ) ;
A62: Suc g2 = Suc g by A60, Th11
.= q . (a,b) by A59, A61, Th17 ;
A63: still_not-bound_in (All (x,p)) = still_not-bound_in (Al2 -Cast (All (x,p))) by Th12
.= still_not-bound_in (All (a,q)) by A61 ;
A64: not b in still_not-bound_in (Ant g2)

proof

assume b in still_not-bound_in (Ant g2) ; :: thesis: contradiction
then consider i being Nat, r being Element of CQC-WFF Al2 such that
A65: ( i in dom (Ant g2) & r = (Ant g2) . i & b in still_not-bound_in r ) by CALCUL_1:def 5;
A66: dom (Ant g2) = dom (Ant g) by A60, Th11;
r = (Ant g) . i by A60, A65, Th11;
then reconsider r = r as Element of CQC-WFF Al by A65, A66, FINSEQ_2:11;
( i in dom (Ant g) & Al2 -Cast r = (Ant g) . i & b in still_not-bound_in (Al2 -Cast r) ) by A60, A65, Th11;
then ( i in dom (Ant g) & r = (Ant g) . i & y in still_not-bound_in r ) by A61, Th12;
hence contradiction by A59, CALCUL_1:def 5; :: thesis: verum

end;

(Ant g2) ^ <*(All (a,q))*> = (PR2 . n) `1 by A59, A60, A61, Th11;
hence PR2,n is_a_correct_step by A58, A59, A60, A61, A62, A63, A64, CALCUL_1:def 7; :: thesis: verum

end;

end;

end;

hence PR2 is a_proof by A6, CALCUL_1:def 8; :: thesis: verum

end;

|- f2 ^ <*('not' (VERUM Al2))*> by A5, A8, CALCUL_1:def 9;
hence PHI |- 'not' (VERUM Al2) by A1, A3, HENMODEL:def 1; :: thesis: verum

end;

hence contradiction by GOEDELCP:24; :: thesis: verum

end;

hence PHI is Al -Consistent ; :: thesis: verum