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 × MembParts ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs } ) ∩ BlockLiftFix ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-pet2parts | ⊢ Pet2Parts = ( SucMap ShiftStable PetParts ) | |
| 2 | dfpetparts2 | ⊢ PetParts = ( ( ( Rels × MembParts ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs } ) ∩ BlockLiftFix ) | |
| 3 | shiftstableeq2 | ⊢ ( PetParts = ( ( ( Rels × MembParts ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs } ) ∩ BlockLiftFix ) → ( SucMap ShiftStable PetParts ) = ( SucMap ShiftStable ( ( ( Rels × MembParts ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs } ) ∩ BlockLiftFix ) ) ) | |
| 4 | 2 3 | ax-mp | ⊢ ( SucMap ShiftStable PetParts ) = ( SucMap ShiftStable ( ( ( Rels × MembParts ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs } ) ∩ BlockLiftFix ) ) |
| 5 | 1 4 | eqtri | ⊢ Pet2Parts = ( SucMap ShiftStable ( ( ( Rels × MembParts ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs } ) ∩ BlockLiftFix ) ) |