Theorem focdmex

Description: The codomain of an onto function is a set if its domain is a set. (Contributed by AV, 4-May-2021)

	Ref	Expression
Assertion	focdmex	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		fof	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
2	1	anim2i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) )
3	2	ancomd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) )
4		fex	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
5		rnexg	⊢ ( 𝐹 ∈ V → ran 𝐹 ∈ V )
6	3 4 5	3syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ran 𝐹 ∈ V )
7		forn	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
8	7	eleq1d	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ran 𝐹 ∈ V ↔ 𝐵 ∈ V ) )
9	8	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ( ran 𝐹 ∈ V ↔ 𝐵 ∈ V ) )
10	6 9	mpbid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ∈ V )