set e = the Element of vSUB A;
defpred S1[ object ] means for D being non empty set st D is A -Sub-closed holds
$1 in D;
consider D0 being set such that
A1:
for x being object holds
( x in D0 iff ( x in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & S1[x] ) )
from XBOOLE_0:sch 1();
0 in QC-symbols A
by QC_LANG1:3;
then
( [<*[0,0]*>, the Element of vSUB A] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for D being non empty set st D is A -Sub-closed holds
[<*[0,0]*>, the Element of vSUB A] in D ) )
by Lm4;
then reconsider D0 = D0 as non empty set by A1;
take
D0
; ( D0 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )
D0 c= [:([:NAT,(QC-symbols A):] *),(vSUB A):]
by A1;
hence
D0 is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):]
; SUBSTUT1:def 16 ( ( for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0 ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in D0 ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )
thus
for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0
( ( for e being Element of vSUB A holds [<*[0,0]*>,e] in D0 ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )proof
let k be
Nat;
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0let p be
QC-pred_symbol of
k,
A;
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0let ll be
QC-variable_list of
k,
A;
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0let e be
Element of
vSUB A;
[(<*p*> ^ ll),e] in D0
(
[(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for
D being non
empty set st
D is
A -Sub-closed holds
[(<*p*> ^ ll),e] in D ) )
by Lm5;
hence
[(<*p*> ^ ll),e] in D0
by A1;
verum
end;
thus
for e being Element of vSUB A holds [<*[0,0]*>,e] in D0
( ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )proof
let e be
Element of
vSUB A;
[<*[0,0]*>,e] in D0
0 in QC-symbols A
by QC_LANG1:3;
then
(
[<*[0,0]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for
D being non
empty set st
D is
A -Sub-closed holds
[<*[0,0]*>,e] in D ) )
by Lm4;
hence
[<*[0,0]*>,e] in D0
by A1;
verum
end;
thus
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0
( ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )proof
let p be
FinSequence of
[:NAT,(QC-symbols A):];
for e being Element of vSUB A st [p,e] in D0 holds
[(<*[1,0]*> ^ p),e] in D0let e be
Element of
vSUB A;
( [p,e] in D0 implies [(<*[1,0]*> ^ p),e] in D0 )
assume A2:
[p,e] in D0
;
[(<*[1,0]*> ^ p),e] in D0
A3:
for
D being non
empty set st
D is
A -Sub-closed holds
[(<*[1,0]*> ^ p),e] in D
0 in QC-symbols A
by QC_LANG1:3;
then
[1,0] in [:NAT,(QC-symbols A):]
by ZFMISC_1:87;
then
(
rng <*[1,0]*> = {[1,0]} &
{[1,0]} c= [:NAT,(QC-symbols A):] )
by FINSEQ_1:39, ZFMISC_1:31;
then reconsider y =
<*[1,0]*> as
FinSequence of
[:NAT,(QC-symbols A):] by FINSEQ_1:def 4;
y ^ p is
FinSequence of
[:NAT,(QC-symbols A):]
;
then
<*[1,0]*> ^ p in [:NAT,(QC-symbols A):] *
by FINSEQ_1:def 11;
then
[(<*[1,0]*> ^ p),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
by ZFMISC_1:def 2;
hence
[(<*[1,0]*> ^ p),e] in D0
by A1, A3;
verum
end;
thus
for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0
( ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds
D0 c= D ) )proof
let p,
q be
FinSequence of
[:NAT,(QC-symbols A):];
for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds
[((<*[2,0]*> ^ p) ^ q),e] in D0let e be
Element of
vSUB A;
( [p,e] in D0 & [q,e] in D0 implies [((<*[2,0]*> ^ p) ^ q),e] in D0 )
assume A5:
(
[p,e] in D0 &
[q,e] in D0 )
;
[((<*[2,0]*> ^ p) ^ q),e] in D0
A6:
for
D being non
empty set st
D is
A -Sub-closed holds
[((<*[2,0]*> ^ p) ^ q),e] in D
0 in QC-symbols A
by QC_LANG1:3;
then
[2,0] in [:NAT,(QC-symbols A):]
by ZFMISC_1:87;
then
(
rng <*[2,0]*> = {[2,0]} &
{[2,0]} c= [:NAT,(QC-symbols A):] )
by FINSEQ_1:39, ZFMISC_1:31;
then reconsider y =
<*[2,0]*> as
FinSequence of
[:NAT,(QC-symbols A):] by FINSEQ_1:def 4;
(y ^ p) ^ q is
FinSequence of
[:NAT,(QC-symbols A):]
;
then
(<*[2,0]*> ^ p) ^ q in [:NAT,(QC-symbols A):] *
by FINSEQ_1:def 11;
then
[((<*[2,0]*> ^ p) ^ q),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
by ZFMISC_1:def 2;
hence
[((<*[2,0]*> ^ p) ^ q),e] in D0
by A1, A6;
verum
end;
thus
for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0
for D being non empty set st D is A -Sub-closed holds
D0 c= Dproof
let x be
bound_QC-variable of
A;
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0let p be
FinSequence of
[:NAT,(QC-symbols A):];
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0let e be
Element of
vSUB A;
( [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 )
assume A8:
[p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0
;
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0
A9:
for
D being non
empty set st
D is
A -Sub-closed holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D
proof
let D be non
empty set ;
( D is A -Sub-closed implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in D )
assume A10:
D is
A -Sub-closed
;
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D
then
[p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D
by A1, A8;
hence
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D
by A10;
verum
end;
(<*[3,0]*> ^ <*x*>) ^ p is
FinSequence of
[:NAT,(QC-symbols A):]
by Lm3;
then
(<*[3,0]*> ^ <*x*>) ^ p in [:NAT,(QC-symbols A):] *
by FINSEQ_1:def 11;
then
[((<*[3,0]*> ^ <*x*>) ^ p),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):]
by ZFMISC_1:def 2;
hence
[((<*[3,0]*> ^ <*x*>) ^ p),e] in D0
by A1, A9;
verum
end;
let D be non empty set ; ( D is A -Sub-closed implies D0 c= D )
assume A11:
D is A -Sub-closed
; D0 c= D
let x be object ; TARSKI:def 3 ( not x in D0 or x in D )
assume
x in D0
; x in D
hence
x in D
by A1, A11; verum