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