Definition df-pet2ers

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 ). (Contributed by Peter Mazsa, 19-Feb-2026)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpet2ers	⊢ Pet2Ers
1		csucmap	⊢ SucMap
2		cpeters	⊢ PetErs
3	1 2	cshiftstable	⊢ ( SucMap ShiftStable PetErs )
4	0 3	wceq	⊢ Pet2Ers = ( SucMap ShiftStable PetErs )