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

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 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 ∈ V → suc ⁡ m ∈ V
3 2 elv ⊢ suc ⁡ m ∈ V
4 3 isseti ⊢ ∃ n n = 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 ⊢ suc ⁡ m = n ↔ n = 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 |-