Theorem pets2eq

Description: Grade-stable generalized partition-equivalence identification. After applying the same grade-stability operator ( SucMap ShiftStable ) to both sides, the grade-stable pet classes still coincide. Confirms that the grade/tower infrastructure is orthogonal to the partition-vs-equivalence viewpoint: stability is preserved under the PetParts = PetErs identification. This is the level at which we can freely work on whichever side is more convenient ( Parts for block discipline, Ers for equivalence reasoning), without changing the stable notion of "pet". (Contributed by Peter Mazsa, 19-Feb-2026)

	Ref	Expression
Assertion	pets2eq	|- Pet2Parts = Pet2Ers

Proof

Step	Hyp	Ref	Expression
1		petseq	|- PetParts = PetErs
2		shiftstableeq2	|- ( PetParts = PetErs -> ( SucMap ShiftStable PetParts ) = ( SucMap ShiftStable PetErs ) )
3	1 2	ax-mp	|- ( SucMap ShiftStable PetParts ) = ( SucMap ShiftStable PetErs )
4		df-pet2parts	|- Pet2Parts = ( SucMap ShiftStable PetParts )
5		df-pet2ers	|- Pet2Ers = ( SucMap ShiftStable PetErs )
6	3 4 5	3eqtr4i	|- Pet2Parts = Pet2Ers