let X, Y be set ; :: thesis: ( X c= Y & Y is epsilon-transitive implies the_transitive-closure_of X c= Y )
assume that
A1: X c= Y and
A2: Y is epsilon-transitive ; :: thesis: the_transitive-closure_of X c= Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the_transitive-closure_of X or x in Y )
assume x in the_transitive-closure_of X ; :: thesis: x in Y
then consider f being Function, n being Element of omega such that
A3: x in f . n and
dom f = omega and
A4: f . 0 = X and
A5: for k being Nat holds f . (succ k) = union (f . k) by Def7;
defpred S1[ Nat] means f . $1 c= Y;
A6: S1[ 0 ] by A1, A4;
A7: for k being Nat st S1[k] holds
S1[ succ k]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[ succ k] )
assume f . k c= Y ; :: thesis: S1[ succ k]
then A8: union (f . k) c= union Y by ZFMISC_1:77;
( f . (succ k) = union (f . k) & union Y c= Y ) by A2, A5, Th48;
hence S1[ succ k] by A8, XBOOLE_1:1; :: thesis: verum
end;
S1[n] from ORDINAL2:sch 17(A6, A7);
hence x in Y by A3; :: thesis: verum