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 = { ⟨ 𝑚 , 𝑛 ⟩ ∣ suc 𝑚 = 𝑛 }

Proof

Step	Hyp	Ref	Expression
1		df-succf	⊢ Succ = ( Cup ∘ ( I ⊗ Singleton ) )
2		df-co	⊢ ( Cup ∘ ( I ⊗ Singleton ) ) = { ⟨ 𝑚 , 𝑛 ⟩ ∣ ∃ 𝑥 ( 𝑚 ( I ⊗ Singleton ) 𝑥 ∧ 𝑥 Cup 𝑛 ) }
3		vex	⊢ 𝑚 ∈ V
4		vex	⊢ 𝑛 ∈ V
5	3 4	lemsuccf	⊢ ( ∃ 𝑥 ( 𝑚 ( I ⊗ Singleton ) 𝑥 ∧ 𝑥 Cup 𝑛 ) ↔ 𝑛 = suc 𝑚 )
6		eqcom	⊢ ( 𝑛 = suc 𝑚 ↔ suc 𝑚 = 𝑛 )
7	5 6	bitri	⊢ ( ∃ 𝑥 ( 𝑚 ( I ⊗ Singleton ) 𝑥 ∧ 𝑥 Cup 𝑛 ) ↔ suc 𝑚 = 𝑛 )
8	7	opabbii	⊢ { ⟨ 𝑚 , 𝑛 ⟩ ∣ ∃ 𝑥 ( 𝑚 ( I ⊗ Singleton ) 𝑥 ∧ 𝑥 Cup 𝑛 ) } = { ⟨ 𝑚 , 𝑛 ⟩ ∣ suc 𝑚 = 𝑛 }
9	1 2 8	3eqtri	⊢ Succ = { ⟨ 𝑚 , 𝑛 ⟩ ∣ suc 𝑚 = 𝑛 }