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 dom SucMap = V

Proof

Step Hyp Ref Expression
1 ssv ⊢ dom SucMap ⊆ V
2 sucexg ⊢ ( 𝑚 ∈ V → suc 𝑚 ∈ V )
3 2 elv ⊢ suc 𝑚 ∈ V
4 3 isseti ⊢ ∃ 𝑛 𝑛 = suc 𝑚
5 brsucmap ⊢ ( ( 𝑚 ∈ V ∧ 𝑛 ∈ V ) → ( 𝑚 SucMap 𝑛 ↔ suc 𝑚 = 𝑛 ) )
6 5 el2v ⊢ ( 𝑚 SucMap 𝑛 ↔ suc 𝑚 = 𝑛 )
7 eqcom ⊢ ( suc 𝑚 = 𝑛 ↔ 𝑛 = suc 𝑚 )
8 6 7 bitri ⊢ ( 𝑚 SucMap 𝑛 ↔ 𝑛 = suc 𝑚 )
9 8 exbii ⊢ ( ∃ 𝑛 𝑚 SucMap 𝑛 ↔ ∃ 𝑛 𝑛 = suc 𝑚 )
10 4 9 mpbir ⊢ ∃ 𝑛 𝑚 SucMap 𝑛
11 10 rgenw ⊢ ∀ 𝑚 ∈ V ∃ 𝑛 𝑚 SucMap 𝑛
12 ssdmral ⊢ ( V ⊆ dom SucMap ↔ ∀ 𝑚 ∈ V ∃ 𝑛 𝑚 SucMap 𝑛 )
13 11 12 mpbir ⊢ V ⊆ dom SucMap
14 1 13 eqssi ⊢ dom SucMap = V