A5:
SepQuadruples F1() is_Sep-closed_on F1()
by Def13;
set Y = { [p,k,K,f] where p is Element of CQC-WFF , k is Element of NAT , f is Element of Funcs bound_QC-variables ,bound_QC-variables , K is Finite_Subset of bound_QC-variables : P1[p,k,K,f] } ;
reconsider X = (SepQuadruples F1()) /\ { [p,k,K,f] where p is Element of CQC-WFF , k is Element of NAT , f is Element of Funcs bound_QC-variables ,bound_QC-variables , K is Finite_Subset of bound_QC-variables : P1[p,k,K,f] } as Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] ;
X is_Sep-closed_on F1()
proof
A6:
[F1(),(index F1()),({}. bound_QC-variables ),(id bound_QC-variables )] in SepQuadruples F1()
by Th31;
[F1(),(index F1()),({}. bound_QC-variables ),(id bound_QC-variables )] in { [p,k,K,f] where p is Element of CQC-WFF , k is Element of NAT , f is Element of Funcs bound_QC-variables ,bound_QC-variables , K is Finite_Subset of bound_QC-variables : P1[p,k,K,f] }
by A1;
hence
[F1(),(index F1()),({}. bound_QC-variables ),(id bound_QC-variables )] in X
by A6, XBOOLE_0:def 4;
:: according to CQC_SIM1:def 12 :: thesis: ( ( for q being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' q),k,K,f] in X holds
[q,k,K,f] in X ) & ( for q, r being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(q '&' r),k,K,f] in X holds
( [q,k,K,f] in X & [r,(k + (QuantNbr q)),K,f] in X ) ) & ( for q being Element of CQC-WFF
for x being Element of bound_QC-variables
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in X holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in X ) )
thus
for
q being
Element of
CQC-WFF for
k being
Element of
NAT for
K being
Finite_Subset of
bound_QC-variables for
f being
Element of
Funcs bound_QC-variables ,
bound_QC-variables st
[('not' q),k,K,f] in X holds
[q,k,K,f] in X
:: thesis: ( ( for q, r being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(q '&' r),k,K,f] in X holds
( [q,k,K,f] in X & [r,(k + (QuantNbr q)),K,f] in X ) ) & ( for q being Element of CQC-WFF
for x being Element of bound_QC-variables
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in X holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in X ) )proof
let q be
Element of
CQC-WFF ;
:: thesis: for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' q),k,K,f] in X holds
[q,k,K,f] in Xlet k be
Element of
NAT ;
:: thesis: for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' q),k,K,f] in X holds
[q,k,K,f] in Xlet K be
Finite_Subset of
bound_QC-variables ;
:: thesis: for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' q),k,K,f] in X holds
[q,k,K,f] in Xlet f be
Element of
Funcs bound_QC-variables ,
bound_QC-variables ;
:: thesis: ( [('not' q),k,K,f] in X implies [q,k,K,f] in X )
assume A7:
[('not' q),k,K,f] in X
;
:: thesis: [q,k,K,f] in X
then A8:
[('not' q),k,K,f] in SepQuadruples F1()
by XBOOLE_0:def 4;
[('not' q),k,K,f] in { [p,k,K,f] where p is Element of CQC-WFF , k is Element of NAT , f is Element of Funcs bound_QC-variables ,bound_QC-variables , K is Finite_Subset of bound_QC-variables : P1[p,k,K,f] }
by A7, XBOOLE_0:def 4;
then consider p being
Element of
CQC-WFF ,
i being
Element of
NAT ,
h being
Element of
Funcs bound_QC-variables ,
bound_QC-variables ,
L being
Finite_Subset of
bound_QC-variables such that A9:
[('not' q),k,K,f] = [p,i,L,h]
and A10:
P1[
p,
i,
L,
h]
;
(
'not' q = p &
k = i &
K = L &
f = h )
by A9, MCART_1:33;
then
P1[
q,
k,
K,
f]
by A2, A8, A10;
then
(
[q,k,K,f] in { [p,k,K,f] where p is Element of CQC-WFF , k is Element of NAT , f is Element of Funcs bound_QC-variables ,bound_QC-variables , K is Finite_Subset of bound_QC-variables : P1[p,k,K,f] } &
[q,k,K,f] in SepQuadruples F1() )
by A5, A8, Def12;
hence
[q,k,K,f] in X
by XBOOLE_0:def 4;
:: thesis: verum
end;
thus
for
q,
r being
Element of
CQC-WFF for
k being
Element of
NAT for
K being
Finite_Subset of
bound_QC-variables for
f being
Element of
Funcs bound_QC-variables ,
bound_QC-variables st
[(q '&' r),k,K,f] in X holds
(
[q,k,K,f] in X &
[r,(k + (QuantNbr q)),K,f] in X )
:: thesis: for q being Element of CQC-WFF
for x being Element of bound_QC-variables
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in X holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Xproof
let q,
r be
Element of
CQC-WFF ;
:: thesis: for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(q '&' r),k,K,f] in X holds
( [q,k,K,f] in X & [r,(k + (QuantNbr q)),K,f] in X )let k be
Element of
NAT ;
:: thesis: for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(q '&' r),k,K,f] in X holds
( [q,k,K,f] in X & [r,(k + (QuantNbr q)),K,f] in X )let K be
Finite_Subset of
bound_QC-variables ;
:: thesis: for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(q '&' r),k,K,f] in X holds
( [q,k,K,f] in X & [r,(k + (QuantNbr q)),K,f] in X )let f be
Element of
Funcs bound_QC-variables ,
bound_QC-variables ;
:: thesis: ( [(q '&' r),k,K,f] in X implies ( [q,k,K,f] in X & [r,(k + (QuantNbr q)),K,f] in X ) )
assume A11:
[(q '&' r),k,K,f] in X
;
:: thesis: ( [q,k,K,f] in X & [r,(k + (QuantNbr q)),K,f] in X )
then A12:
[(q '&' r),k,K,f] in SepQuadruples F1()
by XBOOLE_0:def 4;
[(q '&' r),k,K,f] in { [p,k,K,f] where p is Element of CQC-WFF , k is Element of NAT , f is Element of Funcs bound_QC-variables ,bound_QC-variables , K is Finite_Subset of bound_QC-variables : P1[p,k,K,f] }
by A11, XBOOLE_0:def 4;
then consider p being
Element of
CQC-WFF ,
i being
Element of
NAT ,
h being
Element of
Funcs bound_QC-variables ,
bound_QC-variables ,
L being
Finite_Subset of
bound_QC-variables such that A13:
[(q '&' r),k,K,f] = [p,i,L,h]
and A14:
P1[
p,
i,
L,
h]
;
(
q '&' r = p &
k = i &
K = L &
f = h )
by A13, MCART_1:33;
then
(
P1[
q,
k,
K,
f] &
P1[
r,
k + (QuantNbr q),
K,
f] )
by A3, A12, A14;
then A15:
(
[q,k,K,f] in { [p,k,K,f] where p is Element of CQC-WFF , k is Element of NAT , f is Element of Funcs bound_QC-variables ,bound_QC-variables , K is Finite_Subset of bound_QC-variables : P1[p,k,K,f] } &
[r,(k + (QuantNbr q)),K,f] in { [p,k,K,f] where p is Element of CQC-WFF , k is Element of NAT , f is Element of Funcs bound_QC-variables ,bound_QC-variables , K is Finite_Subset of bound_QC-variables : P1[p,k,K,f] } )
;
(
[q,k,K,f] in SepQuadruples F1() &
[r,(k + (QuantNbr q)),K,f] in SepQuadruples F1() )
by A5, A12, Def12;
hence
(
[q,k,K,f] in X &
[r,(k + (QuantNbr q)),K,f] in X )
by A15, XBOOLE_0:def 4;
:: thesis: verum
end;
let q be
Element of
CQC-WFF ;
:: thesis: for x being Element of bound_QC-variables
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in X holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Xlet x be
Element of
bound_QC-variables ;
:: thesis: for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in X holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Xlet k be
Element of
NAT ;
:: thesis: for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in X holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Xlet K be
Finite_Subset of
bound_QC-variables ;
:: thesis: for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in X holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Xlet f be
Element of
Funcs bound_QC-variables ,
bound_QC-variables ;
:: thesis: ( [(All x,q),k,K,f] in X implies [q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in X )
assume A16:
[(All x,q),k,K,f] in X
;
:: thesis: [q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in X
then A17:
[(All x,q),k,K,f] in SepQuadruples F1()
by XBOOLE_0:def 4;
[(All x,q),k,K,f] in { [p,k,K,f] where p is Element of CQC-WFF , k is Element of NAT , f is Element of Funcs bound_QC-variables ,bound_QC-variables , K is Finite_Subset of bound_QC-variables : P1[p,k,K,f] }
by A16, XBOOLE_0:def 4;
then consider p being
Element of
CQC-WFF ,
i being
Element of
NAT ,
h being
Element of
Funcs bound_QC-variables ,
bound_QC-variables ,
L being
Finite_Subset of
bound_QC-variables such that A18:
[(All x,q),k,K,f] = [p,i,L,h]
and A19:
P1[
p,
i,
L,
h]
;
f +* (x .--> (x. k)) is
Function of
bound_QC-variables ,
bound_QC-variables
by Lm1;
then reconsider g =
f +* (x .--> (x. k)) as
Element of
Funcs bound_QC-variables ,
bound_QC-variables by FUNCT_2:11;
(
All x,
q = p &
k = i &
K = L &
f = h )
by A18, MCART_1:33;
then
P1[
q,
k + 1,
K \/ {x},
g]
by A4, A17, A19;
then A20:
[q,(k + 1),(K \/ {.x.}),(f +* (x .--> (x. k)))] in { [p,k,K,f] where p is Element of CQC-WFF , k is Element of NAT , f is Element of Funcs bound_QC-variables ,bound_QC-variables , K is Finite_Subset of bound_QC-variables : P1[p,k,K,f] }
;
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in SepQuadruples F1()
by A5, A17, Def12;
hence
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in X
by A20, XBOOLE_0:def 4;
:: thesis: verum
end;
then A21:
SepQuadruples F1() c= X
by Def13;
let q be Element of CQC-WFF ; :: thesis: for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [q,k,K,f] in SepQuadruples F1() holds
P1[q,k,K,f]
let k be Element of NAT ; :: thesis: for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [q,k,K,f] in SepQuadruples F1() holds
P1[q,k,K,f]
let K be Finite_Subset of bound_QC-variables ; :: thesis: for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [q,k,K,f] in SepQuadruples F1() holds
P1[q,k,K,f]
let f be Element of Funcs bound_QC-variables ,bound_QC-variables ; :: thesis: ( [q,k,K,f] in SepQuadruples F1() implies P1[q,k,K,f] )
assume
[q,k,K,f] in SepQuadruples F1()
; :: thesis: P1[q,k,K,f]
then
[q,k,K,f] in { [p,k,K,f] where p is Element of CQC-WFF , k is Element of NAT , f is Element of Funcs bound_QC-variables ,bound_QC-variables , K is Finite_Subset of bound_QC-variables : P1[p,k,K,f] }
by A21, XBOOLE_0:def 4;
then consider p being Element of CQC-WFF , i being Element of NAT , h being Element of Funcs bound_QC-variables ,bound_QC-variables , L being Finite_Subset of bound_QC-variables such that
A22:
[q,k,K,f] = [p,i,L,h]
and
A23:
P1[p,i,L,h]
;
( q = p & k = i & K = L & f = h )
by A22, MCART_1:33;
hence
P1[q,k,K,f]
by A23; :: thesis: verum