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

Metamath Proof Explorer

Theorem eleqvrels2

Description: Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021)

Ref Expression
Assertion eleqvrels2 ( 𝑅 ∈ EqvRels ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) ∧ 𝑅 ∈ Rels ) )

Proof

Step Hyp Ref Expression
1 dfeqvrels2 ⊢ EqvRels = { 𝑟 ∈ Rels ∣ ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) }
2 dmeq ⊢ ( 𝑟 = 𝑅 → dom 𝑟 = dom 𝑅 )
3 2 reseq2d ⊢ ( 𝑟 = 𝑅 → ( I ↾ dom 𝑟 ) = ( I ↾ dom 𝑅 ) )
4 id ⊢ ( 𝑟 = 𝑅 → 𝑟 = 𝑅 )
5 3 4 sseq12d ⊢ ( 𝑟 = 𝑅 → ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ↔ ( I ↾ dom 𝑅 ) ⊆ 𝑅 ) )
6 cnveq ⊢ ( 𝑟 = 𝑅 → ◡ 𝑟 = ◡ 𝑅 )
7 6 4 sseq12d ⊢ ( 𝑟 = 𝑅 → ( ◡ 𝑟 ⊆ 𝑟 ↔ ◡ 𝑅 ⊆ 𝑅 ) )
8 coideq ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ∘ 𝑟 ) = ( 𝑅 ∘ 𝑅 ) )
9 8 4 sseq12d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ↔ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) )
10 5 7 9 3anbi123d ⊢ ( 𝑟 = 𝑅 → ( ( ( I ↾ dom 𝑟 ) ⊆ 𝑟 ∧ ◡ 𝑟 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ↔ ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) ) )
11 1 10 rabeqel ⊢ ( 𝑅 ∈ EqvRels ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) ∧ 𝑅 ∈ Rels ) )