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 Could not format assertion : No typesetting found for |- Suc = { n | E! m e. n ( m C_ n /\ suc m = n ) } with typecode |-

Proof

Step Hyp Ref Expression
1 dfsuccl3 Could not format Suc = { n | E! m suc m = n } : No typesetting found for |- Suc = { n | E! m suc m = n } with typecode |-
2 sucidg ⊢ m ∈ V → m ∈ suc ⁡ m
3 2 elv ⊢ m ∈ suc ⁡ m
4 eleq2 ⊢ suc ⁡ m = n → m ∈ suc ⁡ m ↔ m ∈ n
5 3 4 mpbii ⊢ suc ⁡ m = n → m ∈ n
6 sssucid ⊢ m ⊆ suc ⁡ m
7 sseq2 ⊢ suc ⁡ m = n → m ⊆ suc ⁡ m ↔ m ⊆ n
8 6 7 mpbii ⊢ suc ⁡ m = n → m ⊆ n
9 5 8 jca ⊢ suc ⁡ m = n → m ∈ n ∧ m ⊆ n
10 9 pm4.71ri ⊢ suc ⁡ m = n ↔ m ∈ n ∧ m ⊆ n ∧ suc ⁡ m = n
11 df-3an ⊢ m ∈ n ∧ m ⊆ n ∧ suc ⁡ m = n ↔ m ∈ n ∧ m ⊆ n ∧ suc ⁡ m = n
12 3anass ⊢ m ∈ n ∧ m ⊆ n ∧ suc ⁡ m = n ↔ m ∈ n ∧ m ⊆ n ∧ suc ⁡ m = n
13 10 11 12 3bitr2i ⊢ suc ⁡ m = n ↔ m ∈ n ∧ m ⊆ n ∧ suc ⁡ m = n
14 13 eubii ⊢ ∃! m suc ⁡ m = n ↔ ∃! m m ∈ n ∧ m ⊆ n ∧ suc ⁡ m = n
15 df-reu ⊢ ∃! m ∈ n m ⊆ n ∧ suc ⁡ m = n ↔ ∃! m m ∈ n ∧ m ⊆ n ∧ suc ⁡ m = n
16 14 15 bitr4i ⊢ ∃! m suc ⁡ m = n ↔ ∃! m ∈ n m ⊆ n ∧ suc ⁡ m = n
17 16 abbii ⊢ n | ∃! m suc ⁡ m = n = n | ∃! m ∈ n m ⊆ n ∧ suc ⁡ m = n
18 1 17 eqtri Could not format Suc = { n | E! m e. n ( m C_ n /\ suc m = n ) } : No typesetting found for |- Suc = { n | E! m e. n ( m C_ n /\ suc m = n ) } with typecode |-