Metamath Proof Explorer

Theorem fornex

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

Ref Expression
Assertion fornex ⊢ A ∈ C → F : A ⟶ onto B → B ∈ V

Proof

Step Hyp Ref Expression
1 fofun ⊢ F : A ⟶ onto B → Fun ⁡ F
2 funrnex ⊢ dom ⁡ F ∈ C → Fun ⁡ F → ran ⁡ F ∈ V
3 1 2 syl5com ⊢ F : A ⟶ onto B → dom ⁡ F ∈ C → ran ⁡ F ∈ V
4 fof ⊢ F : A ⟶ onto B → F : A ⟶ B
5 4 fdmd ⊢ F : A ⟶ onto B → dom ⁡ F = A
6 5 eleq1d ⊢ F : A ⟶ onto B → dom ⁡ F ∈ C ↔ A ∈ C
7 forn ⊢ F : A ⟶ onto B → ran ⁡ F = B
8 7 eleq1d ⊢ F : A ⟶ onto B → ran ⁡ F ∈ V ↔ B ∈ V
9 3 6 8 3imtr3d ⊢ F : A ⟶ onto B → A ∈ C → B ∈ V
10 9 com12 ⊢ A ∈ C → F : A ⟶ onto B → B ∈ V