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	⊢ ( 𝐴 ∈ 𝐶 → ( 𝐹 : 𝐴 –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 ) )