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

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 )

hence
phi " A is epsilon-transitive epsilon-connected set
by ORDINAL1:19; :: thesis: verum( 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

end;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;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