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

Metamath Proof Explorer

Theorem eqvrelcoss3

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

Ref Expression
Assertion eqvrelcoss3 ( EqvRel ≀ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) )

Proof

Step Hyp Ref Expression
1 relcoss ⊢ Rel ≀ 𝑅
2 1 biantru ⊢ ( ( ∀ 𝑥 ∈ dom ≀ 𝑅 𝑥 ≀ 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) ) ↔ ( ( ∀ 𝑥 ∈ dom ≀ 𝑅 𝑥 ≀ 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) ) ∧ Rel ≀ 𝑅 ) )
3 refrelcosslem ⊢ ∀ 𝑥 ∈ dom ≀ 𝑅 𝑥 ≀ 𝑅 𝑥
4 symrelcoss3 ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 ) ∧ Rel ≀ 𝑅 )
5 4 simpli ⊢ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 )
6 3 5 triantru3 ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) ↔ ( ∀ 𝑥 ∈ dom ≀ 𝑅 𝑥 ≀ 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) ) )
7 dfeqvrel3 ⊢ ( EqvRel ≀ 𝑅 ↔ ( ( ∀ 𝑥 ∈ dom ≀ 𝑅 𝑥 ≀ 𝑅 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≀ 𝑅 𝑦 → 𝑦 ≀ 𝑅 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) ) ∧ Rel ≀ 𝑅 ) )
8 2 6 7 3bitr4ri ⊢ ( EqvRel ≀ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) )