Theorem refrelcoss3

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

	Ref	Expression
Assertion	refrelcoss3	⊢ ( ∀ 𝑥 ∈ dom ≀ 𝑅 ∀ 𝑦 ∈ ran ≀ 𝑅 ( 𝑥 = 𝑦 → 𝑥 ≀ 𝑅 𝑦 ) ∧ Rel ≀ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		refrelcosslem	⊢ ∀ 𝑥 ∈ dom ≀ 𝑅 𝑥 ≀ 𝑅 𝑥
2		idinxpssinxp4	⊢ ( ∀ 𝑥 ∈ dom ≀ 𝑅 ∀ 𝑦 ∈ dom ≀ 𝑅 ( 𝑥 = 𝑦 → 𝑥 ≀ 𝑅 𝑦 ) ↔ ∀ 𝑥 ∈ dom ≀ 𝑅 𝑥 ≀ 𝑅 𝑥 )
3	1 2	mpbir	⊢ ∀ 𝑥 ∈ dom ≀ 𝑅 ∀ 𝑦 ∈ dom ≀ 𝑅 ( 𝑥 = 𝑦 → 𝑥 ≀ 𝑅 𝑦 )
4		rncossdmcoss	⊢ ran ≀ 𝑅 = dom ≀ 𝑅
5	4	raleqi	⊢ ( ∀ 𝑦 ∈ ran ≀ 𝑅 ( 𝑥 = 𝑦 → 𝑥 ≀ 𝑅 𝑦 ) ↔ ∀ 𝑦 ∈ dom ≀ 𝑅 ( 𝑥 = 𝑦 → 𝑥 ≀ 𝑅 𝑦 ) )
6	5	ralbii	⊢ ( ∀ 𝑥 ∈ dom ≀ 𝑅 ∀ 𝑦 ∈ ran ≀ 𝑅 ( 𝑥 = 𝑦 → 𝑥 ≀ 𝑅 𝑦 ) ↔ ∀ 𝑥 ∈ dom ≀ 𝑅 ∀ 𝑦 ∈ dom ≀ 𝑅 ( 𝑥 = 𝑦 → 𝑥 ≀ 𝑅 𝑦 ) )
7	3 6	mpbir	⊢ ∀ 𝑥 ∈ dom ≀ 𝑅 ∀ 𝑦 ∈ ran ≀ 𝑅 ( 𝑥 = 𝑦 → 𝑥 ≀ 𝑅 𝑦 )
8		relcoss	⊢ Rel ≀ 𝑅
9	7 8	pm3.2i	⊢ ( ∀ 𝑥 ∈ dom ≀ 𝑅 ∀ 𝑦 ∈ ran ≀ 𝑅 ( 𝑥 = 𝑦 → 𝑥 ≀ 𝑅 𝑦 ) ∧ Rel ≀ 𝑅 )