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

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