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

Metamath Proof Explorer

Theorem dfsuccf2

Description: Alternate definition of Scott Fenton's version of Succ , cf. df-sucmap . (Contributed by Peter Mazsa, 6-Jan-2026)

Ref Expression
Assertion dfsuccf2 
|- Succ = { <. m , n >. | suc m = n }

Proof

Step Hyp Ref Expression
1 df-succf 
 |-  Succ = ( Cup o. ( _I (x) Singleton ) )
2 df-co 
 |-  ( Cup o. ( _I (x) Singleton ) ) = { <. m , n >. | E. x ( m ( _I (x) Singleton ) x /\ x Cup n ) }
3 vex 
 |-  m e. _V
4 vex 
 |-  n e. _V
5 3 4 lemsuccf 
 |-  ( E. x ( m ( _I (x) Singleton ) x /\ x Cup n ) <-> n = suc m )
6 eqcom 
 |-  ( n = suc m <-> suc m = n )
7 5 6 bitri 
 |-  ( E. x ( m ( _I (x) Singleton ) x /\ x Cup n ) <-> suc m = n )
8 7 opabbii 
 |-  { <. m , n >. | E. x ( m ( _I (x) Singleton ) x /\ x Cup n ) } = { <. m , n >. | suc m = n }
9 1 2 8 3eqtri 
 |-  Succ = { <. m , n >. | suc m = n }