This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )