This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) }