set S = [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):];
set A = { X where X is Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] : X is_Sep-closed_on p } ;
{ X where X is Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] : X is_Sep-closed_on p } c= bool [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]
proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in { X where X is Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] : X is_Sep-closed_on p } or a in bool [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] )
assume
a in { X where X is Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] : X is_Sep-closed_on p }
;
:: thesis: a in bool [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]
then
ex
X being
Subset of
[:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st
(
X = a &
X is_Sep-closed_on p )
;
hence
a in bool [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]
;
:: thesis: verum
end;
then reconsider A = { X where X is Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] : X is_Sep-closed_on p } as Subset-Family of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] ;
take X = meet A; :: thesis: ( X is_Sep-closed_on p & ( for D being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st D is_Sep-closed_on p holds
X c= D ) )
set B = [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):];
[#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] is_Sep-closed_on p
proof
thus
[p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]
by MCART_1:84;
:: 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 [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] holds
[q,k,K,f] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] ) & ( 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 [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] holds
( [q,k,K,f] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] & [r,(k + (QuantNbr q)),K,f] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] ) ) & ( 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 [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] ) )
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 [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] holds
[q,k,K,f] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]
by MCART_1:84;
:: 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 [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] holds
( [q,k,K,f] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] & [r,(k + (QuantNbr q)),K,f] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] ) ) & ( 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 [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] ) )
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 [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] holds
(
[q,k,K,f] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] &
[r,(k + (QuantNbr q)),K,f] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] )
by MCART_1:84;
:: 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 [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]
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 [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]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 [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]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 [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]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 [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]let f be
Element of
Funcs bound_QC-variables ,
bound_QC-variables ;
:: thesis: ( [(All x,q),k,K,f] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] implies [q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] )
assume
[(All x,q),k,K,f] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]
;
:: thesis: [q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]
A1:
dom (f +* (x .--> (x. k))) =
(dom f) \/ (dom (x .--> (x. k)))
by FUNCT_4:def 1
.=
bound_QC-variables \/ (dom (x .--> (x. k)))
by FUNCT_2:def 1
.=
bound_QC-variables \/ {x}
by FUNCOP_1:19
.=
bound_QC-variables
by ZFMISC_1:46
;
A2:
rng (f +* (x .--> (x. k))) c= (rng f) \/ (rng (x .--> (x. k)))
by FUNCT_4:18;
A3:
rng f c= bound_QC-variables
by RELAT_1:def 19;
A4:
rng (x .--> (x. k)) = {(x. k)}
by FUNCOP_1:14;
bound_QC-variables \/ {(x. k)} = bound_QC-variables
by ZFMISC_1:46;
then
(rng f) \/ (rng (x .--> (x. k))) c= bound_QC-variables
by A3, A4, XBOOLE_1:9;
then
(
dom (f +* (x .--> (x. k))) = bound_QC-variables &
rng (f +* (x .--> (x. k))) c= bound_QC-variables )
by A1, A2, XBOOLE_1:1;
then
f +* (x .--> (x. k)) is
Function of
bound_QC-variables ,
bound_QC-variables
by FUNCT_2:def 1, RELSET_1:11;
then reconsider ff =
f +* (x .--> (x. k)) as
Element of
Funcs bound_QC-variables ,
bound_QC-variables by FUNCT_2:11;
[q,(k + 1),(K \/ {.x.}),ff] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]
by MCART_1:84;
hence
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in [#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]
;
:: thesis: verum
end;
then A5:
[#] [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] in A
;
for Y being set st Y in A holds
[p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] in Y
proof
let Y be
set ;
:: thesis: ( Y in A implies [p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] in Y )
assume
Y in A
;
:: thesis: [p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] in Y
then
ex
X being
Subset of
[:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st
(
X = Y &
X is_Sep-closed_on p )
;
hence
[p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] in Y
by Def12;
:: thesis: verum
end;
hence
[p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] in X
by A5, SETFAM_1:def 1; :: 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 ) & ( for D being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st D is_Sep-closed_on p holds
X c= D ) )
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 ) & ( for D being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st D is_Sep-closed_on p holds
X c= D ) )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 A6:
[('not' q),k,K,f] in X
;
:: thesis: [q,k,K,f] in X
for
Y being
set st
Y in A holds
[q,k,K,f] in Y
proof
let Y be
set ;
:: thesis: ( Y in A implies [q,k,K,f] in Y )
assume A7:
Y in A
;
:: thesis: [q,k,K,f] in Y
then A8:
ex
X being
Subset of
[:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st
(
X = Y &
X is_Sep-closed_on p )
;
[('not' q),k,K,f] in Y
by A6, A7, SETFAM_1:def 1;
hence
[q,k,K,f] in Y
by A8, Def12;
:: thesis: verum
end;
hence
[q,k,K,f] in X
by A5, SETFAM_1:def 1;
:: 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 ) & ( for D being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st D is_Sep-closed_on p holds
X c= D ) )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 A9:
[(q '&' r),k,K,f] in X
;
:: thesis: ( [q,k,K,f] in X & [r,(k + (QuantNbr q)),K,f] in X )
for
Y being
set st
Y in A holds
[q,k,K,f] in Y
proof
let Y be
set ;
:: thesis: ( Y in A implies [q,k,K,f] in Y )
assume A10:
Y in A
;
:: thesis: [q,k,K,f] in Y
then A11:
ex
X being
Subset of
[:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st
(
X = Y &
X is_Sep-closed_on p )
;
[(q '&' r),k,K,f] in Y
by A9, A10, SETFAM_1:def 1;
hence
[q,k,K,f] in Y
by A11, Def12;
:: thesis: verum
end;
hence
[q,k,K,f] in X
by A5, SETFAM_1:def 1;
:: thesis: [r,(k + (QuantNbr q)),K,f] in X
for
Y being
set st
Y in A holds
[r,(k + (QuantNbr q)),K,f] in Y
proof
let Y be
set ;
:: thesis: ( Y in A implies [r,(k + (QuantNbr q)),K,f] in Y )
assume A12:
Y in A
;
:: thesis: [r,(k + (QuantNbr q)),K,f] in Y
then A13:
ex
X being
Subset of
[:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st
(
X = Y &
X is_Sep-closed_on p )
;
[(q '&' r),k,K,f] in Y
by A9, A12, SETFAM_1:def 1;
hence
[r,(k + (QuantNbr q)),K,f] in Y
by A13, Def12;
:: thesis: verum
end;
hence
[r,(k + (QuantNbr q)),K,f] in X
by A5, SETFAM_1:def 1;
:: thesis: verum
end;
thus
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
:: thesis: for D being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st D is_Sep-closed_on p holds
X c= Dproof
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 A14:
[(All x,q),k,K,f] in X
;
:: thesis: [q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in X
for
Y being
set st
Y in A holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Y
proof
let Y be
set ;
:: thesis: ( Y in A implies [q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Y )
assume A15:
Y in A
;
:: thesis: [q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Y
then A16:
ex
X being
Subset of
[:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st
(
X = Y &
X is_Sep-closed_on p )
;
[(All x,q),k,K,f] in Y
by A14, A15, SETFAM_1:def 1;
hence
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Y
by A16, Def12;
:: thesis: verum
end;
hence
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in X
by A5, SETFAM_1:def 1;
:: thesis: verum
end;
let D be Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]; :: thesis: ( D is_Sep-closed_on p implies X c= D )
assume
D is_Sep-closed_on p
; :: thesis: X c= D
then
D in A
;
hence
X c= D
by SETFAM_1:4; :: thesis: verum