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