Definition df-peters 39473

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 39480 (using typesafepets 39479 and mpets 39460). The explicit typing (𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) is included for the same reason as in df-petparts 39472: 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 38714	. 2 class PetErs
2		vr	. . . . . . 7 setvar 𝑟
3	2	cv 1561	. . . . . 6 class 𝑟
4		crels 38689	. . . . . 6 class Rels
5	3, 4	wcel 2144	. . . . 5 wff 𝑟 ∈ Rels
6		vn	. . . . . . 7 setvar 𝑛
7	6	cv 1561	. . . . . 6 class 𝑛
8		ccomembers 38716	. . . . . 6 class CoMembErs
9	7, 8	wcel 2144	. . . . 5 wff 𝑛 ∈ CoMembErs
10	5, 9	wa 399	. . . 4 wff (𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs )
11		cep 5548	. . . . . . . . 9 class E
12	11	ccnv 5648	. . . . . . . 8 class ◡ E
13	12, 7	cres 5651	. . . . . . 7 class (◡ E ↾ 𝑛)
14	3, 13	cxrn 38678	. . . . . 6 class (𝑟 ⋉ (◡ E ↾ 𝑛))
15	14	ccoss 38687	. . . . 5 class ≀ (𝑟 ⋉ (◡ E ↾ 𝑛))
16		cers 38712	. . . . 5 class Ers
17	15, 7, 16	wbr 5102	. . . 4 wff ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) Ers 𝑛
18	10, 17	wa 399	. . 3 wff ((𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) Ers 𝑛)
19	18, 2, 6	copab 5164	. 2 class {⟨𝑟, 𝑛⟩ ∣ ((𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) Ers 𝑛)}
20	1, 19	wceq 1562	1 wff PetErs = {⟨𝑟, 𝑛⟩ ∣ ((𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) Ers 𝑛)}

This definition is referenced by:  dfpeters2  39478  petseq  39480