Theorem pets2eq 39712

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 39711	. . 3 ⊢ PetParts = PetErs
2		shiftstableeq2 39218	. . 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 39705	. 2 ⊢ Pet2Parts = ( SucMap ShiftStable PetParts )
5		df-pet2ers 39706	. 2 ⊢ Pet2Ers = ( SucMap ShiftStable PetErs )
6	3, 4, 5	3eqtr4i 2795	1 ⊢ Pet2Parts = Pet2Ers

This proof depends on syntax axioms:   = wceq 1570   SucMap csucmap 38913   ShiftStable cshiftstable 38917   PetErs cpeters 38945   Pet2Ers cpet2ers 38946   PetParts cpetparts 38962   Pet2Parts cpet2parts 38963

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3367  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-eprel 5559  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fo 6543  df-fv 6545  df-1st 7989  df-2nd 7990  df-ec 8701  df-qs 8705  df-xrn 39115  df-rels 39175  df-shiftstable 39217  df-coss 39236  df-coels 39237  df-ssr 39313  df-refs 39325  df-refrels 39326  df-refrel 39327  df-cnvrefs 39340  df-cnvrefrels 39341  df-cnvrefrel 39342  df-syms 39357  df-symrels 39358  df-symrel 39359  df-trs 39391  df-trrels 39392  df-trrel 39393  df-eqvrels 39403  df-eqvrel 39404  df-coeleqvrel 39406  df-dmqss 39457  df-dmqs 39458  df-ers 39483  df-erALTV 39484  df-comembers 39485  df-comember 39486  df-funALTV 39502  df-disjss 39523  df-disjs 39524  df-disjALTV 39525  df-eldisj 39527  df-parts 39603  df-part 39604  df-membparts 39605  df-membpart 39606  df-petparts 39703  df-peters 39704  df-pet2parts 39705  df-pet2ers 39706

This theorem is used by: (None)