Metamath Proof Explorer

Theorem eqvrelcoss3

Description: Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 28-Apr-2019)

Ref Expression
Assertion eqvrelcoss3 ⊢ EqvRel ≀ R ↔ ∀ x ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x ≀ R z

Proof

Step Hyp Ref Expression
1 relcoss ⊢ Rel ⁡ ≀ R
2 1 biantru ⊢ ∀ x ∈ dom ⁡ ≀ R x ≀ R x ∧ ∀ x ∀ y x ≀ R y → y ≀ R x ∧ ∀ x ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x ≀ R z ↔ ∀ x ∈ dom ⁡ ≀ R x ≀ R x ∧ ∀ x ∀ y x ≀ R y → y ≀ R x ∧ ∀ x ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x ≀ R z ∧ Rel ⁡ ≀ R
3 refrelcosslem ⊢ ∀ x ∈ dom ⁡ ≀ R x ≀ R x
4 symrelcoss3 ⊢ ∀ x ∀ y x ≀ R y → y ≀ R x ∧ Rel ⁡ ≀ R
5 4 simpli ⊢ ∀ x ∀ y x ≀ R y → y ≀ R x
6 3 5 triantru3 ⊢ ∀ x ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x ≀ R z ↔ ∀ x ∈ dom ⁡ ≀ R x ≀ R x ∧ ∀ x ∀ y x ≀ R y → y ≀ R x ∧ ∀ x ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x ≀ R z
7 dfeqvrel3 ⊢ EqvRel ≀ R ↔ ∀ x ∈ dom ⁡ ≀ R x ≀ R x ∧ ∀ x ∀ y x ≀ R y → y ≀ R x ∧ ∀ x ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x ≀ R z ∧ Rel ⁡ ≀ R
8 2 6 7 3bitr4ri ⊢ EqvRel ≀ R ↔ ∀ x ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x ≀ R z