Theorem cossssid5

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

	Ref	Expression
Assertion	cossssid5	⊢ ( ≀ 𝑅 ⊆ I ↔ ∀ 𝑥 ∈ ran 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑦 ] ◡ 𝑅 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		cossssid4	⊢ ( ≀ 𝑅 ⊆ I ↔ ∀ 𝑢 ∃* 𝑥 𝑢 𝑅 𝑥 )
2		ineccnvmo2	⊢ ( ∀ 𝑥 ∈ ran 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑦 ] ◡ 𝑅 ) = ∅ ) ↔ ∀ 𝑢 ∃* 𝑥 𝑢 𝑅 𝑥 )
3	1 2	bitr4i	⊢ ( ≀ 𝑅 ⊆ I ↔ ∀ 𝑥 ∈ ran 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 ∨ ( [ 𝑥 ] ◡ 𝑅 ∩ [ 𝑦 ] ◡ 𝑅 ) = ∅ ) )