let X be Subset of CQC-WFF ; :: thesis: for p being Element of CQC-WFF holds
( X |- p iff not X \/ {('not' p)} is Consistent )
let p be Element of CQC-WFF ; :: thesis: ( X |- p iff not X \/ {('not' p)} is Consistent )
thus
( X |- p implies not X \/ {('not' p)} is Consistent )
:: thesis: ( not X \/ {('not' p)} is Consistent implies X |- p )
thus
( not X \/ {('not' p)} is Consistent implies X |- p )
:: thesis: verumproof
assume
not
X \/ {('not' p)} is
Consistent
;
:: thesis: X |- p
then
X \/ {('not' p)} |- p
by Th6;
then consider f being
FinSequence of
CQC-WFF such that A7:
(
rng f c= X \/ {('not' p)} &
|- f ^ <*p*> )
by Def2;
now assume
not
rng f c= X
;
:: thesis: X |- pthen consider a being
set such that A8:
(
a in rng f & not
a in X )
by TARSKI:def 3;
reconsider B =
dom f as
finite set ;
reconsider A =
f " {('not' p)} as
finite set ;
set n =
card A;
set g =
f - {('not' p)};
set h =
(f - {('not' p)}) ^ (IdFinS ('not' p),(card A));
A9:
len (IdFinS ('not' p),(card A)) = card A
by FINSEQ_1:def 18;
defpred S1[
Nat,
set ]
means ( ( $1
in Seg (len (f - {('not' p)})) implies $2
= (Sgm (B \ A)) . $1 ) & ( $1
in seq (len (f - {('not' p)})),
(card A) implies $2
= (Sgm A) . ($1 - (len (f - {('not' p)}))) ) );
A12:
for
k being
Nat st
k in Seg (len ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A)))) holds
ex
a being
set st
S1[
k,
a]
consider F being
FinSequence such that A15:
(
dom F = Seg (len ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A)))) & ( for
k being
Nat st
k in Seg (len ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A)))) holds
S1[
k,
F . k] ) )
from FINSEQ_1:sch 1(A12);
A16:
len ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A))) =
(len (f - {('not' p)})) + (len (IdFinS ('not' p),(card A)))
by FINSEQ_1:35
.=
((len f) - (card A)) + (len (IdFinS ('not' p),(card A)))
by FINSEQ_3:66
.=
((len f) - (card A)) + (card A)
by FINSEQ_1:def 18
.=
len f
;
then A17:
dom F = B
by A15, FINSEQ_1:def 3;
reconsider C =
B \ A as
finite set ;
then A19:
C c= Seg (len f)
by TARSKI:def 3;
then A20:
dom (Sgm C) = Seg (card C)
by FINSEQ_3:45;
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 - {('not' p)})
by FINSEQ_3:66
;
A c= B
by RELAT_1:167;
then A22:
A c= Seg (len f)
by FINSEQ_1:def 3;
A27:
rng F = B
proof
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 A36:
a in B
;
:: thesis: a in rng F
A37:
now assume A38:
a in A
;
:: thesis: a in rng F
rng (Sgm A) = A
by A22, FINSEQ_1:def 13;
then consider i being
Nat such that A39:
(
i in dom (Sgm A) &
(Sgm A) . i = a )
by A38, FINSEQ_2:11;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 13;
set m =
i + (len (f - {('not' p)}));
len (Sgm A) = card A
by A22, FINSEQ_3:44;
then A40:
( 1
<= i &
i <= card A )
by A39, FINSEQ_3:27;
then A41:
( 1
+ (len (f - {('not' p)})) <= i + (len (f - {('not' p)})) &
i + (len (f - {('not' p)})) <= (card A) + (len (f - {('not' p)})) )
by XREAL_1:8;
then A42:
i + (len (f - {('not' p)})) in seq (len (f - {('not' p)})),
(card A)
by CALCUL_2:1;
i <= i + (len (f - {('not' p)}))
by NAT_1:11;
then A43:
( 1
<= i + (len (f - {('not' p)})) &
i + (len (f - {('not' p)})) <= (len (f - {('not' p)})) + (len (IdFinS ('not' p),(card A))) )
by A40, A41, FINSEQ_1:def 18, XXREAL_0:2;
then
i + (len (f - {('not' p)})) <= len ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A)))
by FINSEQ_1:35;
then
i + (len (f - {('not' p)})) in dom ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A)))
by A43, FINSEQ_3:27;
then A44:
i + (len (f - {('not' p)})) in Seg (len ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A))))
by FINSEQ_1:def 3;
a = (Sgm A) . ((i + (len (f - {('not' p)}))) - (len (f - {('not' p)})))
by A39;
then
a = F . (i + (len (f - {('not' p)})))
by A15, A42, A44;
hence
a in rng F
by A15, A44, FUNCT_1:12;
:: thesis: verum end;
now assume
not
a in A
;
:: thesis: a in rng Fthen A45:
a in C
by A36, XBOOLE_0:def 5;
then
C c= Seg (len f)
by TARSKI:def 3;
then
a in rng (Sgm C)
by A45, FINSEQ_1:def 13;
then consider i being
Nat such that A47:
(
i in dom (Sgm C) &
(Sgm C) . i = a )
by FINSEQ_2:11;
len (Sgm C) = len (f - {('not' p)})
by A20, A21, FINSEQ_1:def 3;
then A48:
( 1
<= i &
i <= len (f - {('not' p)}) )
by A47, FINSEQ_3:27;
then A49:
i in Seg (len (f - {('not' p)}))
by FINSEQ_1:3;
len (f - {('not' p)}) <= len ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A)))
by CALCUL_1:6;
then
i <= len ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A)))
by A48, XXREAL_0:2;
then A50:
i in Seg (len ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A))))
by A48, FINSEQ_1:3;
then
a = F . i
by A15, A47, A49;
hence
a in rng F
by A15, A50, FUNCT_1:12;
:: thesis: verum end;
hence
a in rng F
by A37;
:: thesis: verum
end; then reconsider F =
F as
Relation of
B,
B by A17, RELSET_1:11;
(
B = {} implies
B = {} )
;
then reconsider F =
F as
Function of
B,
B by A17, FUNCT_2:def 1;
F is
one-to-one
proof
let a1 be
set ;
:: according to FUNCT_1:def 8 :: thesis: for b1 being set holds
( not a1 in dom F or not b1 in dom F or not F . a1 = F . b1 or a1 = b1 )let a2 be
set ;
:: thesis: ( not a1 in dom F or not a2 in dom F or not F . a1 = F . a2 or a1 = a2 )
assume A51:
(
a1 in dom F &
a2 in dom F &
F . a1 = F . a2 )
;
:: thesis: a1 = a2
A52:
(
a1 in (Seg (len (f - {('not' p)}))) \/ (seq (len (f - {('not' p)})),(card A)) &
a2 in (Seg (len (f - {('not' p)}))) \/ (seq (len (f - {('not' p)})),(card A)) )
by A9, A15, A51, Lm1;
A53:
now assume A54:
a1 in Seg (len (f - {('not' p)}))
;
:: thesis: a1 = a2A56:
F . a1 = (Sgm C) . a1
by A15, A51, A54;
A57:
a1 in dom (Sgm C)
by A19, A21, A54, FINSEQ_3:45;
then
F . a1 in rng (Sgm C)
by A56, FUNCT_1:12;
then A58:
F . a1 in C
by A19, FINSEQ_1:def 13;
A59:
now assume A60:
a2 in Seg (len (f - {('not' p)}))
;
:: thesis: a1 = a2A61:
F . a2 = (Sgm C) . a2
by A15, A51, A60;
A62:
a2 in dom (Sgm C)
by A19, A21, A60, FINSEQ_3:45;
A63:
(Sgm C) . a1 = (Sgm C) . a2
by A15, A51, A54, A61;
Sgm C is
one-to-one
by A19, FINSEQ_3:99;
hence
a1 = a2
by A57, A62, A63, FUNCT_1:def 8;
:: thesis: verum end; hence
a1 = a2
by A52, A59, XBOOLE_0:def 3;
:: thesis: verum end;
now assume A65:
a1 in seq (len (f - {('not' p)})),
(card A)
;
:: thesis: a1 = a2then reconsider i =
a1 as
Element of
NAT ;
A66:
i - (len (f - {('not' p)})) in dom (Sgm A)
by A23, A65;
(Sgm A) . (i - (len (f - {('not' p)}))) in rng (Sgm A)
by A23, A65, FUNCT_1:12;
then
F . a1 in rng (Sgm A)
by A15, A51, A65;
then A67:
F . a1 in A
by A22, FINSEQ_1:def 13;
A68:
now assume A69:
a2 in seq (len (f - {('not' p)})),
(card A)
;
:: thesis: a1 = a2then reconsider i1 =
a2 as
Element of
NAT ;
A70:
F . a2 = (Sgm A) . (i1 - (len (f - {('not' p)})))
by A15, A51, A69;
A71:
i1 - (len (f - {('not' p)})) in dom (Sgm A)
by A23, A69;
A72:
(Sgm A) . (i1 - (len (f - {('not' p)}))) = (Sgm A) . (i - (len (f - {('not' p)})))
by A15, A51, A65, A70;
Sgm A is
one-to-one
by A22, FINSEQ_3:99;
then
i1 - (len (f - {('not' p)})) = i - (len (f - {('not' p)}))
by A66, A71, A72, FUNCT_1:def 8;
hence
a1 = a2
;
:: thesis: verum end; hence
a1 = a2
by A52, A68, XBOOLE_0:def 3;
:: thesis: verum end;
hence
a1 = a2
by A52, A53, XBOOLE_0:def 3;
:: thesis: verum
end; then reconsider F =
F as
Permutation of
(dom f) by A27, FUNCT_2:83;
A75:
Per f,
F = (f - {('not' p)}) ^ (IdFinS ('not' p),(card A))
proof
A76:
dom (Per f,F) =
B
by CALCUL_2:19
.=
dom F
by A15, A16, FINSEQ_1:def 3
.=
dom ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A)))
by A15, FINSEQ_1:def 3
;
now let k be
Nat;
:: thesis: ( k in dom ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A))) implies (Per f,F) . k = ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A))) . k )assume A77:
k in dom ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A)))
;
:: thesis: (Per f,F) . k = ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A))) . kA78:
k in Seg (len ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A))))
by A77, FINSEQ_1:def 3;
A79:
now assume A80:
k in dom (f - {('not' p)})
;
:: thesis: (Per f,F) . k = ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A))) . kthen A81:
k in dom (Sgm C)
by A20, A21, FINSEQ_1:def 3;
k in Seg (len (f - {('not' p)}))
by A80, FINSEQ_1:def 3;
then A82:
F . k = (Sgm C) . k
by A15, A78;
k in dom (F * f)
by A76, A77, CALCUL_2:def 2;
then
(F * f) . k = f . ((Sgm C) . k)
by A82, FUNCT_1:22;
hence (Per f,F) . k =
f . ((Sgm C) . k)
by CALCUL_2:def 2
.=
((Sgm C) * f) . k
by A81, FUNCT_1:23
.=
(f - {('not' p)}) . k
by FINSEQ_3:def 1
.=
((f - {('not' p)}) ^ (IdFinS ('not' p),(card A))) . k
by A80, FINSEQ_1:def 7
;
:: thesis: verum end; now given i being
Nat such that A83:
(
i in dom (IdFinS ('not' p),(card A)) &
k = (len (f - {('not' p)})) + i )
;
:: thesis: (Per f,F) . k = ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A))) . k
len (IdFinS ('not' p),(card A)) = card A
by FINSEQ_1:def 18;
then A84:
( 1
<= i &
i <= card A )
by A83, FINSEQ_3:27;
then
( 1
+ (len (f - {('not' p)})) <= k &
k <= (card A) + (len (f - {('not' p)})) )
by A83, XREAL_1:8;
then A85:
k in seq (len (f - {('not' p)})),
(card A)
by CALCUL_2:1;
then
F . k = (Sgm A) . (k - (len (f - {('not' p)})))
by A15, A78;
then
F . k in rng (Sgm A)
by A23, A85, FUNCT_1:12;
then
F . k in A
by A22, FINSEQ_1:def 13;
then
f . (F . k) in {('not' p)}
by FUNCT_1:def 13;
then A86:
f . (F . k) = 'not' p
by TARSKI:def 1;
k in dom (F * f)
by A76, A77, CALCUL_2:def 2;
then
(F * f) . k = 'not' p
by A86, FUNCT_1:22;
then A87:
(Per f,F) . k = 'not' p
by CALCUL_2:def 2;
i in Seg (card A)
by A84, FINSEQ_1:3;
hence (Per f,F) . k =
(IdFinS ('not' p),(card A)) . i
by A87, FUNCOP_1:13
.=
((f - {('not' p)}) ^ (IdFinS ('not' p),(card A))) . k
by A83, FINSEQ_1:def 7
;
:: thesis: verum end; hence
(Per f,F) . k = ((f - {('not' p)}) ^ (IdFinS ('not' p),(card A))) . k
by A77, A79, FINSEQ_1:38;
:: thesis: verum end;
hence
Per f,
F = (f - {('not' p)}) ^ (IdFinS ('not' p),(card A))
by A76, FINSEQ_1:17;
:: thesis: verum
end; then reconsider h =
(f - {('not' p)}) ^ (IdFinS ('not' p),(card A)) as
FinSequence of
CQC-WFF ;
A88:
|- h ^ <*p*>
by A7, A75, CALCUL_2:30;
(
a in X or
a in {('not' p)} )
by A7, A8, XBOOLE_0:def 3;
then
a = 'not' p
by A8, TARSKI:def 1;
then consider i being
Nat such that A89:
(
i in B &
f . i = 'not' p )
by A8, FINSEQ_2:11;
consider j being
Nat such that A90:
(
j in dom F &
F . j = i )
by A27, A89, FINSEQ_2:11;
(F * f) . j = 'not' p
by A89, A90, FUNCT_1:23;
then A91:
h . j = 'not' p
by A75, CALCUL_2:def 2;
j in dom f
by A90;
then
j in dom h
by A75, CALCUL_2:19;
then consider k being
Nat such that A95:
(
k in dom (IdFinS ('not' p),(card A)) &
j = (len (f - {('not' p)})) + k )
by A92, FINSEQ_1:38;
reconsider g =
f - {('not' p)} as
FinSequence of
CQC-WFF by FINSEQ_3:93;
( 1
<= k &
k <= len (IdFinS ('not' p),(card A)) )
by A95, FINSEQ_3:27;
then
1
<= len (IdFinS ('not' p),(card A))
by XXREAL_0:2;
then
1
<= card A
by FINSEQ_1:def 18;
then A96:
|- (g ^ <*('not' p)*>) ^ <*p*>
by A88, CALCUL_2:32;
|- (g ^ <*p*>) ^ <*p*>
by CALCUL_2:21;
then A97:
|- g ^ <*p*>
by A96, CALCUL_2:26;
A98:
rng g = (rng f) \ {('not' p)}
by FINSEQ_3:72;
(rng f) \ {('not' p)} c= (X \/ {('not' p)}) \ {('not' p)}
by A7, XBOOLE_1:33;
then A99:
rng g c= X \ {('not' p)}
by A98, XBOOLE_1:40;
X \ {('not' p)} c= X
by XBOOLE_1:36;
then
rng g c= X
by A99, XBOOLE_1:1;
hence
X |- p
by A97, Def2;
:: thesis: verum end;
hence
X |- p
by A7, Def2;
:: thesis: verum
end;