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 = { n | E! m e. n ( m C_ n /\ suc m = n ) }

Proof

Step Hyp Ref Expression
1 dfsuccl3 
 |-  Suc = { n | E! m suc m = n }
2 sucidg 
 |-  ( m e. _V -> m e. suc m )
3 2 elv 
 |-  m e. suc m
4 eleq2 
 |-  ( suc m = n -> ( m e. suc m <-> m e. n ) )
5 3 4 mpbii 
 |-  ( suc m = n -> m e. n )
6 sssucid 
 |-  m C_ suc m
7 sseq2 
 |-  ( suc m = n -> ( m C_ suc m <-> m C_ n ) )
8 6 7 mpbii 
 |-  ( suc m = n -> m C_ n )
9 5 8 jca 
 |-  ( suc m = n -> ( m e. n /\ m C_ n ) )
10 9 pm4.71ri 
 |-  ( suc m = n <-> ( ( m e. n /\ m C_ n ) /\ suc m = n ) )
11 df-3an 
 |-  ( ( m e. n /\ m C_ n /\ suc m = n ) <-> ( ( m e. n /\ m C_ n ) /\ suc m = n ) )
12 3anass 
 |-  ( ( m e. n /\ m C_ n /\ suc m = n ) <-> ( m e. n /\ ( m C_ n /\ suc m = n ) ) )
13 10 11 12 3bitr2i 
 |-  ( suc m = n <-> ( m e. n /\ ( m C_ n /\ suc m = n ) ) )
14 13 eubii 
 |-  ( E! m suc m = n <-> E! m ( m e. n /\ ( m C_ n /\ suc m = n ) ) )
15 df-reu 
 |-  ( E! m e. n ( m C_ n /\ suc m = n ) <-> E! m ( m e. n /\ ( m C_ n /\ suc m = n ) ) )
16 14 15 bitr4i 
 |-  ( E! m suc m = n <-> E! m e. n ( m C_ n /\ suc m = n ) )
17 16 abbii 
 |-  { n | E! m suc m = n } = { n | E! m e. n ( m C_ n /\ suc m = n ) }
18 1 17 eqtri 
 |-  Suc = { n | E! m e. n ( m C_ n /\ suc m = n ) }