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

Metamath Proof Explorer

Theorem focdmex

Description: If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004)

Ref Expression
Assertion focdmex ( 𝐴 ∈ 𝐶 → ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐵 ∈ V ) )

Proof

Step Hyp Ref Expression
1 fofun ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → Fun 𝐹 )
2 funrnex ⊢ ( dom 𝐹 ∈ 𝐶 → ( Fun 𝐹 → ran 𝐹 ∈ V ) )
3 1 2 syl5com ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( dom 𝐹 ∈ 𝐶 → ran 𝐹 ∈ V ) )
4 fof ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
5 4 fdmd ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → dom 𝐹 = 𝐴 )
6 5 eleq1d ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( dom 𝐹 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶 ) )
7 forn ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
8 7 eleq1d ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ran 𝐹 ∈ V ↔ 𝐵 ∈ V ) )
9 3 6 8 3imtr3d ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝐴 ∈ 𝐶 → 𝐵 ∈ V ) )
10 9 com12 ⊢ ( 𝐴 ∈ 𝐶 → ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐵 ∈ V ) )