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

Metamath Proof Explorer

Theorem restidsing

Description: Restriction of the identity to a singleton. (Contributed by FL, 2-Aug-2009) (Proof shortened by JJ, 25-Aug-2021) (Proof shortened by Peter Mazsa, 6-Oct-2022)

Ref Expression
Assertion restidsing ( I ↾ { 𝐴 } ) = ( { 𝐴 } × { 𝐴 } )

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ( I ↾ { 𝐴 } )
2 relxp ⊢ Rel ( { 𝐴 } × { 𝐴 } )
3 velsn ⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
4 velsn ⊢ ( 𝑦 ∈ { 𝐴 } ↔ 𝑦 = 𝐴 )
5 3 4 anbi12i ⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) )
6 vex ⊢ 𝑦 ∈ V
7 6 ideq ⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
8 3 7 anbi12i ⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 I 𝑦 ) ↔ ( 𝑥 = 𝐴 ∧ 𝑥 = 𝑦 ) )
9 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝐴 = 𝑦 ) )
10 eqcom ⊢ ( 𝐴 = 𝑦 ↔ 𝑦 = 𝐴 )
11 9 10 bitrdi ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝑦 = 𝐴 ) )
12 11 pm5.32i ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑥 = 𝑦 ) ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) )
13 8 12 bitri ⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 I 𝑦 ) ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) )
14 df-br ⊢ ( 𝑥 I 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ I )
15 14 anbi2i ⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 I 𝑦 ) ↔ ( 𝑥 ∈ { 𝐴 } ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
16 5 13 15 3bitr2ri ⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) ↔ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) )
17 6 opelresi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ { 𝐴 } ) ↔ ( 𝑥 ∈ { 𝐴 } ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
18 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝐴 } × { 𝐴 } ) ↔ ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ { 𝐴 } ) )
19 16 17 18 3bitr4i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ { 𝐴 } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝐴 } × { 𝐴 } ) )
20 1 2 19 eqrelriiv ⊢ ( I ↾ { 𝐴 } ) = ( { 𝐴 } × { 𝐴 } )