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 ↾ 𝐴 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) = ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ )
2 1 fmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝑅 ↔ ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) : 𝐴 ⟶ 𝑅 )
3 opex ⊢ ⟨ 𝑥 , 𝑥 ⟩ ∈ V
4 3 1 fnmpti ⊢ ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) Fn 𝐴
5 df-f ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) : 𝐴 ⟶ 𝑅 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) Fn 𝐴 ∧ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ⊆ 𝑅 ) )
6 4 5 mpbiran ⊢ ( ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) : 𝐴 ⟶ 𝑅 ↔ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ⊆ 𝑅 )
7 2 6 bitri ⊢ ( ∀ 𝑥 ∈ 𝐴 ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝑅 ↔ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ⊆ 𝑅 )
8 df-br ⊢ ( 𝑥 𝑅 𝑥 ↔ ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝑅 )
9 8 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝑅 )
10 mptresid ⊢ ( I ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑥 )
11 vex ⊢ 𝑥 ∈ V
12 11 fnasrn ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) = ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ )
13 10 12 eqtri ⊢ ( I ↾ 𝐴 ) = ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ )
14 13 sseq1i ⊢ ( ( I ↾ 𝐴 ) ⊆ 𝑅 ↔ ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , 𝑥 ⟩ ) ⊆ 𝑅 )
15 7 9 14 3bitr4ri ⊢ ( ( I ↾ 𝐴 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 )