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	Could not format assertion : No typesetting found for |- PetParts = PetErs with typecode |-

Proof

Step	Hyp	Ref	Expression
1		typesafepets	$$⊢\left(n\in \mathrm{MembParts}\wedge r\in \mathrm{V}\right)\to \left(r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Parts}n\leftrightarrow \wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n\right)$$
2	1	elvd	$$⊢n\in \mathrm{MembParts}\to \left(r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Parts}n\leftrightarrow \wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n\right)$$
3	2	adantl	$$⊢\left(r\in \mathrm{Rels}\wedge n\in \mathrm{MembParts}\right)\to \left(r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Parts}n\leftrightarrow \wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n\right)$$
4	3	pm5.32i	$$⊢\left(\left(r\in \mathrm{Rels}\wedge n\in \mathrm{MembParts}\right)\wedge r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Parts}n\right)\leftrightarrow \left(\left(r\in \mathrm{Rels}\wedge n\in \mathrm{MembParts}\right)\wedge \wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n\right)$$
5		mpets	$$⊢\mathrm{MembParts}=\mathrm{CoMembErs}$$
6	5	eleq2i	$$⊢n\in \mathrm{MembParts}\leftrightarrow n\in \mathrm{CoMembErs}$$
7	6	anbi2i	$$⊢\left(r\in \mathrm{Rels}\wedge n\in \mathrm{MembParts}\right)\leftrightarrow \left(r\in \mathrm{Rels}\wedge n\in \mathrm{CoMembErs}\right)$$
8	4 7	bianbi	$$⊢\left(\left(r\in \mathrm{Rels}\wedge n\in \mathrm{MembParts}\right)\wedge r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Parts}n\right)\leftrightarrow \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)$$
9	8	opabbii	$$⊢\left\{⟨r,n⟩|\left(\left(r\in \mathrm{Rels}\wedge n\in \mathrm{MembParts}\right)\wedge r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Parts}n\right)\right\}=\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\}$$
10		df-petparts	Could not format PetParts = { <. r , n >. | ( ( r e. Rels /\ n e. MembParts ) /\ ( r |X. ( `' _E |` n ) ) Parts n ) } : No typesetting found for |- PetParts = { <. r , n >. | ( ( r e. Rels /\ n e. MembParts ) /\ ( r |X. ( `' _E |` n ) ) Parts n ) } with typecode |-
11		df-peters	Could not format PetErs = { <. r , n >. | ( ( r e. Rels /\ n e. CoMembErs ) /\ ,~ ( r |X. ( `' _E |` n ) ) Ers n ) } : No typesetting found for |- PetErs = { <. r , n >. | ( ( r e. Rels /\ n e. CoMembErs ) /\ ,~ ( r |X. ( `' _E |` n ) ) Ers n ) } with typecode |-
12	9 10 11	3eqtr4i	Could not format PetParts = PetErs : No typesetting found for |- PetParts = PetErs with typecode |-