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 ≀ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) )