Metamath Proof Explorer


Theorem idrefALT

Description: Alternate proof of idref not relying on definitions related to functions. 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) (Proof shortened by BJ, 28-Aug-2022) The "proof modification is discouraged" tag is here only because this is an *ALT result. (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion idrefALT ( ( I ↾ 𝐴 ) ⊆ 𝑅 ↔ ∀ 𝑥𝐴 𝑥 𝑅 𝑥 )

Proof

Step Hyp Ref Expression
1 dfss2 ( ( I ↾ 𝐴 ) ⊆ 𝑅 ↔ ∀ 𝑦 ( 𝑦 ∈ ( I ↾ 𝐴 ) → 𝑦𝑅 ) )
2 elrid ( 𝑦 ∈ ( I ↾ 𝐴 ) ↔ ∃ 𝑥𝐴 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ )
3 2 imbi1i ( ( 𝑦 ∈ ( I ↾ 𝐴 ) → 𝑦𝑅 ) ↔ ( ∃ 𝑥𝐴 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → 𝑦𝑅 ) )
4 r19.23v ( ∀ 𝑥𝐴 ( 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → 𝑦𝑅 ) ↔ ( ∃ 𝑥𝐴 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → 𝑦𝑅 ) )
5 eleq1 ( 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → ( 𝑦𝑅 ↔ ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝑅 ) )
6 df-br ( 𝑥 𝑅 𝑥 ↔ ⟨ 𝑥 , 𝑥 ⟩ ∈ 𝑅 )
7 5 6 bitr4di ( 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → ( 𝑦𝑅𝑥 𝑅 𝑥 ) )
8 7 pm5.74i ( ( 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → 𝑦𝑅 ) ↔ ( 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → 𝑥 𝑅 𝑥 ) )
9 8 ralbii ( ∀ 𝑥𝐴 ( 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → 𝑦𝑅 ) ↔ ∀ 𝑥𝐴 ( 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → 𝑥 𝑅 𝑥 ) )
10 3 4 9 3bitr2i ( ( 𝑦 ∈ ( I ↾ 𝐴 ) → 𝑦𝑅 ) ↔ ∀ 𝑥𝐴 ( 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → 𝑥 𝑅 𝑥 ) )
11 10 albii ( ∀ 𝑦 ( 𝑦 ∈ ( I ↾ 𝐴 ) → 𝑦𝑅 ) ↔ ∀ 𝑦𝑥𝐴 ( 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → 𝑥 𝑅 𝑥 ) )
12 ralcom4 ( ∀ 𝑥𝐴𝑦 ( 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → 𝑥 𝑅 𝑥 ) ↔ ∀ 𝑦𝑥𝐴 ( 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → 𝑥 𝑅 𝑥 ) )
13 opex 𝑥 , 𝑥 ⟩ ∈ V
14 biidd ( 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → ( 𝑥 𝑅 𝑥𝑥 𝑅 𝑥 ) )
15 13 14 ceqsalv ( ∀ 𝑦 ( 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → 𝑥 𝑅 𝑥 ) ↔ 𝑥 𝑅 𝑥 )
16 15 ralbii ( ∀ 𝑥𝐴𝑦 ( 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ → 𝑥 𝑅 𝑥 ) ↔ ∀ 𝑥𝐴 𝑥 𝑅 𝑥 )
17 11 12 16 3bitr2i ( ∀ 𝑦 ( 𝑦 ∈ ( I ↾ 𝐴 ) → 𝑦𝑅 ) ↔ ∀ 𝑥𝐴 𝑥 𝑅 𝑥 )
18 1 17 bitri ( ( I ↾ 𝐴 ) ⊆ 𝑅 ↔ ∀ 𝑥𝐴 𝑥 𝑅 𝑥 )