Theorem fnex 3604

Description: If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of funimaexg 3572.

Assertion

Ref	Expression
fnex	|- ((F Fn A /\ A e. B) -> F e. V)

Proof of Theorem fnex

Step	Hyp	Ref	Expression
1		ssexg 2718	. 2 |- ((F (_ (dom F X. ran F) /\ (dom F X. ran F) e. V) -> F e. V)
2		fnrel 3583	. . . 4 |- (F Fn A -> Rel F)
3		relssdr 3510	. . . 4 |- (Rel F -> F (_ (dom F X. ran F))
4	2, 3	syl 10	. . 3 |- (F Fn A -> F (_ (dom F X. ran F))
5	4	adantr 389	. 2 |- ((F Fn A /\ A e. B) -> F (_ (dom F X. ran F))
6		xpexg 3256	. . 3 |- ((dom F e. B /\ ran F e. V) -> (dom F X. ran F) e. V)
7		fndm 3584	. . . . 5 |- (F Fn A -> dom F = A)
8	7	eleq1d 1539	. . . 4 |- (F Fn A -> (dom F e. B <-> A e. B))
9	8	biimpar 417	. . 3 |- ((F Fn A /\ A e. B) -> dom F e. B)
10		funimaexg 3572	. . . . 5 |- ((Fun F /\ A e. B) -> (F"A) e. V)
11		fnfun 3582	. . . . 5 |- (F Fn A -> Fun F)
12	10, 11	sylan 448	. . . 4 |- ((F Fn A /\ A e. B) -> (F"A) e. V)
13	7	imaeq2d 3401	. . . . . . 7 |- (F Fn A -> (F"dom F) = (F"A))
14		imadmrn 3411	. . . . . . 7 |- (F"dom F) = ran F
15	13, 14	syl5eqr 1520	. . . . . 6 |- (F Fn A -> ran F = (F"A))
16	15	eleq1d 1539	. . . . 5 |- (F Fn A -> (ran F e. V <-> (F"A) e. V))
17	16	biimpar 417	. . . 4 |- ((F Fn A /\ (F"A) e. V) -> ran F e. V)
18	12, 17	syldan 467	. . 3 |- ((F Fn A /\ A e. B) -> ran F e. V)
19	6, 9, 18	sylanc 471	. 2 |- ((F Fn A /\ A e. B) -> (dom F X. ran F) e. V)
20	1, 5, 19	sylanc 471	1 |- ((F Fn A /\ A e. B) -> F e. V)

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 957  Vcvv 1809   (_ wss 2045   X. cxp 3165  dom cdm 3167  ran crn 3168  "cima 3170  Rel wrel 3172  Fun wfun 3173   Fn wfn 3174

This theorem is referenced by:  funex 3605  fex 3649  tfrlem12 3919  f1oeng 4389  unfilem3 4539  aceq3lem 4719  ac6lem 4741  ser1absdiflem 6895  climaddc 7101  climmulc 7102  caucvg3a 7133  caucvg3aOLD 7134  caucvg3lem 7136  caucvg3lemOLD 7137  cvgcmp2clem 7153  geolimilem 7206

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2690  ax-sep 2700  ax-pow 2739  ax-pr 2776  ax-un 2863

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-rex 1649  df-v 1810  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-nul 2279  df-pw 2400  df-sn 2410  df-pr 2411  df-op 2414  df-uni 2501  df-br 2617  df-opab 2664  df-id 2832  df-xp 3181  df-rel 3182  df-cnv 3183  df-co 3184  df-dm 3185  df-rn 3186  df-res 3187  df-ima 3188  df-fun 3189  df-fn 3190

Copyright terms: Public domain