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

Metamath Proof Explorer

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 𝑚 = 𝑛 ) }