This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ≀ 𝑅 )