let X be Subset of CQC-WFF ; :: thesis: for p being Element of CQC-WFF holds
( X |- 'not' p iff not X \/ {p} is Consistent )
let p be Element of CQC-WFF ; :: thesis: ( X |- 'not' p iff not X \/ {p} is Consistent )
thus ( X |- 'not' p implies not X \/ {p} is Consistent ) :: thesis: ( not X \/ {p} is Consistent implies X |- 'not' p )

proof

assume X |- 'not' p ; :: thesis: not X \/ {p} is Consistent
then consider f being FinSequence of CQC-WFF such that
A1: rng f c= X and
A2: |- f ^ <*('not' p)*> by Def2;
set f2 = f ^ <*p*>;
set f1 = (f ^ <*p*>) ^ <*p*>;
A3: Ant ((f ^ <*p*>) ^ <*p*>) = f ^ <*p*> by CALCUL_1:5;
1 in Seg 1 by FINSEQ_1:3;
then 1 in dom <*p*> by FINSEQ_1:55;
then A4: (len f) + 1 in dom (Ant ((f ^ <*p*>) ^ <*p*>)) by A3, FINSEQ_1:41;
Suc ((f ^ <*p*>) ^ <*p*>) = p by CALCUL_1:5;
then (Ant ((f ^ <*p*>) ^ <*p*>)) . ((len f) + 1) = Suc ((f ^ <*p*>) ^ <*p*>) by A3, FINSEQ_1:59;
then Suc ((f ^ <*p*>) ^ <*p*>) is_tail_of Ant ((f ^ <*p*>) ^ <*p*>) by A4, CALCUL_1:def 16;
then A5: |- (f ^ <*p*>) ^ <*p*> by CALCUL_1:33;
A6: 0 + 1 <= len (f ^ <*p*>) by CALCUL_1:10;
( Ant (f ^ <*p*>) = f & Suc (f ^ <*p*>) = p ) by CALCUL_1:5;
then A7: rng (f ^ <*p*>) = (rng f) \/ {p} by A6, CALCUL_1:3;
|- (f ^ <*p*>) ^ <*('not' p)*> by A2, Th5;
then not f ^ <*p*> is Consistent by A5, Def4;
hence not X \/ {p} is Consistent by A1, A7, Th4, XBOOLE_1:9; :: thesis: verum

end;

thus ( not X \/ {p} is Consistent implies X |- 'not' p ) :: thesis: verum

proof

assume not X \/ {p} is Consistent ; :: thesis: X |- 'not' p
then X \/ {p} |- 'not' p by Th6;
then consider f being FinSequence of CQC-WFF such that
A8: rng f c= X \/ {p} and
A9: |- f ^ <*('not' p)*> by Def2;

now

set g = f - {p};
reconsider A = f " {p} as finite set ;
reconsider B = dom f as finite set ;
set n = card A;
set h = (f - {p}) ^ (IdFinS p,(card A));
A10: len (IdFinS p,(card A)) = card A by FINSEQ_1:def 18;
A c= B by RELAT_1:167;
then A11: A c= Seg (len f) by FINSEQ_1:def 3;

A12: now

let i be Element of NAT ; :: thesis: ( i in seq (len (f - {p})),(card A) implies i - (len (f - {p})) in dom (Sgm A) )
reconsider j = i - (len (f - {p})) as Integer ;
assume A13: i in seq (len (f - {p})),(card A) ; :: thesis: i - (len (f - {p})) in dom (Sgm A)
then A14: 1 + (len (f - {p})) <= i by CALCUL_2:1;
then A15: 1 <= j by XREAL_1:21;
i <= (card A) + (len (f - {p})) by A13, CALCUL_2:1;
then A16: j <= card A by XREAL_1:22;
0 <= j by A14, XREAL_1:21;
then reconsider j = j as Element of NAT by INT_1:16;
j in Seg (card A) by A15, A16, FINSEQ_1:3;
hence i - (len (f - {p})) in dom (Sgm A) by A11, FINSEQ_3:45; :: thesis: verum

end;

assume not rng f c= X ; :: thesis: X |- 'not' p
then consider a being set such that
A17: a in rng f and
A18: not a in X by TARSKI:def 3;
( a in X or a in {p} ) by A8, A17, XBOOLE_0:def 3;
then a = p by A18, TARSKI:def 1;
then consider i being Nat such that
A19: i in B and
A20: f . i = p by A17, FINSEQ_2:11;
reconsider C = B \ A as finite set ;
defpred S₁[ Nat, set ] means ( ( $1 in Seg (len (f - {p})) implies $2 = (Sgm (B \ A)) . $1 ) & ( $1 in seq (len (f - {p})),(card A) implies $2 = (Sgm A) . ($1 - (len (f - {p}))) ) );
A21: card C = (card B) - (card A) by CARD_2:63, RELAT_1:167
.= (card (Seg (len f))) - (card A) by FINSEQ_1:def 3
.= (len f) - (card A) by FINSEQ_1:78
.= len (f - {p}) by FINSEQ_3:66 ;
A22: for k being Nat st k in Seg (len ((f - {p}) ^ (IdFinS p,(card A)))) holds
ex a being set st S₁[k,a]

proof

let k be Nat; :: thesis: ( k in Seg (len ((f - {p}) ^ (IdFinS p,(card A)))) implies ex a being set st S₁[k,a] )
assume k in Seg (len ((f - {p}) ^ (IdFinS p,(card A)))) ; :: thesis: ex a being set st S₁[k,a]

now

assume A23: k in Seg (len (f - {p})) ; :: thesis: ex a being set st S₁[k,a]
take a = (Sgm (B \ A)) . k; :: thesis: S₁[k,a]
Seg (len (f - {p})) misses seq (len (f - {p})),(card A) by CALCUL_2:8;
hence S₁[k,a] by A23, XBOOLE_0:3; :: thesis: verum

end;

hence ex a being set st S₁[k,a] ; :: thesis: verum

end;

consider F being FinSequence such that
A24: ( dom F = Seg (len ((f - {p}) ^ (IdFinS p,(card A)))) & ( for k being Nat st k in Seg (len ((f - {p}) ^ (IdFinS p,(card A)))) holds
S₁[k,F . k] ) ) from FINSEQ_1:sch 1(A22);

now

let b be set ; :: thesis: ( b in C implies b in Seg (len f) )
assume b in C ; :: thesis: b in Seg (len f)
then b in dom f ;
hence b in Seg (len f) by FINSEQ_1:def 3; :: thesis: verum

end;

then A25: C c= Seg (len f) by TARSKI:def 3;
then A26: dom (Sgm C) = Seg (card C) by FINSEQ_3:45;
A27: rng F = B

proof

now

let a be set ; :: thesis: ( a in rng F implies a in B )
assume a in rng F ; :: thesis: a in B
then consider i being Nat such that
A28: i in dom F and
A29: F . i = a by FINSEQ_2:11;

A30: now

assume i in Seg (len (f - {p})) ; :: thesis: a in B
then ( a = (Sgm C) . i & i in dom (Sgm C) ) by A24, A25, A21, A28, A29, FINSEQ_3:45;
then a in rng (Sgm C) by FUNCT_1:12;
then a in C by A25, FINSEQ_1:def 13;
hence a in B ; :: thesis: verum

end;

A31: now

A32: rng (Sgm A) = A by A11, FINSEQ_1:def 13;
A33: A c= B by RELAT_1:167;
assume A34: i in seq (len (f - {p})),(card A) ; :: thesis: a in B
then a = (Sgm A) . (i - (len (f - {p}))) by A24, A28, A29;
then a in A by A12, A34, A32, FUNCT_1:12;
hence a in B by A33; :: thesis: verum

end;

i in (Seg (len (f - {p}))) \/ (seq (len (f - {p})),(card A)) by A10, A24, A28, Lm1;
hence a in B by A30, A31, XBOOLE_0:def 3; :: thesis: verum

end;

hence rng F c= B by TARSKI:def 3; :: according to XBOOLE_0:def 10 :: thesis: B c= rng F
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in B or a in rng F )
assume A35: a in B ; :: thesis: a in rng F

A36: now

now

let b be set ; :: thesis: ( b in C implies b in Seg (len f) )
assume b in C ; :: thesis: b in Seg (len f)
then b in dom f ;
hence b in Seg (len f) by FINSEQ_1:def 3; :: thesis: verum

end;

then A37: C c= Seg (len f) by TARSKI:def 3;
assume not a in A ; :: thesis: a in rng F
then a in C by A35, XBOOLE_0:def 5;
then a in rng (Sgm C) by A37, FINSEQ_1:def 13;
then consider i being Nat such that
A38: i in dom (Sgm C) and
A39: (Sgm C) . i = a by FINSEQ_2:11;
A40: 1 <= i by A38, FINSEQ_3:27;
len (Sgm C) = len (f - {p}) by A26, A21, FINSEQ_1:def 3;
then A41: i <= len (f - {p}) by A38, FINSEQ_3:27;
len (f - {p}) <= len ((f - {p}) ^ (IdFinS p,(card A))) by CALCUL_1:6;
then i <= len ((f - {p}) ^ (IdFinS p,(card A))) by A41, XXREAL_0:2;
then A42: i in Seg (len ((f - {p}) ^ (IdFinS p,(card A)))) by A40, FINSEQ_1:3;
i in Seg (len (f - {p})) by A40, A41, FINSEQ_1:3;
then a = F . i by A24, A39, A42;
hence a in rng F by A24, A42, FUNCT_1:12; :: thesis: verum

end;

now

assume A43: a in A ; :: thesis: a in rng F
rng (Sgm A) = A by A11, FINSEQ_1:def 13;
then consider i being Nat such that
A44: i in dom (Sgm A) and
A45: (Sgm A) . i = a by A43, FINSEQ_2:11;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
set m = i + (len (f - {p}));
len (Sgm A) = card A by A11, FINSEQ_3:44;
then i <= card A by A44, FINSEQ_3:27;
then A46: i + (len (f - {p})) <= (card A) + (len (f - {p})) by XREAL_1:8;
then i + (len (f - {p})) <= (len (f - {p})) + (len (IdFinS p,(card A))) by FINSEQ_1:def 18;
then A47: i + (len (f - {p})) <= len ((f - {p}) ^ (IdFinS p,(card A))) by FINSEQ_1:35;
A48: 1 <= i by A44, FINSEQ_3:27;
then 1 + (len (f - {p})) <= i + (len (f - {p})) by XREAL_1:8;
then A49: i + (len (f - {p})) in seq (len (f - {p})),(card A) by A46, CALCUL_2:1;
i <= i + (len (f - {p})) by NAT_1:11;
then 1 <= i + (len (f - {p})) by A48, XXREAL_0:2;
then i + (len (f - {p})) in dom ((f - {p}) ^ (IdFinS p,(card A))) by A47, FINSEQ_3:27;
then A50: i + (len (f - {p})) in Seg (len ((f - {p}) ^ (IdFinS p,(card A)))) by FINSEQ_1:def 3;
a = (Sgm A) . ((i + (len (f - {p}))) - (len (f - {p}))) by A45;
then a = F . (i + (len (f - {p}))) by A24, A49, A50;
hence a in rng F by A24, A50, FUNCT_1:12; :: thesis: verum

end;

hence a in rng F by A36; :: thesis: verum

end;

A51: len ((f - {p}) ^ (IdFinS p,(card A))) = (len (f - {p})) + (len (IdFinS p,(card A))) by FINSEQ_1:35
.= ((len f) - (card A)) + (len (IdFinS p,(card A))) by FINSEQ_3:66
.= ((len f) - (card A)) + (card A) by FINSEQ_1:def 18
.= len f ;
then A52: dom F = B by A24, FINSEQ_1:def 3;
then reconsider F = F as Relation of B,B by A27, RELSET_1:11;
( B = {} implies B = {} ) ;
then reconsider F = F as Function of B,B by A52, FUNCT_2:def 1;
F is one-to-one

proof

let a1 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not a1 in proj1 F or not b₁ in proj1 F or not F . a1 = F . b₁ or a1 = b₁ )
let a2 be set ; :: thesis: ( not a1 in proj1 F or not a2 in proj1 F or not F . a1 = F . a2 or a1 = a2 )
assume that
A53: a1 in dom F and
A54: a2 in dom F and
A55: F . a1 = F . a2 ; :: thesis: a1 = a2
A56: a2 in (Seg (len (f - {p}))) \/ (seq (len (f - {p})),(card A)) by A10, A24, A54, Lm1;

A57: now

assume A58: a1 in Seg (len (f - {p})) ; :: thesis: a1 = a2
then A59: a1 in dom (Sgm C) by A25, A21, FINSEQ_3:45;
F . a1 = (Sgm C) . a1 by A24, A53, A58;
then F . a1 in rng (Sgm C) by A59, FUNCT_1:12;
then A60: F . a1 in C by A25, FINSEQ_1:def 13;

A61: now

assume A62: a2 in seq (len (f - {p})),(card A) ; :: thesis: contradiction
then reconsider i = a2 as Element of NAT ;
(Sgm A) . (i - (len (f - {p}))) in rng (Sgm A) by A12, A62, FUNCT_1:12;
then F . a2 in rng (Sgm A) by A24, A54, A62;
then F . a2 in A by A11, FINSEQ_1:def 13;
hence contradiction by A55, A60, XBOOLE_0:def 5; :: thesis: verum

end;

now

assume A63: a2 in Seg (len (f - {p})) ; :: thesis: a1 = a2
then F . a2 = (Sgm C) . a2 by A24, A54;
then A64: (Sgm C) . a1 = (Sgm C) . a2 by A24, A53, A55, A58;
A65: Sgm C is one-to-one by A25, FINSEQ_3:99;
a2 in dom (Sgm C) by A25, A21, A63, FINSEQ_3:45;
hence a1 = a2 by A59, A64, A65, FUNCT_1:def 8; :: thesis: verum

end;

hence a1 = a2 by A56, A61, XBOOLE_0:def 3; :: thesis: verum

end;

A66: now

assume A67: a1 in seq (len (f - {p})),(card A) ; :: thesis: a1 = a2
then reconsider i = a1 as Element of NAT ;
A68: i - (len (f - {p})) in dom (Sgm A) by A12, A67;

A69: now

assume A70: a2 in seq (len (f - {p})),(card A) ; :: thesis: a1 = a2
then reconsider i1 = a2 as Element of NAT ;
F . a2 = (Sgm A) . (i1 - (len (f - {p}))) by A24, A54, A70;
then A71: (Sgm A) . (i1 - (len (f - {p}))) = (Sgm A) . (i - (len (f - {p}))) by A24, A53, A55, A67;
A72: Sgm A is one-to-one by A11, FINSEQ_3:99;
i1 - (len (f - {p})) in dom (Sgm A) by A12, A70;
then (i1 - (len (f - {p}))) + (len (f - {p})) = (i - (len (f - {p}))) + (len (f - {p})) by A68, A71, A72, FUNCT_1:def 8;
hence a1 = a2 ; :: thesis: verum

end;

(Sgm A) . (i - (len (f - {p}))) in rng (Sgm A) by A12, A67, FUNCT_1:12;
then F . a1 in rng (Sgm A) by A24, A53, A67;
then A73: F . a1 in A by A11, FINSEQ_1:def 13;

now

assume a2 in Seg (len (f - {p})) ; :: thesis: contradiction
then ( F . a2 = (Sgm C) . a2 & a2 in dom (Sgm C) ) by A24, A25, A21, A54, FINSEQ_3:45;
then F . a2 in rng (Sgm C) by FUNCT_1:12;
then F . a2 in C by A25, FINSEQ_1:def 13;
hence contradiction by A55, A73, XBOOLE_0:def 5; :: thesis: verum

end;

hence a1 = a2 by A56, A69, XBOOLE_0:def 3; :: thesis: verum

end;

a1 in (Seg (len (f - {p}))) \/ (seq (len (f - {p})),(card A)) by A10, A24, A53, Lm1;
hence a1 = a2 by A57, A66, XBOOLE_0:def 3; :: thesis: verum

end;

then reconsider F = F as Permutation of (dom f) by A27, FUNCT_2:83;
consider j being Nat such that
A74: j in dom F and
A75: F . j = i by A27, A19, FINSEQ_2:11;
A76: dom (Per f,F) = B by CALCUL_2:19
.= dom F by A24, A51, FINSEQ_1:def 3
.= dom ((f - {p}) ^ (IdFinS p,(card A))) by A24, FINSEQ_1:def 3 ;

A77: now

let k be Nat; :: thesis: ( k in dom ((f - {p}) ^ (IdFinS p,(card A))) implies (Per f,F) . k = ((f - {p}) ^ (IdFinS p,(card A))) . k )
assume A78: k in dom ((f - {p}) ^ (IdFinS p,(card A))) ; :: thesis: (Per f,F) . k = ((f - {p}) ^ (IdFinS p,(card A))) . k
A79: k in Seg (len ((f - {p}) ^ (IdFinS p,(card A)))) by A78, FINSEQ_1:def 3;

A80: now

A81: k in dom (F * f) by A76, A78, CALCUL_2:def 2;
given i being Nat such that A82: i in dom (IdFinS p,(card A)) and
A83: k = (len (f - {p})) + i ; :: thesis: (Per f,F) . k = ((f - {p}) ^ (IdFinS p,(card A))) . k
len (IdFinS p,(card A)) = card A by FINSEQ_1:def 18;
then A84: i <= card A by A82, FINSEQ_3:27;
then A85: k <= (card A) + (len (f - {p})) by A83, XREAL_1:8;
A86: 1 <= i by A82, FINSEQ_3:27;
then 1 + (len (f - {p})) <= k by A83, XREAL_1:8;
then A87: k in seq (len (f - {p})),(card A) by A85, CALCUL_2:1;
then F . k = (Sgm A) . (k - (len (f - {p}))) by A24, A79;
then F . k in rng (Sgm A) by A12, A87, FUNCT_1:12;
then F . k in A by A11, FINSEQ_1:def 13;
then f . (F . k) in {p} by FUNCT_1:def 13;
then f . (F . k) = p by TARSKI:def 1;
then (F * f) . k = p by A81, FUNCT_1:22;
then A88: (Per f,F) . k = p by CALCUL_2:def 2;
i in Seg (card A) by A86, A84, FINSEQ_1:3;
hence (Per f,F) . k = (IdFinS p,(card A)) . i by A88, FUNCOP_1:13
.= ((f - {p}) ^ (IdFinS p,(card A))) . k by A82, A83, FINSEQ_1:def 7 ;
:: thesis: verum

end;

now

assume A89: k in dom (f - {p}) ; :: thesis: (Per f,F) . k = ((f - {p}) ^ (IdFinS p,(card A))) . k
then A90: k in dom (Sgm C) by A26, A21, FINSEQ_1:def 3;
k in Seg (len (f - {p})) by A89, FINSEQ_1:def 3;
then A91: F . k = (Sgm C) . k by A24, A79;
k in dom (F * f) by A76, A78, CALCUL_2:def 2;
then (F * f) . k = f . ((Sgm C) . k) by A91, FUNCT_1:22;
hence (Per f,F) . k = f . ((Sgm C) . k) by CALCUL_2:def 2
.= ((Sgm C) * f) . k by A90, FUNCT_1:23
.= (f - {p}) . k by FINSEQ_3:def 1
.= ((f - {p}) ^ (IdFinS p,(card A))) . k by A89, FINSEQ_1:def 7 ;
:: thesis: verum

end;

hence (Per f,F) . k = ((f - {p}) ^ (IdFinS p,(card A))) . k by A78, A80, FINSEQ_1:38; :: thesis: verum

end;

then A92: Per f,F = (f - {p}) ^ (IdFinS p,(card A)) by A76, FINSEQ_1:17;
reconsider h = (f - {p}) ^ (IdFinS p,(card A)) as FinSequence of CQC-WFF by A76, A77, FINSEQ_1:17;
(F * f) . j = p by A20, A74, A75, FUNCT_1:23;
then A93: h . j = p by A92, CALCUL_2:def 2;

A94: now

assume A95: j in dom (f - {p}) ; :: thesis: contradiction
then (f - {p}) . j = p by A93, FINSEQ_1:def 7;
then A96: (f - {p}) . j in {p} by TARSKI:def 1;
A97: rng (f - {p}) = (rng f) \ {p} by FINSEQ_3:72;
(f - {p}) . j in rng (f - {p}) by A95, FUNCT_1:12;
hence contradiction by A96, A97, XBOOLE_0:def 5; :: thesis: verum

end;

j in dom f by A74;
then j in dom h by A76, CALCUL_2:19;
then consider k being Nat such that
A98: k in dom (IdFinS p,(card A)) and
j = (len (f - {p})) + k by A94, FINSEQ_1:38;
reconsider g = f - {p} as FinSequence of CQC-WFF by FINSEQ_3:93;
( 1 <= k & k <= len (IdFinS p,(card A)) ) by A98, FINSEQ_3:27;
then 1 <= len (IdFinS p,(card A)) by XXREAL_0:2;
then A99: 1 <= card A by FINSEQ_1:def 18;
|- h ^ <*('not' p)*> by A9, A92, CALCUL_2:30;
then A100: |- (g ^ <*p*>) ^ <*('not' p)*> by A99, CALCUL_2:32;
( rng g = (rng f) \ {p} & (rng f) \ {p} c= (X \/ {p}) \ {p} ) by A8, FINSEQ_3:72, XBOOLE_1:33;
then A101: rng g c= X \ {p} by XBOOLE_1:40;
X \ {p} c= X by XBOOLE_1:36;
then A102: rng g c= X by A101, XBOOLE_1:1;
|- (g ^ <*('not' p)*>) ^ <*('not' p)*> by CALCUL_2:21;
then |- g ^ <*('not' p)*> by A100, CALCUL_2:26;
hence X |- 'not' p by A102, Def2; :: thesis: verum

end;

hence X |- 'not' p by A9, Def2; :: thesis: verum

end;