Theorem fonex

Description: The domain of a surjection is a proper class if the range is a proper class as well. Can be used to prove that if a structure component extractor restricted to a class maps onto a proper class, then the class is a proper class as well. (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Hypotheses	fonex.1	⊢ 𝐵 ∉ V
	fonex.2	⊢ 𝐹 : 𝐴 –onto→ 𝐵
Assertion	fonex	⊢ 𝐴 ∉ V

Proof

Step	Hyp	Ref	Expression
1		fonex.1	⊢ 𝐵 ∉ V
2		fonex.2	⊢ 𝐹 : 𝐴 –onto→ 𝐵
3	1	neli	⊢ ¬ 𝐵 ∈ V
4		fofun	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → Fun 𝐹 )
5	2 4	ax-mp	⊢ Fun 𝐹
6		funrnex	⊢ ( dom 𝐹 ∈ V → ( Fun 𝐹 → ran 𝐹 ∈ V ) )
7	5 6	mpi	⊢ ( dom 𝐹 ∈ V → ran 𝐹 ∈ V )
8		fofn	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 Fn 𝐴 )
9	2 8	ax-mp	⊢ 𝐹 Fn 𝐴
10	9	fndmi	⊢ dom 𝐹 = 𝐴
11	10	eleq1i	⊢ ( dom 𝐹 ∈ V ↔ 𝐴 ∈ V )
12		forn	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
13	2 12	ax-mp	⊢ ran 𝐹 = 𝐵
14	13	eleq1i	⊢ ( ran 𝐹 ∈ V ↔ 𝐵 ∈ V )
15	7 11 14	3imtr3i	⊢ ( 𝐴 ∈ V → 𝐵 ∈ V )
16	3 15	mto	⊢ ¬ 𝐴 ∈ V
17	16	nelir	⊢ 𝐴 ∉ V