Theorem refrelcoss2

Description: The class of cosets by R is reflexive, see dfrefrel2 . (Contributed by Peter Mazsa, 30-Jul-2019)

	Ref	Expression
Assertion	refrelcoss2	⊢ ( ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		refrelcoss3	⊢ ( ∀ 𝑥 ∈ dom ≀ 𝑅 ∀ 𝑦 ∈ ran ≀ 𝑅 ( 𝑥 = 𝑦 → 𝑥 ≀ 𝑅 𝑦 ) ∧ Rel ≀ 𝑅 )
2		idinxpss	⊢ ( ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) ⊆ ≀ 𝑅 ↔ ∀ 𝑥 ∈ dom ≀ 𝑅 ∀ 𝑦 ∈ ran ≀ 𝑅 ( 𝑥 = 𝑦 → 𝑥 ≀ 𝑅 𝑦 ) )
3	2	anbi1i	⊢ ( ( ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅 ) ↔ ( ∀ 𝑥 ∈ dom ≀ 𝑅 ∀ 𝑦 ∈ ran ≀ 𝑅 ( 𝑥 = 𝑦 → 𝑥 ≀ 𝑅 𝑦 ) ∧ Rel ≀ 𝑅 ) )
4	1 3	mpbir	⊢ ( ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅 )