Theorem pets2eq 39147

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.)

Assertion

Ref	Expression
pets2eq	⊢ Pet2Parts = Pet2Ers

Proof of Theorem pets2eq

Step	Hyp	Ref	Expression
1		petseq 39146	. . 3 ⊢ PetParts = PetErs
2		shiftstableeq2 38653	. . 3 ⊢ ( PetParts = PetErs → ( SucMap ShiftStable PetParts ) = ( SucMap ShiftStable PetErs ))
3	1, 2	ax-mp 5	. 2 ⊢ ( SucMap ShiftStable PetParts ) = ( SucMap ShiftStable PetErs )
4		df-pet2parts 39140	. 2 ⊢ Pet2Parts = ( SucMap ShiftStable PetParts )
5		df-pet2ers 39141	. 2 ⊢ Pet2Ers = ( SucMap ShiftStable PetErs )
6	3, 4, 5	3eqtr4i 2768	1 ⊢ Pet2Parts = Pet2Ers

Syntax hints:   = wceq 1542   SucMap csucmap 38348   ShiftStable cshiftstable 38352   PetErs cpeters 38380   Pet2Ers cpet2ers 38381   PetParts cpetparts 38397   Pet2Parts cpet2parts 38398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707  ax-rep 5223  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rmo 3349  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4947  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5518  df-eprel 5523  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-fo 6497  df-fv 6499  df-1st 7933  df-2nd 7934  df-ec 8637  df-qs 8641  df-xrn 38550  df-rels 38610  df-shiftstable 38652  df-coss 38671  df-coels 38672  df-ssr 38748  df-refs 38760  df-refrels 38761  df-refrel 38762  df-cnvrefs 38775  df-cnvrefrels 38776  df-cnvrefrel 38777  df-syms 38792  df-symrels 38793  df-symrel 38794  df-trs 38826  df-trrels 38827  df-trrel 38828  df-eqvrels 38838  df-eqvrel 38839  df-coeleqvrel 38841  df-dmqss 38892  df-dmqs 38893  df-ers 38918  df-erALTV 38919  df-comembers 38920  df-comember 38921  df-funALTV 38937  df-disjss 38958  df-disjs 38959  df-disjALTV 38960  df-eldisj 38962  df-parts 39038  df-part 39039  df-membparts 39040  df-membpart 39041  df-petparts 39138  df-peters 39139  df-pet2parts 39140  df-pet2ers 39141

This theorem is referenced by: (None)