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 = { <. r , n >. | ( ( r e. Rels /\ n e. CoMembErs ) /\ ,~ ( r |X. ( `' _E |` n ) ) Ers n ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpeters	|- PetErs
1		vr	|- r
2		vn	|- n
3	1	cv	|- r
4		crels	|- Rels
5	3 4	wcel	|- r e. Rels
6	2	cv	|- n
7		ccomembers	|- CoMembErs
8	6 7	wcel	|- n e. CoMembErs
9	5 8	wa	|- ( r e. Rels /\ n e. CoMembErs )
10		cep	|- _E
11	10	ccnv	|- `' _E
12	11 6	cres	|- ( `' _E |` n )
13	3 12	cxrn	|- ( r |X. ( `' _E |` n ) )
14	13	ccoss	|- ,~ ( r |X. ( `' _E |` n ) )
15		cers	|- Ers
16	14 6 15	wbr	|- ,~ ( r |X. ( `' _E |` n ) ) Ers n
17	9 16	wa	|- ( ( r e. Rels /\ n e. CoMembErs ) /\ ,~ ( r |X. ( `' _E |` n ) ) Ers n )
18	17 1 2	copab	|- { <. r , n >. | ( ( r e. Rels /\ n e. CoMembErs ) /\ ,~ ( r |X. ( `' _E |` n ) ) Ers n ) }
19	0 18	wceq	|- PetErs = { <. r , n >. | ( ( r e. Rels /\ n e. CoMembErs ) /\ ,~ ( r |X. ( `' _E |` n ) ) Ers n ) }