Metamath Proof Explorer


Theorem fnexALT

Description: Alternate proof of fnex , derived using the Axiom of Replacement in the form of funimaexg . This version uses ax-pow and ax-un , whereas fnex does not. (Contributed by NM, 14-Aug-1994) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion fnexALT ( ( 𝐹 Fn 𝐴𝐴𝐵 ) → 𝐹 ∈ V )

Proof

Step Hyp Ref Expression
1 fnrel ( 𝐹 Fn 𝐴 → Rel 𝐹 )
2 relssdmrn ( Rel 𝐹𝐹 ⊆ ( dom 𝐹 × ran 𝐹 ) )
3 1 2 syl ( 𝐹 Fn 𝐴𝐹 ⊆ ( dom 𝐹 × ran 𝐹 ) )
4 3 adantr ( ( 𝐹 Fn 𝐴𝐴𝐵 ) → 𝐹 ⊆ ( dom 𝐹 × ran 𝐹 ) )
5 fndm ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
6 5 eleq1d ( 𝐹 Fn 𝐴 → ( dom 𝐹𝐵𝐴𝐵 ) )
7 6 biimpar ( ( 𝐹 Fn 𝐴𝐴𝐵 ) → dom 𝐹𝐵 )
8 fnfun ( 𝐹 Fn 𝐴 → Fun 𝐹 )
9 funimaexg ( ( Fun 𝐹𝐴𝐵 ) → ( 𝐹𝐴 ) ∈ V )
10 8 9 sylan ( ( 𝐹 Fn 𝐴𝐴𝐵 ) → ( 𝐹𝐴 ) ∈ V )
11 imadmrn ( 𝐹 “ dom 𝐹 ) = ran 𝐹
12 5 imaeq2d ( 𝐹 Fn 𝐴 → ( 𝐹 “ dom 𝐹 ) = ( 𝐹𝐴 ) )
13 11 12 eqtr3id ( 𝐹 Fn 𝐴 → ran 𝐹 = ( 𝐹𝐴 ) )
14 13 eleq1d ( 𝐹 Fn 𝐴 → ( ran 𝐹 ∈ V ↔ ( 𝐹𝐴 ) ∈ V ) )
15 14 biimpar ( ( 𝐹 Fn 𝐴 ∧ ( 𝐹𝐴 ) ∈ V ) → ran 𝐹 ∈ V )
16 10 15 syldan ( ( 𝐹 Fn 𝐴𝐴𝐵 ) → ran 𝐹 ∈ V )
17 xpexg ( ( dom 𝐹𝐵 ∧ ran 𝐹 ∈ V ) → ( dom 𝐹 × ran 𝐹 ) ∈ V )
18 7 16 17 syl2anc ( ( 𝐹 Fn 𝐴𝐴𝐵 ) → ( dom 𝐹 × ran 𝐹 ) ∈ V )
19 ssexg ( ( 𝐹 ⊆ ( dom 𝐹 × ran 𝐹 ) ∧ ( dom 𝐹 × ran 𝐹 ) ∈ V ) → 𝐹 ∈ V )
20 4 18 19 syl2anc ( ( 𝐹 Fn 𝐴𝐴𝐵 ) → 𝐹 ∈ V )