Definition df-petparts 39901

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

⟨𝑟, 𝑛⟩ ∈ PetParts means:

(1) 𝑟 is a set-relation (𝑟 ∈ Rels), and

(2) 𝑛 is a membership block-carrier (𝑛 ∈ MembParts), and

(3) the block-lift span (𝑟 ⋉ (^◡ E ↾ 𝑛)) is a generalized partition on its natural quotient-carrier 𝑛 (i.e. (𝑟 ⋉ (^◡ E ↾ 𝑛)) Parts 𝑛).

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

The explicit typing (𝑟 ∈ Rels ∧ 𝑛 ∈ 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 39905 be written as clean intersections whose first conjunct is exactly the typedness module ( Rels × MembParts ). (Contributed by Peter Mazsa, 19-Feb-2026.) (Revised by Peter Mazsa, 25-Feb-2026.)

Assertion

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

Distinct variable group:   𝑛,𝑟

Detailed syntax breakdown of Definition df-petparts

Step	Hyp	Ref	Expression
1		cpetparts 39160	. 2 class PetParts
2		vr	. . . . . . 7 setvar 𝑟
3	2	cv 1568	. . . . . 6 class 𝑟
4		crels 39118	. . . . . 6 class Rels
5	3, 4	wcel 2144	. . . . 5 wff 𝑟 ∈ Rels
6		vn	. . . . . . 7 setvar 𝑛
7	6	cv 1568	. . . . . 6 class 𝑛
8		cmembparts 39158	. . . . . 6 class MembParts
9	7, 8	wcel 2144	. . . . 5 wff 𝑛 ∈ MembParts
10	5, 9	wa 401	. . . 4 wff (𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts )
11		cep 5549	. . . . . . . 8 class E
12	11	ccnv 5649	. . . . . . 7 class ◡ E
13	12, 7	cres 5652	. . . . . 6 class (◡ E ↾ 𝑛)
14	3, 13	cxrn 39107	. . . . 5 class (𝑟 ⋉ (◡ E ↾ 𝑛))
15		cparts 39156	. . . . 5 class Parts
16	14, 7, 15	wbr 5102	. . . 4 wff (𝑟 ⋉ (◡ E ↾ 𝑛)) Parts 𝑛
17	10, 16	wa 401	. . 3 wff ((𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ∧ (𝑟 ⋉ (◡ E ↾ 𝑛)) Parts 𝑛)
18	17, 2, 6	copab 5166	. 2 class {⟨𝑟, 𝑛⟩ ∣ ((𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ∧ (𝑟 ⋉ (◡ E ↾ 𝑛)) Parts 𝑛)}
19	1, 18	wceq 1569	1 wff PetParts = {⟨𝑟, 𝑛⟩ ∣ ((𝑟 ∈ Rels ∧ 𝑛 ∈ MembParts ) ∧ (𝑟 ⋉ (◡ E ↾ 𝑛)) Parts 𝑛)}

This definition is used by:  dfpetparts2  39905  petseq  39909