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

Metamath Proof Explorer

Theorem sucmapsuc

Description: A set is succeeded by its successor. (Contributed by Peter Mazsa, 7-Jan-2026)

Ref Expression
Assertion sucmapsuc Could not format assertion : No typesetting found for |- ( M e. V -> M SucMap suc M ) with typecode |-

Proof

Step Hyp Ref Expression
1 eqid ⊢ suc ⁡ M = suc ⁡ M
2 sucexg ⊢ M ∈ V → suc ⁡ M ∈ V
3 brsucmap Could not format ( ( M e. V /\ suc M e. _V ) -> ( M SucMap suc M <-> suc M = suc M ) ) : No typesetting found for |- ( ( M e. V /\ suc M e. _V ) -> ( M SucMap suc M <-> suc M = suc M ) ) with typecode |-
4 2 3 mpdan Could not format ( M e. V -> ( M SucMap suc M <-> suc M = suc M ) ) : No typesetting found for |- ( M e. V -> ( M SucMap suc M <-> suc M = suc M ) ) with typecode |-
5 1 4 mpbiri Could not format ( M e. V -> M SucMap suc M ) : No typesetting found for |- ( M e. V -> M SucMap suc M ) with typecode |-