This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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