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

Metamath Proof Explorer

Theorem dfeqvrel3

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

Ref Expression
Assertion dfeqvrel3 ( EqvRel 𝑅 ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ∧ Rel 𝑅 ) )

Proof

Step Hyp Ref Expression
1 df-eqvrel ⊢ ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅 ) )
2 refsymrel3 ⊢ ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ Rel 𝑅 ) )
3 dftrrel3 ⊢ ( TrRel 𝑅 ↔ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ∧ Rel 𝑅 ) )
4 2 3 anbi12i ⊢ ( ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ∧ TrRel 𝑅 ) ↔ ( ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ Rel 𝑅 ) ∧ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ∧ Rel 𝑅 ) ) )
5 df-3an ⊢ ( ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅 ) ↔ ( ( RefRel 𝑅 ∧ SymRel 𝑅 ) ∧ TrRel 𝑅 ) )
6 df-3an ⊢ ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
7 6 anbi1i ⊢ ( ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ∧ Rel 𝑅 ) ↔ ( ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ∧ Rel 𝑅 ) )
8 3anan32 ⊢ ( ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ Rel 𝑅 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ∧ Rel 𝑅 ) )
9 anandi3r ⊢ ( ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ Rel 𝑅 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ Rel 𝑅 ) ∧ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ∧ Rel 𝑅 ) ) )
10 7 8 9 3bitr2i ⊢ ( ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ∧ Rel 𝑅 ) ↔ ( ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) ∧ Rel 𝑅 ) ∧ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ∧ Rel 𝑅 ) ) )
11 4 5 10 3bitr4i ⊢ ( ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅 ) ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ∧ Rel 𝑅 ) )
12 1 11 bitri ⊢ ( EqvRel 𝑅 ↔ ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ∧ Rel 𝑅 ) )