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	$$⊢\mathrm{suc}M=\mathrm{suc}M$$
2		sucexg	$$⊢M\in V\to \mathrm{suc}M\in \mathrm{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 |-