Theorem dfpet2parts2

Description: Grade stability applied to the decomposed PetParts modules.

Pet2Parts is obtained by applying the grade-stability operator SucMap ShiftStable (see df-shiftstable ) to the modular intersection from dfpetparts2 . This makes the two orthogonal stability axes explicit:

(E) semantic stability / equilibrium: BlockLiftFix ,

(G) grade stability: SucMap ShiftStable ,

assembled on top of typedness and disjoint-span base modules.

This is the principled "extra level" that does not arise for Disjs : disjoint relations already bundle their internal map/carrier consistency via QMap and ElDisjs (see dfdisjs6 / dfdisjs7 ), while the present construction has an additional external grading axis imposed by the canonical successor map SucMap . (Contributed by Peter Mazsa, 20-Feb-2026) (Revised by Peter Mazsa, 25-Feb-2026)

	Ref	Expression
Assertion	dfpet2parts2	|- Pet2Parts = ( SucMap ShiftStable ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) )

Proof

Step	Hyp	Ref	Expression
1		df-pet2parts	|- Pet2Parts = ( SucMap ShiftStable PetParts )
2		dfpetparts2	|- PetParts = ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix )
3		shiftstableeq2	|- ( PetParts = ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) -> ( SucMap ShiftStable PetParts ) = ( SucMap ShiftStable ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) ) )
4	2 3	ax-mp	|- ( SucMap ShiftStable PetParts ) = ( SucMap ShiftStable ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) )
5	1 4	eqtri	|- Pet2Parts = ( SucMap ShiftStable ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) )