let X, W be set ; ( W is Tarski & ( ( X in W & W is epsilon-transitive ) or ( X in W & X c= W ) or ( card X in card W & X c= W ) ) implies Funcs (X,W) c= W )
assume A1:
W is Tarski
; ( ( not ( X in W & W is epsilon-transitive ) & not ( X in W & X c= W ) & not ( card X in card W & X c= W ) ) or Funcs (X,W) c= W )
assume A2:
( ( X in W & W is epsilon-transitive ) or ( X in W & X c= W ) or ( card X in card W & X c= W ) )
; Funcs (X,W) c= W
A3:
card X in card W
by A1, A2, Th1;
let x be object ; TARSKI:def 3 ( not x in Funcs (X,W) or x in W )
assume A4:
x in Funcs (X,W)
; x in W
then consider f being Function such that
A5:
x = f
and
A6:
dom f = X
and
A7:
rng f c= W
by FUNCT_2:def 2;
A8:
X c= W
by A2;
A9:
f c= W
proof
let y be
object ;
TARSKI:def 3 ( not y in f or y in W )
assume A10:
y in f
;
y in W
then consider y1,
y2 being
object such that A11:
[y1,y2] = y
by RELAT_1:def 1;
A12:
y1 in dom f
by A10, A11, FUNCT_1:1;
y2 = f . y1
by A10, A11, FUNCT_1:1;
then
y2 in rng f
by A12, FUNCT_1:def 3;
hence
y in W
by A1, A8, A6, A7, A11, A12, Th3;
verum
end;
card f = card X
by A4, A5, CARD_2:3;
hence
x in W
by A1, A3, A5, A9, CLASSES1:1; verum