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	$$⊢B\notin \mathrm{V}$$
	fonex.2	$$⊢F:A\underset{onto}{⟶}B$$
Assertion	fonex	$$⊢A\notin \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		fonex.1	$$⊢B\notin \mathrm{V}$$
2		fonex.2	$$⊢F:A\underset{onto}{⟶}B$$
3	1	neli	$$⊢\neg B\in \mathrm{V}$$
4		fofun	$$⊢F:A\underset{onto}{⟶}B\to \mathrm{Fun}F$$
5	2 4	ax-mp	$$⊢\mathrm{Fun}F$$
6		funrnex	$$⊢\mathrm{dom}F\in \mathrm{V}\to \left(\mathrm{Fun}F\to \mathrm{ran}F\in \mathrm{V}\right)$$
7	5 6	mpi	$$⊢\mathrm{dom}F\in \mathrm{V}\to \mathrm{ran}F\in \mathrm{V}$$
8		fofn	$$⊢F:A\underset{onto}{⟶}B\to FFnA$$
9	2 8	ax-mp	$$⊢FFnA$$
10	9	fndmi	$$⊢\mathrm{dom}F=A$$
11	10	eleq1i	$$⊢\mathrm{dom}F\in \mathrm{V}\leftrightarrow A\in \mathrm{V}$$
12		forn	$$⊢F:A\underset{onto}{⟶}B\to \mathrm{ran}F=B$$
13	2 12	ax-mp	$$⊢\mathrm{ran}F=B$$
14	13	eleq1i	$$⊢\mathrm{ran}F\in \mathrm{V}\leftrightarrow B\in \mathrm{V}$$
15	7 11 14	3imtr3i	$$⊢A\in \mathrm{V}\to B\in \mathrm{V}$$
16	3 15	mto	$$⊢\neg A\in \mathrm{V}$$
17	16	nelir	$$⊢A\notin \mathrm{V}$$