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 𝑅 ) )