Metamath Proof Explorer

Theorem dmsucmap

Description: The domain of the successor map is the universe. (Contributed by Peter Mazsa, 7-Jan-2026)

Ref Expression
Assertion dmsucmap 
|- dom SucMap = _V

Proof

Step Hyp Ref Expression
1 ssv 
 |-  dom SucMap C_ _V
2 sucexg 
 |-  ( m e. _V -> suc m e. _V )
3 2 elv 
 |-  suc m e. _V
4 3 isseti 
 |-  E. n n = suc m
5 brsucmap 
 |-  ( ( m e. _V /\ n e. _V ) -> ( m SucMap n <-> suc m = n ) )
6 5 el2v 
 |-  ( m SucMap n <-> suc m = n )
7 eqcom 
 |-  ( suc m = n <-> n = suc m )
8 6 7 bitri 
 |-  ( m SucMap n <-> n = suc m )
9 8 exbii 
 |-  ( E. n m SucMap n <-> E. n n = suc m )
10 4 9 mpbir 
 |-  E. n m SucMap n
11 10 rgenw 
 |-  A. m e. _V E. n m SucMap n
12 ssdmral 
 |-  ( _V C_ dom SucMap <-> A. m e. _V E. n m SucMap n )
13 11 12 mpbir 
 |-  _V C_ dom SucMap
14 1 13 eqssi 
 |-  dom SucMap = _V