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

Metamath Proof Explorer

Theorem cossssid3

Description: Equivalent expressions for the class of cosets by R to be a subset of the identity class. (Contributed by Peter Mazsa, 10-Mar-2019)

Ref Expression
Assertion cossssid3 ( ≀ 𝑅 ⊆ I ↔ ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) )

Proof

Step Hyp Ref Expression
1 cossssid2 ⊢ ( ≀ 𝑅 ⊆ I ↔ ∀ 𝑥 ∀ 𝑦 ( ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) )
2 19.23v ⊢ ( ∀ 𝑢 ( ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) )
3 2 albii ⊢ ( ∀ 𝑦 ∀ 𝑢 ( ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ( ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) )
4 alcom ⊢ ( ∀ 𝑦 ∀ 𝑢 ( ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑢 ∀ 𝑦 ( ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) )
5 3 4 bitr3i ⊢ ( ∀ 𝑦 ( ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑢 ∀ 𝑦 ( ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) )
6 5 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑢 ∀ 𝑦 ( ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) )
7 alcom ⊢ ( ∀ 𝑥 ∀ 𝑢 ∀ 𝑦 ( ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) )
8 1 6 7 3bitri ⊢ ( ≀ 𝑅 ⊆ I ↔ ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) )