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	⊢ PetParts = ( ( ( Rels × MembParts ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs } ) ∩ BlockLiftFix )

Proof

Step	Hyp	Ref	Expression
1		inopab	⊢ ( { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs } ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 } ) = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs ∧ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 ) }
2		df-blockliftfix	⊢ BlockLiftFix = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 }
3	2	ineq2i	⊢ ( { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs } ∩ BlockLiftFix ) = ( { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs } ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 } )
4		xrncnvepresex	⊢ ( ( 𝑛 ∈ V ∧ 𝑟 ∈ V ) → ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ V )
5	4	el2v	⊢ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ V
6		brparts2	⊢ ( ( 𝑛 ∈ V ∧ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ V ) → ( ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 ↔ ( ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs ∧ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 ) ) )
7	6	el2v1	⊢ ( ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ V → ( ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 ↔ ( ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs ∧ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 ) ) )
8	5 7	ax-mp	⊢ ( ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 ↔ ( ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs ∧ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 ) )
9	8	opabbii	⊢ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 } = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs ∧ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 ) }
10	1 3 9	3eqtr4ri	⊢ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 } = ( { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs } ∩ BlockLiftFix )
11	10	ineq2i	⊢ ( ( Rels × MembParts ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 } ) = ( ( Rels × MembParts ) ∩ ( { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs } ∩ BlockLiftFix ) )
12		inopab	⊢ ( { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) } ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 } ) = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ∧ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 ) }
13		df-xp	⊢ ( Rels × MembParts ) = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) }
14	13	ineq1i	⊢ ( ( Rels × MembParts ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 } ) = ( { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) } ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 } )
15		df-petparts	⊢ PetParts = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ∧ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 ) }
16	12 14 15	3eqtr4ri	⊢ PetParts = ( ( Rels × MembParts ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 } )
17		inass	⊢ ( ( ( Rels × MembParts ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs } ) ∩ BlockLiftFix ) = ( ( Rels × MembParts ) ∩ ( { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs } ∩ BlockLiftFix ) )
18	11 16 17	3eqtr4i	⊢ PetParts = ( ( ( Rels × MembParts ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ Disjs } ) ∩ BlockLiftFix )