Theorem petseq

Description: Generalized partition-equivalence identification.

The partition-side scheme PetParts and the equivalence-side scheme PetErs define the same class of spans (pairs <. r , n >. ).

This plays the same organizational role for lifted spans that mpets plays for carriers: mpets identifies MembParts with CoMembErs at the membership-carrier level, while petseq identifies the corresponding span-level predicates built from Parts and Ers .

Unlike the earlier broad pets , the bridge used here is the type-safe span theorem typesafepets , which restricts to membership block-carriers. Since typedness ( r e. Rels and the appropriate carrier condition) is now built directly into PetParts and PetErs , this theorem can be used downstream without repeatedly re-establishing basic typing premises. (Contributed by Peter Mazsa, 19-Feb-2026)

	Ref	Expression
Assertion	petseq	|- PetParts = PetErs

Proof

Step	Hyp	Ref	Expression
1		typesafepets	|- ( ( n e. MembParts /\ r e. _V ) -> ( ( r |X. ( `' _E |` n ) ) Parts n <-> ,~ ( r |X. ( `' _E |` n ) ) Ers n ) )
2	1	elvd	|- ( n e. MembParts -> ( ( r |X. ( `' _E |` n ) ) Parts n <-> ,~ ( r |X. ( `' _E |` n ) ) Ers n ) )
3	2	adantl	|- ( ( r e. Rels /\ n e. MembParts ) -> ( ( r |X. ( `' _E |` n ) ) Parts n <-> ,~ ( r |X. ( `' _E |` n ) ) Ers n ) )
4	3	pm5.32i	|- ( ( ( r e. Rels /\ n e. MembParts ) /\ ( r |X. ( `' _E |` n ) ) Parts n ) <-> ( ( r e. Rels /\ n e. MembParts ) /\ ,~ ( r |X. ( `' _E |` n ) ) Ers n ) )
5		mpets	|- MembParts = CoMembErs
6	5	eleq2i	|- ( n e. MembParts <-> n e. CoMembErs )
7	6	anbi2i	|- ( ( r e. Rels /\ n e. MembParts ) <-> ( r e. Rels /\ n e. CoMembErs ) )
8	4 7	bianbi	|- ( ( ( r e. Rels /\ n e. MembParts ) /\ ( r |X. ( `' _E |` n ) ) Parts n ) <-> ( ( r e. Rels /\ n e. CoMembErs ) /\ ,~ ( r |X. ( `' _E |` n ) ) Ers n ) )
9	8	opabbii	|- { <. r , n >. | ( ( r e. Rels /\ n e. MembParts ) /\ ( r |X. ( `' _E |` n ) ) Parts n ) } = { <. r , n >. | ( ( r e. Rels /\ n e. CoMembErs ) /\ ,~ ( r |X. ( `' _E |` n ) ) Ers n ) }
10		df-petparts	|- PetParts = { <. r , n >. | ( ( r e. Rels /\ n e. MembParts ) /\ ( r |X. ( `' _E |` n ) ) Parts n ) }
11		df-peters	|- PetErs = { <. r , n >. | ( ( r e. Rels /\ n e. CoMembErs ) /\ ,~ ( r |X. ( `' _E |` n ) ) Ers n ) }
12	9 10 11	3eqtr4i	|- PetParts = PetErs