This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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