Theorem dfeqvrels2

Description: Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019)

	Ref	Expression
Assertion	dfeqvrels2	⊢ EqvRels = { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) }

Proof

Step	Hyp	Ref	Expression
1		df-eqvrels	⊢ EqvRels = ( ( RefRels ∩ SymRels ) ∩ TrRels )
2		refsymrels2	⊢ ( RefRels ∩ SymRels ) = { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ) }
3		dftrrels2	⊢ TrRels = { 𝑟 ∈ Rels ∣ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 }
4	2 3	ineq12i	⊢ ( ( RefRels ∩ SymRels ) ∩ TrRels ) = ( { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ) } ∩ { 𝑟 ∈ Rels ∣ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 } )
5		inrab	⊢ ( { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ) } ∩ { 𝑟 ∈ Rels ∣ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 } ) = { 𝑟 ∈ Rels ∣ ( ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ) ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) }
6	1 4 5	3eqtri	⊢ EqvRels = { 𝑟 ∈ Rels ∣ ( ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ) ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) }
7		df-3an	⊢ ( ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ↔ ( ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ) ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) )
8	7	rabbii	⊢ { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } = { 𝑟 ∈ Rels ∣ ( ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ) ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) }
9	6 8	eqtr4i	⊢ EqvRels = { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) }