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	Could not format assertion : No typesetting found for |- PetErs = { <. r , n >. | ( ( r e. Rels /\ n e. CoMembErs ) /\ ,~ ( r |X. ( `' _E |` n ) ) Ers n ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpeters	Could not format PetErs : No typesetting found for class PetErs with typecode class
1		vr	$$setvarr$$
2		vn	$$setvarn$$
3	1	cv	$$setvarr$$
4		crels	$$class\mathrm{Rels}$$
5	3 4	wcel	$$wffr\in \mathrm{Rels}$$
6	2	cv	$$setvarn$$
7		ccomembers	$$class\mathrm{CoMembErs}$$
8	6 7	wcel	$$wffn\in \mathrm{CoMembErs}$$
9	5 8	wa	$$wff\left(r\in \mathrm{Rels}\wedge n\in \mathrm{CoMembErs}\right)$$
10		cep	$$class\mathrm{E}$$
11	10	ccnv	$$class{\mathrm{E}}^{-1}$$
12	11 6	cres	$$class\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)$$
13	3 12	cxrn	$$classr⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)$$
14	13	ccoss	$$class\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)$$
15		cers	$$class\mathrm{Ers}$$
16	14 6 15	wbr	$$wff\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n$$
17	9 16	wa	$$wff\left(\left(r\in \mathrm{Rels}\wedge n\in \mathrm{CoMembErs}\right)\wedge \wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n\right)$$
18	17 1 2	copab	$$class\left\{⟨r,n⟩|\left(\left(r\in \mathrm{Rels}\wedge n\in \mathrm{CoMembErs}\right)\wedge \wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n\right)\right\}$$
19	0 18	wceq	Could not format PetErs = { <. r , n >. | ( ( r e. Rels /\ n e. CoMembErs ) /\ ,~ ( r |X. ( `' _E |` n ) ) Ers n ) } : No typesetting found for wff PetErs = { <. r , n >. | ( ( r e. Rels /\ n e. CoMembErs ) /\ ,~ ( r |X. ( `' _E |` n ) ) Ers n ) } with typecode wff