set A2 = { t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in p } ;
ex t being QC-symbol of A st t in { t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in p }
proof
now :: thesis: ex t being QC-symbol of A st t in { t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in p }
per cases ( still_not-bound_in p = {} or still_not-bound_in p <> {} ) ;
suppose still_not-bound_in p = {} ; :: thesis: ex t being QC-symbol of A st t in { t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in p }
then for u being QC-symbol of A st 0 A <= u holds
not x. u in still_not-bound_in p ;
then 0 A in { t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in p } ;
hence ex t being QC-symbol of A st t in { t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in p } ; :: thesis: verum
end;
suppose A1: still_not-bound_in p <> {} ; :: thesis: ex t being QC-symbol of A st t in { t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in p }
defpred S1[ QC-symbol of A] means x. A in still_not-bound_in p;
defpred S2[ object , object ] means for t being QC-symbol of A st t = p holds
x. t = A;
A2: { t where t is QC-symbol of A : S1[t] } c= QC-symbols A from FRAENKEL:sch 10();
A3: for e being object st e in still_not-bound_in p holds
ex b being object st
( b in QC-symbols A & S2[e,b] )
proof
let e be object ; :: thesis: ( e in still_not-bound_in p implies ex b being object st
( b in QC-symbols A & S2[e,b] ) )
assume e in still_not-bound_in p ; :: thesis: ex b being object st
( b in QC-symbols A & S2[e,b] )
then reconsider e = e as bound_QC-variable of A ;
consider t being QC-symbol of A such that
A4: x. t = e by QC_LANG3:30;
reconsider t = t as set ;
take t ; :: thesis: ( t in QC-symbols A & S2[e,t] )
thus ( t in QC-symbols A & S2[e,t] ) by A4; :: thesis: verum
end;
consider f being Function such that
A5: ( dom f = still_not-bound_in p & rng f c= QC-symbols A ) and
for e being object st e in still_not-bound_in p holds
S2[e,f . e] from FUNCT_1:sch 6(A3);
reconsider f = f as Function of (still_not-bound_in p),(QC-symbols A) by A5, FUNCT_2:def 1, RELSET_1:4;
set x = the Element of still_not-bound_in p;
reconsider x = the Element of still_not-bound_in p as bound_QC-variable of A by A1, TARSKI:def 3;
consider t being QC-symbol of A such that
A6: x. t = x by QC_LANG3:30;
A7: ex a being set st a in { z where z is QC-symbol of A : x. z in still_not-bound_in p }
proof
take t ; :: thesis: t in { z where z is QC-symbol of A : x. z in still_not-bound_in p }
thus t in { z where z is QC-symbol of A : x. z in still_not-bound_in p } by A1, A6; :: thesis: verum
end;
defpred S3[ QC-symbol of A, QC-symbol of A] means p <= A;
A8: for t, u being QC-symbol of A holds
( S3[t,u] or S3[u,t] ) by QC_LANG1:24;
A9: for t, u, v being QC-symbol of A st S3[t,u] & S3[u,v] holds
S3[t,v] by QC_LANG1:21;
A10: still_not-bound_in p is finite by Th19;
deffunc H5( bound_QC-variable of A) -> QC-symbol of A = x. A;
A11: { H5(b) where b is Element of bound_QC-variables A : b in still_not-bound_in p } is finite from FRAENKEL:sch 21(A10);
 { (x. b) where b is Element of bound_QC-variables A : b in still_not-bound_in p } = { w where w is QC-symbol of A : x. w in still_not-bound_in p }
proof
set S1 = { (x. b) where b is Element of bound_QC-variables A : b in still_not-bound_in p } ;
set S2 = { w where w is QC-symbol of A : x. w in still_not-bound_in p } ;
for s being object st s in { (x. b) where b is Element of bound_QC-variables A : b in still_not-bound_in p } holds
s in { w where w is QC-symbol of A : x. w in still_not-bound_in p }
proof
let s be object ; :: thesis: ( s in { (x. b) where b is Element of bound_QC-variables A : b in still_not-bound_in p } implies s in { w where w is QC-symbol of A : x. w in still_not-bound_in p } )
assume s in { (x. b) where b is Element of bound_QC-variables A : b in still_not-bound_in p } ; :: thesis: s in { w where w is QC-symbol of A : x. w in still_not-bound_in p }
then consider b being Element of bound_QC-variables A such that
A12: ( s = x. b & b in still_not-bound_in p ) ;
reconsider s1 = s as QC-symbol of A by A12;
x. s1 = b by A12, Def1;
hence s in { w where w is QC-symbol of A : x. w in still_not-bound_in p } by A12; :: thesis: verum
end;
hence { (x. b) where b is Element of bound_QC-variables A : b in still_not-bound_in p } c= { w where w is QC-symbol of A : x. w in still_not-bound_in p } ; :: according to XBOOLE_0:def 10 :: thesis: { w where w is QC-symbol of A : x. w in still_not-bound_in p } c= { (x. b) where b is Element of bound_QC-variables A : b in still_not-bound_in p }
for s being object st s in { w where w is QC-symbol of A : x. w in still_not-bound_in p } holds
s in { (x. b) where b is Element of bound_QC-variables A : b in still_not-bound_in p }
proof
let s be object ; :: thesis: ( s in { w where w is QC-symbol of A : x. w in still_not-bound_in p } implies s in { (x. b) where b is Element of bound_QC-variables A : b in still_not-bound_in p } )
assume s in { w where w is QC-symbol of A : x. w in still_not-bound_in p } ; :: thesis: s in { (x. b) where b is Element of bound_QC-variables A : b in still_not-bound_in p }
then consider w being QC-symbol of A such that
A13: ( s = w & x. w in still_not-bound_in p ) ;
x. (x. w) = w by Def1;
hence s in { (x. b) where b is Element of bound_QC-variables A : b in still_not-bound_in p } by A13; :: thesis: verum
end;
hence { w where w is QC-symbol of A : x. w in still_not-bound_in p } c= { (x. b) where b is Element of bound_QC-variables A : b in still_not-bound_in p } ; :: thesis: verum
end;
then A14: ( { w where w is QC-symbol of A : x. w in still_not-bound_in p } is finite & { z where z is QC-symbol of A : x. z in still_not-bound_in p } <> {} & { v where v is QC-symbol of A : x. v in still_not-bound_in p } c= QC-symbols A ) by A11, A2, A7;
consider v being QC-symbol of A such that
v in { w where w is QC-symbol of A : x. w in still_not-bound_in p } and
A15: for t being QC-symbol of A st t in { z where z is QC-symbol of A : x. z in still_not-bound_in p } holds
S3[v,t] from CQC_SIM1:sch 4(A14, A8, A9);
now :: thesis: ex n being Element of QC-symbols A st
( n = v ++ & ( for z being QC-symbol of A st v ++ <= z holds
not x. z in still_not-bound_in p ) )
take n = v ++ ; :: thesis: ( n = v ++ & ( for z being QC-symbol of A st v ++ <= z holds
not x. z in still_not-bound_in p ) )
thus n = v ++ ; :: thesis: for z being QC-symbol of A st v ++ <= z holds
not x. z in still_not-bound_in p
let z be QC-symbol of A; :: thesis: ( v ++ <= z implies not x. z in still_not-bound_in p )
assume that
A16: v ++ <= z and
A17: x. z in still_not-bound_in p ; :: thesis: contradiction
z in { w where w is QC-symbol of A : x. w in still_not-bound_in p } by A17;
then z <= v by A15;
then v ++ <= v by A16, QC_LANG1:21;
then not v < v ++ by QC_LANG1:25;
hence contradiction by QC_LANG1:27; :: thesis: verum
end;
then v ++ in { t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in p } ;
hence ex t being QC-symbol of A st t in { t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in p } ; :: thesis: verum
end;
end;
end;
hence ex t being QC-symbol of A st t in { t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in p } ; :: thesis: verum
end;
hence not NBI p is empty ; :: thesis: verum