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 | Could not format assertion : No typesetting found for |- Pet2Parts = ( SucMap ShiftStable ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) ) with typecode |- |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-pet2parts | Could not format Pet2Parts = ( SucMap ShiftStable PetParts ) : No typesetting found for |- Pet2Parts = ( SucMap ShiftStable PetParts ) with typecode |- | |
| 2 | dfpetparts2 | Could not format PetParts = ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) : No typesetting found for |- PetParts = ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) with typecode |- | |
| 3 | shiftstableeq2 | Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |- | |
| 4 | 2 3 | ax-mp | Could not format ( SucMap ShiftStable PetParts ) = ( SucMap ShiftStable ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) ) : No typesetting found for |- ( SucMap ShiftStable PetParts ) = ( SucMap ShiftStable ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) ) with typecode |- |
| 5 | 1 4 | eqtri | Could not format Pet2Parts = ( SucMap ShiftStable ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) ) : No typesetting found for |- Pet2Parts = ( SucMap ShiftStable ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) ) with typecode |- |