Definition df-peters

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

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

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

(2) n is a carrier recognized on the equivalence side of membership ( n e. CoMembErs ), and

(3) the coset relation of the lifted span, ,( r |X. (`'E |`n ) ) , is an equivalence relation on its natural quotient with carrier n (i.e. ,( r |X. (`' E |`n ) ) Ers n ).

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 (using typesafepets and mpets ). The explicit typing ( r e. Rels /\ n e. CoMembErs ) is included for the same reason as in df-petparts : to make typedness a reusable module. (Contributed by Peter Mazsa, 19-Feb-2026) (Revised by Peter Mazsa, 25-Feb-2026)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpeters	⊢ PetErs
1		vr	⊢ 𝑟
2		vn	⊢ 𝑛
3	1	cv	⊢ 𝑟
4		crels	⊢ Rels
5	3 4	wcel	⊢ 𝑟 ∈ Rels
6	2	cv	⊢ 𝑛
7		ccomembers	⊢ CoMembErs
8	6 7	wcel	⊢ 𝑛 ∈ CoMembErs
9	5 8	wa	⊢ ( 𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs )
10		cep	⊢ E
11	10	ccnv	⊢ ◡ E
12	11 6	cres	⊢ ( ◡ E ↾ 𝑛 )
13	3 12	cxrn	⊢ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) )
14	13	ccoss	⊢ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) )
15		cers	⊢ Ers
16	14 6 15	wbr	⊢ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛
17	9 16	wa	⊢ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 )
18	17 1 2	copab	⊢ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 ) }
19	0 18	wceq	⊢ PetErs = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 ) }