Definition df-peters 39902

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

⟨𝑟, 𝑛⟩ ∈ PetErs means:

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

(2) 𝑛 is a carrier recognized on the equivalence side of membership (𝑛 ∈ CoMembErs), and

(3) the coset relation of the lifted span, ≀ (𝑟 ⋉ (^◡ E ↾ 𝑛)), is an equivalence relation on its natural quotient with carrier 𝑛 (i.e. ≀ (𝑟 ⋉ (^◡ E ↾ 𝑛)) Ers 𝑛).

This packages the equivalence-view of the same lifted construction that underlies PetParts. It is designed to be parallel to PetParts so later proofs can freely choose the partition side (Parts) or the equivalence side (Ers) without rebuilding the bridge each time; the identification is provided by petseq 39909 (using typesafepets 39908 and mpets 39889). The explicit typing (𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) is included for the same reason as in df-petparts 39901: to make typedness a reusable module. (Contributed by Peter Mazsa, 19-Feb-2026.) (Revised by Peter Mazsa, 25-Feb-2026.)

Assertion

Ref	Expression
df-peters	⊢ PetErs = {⟨𝑟, 𝑛⟩ ∣ ((𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) Ers 𝑛)}

Distinct variable group:   𝑛,𝑟

Detailed syntax breakdown of Definition df-peters

Step	Hyp	Ref	Expression
1		cpeters 39143	. 2 class PetErs
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		ccomembers 39145	. . . . . 6 class CoMembErs
9	7, 8	wcel 2144	. . . . 5 wff 𝑛 ∈ CoMembErs
10	5, 9	wa 401	. . . 4 wff (𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs )
11		cep 5549	. . . . . . . . 9 class E
12	11	ccnv 5649	. . . . . . . 8 class ◡ E
13	12, 7	cres 5652	. . . . . . 7 class (◡ E ↾ 𝑛)
14	3, 13	cxrn 39107	. . . . . 6 class (𝑟 ⋉ (◡ E ↾ 𝑛))
15	14	ccoss 39116	. . . . 5 class ≀ (𝑟 ⋉ (◡ E ↾ 𝑛))
16		cers 39141	. . . . 5 class Ers
17	15, 7, 16	wbr 5102	. . . 4 wff ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) Ers 𝑛
18	10, 17	wa 401	. . 3 wff ((𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) Ers 𝑛)
19	18, 2, 6	copab 5166	. 2 class {⟨𝑟, 𝑛⟩ ∣ ((𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) Ers 𝑛)}
20	1, 19	wceq 1569	1 wff PetErs = {⟨𝑟, 𝑛⟩ ∣ ((𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) Ers 𝑛)}

This definition is used by:  dfpeters2  39907  petseq  39909