set A = { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } ;
ex k being Element of NAT st k in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p }
proof
now
per cases ( still_not-bound_in p = {} or still_not-bound_in p <> {} ) ;
suppose still_not-bound_in p = {} ; :: thesis: ex k being Element of NAT st k in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p }
then for i being Element of NAT st 0 <= i holds
not x. i in still_not-bound_in p ;
then 0 in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } ;
hence ex k being Element of NAT st k in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } ; :: thesis: verum
end;
suppose A1: still_not-bound_in p <> {} ; :: thesis: ex k being Element of NAT st k in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p }
defpred S1[ Element of NAT ] means x. p in still_not-bound_in p;
defpred S2[ set , set ] means for n being Element of NAT st n = c2 holds
x. n = p;
A2: { l where l is Element of NAT : S1[l] } c= NAT from FRAENKEL:sch 10();
A3: for e being set st e in still_not-bound_in p holds
ex b being set st
( b in NAT & S2[e,b] )
proof
let e be set ; :: thesis: ( e in still_not-bound_in p implies ex b being set st
( b in NAT & S2[e,b] ) )
assume e in still_not-bound_in p ; :: thesis: ex b being set st
( b in NAT & S2[e,b] )
then reconsider e = e as bound_QC-variable ;
consider i being Element of NAT such that
A4: x. i = e by QC_LANG3:30;
reconsider i = i as set ;
take i ; :: thesis: ( i in NAT & S2[e,i] )
thus ( i in NAT & S2[e,i] ) by A4; :: thesis: verum
end;
consider f being Function such that
A5: ( dom f = still_not-bound_in p & rng f c= NAT ) and
A6: for e being set st e in still_not-bound_in p holds
S2[e,f . e] from FUNCT_1:sch 5(A3);
reconsider f = f as Function of (still_not-bound_in p),NAT by A5, FUNCT_2:def 1, RELSET_1:4;
A7: now
let y be set ; :: thesis: ( ( y in rng f implies y in { k where k is Element of NAT : x. k in still_not-bound_in p } ) & ( y in { k where k is Element of NAT : x. k in still_not-bound_in p } implies y in rng f ) )
thus ( y in rng f implies y in { k where k is Element of NAT : x. k in still_not-bound_in p } ) :: thesis: ( y in { k where k is Element of NAT : x. k in still_not-bound_in p } implies y in rng f )
proof
assume y in rng f ; :: thesis: y in { k where k is Element of NAT : x. k in still_not-bound_in p }
then consider x being set such that
A8: x in dom f and
A9: y = f . x by FUNCT_1:def 3;
reconsider n = f . x as Element of NAT ;
x. n in still_not-bound_in p by A5, A6, A8;
hence y in { k where k is Element of NAT : x. k in still_not-bound_in p } by A9; :: thesis: verum
end;
assume y in { k where k is Element of NAT : x. k in still_not-bound_in p } ; :: thesis: y in rng f
then consider k being Element of NAT such that
A10: y = k and
A11: x. k in still_not-bound_in p ;
reconsider a = x. k as Element of still_not-bound_in p by A11;
reconsider n = f . a as Element of NAT ;
x. n = x. k by A6, A11;
then n = k by ZFMISC_1:27;
hence y in rng f by A5, A10, A11, FUNCT_1:def 3; :: thesis: verum
end;
set x = the Element of still_not-bound_in p;
reconsider x = the Element of still_not-bound_in p as bound_QC-variable by A1, TARSKI:def 3;
consider i being Element of NAT such that
A12: x. i = x by QC_LANG3:30;
A13: ex a being set st a in { k where k is Element of NAT : x. k in still_not-bound_in p }
proof
take i ; :: thesis: i in { k where k is Element of NAT : x. k in still_not-bound_in p }
thus i in { k where k is Element of NAT : x. k in still_not-bound_in p } by A1, A12; :: thesis: verum
end;
defpred S3[ Element of NAT , Element of NAT ] means c2 <= p;
A14: for k, l being Element of NAT holds
( S3[k,l] or S3[l,k] ) ;
A15: for k, l, m being Element of NAT st S3[k,l] & S3[l,m] holds
S3[k,m] by XXREAL_0:2;
still_not-bound_in p is finite by Th20;
then A16: ( { k where k is Element of NAT : x. k in still_not-bound_in p } is finite & { n where n is Element of NAT : x. n in still_not-bound_in p } <> {} & { l where l is Element of NAT : x. l in still_not-bound_in p } c= NAT ) by A13, A2, A7, TARSKI:1;
consider m being Element of NAT such that
m in { k where k is Element of NAT : x. k in still_not-bound_in p } and
A17: for k being Element of NAT st k in { n where n is Element of NAT : x. n in still_not-bound_in p } holds
S3[m,k] from CQC_SIM1:sch 4(A16, A14, A15);
now
take n = m + 1; :: thesis: ( n = m + 1 & ( for i being Element of NAT st m + 1 <= i holds
not x. i in still_not-bound_in p ) )
thus n = m + 1 ; :: thesis: for i being Element of NAT st m + 1 <= i holds
not x. i in still_not-bound_in p
let i be Element of NAT ; :: thesis: ( m + 1 <= i implies not x. i in still_not-bound_in p )
assume that
A18: m + 1 <= i and
A19: x. i in still_not-bound_in p ; :: thesis: contradiction
i in { l where l is Element of NAT : x. l in still_not-bound_in p } by A19;
then i <= m by A17;
hence contradiction by A18, NAT_1:13; :: thesis: verum
end;
then m + 1 in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } ;
hence ex k being Element of NAT st k in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } ; :: thesis: verum
end;
end;
end;
hence ex k being Element of NAT st k in { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } ; :: thesis: verum
end;
hence not NBI p is empty ; :: thesis: verum