Definition df-pet2ers 39141

Description: Define the class of grade- and blocklift-stable equivalence-side general partition-equivalence spans. The equivalence-side analogue of Pet2Parts: stability of PetErs under one-step grade shift along SucMap. Ensures that the equivalence-side formulation supports the same tower/grade infrastructure as the partition-side formulation. SucMap ShiftStable is the grade axis and does not change the equivalence-vs-partition viewpoint (reinforced by pets2eq 39147). (Contributed by Peter Mazsa, 19-Feb-2026.)

Assertion

Ref	Expression
df-pet2ers	⊢ Pet2Ers = ( SucMap ShiftStable PetErs )

Detailed syntax breakdown of Definition df-pet2ers

Step	Hyp	Ref	Expression
1		cpet2ers 38381	. 2 class Pet2Ers
2		csucmap 38348	. . 3 class SucMap
3		cpeters 38380	. . 3 class PetErs
4	2, 3	cshiftstable 38352	. 2 class ( SucMap ShiftStable PetErs )
5	1, 4	wceq 1542	1 wff Pet2Ers = ( SucMap ShiftStable PetErs )

This definition is referenced by:  pets2eq  39147