Theorem dmsucmap

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

	Ref	Expression
Assertion	dmsucmap	Could not format assertion : No typesetting found for |- dom SucMap = _V with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ssv	Could not format dom SucMap C_ _V : No typesetting found for |- dom SucMap C_ _V with typecode |-
2		sucexg	$$⊢m\in \mathrm{V}\to \mathrm{suc}m\in \mathrm{V}$$
3	2	elv	$$⊢\mathrm{suc}m\in \mathrm{V}$$
4	3	isseti	$$⊢\exists nn=\mathrm{suc}m$$
5		brsucmap	Could not format ( ( m e. _V /\ n e. _V ) -> ( m SucMap n <-> suc m = n ) ) : No typesetting found for |- ( ( m e. _V /\ n e. _V ) -> ( m SucMap n <-> suc m = n ) ) with typecode |-
6	5	el2v	Could not format ( m SucMap n <-> suc m = n ) : No typesetting found for |- ( m SucMap n <-> suc m = n ) with typecode |-
7		eqcom	$$⊢\mathrm{suc}m=n\leftrightarrow n=\mathrm{suc}m$$
8	6 7	bitri	Could not format ( m SucMap n <-> n = suc m ) : No typesetting found for |- ( m SucMap n <-> n = suc m ) with typecode |-
9	8	exbii	Could not format ( E. n m SucMap n <-> E. n n = suc m ) : No typesetting found for |- ( E. n m SucMap n <-> E. n n = suc m ) with typecode |-
10	4 9	mpbir	Could not format E. n m SucMap n : No typesetting found for |- E. n m SucMap n with typecode |-
11	10	rgenw	Could not format A. m e. _V E. n m SucMap n : No typesetting found for |- A. m e. _V E. n m SucMap n with typecode |-
12		ssdmral	Could not format ( _V C_ dom SucMap <-> A. m e. _V E. n m SucMap n ) : No typesetting found for |- ( _V C_ dom SucMap <-> A. m e. _V E. n m SucMap n ) with typecode |-
13	11 12	mpbir	Could not format _V C_ dom SucMap : No typesetting found for |- _V C_ dom SucMap with typecode |-
14	1 13	eqssi	Could not format dom SucMap = _V : No typesetting found for |- dom SucMap = _V with typecode |-