Description: Alternate definition of PetParts as typedness + disjoint-span + block-lift equilibrium.
This theorem is the key modularization step. It decomposes PetParts into the intersection of three orthogonal modules:
(T) typedness: <. r , n >. e. ( Rels X. MembParts ) ,
(D) disjoint-span: ( r |X. (`' _E |`n ) ) e. Disjs ,
(E) semantic equilibrium: <. r , n >. e. BlockLiftFix , i.e. the carrier n is a fixpoint of the induced block-generation operator.
Conceptually, (D) provides the disjointness/quotient discipline for the lifted span, while (E) prevents hidden carrier drift (refinement or coarsening of what counts as a block) by enforcing the fixpoint equation. The point of this theorem is that these constraints can be imposed and reused independently by later constructions, while their intersection recovers the intended Parts-based notion.
This mirrors the internal packaging of Disjs (see dfdisjs6 / dfdisjs7 ): for disjoint relations, the "map layer + carrier layer" decomposition is internal via QMap and ElDisjs ; for PetParts , the carrier n is an external parameter, so the additional carrier stability must be factored explicitly as BlockLiftFix . (Contributed by Peter Mazsa, 20-Feb-2026) (Revised by Peter Mazsa, 25-Feb-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dfpetparts2 | |- PetParts = ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | inopab | |- ( { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } i^i { <. r , n >. | ( dom ( r |X. ( `' _E |` n ) ) /. ( r |X. ( `' _E |` n ) ) ) = n } ) = { <. r , n >. | ( ( r |X. ( `' _E |` n ) ) e. Disjs /\ ( dom ( r |X. ( `' _E |` n ) ) /. ( r |X. ( `' _E |` n ) ) ) = n ) } |
|
| 2 | df-blockliftfix | |- BlockLiftFix = { <. r , n >. | ( dom ( r |X. ( `' _E |` n ) ) /. ( r |X. ( `' _E |` n ) ) ) = n } |
|
| 3 | 2 | ineq2i | |- ( { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } i^i BlockLiftFix ) = ( { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } i^i { <. r , n >. | ( dom ( r |X. ( `' _E |` n ) ) /. ( r |X. ( `' _E |` n ) ) ) = n } ) |
| 4 | xrncnvepresex | |- ( ( n e. _V /\ r e. _V ) -> ( r |X. ( `' _E |` n ) ) e. _V ) |
|
| 5 | 4 | el2v | |- ( r |X. ( `' _E |` n ) ) e. _V |
| 6 | brparts2 | |- ( ( n e. _V /\ ( r |X. ( `' _E |` n ) ) e. _V ) -> ( ( r |X. ( `' _E |` n ) ) Parts n <-> ( ( r |X. ( `' _E |` n ) ) e. Disjs /\ ( dom ( r |X. ( `' _E |` n ) ) /. ( r |X. ( `' _E |` n ) ) ) = n ) ) ) |
|
| 7 | 6 | el2v1 | |- ( ( r |X. ( `' _E |` n ) ) e. _V -> ( ( r |X. ( `' _E |` n ) ) Parts n <-> ( ( r |X. ( `' _E |` n ) ) e. Disjs /\ ( dom ( r |X. ( `' _E |` n ) ) /. ( r |X. ( `' _E |` n ) ) ) = n ) ) ) |
| 8 | 5 7 | ax-mp | |- ( ( r |X. ( `' _E |` n ) ) Parts n <-> ( ( r |X. ( `' _E |` n ) ) e. Disjs /\ ( dom ( r |X. ( `' _E |` n ) ) /. ( r |X. ( `' _E |` n ) ) ) = n ) ) |
| 9 | 8 | opabbii | |- { <. r , n >. | ( r |X. ( `' _E |` n ) ) Parts n } = { <. r , n >. | ( ( r |X. ( `' _E |` n ) ) e. Disjs /\ ( dom ( r |X. ( `' _E |` n ) ) /. ( r |X. ( `' _E |` n ) ) ) = n ) } |
| 10 | 1 3 9 | 3eqtr4ri | |- { <. r , n >. | ( r |X. ( `' _E |` n ) ) Parts n } = ( { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } i^i BlockLiftFix ) |
| 11 | 10 | ineq2i | |- ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) Parts n } ) = ( ( Rels X. MembParts ) i^i ( { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } i^i BlockLiftFix ) ) |
| 12 | inopab | |- ( { <. r , n >. | ( r e. Rels /\ n e. MembParts ) } i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) Parts n } ) = { <. r , n >. | ( ( r e. Rels /\ n e. MembParts ) /\ ( r |X. ( `' _E |` n ) ) Parts n ) } |
|
| 13 | df-xp | |- ( Rels X. MembParts ) = { <. r , n >. | ( r e. Rels /\ n e. MembParts ) } |
|
| 14 | 13 | ineq1i | |- ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) Parts n } ) = ( { <. r , n >. | ( r e. Rels /\ n e. MembParts ) } i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) Parts n } ) |
| 15 | df-petparts | |- PetParts = { <. r , n >. | ( ( r e. Rels /\ n e. MembParts ) /\ ( r |X. ( `' _E |` n ) ) Parts n ) } |
|
| 16 | 12 14 15 | 3eqtr4ri | |- PetParts = ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) Parts n } ) |
| 17 | inass | |- ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) = ( ( Rels X. MembParts ) i^i ( { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } i^i BlockLiftFix ) ) |
|
| 18 | 11 16 17 | 3eqtr4i | |- PetParts = ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) |