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 }