Theorem cossssid

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

	Ref	Expression
Assertion	cossssid	⊢ ( ≀ 𝑅 ⊆ I ↔ ≀ 𝑅 ⊆ ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iss2	⊢ ( ≀ 𝑅 ⊆ I ↔ ≀ 𝑅 = ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) )
2		refrelcoss2	⊢ ( ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅 )
3	2	simpli	⊢ ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) ⊆ ≀ 𝑅
4		eqss	⊢ ( ≀ 𝑅 = ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) ↔ ( ≀ 𝑅 ⊆ ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) ∧ ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) ⊆ ≀ 𝑅 ) )
5	3 4	mpbiran2	⊢ ( ≀ 𝑅 = ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) ↔ ≀ 𝑅 ⊆ ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) )
6	1 5	bitri	⊢ ( ≀ 𝑅 ⊆ I ↔ ≀ 𝑅 ⊆ ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) )