let y be Surreal; :: thesis: for f being Function st dom f = NAT & y in Union f holds
ex n being Nat st
( y in f . n & ( for m being Nat st y in f . m holds
n <= m ) )
let f be Function; :: thesis: ( dom f = NAT & y in Union f implies ex n being Nat st
( y in f . n & ( for m being Nat st y in f . m holds
n <= m ) ) )
assume A1: ( dom f = NAT & y in Union f ) ; :: thesis: ex n being Nat st
( y in f . n & ( for m being Nat st y in f . m holds
n <= m ) )
defpred S₁[ Nat] means y in f . $1;
consider n being object such that
A2: ( n in dom f & y in f . n ) by A1, CARD_5:2;
reconsider n = n as Nat by A1, A2;
y in f . n by A2;
then A3: ex n being Nat st S₁[n] ;
ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A3);
hence ex n being Nat st
( y in f . n & ( for m being Nat st y in f . m holds
n <= m ) ) ; :: thesis: verum