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