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