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

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