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	Could not format assertion : No typesetting found for |- Pet2Ers = ( SucMap ShiftStable PetErs ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpet2ers	Could not format Pet2Ers : No typesetting found for class Pet2Ers with typecode class
1		csucmap	Could not format SucMap : No typesetting found for class SucMap with typecode class
2		cpeters	Could not format PetErs : No typesetting found for class PetErs with typecode class
3	1 2	cshiftstable	Could not format ( SucMap ShiftStable PetErs ) : No typesetting found for class ( SucMap ShiftStable PetErs ) with typecode class
4	0 3	wceq	Could not format Pet2Ers = ( SucMap ShiftStable PetErs ) : No typesetting found for wff Pet2Ers = ( SucMap ShiftStable PetErs ) with typecode wff