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)):] ;
A5: SepQuadruples F1() is_Sep-closed_on F1() by Def13;
X is_Sep-closed_on F1()
proof
A6: [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;
[F1(),(index F1()),({}. bound_QC-variables),(id bound_QC-variables)] in SepQuadruples F1() by Th31;
hence [F1(),(index F1()),({}. bound_QC-variables),(id bound_QC-variables)] in X by A6, XBOOLE_0:def 4; :: according to CQC_SIM1:def 11 :: 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 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 [('not' q),k,K,f] in X holds
[q,k,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 [('not' q),k,K,f] in X holds
[q,k,K,f] in X
let 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] ;
A11: k = i by A9, MCART_1:29;
A12: f = h by A9, MCART_1:29;
A13: K = L by A9, MCART_1:29;
'not' q = p by A9, MCART_1:29;
then P1[q,k,K,f] by A2, A8, A10, A11, A13, A12;
then A14: [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 A14, 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 X
proof
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 A15: [(q '&' r),k,K,f] in X ; :: thesis: ( [q,k,K,f] in X & [r,(k + (QuantNbr q)),K,f] in X )
then A16: [(q '&' r),k,K,f] in SepQuadruples F1() by XBOOLE_0:def 4;
then A17: [r,(k + (QuantNbr q)),K,f] in SepQuadruples F1() by A5, Def12;
[(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 A15, 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: [(q '&' r),k,K,f] = [p,i,L,h] and
A19: P1[p,i,L,h] ;
A20: k = i by A18, MCART_1:29;
A21: f = h by A18, MCART_1:29;
A22: K = L by A18, MCART_1:29;
A23: q '&' r = p by A18, MCART_1:29;
then P1[q,k,K,f] by A3, A16, A19, A20, A22, A21;
then A24: [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] } ;
P1[r,k + (QuantNbr q),K,f] by A3, A16, A19, A23, A20, A22, A21;
then A25: [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() by A5, A16, Def12;
hence ( [q,k,K,f] in X & [r,(k + (QuantNbr q)),K,f] in X ) by A24, A25, A17, 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 X
let 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 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 [(All (x,q)),k,K,f] in X holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] 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 [(All (x,q)),k,K,f] in X holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in X
let 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 A26: [(All (x,q)),k,K,f] in X ; :: thesis: [q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in X
then A27: [(All (x,q)),k,K,f] in SepQuadruples F1() by XBOOLE_0:def 4;
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:8;
[(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 A26, 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
A28: [(All (x,q)),k,K,f] = [p,i,L,h] and
A29: P1[p,i,L,h] ;
A30: k = i by A28, MCART_1:29;
A31: f = h by A28, MCART_1:29;
A32: K = L by A28, MCART_1:29;
All (x,q) = p by A28, MCART_1:29;
then P1[q,k + 1,K \/ {x},g] by A4, A27, A29, A30, A32, A31;
then A33: [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, A27, Def12;
hence [q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in X by A33, XBOOLE_0:def 4; :: thesis: verum
end;
then A34: 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 A34, 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
A35: [q,k,K,f] = [p,i,L,h] and
A36: P1[p,i,L,h] ;
A37: k = i by A35, MCART_1:29;
A38: K = L by A35, MCART_1:29;
q = p by A35, MCART_1:29;
hence P1[q,k,K,f] by A35, A36, A37, A38, MCART_1:29; :: thesis: verum