Theorem dfpetparts2

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	Could not format assertion : No typesetting found for |- PetParts = ( ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } ) i^i BlockLiftFix ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		inopab	$$⊢\left\{⟨r,n⟩|r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{Disjs}\right\}\cap \left\{⟨r,n⟩|\mathrm{dom}r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right\}=\left\{⟨r,n⟩|\left(r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{Disjs}\wedge \mathrm{dom}r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right)\right\}$$
2		df-blockliftfix	Could not format BlockLiftFix = { <. r , n >. | ( dom ( r |X. ( `' _E |` n ) ) /. ( r |X. ( `' _E |` n ) ) ) = n } : No typesetting found for |- BlockLiftFix = { <. r , n >. | ( dom ( r |X. ( `' _E |` n ) ) /. ( r |X. ( `' _E |` n ) ) ) = n } with typecode |-
3	2	ineq2i	Could not format ( { <. 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 } ) : No typesetting found for |- ( { <. 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 } ) with typecode |-
4		xrncnvepresex	$$⊢\left(n\in \mathrm{V}\wedge r\in \mathrm{V}\right)\to r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{V}$$
5	4	el2v	$$⊢r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{V}$$
6		brparts2	$$⊢\left(n\in \mathrm{V}\wedge r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{V}\right)\to \left(r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Parts}n\leftrightarrow \left(r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{Disjs}\wedge \mathrm{dom}r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right)\right)$$
7	6	el2v1	$$⊢r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{V}\to \left(r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Parts}n\leftrightarrow \left(r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{Disjs}\wedge \mathrm{dom}r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right)\right)$$
8	5 7	ax-mp	$$⊢r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Parts}n\leftrightarrow \left(r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{Disjs}\wedge \mathrm{dom}r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right)$$
9	8	opabbii	$$⊢\left\{⟨r,n⟩|r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Parts}n\right\}=\left\{⟨r,n⟩|\left(r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{Disjs}\wedge \mathrm{dom}r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right)\right\}$$
10	1 3 9	3eqtr4ri	Could not format { <. r , n >. | ( r |X. ( `' _E |` n ) ) Parts n } = ( { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } i^i BlockLiftFix ) : No typesetting found for |- { <. r , n >. | ( r |X. ( `' _E |` n ) ) Parts n } = ( { <. r , n >. | ( r |X. ( `' _E |` n ) ) e. Disjs } i^i BlockLiftFix ) with typecode |-
11	10	ineq2i	Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
12		inopab	$$⊢\left\{⟨r,n⟩|\left(r\in \mathrm{Rels}\wedge n\in \mathrm{MembParts}\right)\right\}\cap \left\{⟨r,n⟩|r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Parts}n\right\}=\left\{⟨r,n⟩|\left(\left(r\in \mathrm{Rels}\wedge n\in \mathrm{MembParts}\right)\wedge r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Parts}n\right)\right\}$$
13		df-xp	$$⊢\mathrm{Rels}\times \mathrm{MembParts}=\left\{⟨r,n⟩|\left(r\in \mathrm{Rels}\wedge n\in \mathrm{MembParts}\right)\right\}$$
14	13	ineq1i	$$⊢\left(\mathrm{Rels}\times \mathrm{MembParts}\right)\cap \left\{⟨r,n⟩|r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Parts}n\right\}=\left\{⟨r,n⟩|\left(r\in \mathrm{Rels}\wedge n\in \mathrm{MembParts}\right)\right\}\cap \left\{⟨r,n⟩|r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Parts}n\right\}$$
15		df-petparts	Could not format PetParts = { <. r , n >. | ( ( r e. Rels /\ n e. MembParts ) /\ ( r |X. ( `' _E |` n ) ) Parts n ) } : No typesetting found for |- PetParts = { <. r , n >. | ( ( r e. Rels /\ n e. MembParts ) /\ ( r |X. ( `' _E |` n ) ) Parts n ) } with typecode |-
16	12 14 15	3eqtr4ri	Could not format PetParts = ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) Parts n } ) : No typesetting found for |- PetParts = ( ( Rels X. MembParts ) i^i { <. r , n >. | ( r |X. ( `' _E |` n ) ) Parts n } ) with typecode |-
17		inass	Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
18	11 16 17	3eqtr4i	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 |-