let phi be Ordinal-Sequence; :: thesis: for A being Ordinal st phi is increasing holds
phi " A is epsilon-transitive epsilon-connected set
let A be Ordinal; :: thesis: ( phi is increasing implies phi " A is epsilon-transitive epsilon-connected set )
assume A1: for A, B being Ordinal st A in B & B in dom phi holds
phi . A in phi . B ; :: according to ORDINAL2:def 12 :: thesis: phi " A is epsilon-transitive epsilon-connected set
now :: thesis: for X being set st X in phi " A holds
( X is Ordinal & X c= phi " A )
let X be set ; :: thesis: ( X in phi " A implies ( X is Ordinal & X c= phi " A ) )
assume A2: X in phi " A ; :: thesis: ( X is Ordinal & X c= phi " A )
then A3: X in dom phi by FUNCT_1:def 7;
hence X is Ordinal ; :: thesis: X c= phi " A
reconsider B = X as Ordinal by A3;
A4: phi . X in A by A2, FUNCT_1:def 7;
thus X c= phi " A :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in phi " A )
assume A5: x in X ; :: thesis: x in phi " A
then x in B ;
then reconsider C = x, D = phi . B as Ordinal ;
reconsider E = phi . C as Ordinal ;
E in D by A1, A3, A5;
then A6: phi . x in A by A4, ORDINAL1:10;
C in dom phi by A3, A5, ORDINAL1:10;
hence x in phi " A by A6, FUNCT_1:def 7; :: thesis: verum
end;
end;
hence phi " A is epsilon-transitive epsilon-connected set by ORDINAL1:19; :: thesis: verum