Definition df-peters 39821

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 39828 (using typesafepets 39827 and mpets 39808). The explicit typing (𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) is included for the same reason as in df-petparts 39820: 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 39062	. 2 class PetErs
2		vr	. . . . . . 7 setvar 𝑟
3	2	cv 1569	. . . . . 6 class 𝑟
4		crels 39037	. . . . . 6 class Rels
5	3, 4	wcel 2145	. . . . 5 wff 𝑟 ∈ Rels
6		vn	. . . . . . 7 setvar 𝑛
7	6	cv 1569	. . . . . 6 class 𝑛
8		ccomembers 39064	. . . . . 6 class CoMembErs
9	7, 8	wcel 2145	. . . . 5 wff 𝑛 ∈ CoMembErs
10	5, 9	wa 401	. . . 4 wff (𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs )
11		cep 5546	. . . . . . . . 9 class E
12	11	ccnv 5646	. . . . . . . 8 class ◡ E
13	12, 7	cres 5649	. . . . . . 7 class (◡ E ↾ 𝑛)
14	3, 13	cxrn 39026	. . . . . 6 class (𝑟 ⋉ (◡ E ↾ 𝑛))
15	14	ccoss 39035	. . . . 5 class ≀ (𝑟 ⋉ (◡ E ↾ 𝑛))
16		cers 39060	. . . . 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 1570	1 wff PetErs = {⟨𝑟, 𝑛⟩ ∣ ((𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ (𝑟 ⋉ (◡ E ↾ 𝑛)) Ers 𝑛)}

This definition is used by:  dfpeters2  39826  petseq  39828