Theorem fnex 3607

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 3575.

Assertion

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

Proof of Theorem fnex

Step	Hyp	Ref	Expression
1		ssexg 2721	. 2 |- ((F (_ (dom F X. ran F) /\ (dom F X. ran F) e. V) -> F e. V)
2		fnrel 3586	. . . 4 |- (F Fn A -> Rel F)
3		relssdr 3513	. . . 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 3259	. . 3 |- ((dom F e. B /\ ran F e. V) -> (dom F X. ran F) e. V)
7		fndm 3587	. . . . 5 |- (F Fn A -> dom F = A)
8	7	eleq1d 1540	. . . 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 3575	. . . . 5 |- ((Fun F /\ A e. B) -> (F"A) e. V)
11		fnfun 3585	. . . . 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 3404	. . . . . . 7 |- (F Fn A -> (F"dom F) = (F"A))
14		imadmrn 3414	. . . . . . 7 |- (F"dom F) = ran F
15	13, 14	syl5eqr 1521	. . . . . 6 |- (F Fn A -> ran F = (F"A))
16	15	eleq1d 1540	. . . . 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 958  Vcvv 1811   (_ wss 2047   X. cxp 3168  dom cdm 3170  ran crn 3171  "cima 3173  Rel wrel 3175  Fun wfun 3176   Fn wfn 3177

This theorem is referenced by:  funex 3608  fex 3652  tfrlem12 3922  f1oeng 4395  unfilem3 4550  aceq3lem 4732  ac6lem 4754  ser1absdiflem 6929  climaddc 7132  climmulc 7133  caucvg3a 7164  caucvg3lem 7166  cvgcmp2clem 7182  geolimilem 7235

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703  ax-pow 2742  ax-pr 2779  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-id 2835  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fun 3192  df-fn 3193

Copyright terms: Public domain