let X be set ; :: thesis: for psi being Ordinal-Sequence holds Union (X |` psi) is epsilon-transitive epsilon-connected set
let psi be Ordinal-Sequence; :: thesis: Union (X |` psi) is epsilon-transitive epsilon-connected set
consider A being Ordinal such that
A1: rng psi c= A by ORDINAL2:def 4;
A2: rng (X |` psi) c= rng psi by RELAT_1:87;
A3: now :: thesis: for x being object st x in rng (X |` psi) holds
x is Ordinal
let x be object ; :: thesis: ( x in rng (X |` psi) implies x is Ordinal )
assume x in rng (X |` psi) ; :: thesis: x is Ordinal
then x in A by A1, A2;
hence x is Ordinal ; :: thesis: verum
end;
Union (X |` psi) = union (rng (X |` psi)) by CARD_3:def 4;
hence Union (X |` psi) is epsilon-transitive epsilon-connected set by A3, ORDINAL1:23; :: thesis: verum