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 × CoMembErs ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ EqvRels } ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( dom ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 } )

Proof

Step	Hyp	Ref	Expression
1		brers	⊢ ( 𝑛 ∈ V → ( ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 ↔ ( ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ EqvRels ∧ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) DomainQss 𝑛 ) ) )
2	1	elv	⊢ ( ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 ↔ ( ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ EqvRels ∧ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) DomainQss 𝑛 ) )
3		1cossxrncnvepresex	⊢ ( ( 𝑛 ∈ V ∧ 𝑟 ∈ V ) → ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ V )
4	3	el2v	⊢ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ V
5		brdmqss	⊢ ( ( 𝑛 ∈ V ∧ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ V ) → ( ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) DomainQss 𝑛 ↔ ( dom ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 ) )
6	4 5	mpan2	⊢ ( 𝑛 ∈ V → ( ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) DomainQss 𝑛 ↔ ( dom ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 ) )
7	6	elv	⊢ ( ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) DomainQss 𝑛 ↔ ( dom ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 )
8	7	anbi2i	⊢ ( ( ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ EqvRels ∧ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) DomainQss 𝑛 ) ↔ ( ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ EqvRels ∧ ( dom ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 ) )
9	2 8	bitri	⊢ ( ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 ↔ ( ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ EqvRels ∧ ( dom ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 ) )
10	9	opabbii	⊢ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 } = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ EqvRels ∧ ( dom ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 ) }
11		inopab	⊢ ( { ⟨ 𝑟 , 𝑛 ⟩ ∣ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ EqvRels } ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( dom ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 } ) = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ EqvRels ∧ ( dom ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 ) }
12	10 11	eqtr4i	⊢ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 } = ( { ⟨ 𝑟 , 𝑛 ⟩ ∣ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ EqvRels } ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( dom ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 } )
13	12	ineq2i	⊢ ( ( Rels × CoMembErs ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 } ) = ( ( Rels × CoMembErs ) ∩ ( { ⟨ 𝑟 , 𝑛 ⟩ ∣ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ EqvRels } ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( dom ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 } ) )
14		inopab	⊢ ( { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) } ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 } ) = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 ) }
15		df-xp	⊢ ( Rels × CoMembErs ) = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) }
16	15	ineq1i	⊢ ( ( Rels × CoMembErs ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 } ) = ( { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( 𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) } ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 } )
17		df-peters	⊢ PetErs = { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( ( 𝑟 ∈ Rels ∧ 𝑛 ∈ CoMembErs ) ∧ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 ) }
18	14 16 17	3eqtr4ri	⊢ PetErs = ( ( Rels × CoMembErs ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) Ers 𝑛 } )
19		inass	⊢ ( ( ( Rels × CoMembErs ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ EqvRels } ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( dom ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 } ) = ( ( Rels × CoMembErs ) ∩ ( { ⟨ 𝑟 , 𝑛 ⟩ ∣ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ EqvRels } ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( dom ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 } ) )
20	13 18 19	3eqtr4i	⊢ PetErs = ( ( ( Rels × CoMembErs ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ∈ EqvRels } ) ∩ { ⟨ 𝑟 , 𝑛 ⟩ ∣ ( dom ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) / ≀ ( 𝑟 ⋉ ( ◡ E ↾ 𝑛 ) ) ) = 𝑛 } )