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

Metamath Proof Explorer

Theorem idref

Description: Two ways to state that a relation is reflexive on a class. (Contributed by FL, 15-Jan-2012) (Proof shortened by Mario Carneiro, 3-Nov-2015) (Revised by NM, 30-Mar-2016)

Ref Expression
Assertion idref ⊢ I ↾ A ⊆ R ↔ ∀ x ∈ A x R x

Proof

Step Hyp Ref Expression
1 eqid ⊢ x ∈ A ⟼ x x = x ∈ A ⟼ x x
2 1 fmpt ⊢ ∀ x ∈ A x x ∈ R ↔ x ∈ A ⟼ x x : A ⟶ R
3 opex ⊢ x x ∈ V
4 3 1 fnmpti ⊢ x ∈ A ⟼ x x Fn A
5 df-f ⊢ x ∈ A ⟼ x x : A ⟶ R ↔ x ∈ A ⟼ x x Fn A ∧ ran ⁡ x ∈ A ⟼ x x ⊆ R
6 4 5 mpbiran ⊢ x ∈ A ⟼ x x : A ⟶ R ↔ ran ⁡ x ∈ A ⟼ x x ⊆ R
7 2 6 bitri ⊢ ∀ x ∈ A x x ∈ R ↔ ran ⁡ x ∈ A ⟼ x x ⊆ R
8 df-br ⊢ x R x ↔ x x ∈ R
9 8 ralbii ⊢ ∀ x ∈ A x R x ↔ ∀ x ∈ A x x ∈ R
10 mptresid ⊢ I ↾ A = x ∈ A ⟼ x
11 vex ⊢ x ∈ V
12 11 fnasrn ⊢ x ∈ A ⟼ x = ran ⁡ x ∈ A ⟼ x x
13 10 12 eqtri ⊢ I ↾ A = ran ⁡ x ∈ A ⟼ x x
14 13 sseq1i ⊢ I ↾ A ⊆ R ↔ ran ⁡ x ∈ A ⟼ x x ⊆ R
15 7 9 14 3bitr4ri ⊢ I ↾ A ⊆ R ↔ ∀ x ∈ A x R x