Theorem eqvrelcoss4

Description: Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019) (Revised by Peter Mazsa, 30-Sep-2021)

	Ref	Expression
Assertion	eqvrelcoss4	⊢ ( EqvRel ≀ 𝑅 ↔ ∀ 𝑥 ∀ 𝑧 ( ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) ≠ ∅ → ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		eqvrelcoss3	⊢ ( EqvRel ≀ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) )
2		trcoss2	⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ( ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) ≠ ∅ → ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ ) )
3	1 2	bitri	⊢ ( EqvRel ≀ 𝑅 ↔ ∀ 𝑥 ∀ 𝑧 ( ( [ 𝑥 ] ≀ 𝑅 ∩ [ 𝑧 ] ≀ 𝑅 ) ≠ ∅ → ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑧 ] ◡ 𝑅 ) ≠ ∅ ) )