Theorem dfsuccl4

Description: Alternate definition that incorporates the most desirable properties of the successor class. (Contributed by Peter Mazsa, 30-Jan-2026)

	Ref	Expression
Assertion	dfsuccl4	⊢ Suc = { 𝑛 ∣ ∃! 𝑚 ∈ 𝑛 ( 𝑚 ⊆ 𝑛 ∧ suc 𝑚 = 𝑛 ) }

Proof

Step	Hyp	Ref	Expression
1		dfsuccl3	⊢ Suc = { 𝑛 ∣ ∃! 𝑚 suc 𝑚 = 𝑛 }
2		sucidg	⊢ ( 𝑚 ∈ V → 𝑚 ∈ suc 𝑚 )
3	2	elv	⊢ 𝑚 ∈ suc 𝑚
4		eleq2	⊢ ( suc 𝑚 = 𝑛 → ( 𝑚 ∈ suc 𝑚 ↔ 𝑚 ∈ 𝑛 ) )
5	3 4	mpbii	⊢ ( suc 𝑚 = 𝑛 → 𝑚 ∈ 𝑛 )
6		sssucid	⊢ 𝑚 ⊆ suc 𝑚
7		sseq2	⊢ ( suc 𝑚 = 𝑛 → ( 𝑚 ⊆ suc 𝑚 ↔ 𝑚 ⊆ 𝑛 ) )
8	6 7	mpbii	⊢ ( suc 𝑚 = 𝑛 → 𝑚 ⊆ 𝑛 )
9	5 8	jca	⊢ ( suc 𝑚 = 𝑛 → ( 𝑚 ∈ 𝑛 ∧ 𝑚 ⊆ 𝑛 ) )
10	9	pm4.71ri	⊢ ( suc 𝑚 = 𝑛 ↔ ( ( 𝑚 ∈ 𝑛 ∧ 𝑚 ⊆ 𝑛 ) ∧ suc 𝑚 = 𝑛 ) )
11		df-3an	⊢ ( ( 𝑚 ∈ 𝑛 ∧ 𝑚 ⊆ 𝑛 ∧ suc 𝑚 = 𝑛 ) ↔ ( ( 𝑚 ∈ 𝑛 ∧ 𝑚 ⊆ 𝑛 ) ∧ suc 𝑚 = 𝑛 ) )
12		3anass	⊢ ( ( 𝑚 ∈ 𝑛 ∧ 𝑚 ⊆ 𝑛 ∧ suc 𝑚 = 𝑛 ) ↔ ( 𝑚 ∈ 𝑛 ∧ ( 𝑚 ⊆ 𝑛 ∧ suc 𝑚 = 𝑛 ) ) )
13	10 11 12	3bitr2i	⊢ ( suc 𝑚 = 𝑛 ↔ ( 𝑚 ∈ 𝑛 ∧ ( 𝑚 ⊆ 𝑛 ∧ suc 𝑚 = 𝑛 ) ) )
14	13	eubii	⊢ ( ∃! 𝑚 suc 𝑚 = 𝑛 ↔ ∃! 𝑚 ( 𝑚 ∈ 𝑛 ∧ ( 𝑚 ⊆ 𝑛 ∧ suc 𝑚 = 𝑛 ) ) )
15		df-reu	⊢ ( ∃! 𝑚 ∈ 𝑛 ( 𝑚 ⊆ 𝑛 ∧ suc 𝑚 = 𝑛 ) ↔ ∃! 𝑚 ( 𝑚 ∈ 𝑛 ∧ ( 𝑚 ⊆ 𝑛 ∧ suc 𝑚 = 𝑛 ) ) )
16	14 15	bitr4i	⊢ ( ∃! 𝑚 suc 𝑚 = 𝑛 ↔ ∃! 𝑚 ∈ 𝑛 ( 𝑚 ⊆ 𝑛 ∧ suc 𝑚 = 𝑛 ) )
17	16	abbii	⊢ { 𝑛 ∣ ∃! 𝑚 suc 𝑚 = 𝑛 } = { 𝑛 ∣ ∃! 𝑚 ∈ 𝑛 ( 𝑚 ⊆ 𝑛 ∧ suc 𝑚 = 𝑛 ) }
18	1 17	eqtri	⊢ Suc = { 𝑛 ∣ ∃! 𝑚 ∈ 𝑛 ( 𝑚 ⊆ 𝑛 ∧ suc 𝑚 = 𝑛 ) }