Theorem dfpeters2

Description: Alternate definition of PetErs in fully modular form.

This expands the Ers n predicate into:

(i) a typedness module ( Rels X. CoMembErs ) ,

(ii) an equivalence module for the coset relation ,( r |X. (`' _E |`n ) ) e. EqvRels ,

(iii) the corresponding quotient-carrier (domain quotient) equation dom ,( ... ) /. ,( ... ) = n .

This is the equivalence-side counterpart of the modular decomposition dfpetparts2 on the partition side. (Contributed by Peter Mazsa, 25-Feb-2026)

	Ref	Expression
Assertion	dfpeters2	Could not format assertion : No typesetting found for |- PetErs = ( ( ( Rels X. CoMembErs ) i^i { <. r , n >. | ,~ ( r |X. ( `' _E |` n ) ) e. EqvRels } ) i^i { <. r , n >. | ( dom ,~ ( r |X. ( `' _E |` n ) ) /. ,~ ( r |X. ( `' _E |` n ) ) ) = n } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		brers	$$⊢n\in \mathrm{V}\to \left(\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n\leftrightarrow \left(\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{EqvRels}\wedge \wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{DomainQss}n\right)\right)$$
2	1	elv	$$⊢\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n\leftrightarrow \left(\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{EqvRels}\wedge \wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{DomainQss}n\right)$$
3		1cossxrncnvepresex	$$⊢\left(n\in \mathrm{V}\wedge r\in \mathrm{V}\right)\to \wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{V}$$
4	3	el2v	$$⊢\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{V}$$
5		brdmqss	$$⊢\left(n\in \mathrm{V}\wedge \wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{V}\right)\to \left(\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{DomainQss}n\leftrightarrow \mathrm{dom}\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right)$$
6	4 5	mpan2	$$⊢n\in \mathrm{V}\to \left(\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{DomainQss}n\leftrightarrow \mathrm{dom}\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right)$$
7	6	elv	$$⊢\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{DomainQss}n\leftrightarrow \mathrm{dom}\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n$$
8	7	anbi2i	$$⊢\left(\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{EqvRels}\wedge \wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{DomainQss}n\right)\leftrightarrow \left(\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{EqvRels}\wedge \mathrm{dom}\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right)$$
9	2 8	bitri	$$⊢\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n\leftrightarrow \left(\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{EqvRels}\wedge \mathrm{dom}\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right)$$
10	9	opabbii	$$⊢\left\{⟨r,n⟩|\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n\right\}=\left\{⟨r,n⟩|\left(\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{EqvRels}\wedge \mathrm{dom}\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right)\right\}$$
11		inopab	$$⊢\left\{⟨r,n⟩|\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{EqvRels}\right\}\cap \left\{⟨r,n⟩|\mathrm{dom}\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right\}=\left\{⟨r,n⟩|\left(\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{EqvRels}\wedge \mathrm{dom}\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right)\right\}$$
12	10 11	eqtr4i	$$⊢\left\{⟨r,n⟩|\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n\right\}=\left\{⟨r,n⟩|\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{EqvRels}\right\}\cap \left\{⟨r,n⟩|\mathrm{dom}\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right\}$$
13	12	ineq2i	$$⊢\left(\mathrm{Rels}\times \mathrm{CoMembErs}\right)\cap \left\{⟨r,n⟩|\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n\right\}=\left(\mathrm{Rels}\times \mathrm{CoMembErs}\right)\cap \left(\left\{⟨r,n⟩|\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{EqvRels}\right\}\cap \left\{⟨r,n⟩|\mathrm{dom}\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right\}\right)$$
14		inopab	$$⊢\left\{⟨r,n⟩|\left(r\in \mathrm{Rels}\wedge n\in \mathrm{CoMembErs}\right)\right\}\cap \left\{⟨r,n⟩|\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n\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\}$$
15		df-xp	$$⊢\mathrm{Rels}\times \mathrm{CoMembErs}=\left\{⟨r,n⟩|\left(r\in \mathrm{Rels}\wedge n\in \mathrm{CoMembErs}\right)\right\}$$
16	15	ineq1i	$$⊢\left(\mathrm{Rels}\times \mathrm{CoMembErs}\right)\cap \left\{⟨r,n⟩|\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n\right\}=\left\{⟨r,n⟩|\left(r\in \mathrm{Rels}\wedge n\in \mathrm{CoMembErs}\right)\right\}\cap \left\{⟨r,n⟩|\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\mathrm{Ers}n\right\}$$
17		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 |-
18	14 16 17	3eqtr4ri	Could not format PetErs = ( ( Rels X. CoMembErs ) i^i { <. r , n >. | ,~ ( r |X. ( `' _E |` n ) ) Ers n } ) : No typesetting found for |- PetErs = ( ( Rels X. CoMembErs ) i^i { <. r , n >. | ,~ ( r |X. ( `' _E |` n ) ) Ers n } ) with typecode |-
19		inass	$$⊢\left(\left(\mathrm{Rels}\times \mathrm{CoMembErs}\right)\cap \left\{⟨r,n⟩|\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{EqvRels}\right\}\right)\cap \left\{⟨r,n⟩|\mathrm{dom}\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right\}=\left(\mathrm{Rels}\times \mathrm{CoMembErs}\right)\cap \left(\left\{⟨r,n⟩|\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)\in \mathrm{EqvRels}\right\}\cap \left\{⟨r,n⟩|\mathrm{dom}\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)/\wr r⋉\left({{\mathrm{E}}^{-1}\upharpoonright }_n\right)=n\right\}\right)$$
20	13 18 19	3eqtr4i	Could not format PetErs = ( ( ( Rels X. CoMembErs ) i^i { <. r , n >. | ,~ ( r |X. ( `' _E |` n ) ) e. EqvRels } ) i^i { <. r , n >. | ( dom ,~ ( r |X. ( `' _E |` n ) ) /. ,~ ( r |X. ( `' _E |` n ) ) ) = n } ) : No typesetting found for |- PetErs = ( ( ( Rels X. CoMembErs ) i^i { <. r , n >. | ,~ ( r |X. ( `' _E |` n ) ) e. EqvRels } ) i^i { <. r , n >. | ( dom ,~ ( r |X. ( `' _E |` n ) ) /. ,~ ( r |X. ( `' _E |` n ) ) ) = n } ) with typecode |-