Metamath Proof Explorer


Theorem dfeqvrel2

Description: Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019)

Ref Expression
Assertion dfeqvrel2 ( EqvRel 𝑅 ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ∧ ( 𝑅𝑅 ) ⊆ 𝑅 ) ∧ Rel 𝑅 ) )

Proof

Step Hyp Ref Expression
1 df-eqvrel ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅 ) )
2 refsymrel2 ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ) ∧ Rel 𝑅 ) )
3 dftrrel2 ( TrRel 𝑅 ↔ ( ( 𝑅𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) )
4 2 3 anbi12i ( ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ∧ TrRel 𝑅 ) ↔ ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ) ∧ Rel 𝑅 ) ∧ ( ( 𝑅𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) ) )
5 df-3an ( ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅 ) ↔ ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ∧ TrRel 𝑅 ) )
6 df-3an ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ∧ ( 𝑅𝑅 ) ⊆ 𝑅 ) ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ) ∧ ( 𝑅𝑅 ) ⊆ 𝑅 ) )
7 6 anbi1i ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ∧ ( 𝑅𝑅 ) ⊆ 𝑅 ) ∧ Rel 𝑅 ) ↔ ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ) ∧ ( 𝑅𝑅 ) ⊆ 𝑅 ) ∧ Rel 𝑅 ) )
8 3anan32 ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ) ∧ Rel 𝑅 ∧ ( 𝑅𝑅 ) ⊆ 𝑅 ) ↔ ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ) ∧ ( 𝑅𝑅 ) ⊆ 𝑅 ) ∧ Rel 𝑅 ) )
9 anandi3r ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ) ∧ Rel 𝑅 ∧ ( 𝑅𝑅 ) ⊆ 𝑅 ) ↔ ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ) ∧ Rel 𝑅 ) ∧ ( ( 𝑅𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) ) )
10 7 8 9 3bitr2i ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ∧ ( 𝑅𝑅 ) ⊆ 𝑅 ) ∧ Rel 𝑅 ) ↔ ( ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ) ∧ Rel 𝑅 ) ∧ ( ( 𝑅𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) ) )
11 4 5 10 3bitr4i ( ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅 ) ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ∧ ( 𝑅𝑅 ) ⊆ 𝑅 ) ∧ Rel 𝑅 ) )
12 1 11 bitri ( EqvRel 𝑅 ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ∧ ( 𝑅𝑅 ) ⊆ 𝑅 ) ∧ Rel 𝑅 ) )