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	Could not format assertion : No typesetting found for |- Pet2Parts = Pet2Ers with typecode |-

Proof

Step	Hyp	Ref	Expression
1		petseq	Could not format PetParts = PetErs : No typesetting found for |- PetParts = PetErs with typecode |-
2		shiftstableeq2	Could not format ( PetParts = PetErs -> ( SucMap ShiftStable PetParts ) = ( SucMap ShiftStable PetErs ) ) : No typesetting found for |- ( PetParts = PetErs -> ( SucMap ShiftStable PetParts ) = ( SucMap ShiftStable PetErs ) ) with typecode |-
3	1 2	ax-mp	Could not format ( SucMap ShiftStable PetParts ) = ( SucMap ShiftStable PetErs ) : No typesetting found for |- ( SucMap ShiftStable PetParts ) = ( SucMap ShiftStable PetErs ) with typecode |-
4		df-pet2parts	Could not format Pet2Parts = ( SucMap ShiftStable PetParts ) : No typesetting found for |- Pet2Parts = ( SucMap ShiftStable PetParts ) with typecode |-
5		df-pet2ers	Could not format Pet2Ers = ( SucMap ShiftStable PetErs ) : No typesetting found for |- Pet2Ers = ( SucMap ShiftStable PetErs ) with typecode |-
6	3 4 5	3eqtr4i	Could not format Pet2Parts = Pet2Ers : No typesetting found for |- Pet2Parts = Pet2Ers with typecode |-