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