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 e/ _V
	fonex.2	|- F : A -onto-> B
Assertion	fonex	|- A e/ _V

Proof

Step	Hyp	Ref	Expression
1		fonex.1	|- B e/ _V
2		fonex.2	|- F : A -onto-> B
3	1	neli	|- -. B e. _V
4		fofun	|- ( F : A -onto-> B -> Fun F )
5	2 4	ax-mp	|- Fun F
6		funrnex	|- ( dom F e. _V -> ( Fun F -> ran F e. _V ) )
7	5 6	mpi	|- ( dom F e. _V -> ran F e. _V )
8		fofn	|- ( F : A -onto-> B -> F Fn A )
9	2 8	ax-mp	|- F Fn A
10	9	fndmi	|- dom F = A
11	10	eleq1i	|- ( dom F e. _V <-> A e. _V )
12		forn	|- ( F : A -onto-> B -> ran F = B )
13	2 12	ax-mp	|- ran F = B
14	13	eleq1i	|- ( ran F e. _V <-> B e. _V )
15	7 11 14	3imtr3i	|- ( A e. _V -> B e. _V )
16	3 15	mto	|- -. A e. _V
17	16	nelir	|- A e/ _V