Theorem cossssid4

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

	Ref	Expression
Assertion	cossssid4	⊢ ( ≀ 𝑅 ⊆ I ↔ ∀ 𝑢 ∃* 𝑥 𝑢 𝑅 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		cossssid3	⊢ ( ≀ 𝑅 ⊆ I ↔ ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) )
2		breq2	⊢ ( 𝑥 = 𝑦 → ( 𝑢 𝑅 𝑥 ↔ 𝑢 𝑅 𝑦 ) )
3	2	mo4	⊢ ( ∃* 𝑥 𝑢 𝑅 𝑥 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) )
4	3	albii	⊢ ( ∀ 𝑢 ∃* 𝑥 𝑢 𝑅 𝑥 ↔ ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) )
5	1 4	bitr4i	⊢ ( ≀ 𝑅 ⊆ I ↔ ∀ 𝑢 ∃* 𝑥 𝑢 𝑅 𝑥 )