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	|- 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 } )

Proof

Step	Hyp	Ref	Expression
1		brers	|- ( n e. _V -> ( ,~ ( r |X. ( `' _E |` n ) ) Ers n <-> ( ,~ ( r |X. ( `' _E |` n ) ) e. EqvRels /\ ,~ ( r |X. ( `' _E |` n ) ) DomainQss n ) ) )
2	1	elv	|- ( ,~ ( r |X. ( `' _E |` n ) ) Ers n <-> ( ,~ ( r |X. ( `' _E |` n ) ) e. EqvRels /\ ,~ ( r |X. ( `' _E |` n ) ) DomainQss n ) )
3		1cossxrncnvepresex	|- ( ( n e. _V /\ r e. _V ) -> ,~ ( r |X. ( `' _E |` n ) ) e. _V )
4	3	el2v	|- ,~ ( r |X. ( `' _E |` n ) ) e. _V
5		brdmqss	|- ( ( n e. _V /\ ,~ ( r |X. ( `' _E |` n ) ) e. _V ) -> ( ,~ ( r |X. ( `' _E |` n ) ) DomainQss n <-> ( dom ,~ ( r |X. ( `' _E |` n ) ) /. ,~ ( r |X. ( `' _E |` n ) ) ) = n ) )
6	4 5	mpan2	|- ( n e. _V -> ( ,~ ( r |X. ( `' _E |` n ) ) DomainQss n <-> ( dom ,~ ( r |X. ( `' _E |` n ) ) /. ,~ ( r |X. ( `' _E |` n ) ) ) = n ) )
7	6	elv	|- ( ,~ ( r |X. ( `' _E |` n ) ) DomainQss n <-> ( dom ,~ ( r |X. ( `' _E |` n ) ) /. ,~ ( r |X. ( `' _E |` n ) ) ) = n )
8	7	anbi2i	|- ( ( ,~ ( r |X. ( `' _E |` n ) ) e. EqvRels /\ ,~ ( r |X. ( `' _E |` n ) ) DomainQss n ) <-> ( ,~ ( r |X. ( `' _E |` n ) ) e. EqvRels /\ ( dom ,~ ( r |X. ( `' _E |` n ) ) /. ,~ ( r |X. ( `' _E |` n ) ) ) = n ) )
9	2 8	bitri	|- ( ,~ ( r |X. ( `' _E |` n ) ) Ers n <-> ( ,~ ( r |X. ( `' _E |` n ) ) e. EqvRels /\ ( dom ,~ ( r |X. ( `' _E |` n ) ) /. ,~ ( r |X. ( `' _E |` n ) ) ) = n ) )
10	9	opabbii	|- { <. r , n >. | ,~ ( r |X. ( `' _E |` n ) ) Ers n } = { <. r , n >. | ( ,~ ( r |X. ( `' _E |` n ) ) e. EqvRels /\ ( dom ,~ ( r |X. ( `' _E |` n ) ) /. ,~ ( r |X. ( `' _E |` n ) ) ) = n ) }
11		inopab	|- ( { <. r , n >. | ,~ ( r |X. ( `' _E |` n ) ) e. EqvRels } i^i { <. r , n >. | ( dom ,~ ( r |X. ( `' _E |` n ) ) /. ,~ ( r |X. ( `' _E |` n ) ) ) = n } ) = { <. r , n >. | ( ,~ ( r |X. ( `' _E |` n ) ) e. EqvRels /\ ( dom ,~ ( r |X. ( `' _E |` n ) ) /. ,~ ( r |X. ( `' _E |` n ) ) ) = n ) }
12	10 11	eqtr4i	|- { <. r , n >. | ,~ ( r |X. ( `' _E |` n ) ) Ers n } = ( { <. r , n >. | ,~ ( r |X. ( `' _E |` n ) ) e. EqvRels } i^i { <. r , n >. | ( dom ,~ ( r |X. ( `' _E |` n ) ) /. ,~ ( r |X. ( `' _E |` n ) ) ) = n } )
13	12	ineq2i	|- ( ( Rels X. CoMembErs ) i^i { <. r , n >. | ,~ ( r |X. ( `' _E |` n ) ) Ers n } ) = ( ( 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 } ) )
14		inopab	|- ( { <. r , n >. | ( r e. Rels /\ n e. CoMembErs ) } i^i { <. r , n >. | ,~ ( r |X. ( `' _E |` n ) ) Ers n } ) = { <. r , n >. | ( ( r e. Rels /\ n e. CoMembErs ) /\ ,~ ( r |X. ( `' _E |` n ) ) Ers n ) }
15		df-xp	|- ( Rels X. CoMembErs ) = { <. r , n >. | ( r e. Rels /\ n e. CoMembErs ) }
16	15	ineq1i	|- ( ( Rels X. CoMembErs ) i^i { <. r , n >. | ,~ ( r |X. ( `' _E |` n ) ) Ers n } ) = ( { <. r , n >. | ( r e. Rels /\ n e. CoMembErs ) } i^i { <. r , n >. | ,~ ( r |X. ( `' _E |` n ) ) Ers n } )
17		df-peters	|- PetErs = { <. r , n >. | ( ( r e. Rels /\ n e. CoMembErs ) /\ ,~ ( r |X. ( `' _E |` n ) ) Ers n ) }
18	14 16 17	3eqtr4ri	|- PetErs = ( ( Rels X. CoMembErs ) i^i { <. r , n >. | ,~ ( r |X. ( `' _E |` n ) ) Ers n } )
19		inass	|- ( ( ( 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 } ) = ( ( 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 } ) )
20	13 18 19	3eqtr4i	|- 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 } )