Definition df-petparts

Description: Define the class of partition-side general partition-equivalence spans.

<. r , n >. e. PetParts means:

(1) r is a set-relation ( r e. Rels ), and

(2) n is a membership block-carrier ( n e. MembParts ), and

(3) the block-lift span ( r |X. (`'E |`n ) ) is a generalized partition on its natural quotient-carrier n (i.e. ( r |X. (`' E |`n ) ) Parts n ).

This is the horizontal feasibility base object on the partition side, expressed in the type-safe Parts language.

The explicit typing ( r e. Rels /\ n e. MembParts ) is included at the definition level so later modular refinements can treat typedness as a first-class component (e.g. intersecting a typedness module with disjointness and equilibrium modules) without repeatedly restating it. In particular, it lets decompositions such as dfpetparts2 be written as clean intersections whose first conjunct is exactly the typedness module ( Rels X. MembParts ) . (Contributed by Peter Mazsa, 19-Feb-2026) (Revised by Peter Mazsa, 25-Feb-2026)

	Ref	Expression
Assertion	df-petparts	⊢ PetParts = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ∧ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpetparts	⊢ PetParts
1		vr	⊢ 𝑟
2		vn	⊢ 𝑛
3	1	cv	⊢ 𝑟
4		crels	⊢ Rels
5	3 4	wcel	⊢ 𝑟 ∈ Rels
6	2	cv	⊢ 𝑛
7		cmembparts	⊢ MembParts
8	6 7	wcel	⊢ 𝑛 ∈ MembParts
9	5 8	wa	⊢ ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts )
10		cep	⊢ E
11	10	ccnv	⊢ ◡ E
12	11 6	cres	⊢ ( ◡ E ↾ 𝑛 )
13	3 12	cxrn	⊢ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) )
14		cparts	⊢ Parts
15	13 6 14	wbr	⊢ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛
16	9 15	wa	⊢ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ∧ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 )
17	16 1 2	copab	⊢ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ∧ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 ) }
18	0 17	wceq	⊢ PetParts = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ∧ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Parts 𝑛 ) }