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 ⊢ 𝖲𝗎𝖼𝖼 = m n | suc ⁡ m = n

Proof

Step Hyp Ref Expression
1 df-succf ⊢ 𝖲𝗎𝖼𝖼 = 𝖢𝗎𝗉 ∘ I ⊗ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇
2 df-co ⊢ 𝖢𝗎𝗉 ∘ I ⊗ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 = m n | ∃ x m I ⊗ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 x ∧ x 𝖢𝗎𝗉 n
3 vex ⊢ m ∈ V
4 vex ⊢ n ∈ V
5 3 4 lemsuccf ⊢ ∃ x m I ⊗ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 x ∧ x 𝖢𝗎𝗉 n ↔ n = suc ⁡ m
6 eqcom ⊢ n = suc ⁡ m ↔ suc ⁡ m = n
7 5 6 bitri ⊢ ∃ x m I ⊗ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 x ∧ x 𝖢𝗎𝗉 n ↔ suc ⁡ m = n
8 7 opabbii ⊢ m n | ∃ x m I ⊗ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 x ∧ x 𝖢𝗎𝗉 n = m n | suc ⁡ m = n
9 1 2 8 3eqtri ⊢ 𝖲𝗎𝖼𝖼 = m n | suc ⁡ m = n