Theorem restidsing 14391

Description: Restriction of the identity to a singleton.

Assertion

Ref	Expression
restidsing	|- ( _I |` {A}) = ({A} X. {A})

Proof of Theorem restidsing

Step	Hyp	Ref	Expression
1		relres 4242	. 2 |- Rel ( _I |` {A})
2		relxp 4088	. 2 |- Rel ({A} X. {A})
3		df-br 3339	. . . . . 6 |- (x _I y <-> <.x, y>. e. _I )
4	3	bicomi 189	. . . . 5 |- (<.x, y>. e. _I <-> x _I y)
5	4	anbi1i 539	. . . 4 |- ((<.x, y>. e. _I /\ x e. {A}) <-> (x _I y /\ x e. {A}))
6		simpr 350	. . . . . 6 |- ((x _I y /\ x e. {A}) -> x e. {A})
7		visset 2295	. . . . . . . . . 10 |- y e. _V
8		ideqg 4114	. . . . . . . . . . 11 |- (y e. _V -> (x _I y <-> x = y))
9	8	biimpd 170	. . . . . . . . . 10 |- (y e. _V -> (x _I y -> x = y))
10	7, 9	ax-mp 7	. . . . . . . . 9 |- (x _I y -> x = y)
11		eqtr2 1905	. . . . . . . . . . 11 |- ((x = y /\ x = A) -> y = A)
12	11	ex 402	. . . . . . . . . 10 |- (x = y -> (x = A -> y = A))
13		elsn 3058	. . . . . . . . . 10 |- (y e. {A} <-> y = A)
14	12, 13	syl6ibr 230	. . . . . . . . 9 |- (x = y -> (x = A -> y e. {A}))
15	10, 14	syl 12	. . . . . . . 8 |- (x _I y -> (x = A -> y e. {A}))
16		elsn 3058	. . . . . . . 8 |- (x e. {A} <-> x = A)
17	15, 16	syl5ib 223	. . . . . . 7 |- (x _I y -> (x e. {A} -> y e. {A}))
18	17	imp 377	. . . . . 6 |- ((x _I y /\ x e. {A}) -> y e. {A})
19	6, 18	jca 310	. . . . 5 |- ((x _I y /\ x e. {A}) -> (x e. {A} /\ y e. {A}))
20		eqtr3 1907	. . . . . . . . . . . 12 |- ((y = A /\ x = A) -> y = x)
21	7	ideq 4116	. . . . . . . . . . . . 13 |- (x _I y <-> x = y)
22		equcom 1488	. . . . . . . . . . . . 13 |- (x = y <-> y = x)
23	21, 22	bitri 190	. . . . . . . . . . . 12 |- (x _I y <-> y = x)
24	20, 23	sylibr 217	. . . . . . . . . . 11 |- ((y = A /\ x = A) -> x _I y)
25	24	ex 402	. . . . . . . . . 10 |- (y = A -> (x = A -> x _I y))
26	13, 25	sylbi 216	. . . . . . . . 9 |- (y e. {A} -> (x = A -> x _I y))
27	26	com12 14	. . . . . . . 8 |- (x = A -> (y e. {A} -> x _I y))
28	16, 27	sylbi 216	. . . . . . 7 |- (x e. {A} -> (y e. {A} -> x _I y))
29	28	imp 377	. . . . . 6 |- ((x e. {A} /\ y e. {A}) -> x _I y)
30		simpl 346	. . . . . 6 |- ((x e. {A} /\ y e. {A}) -> x e. {A})
31	29, 30	jca 310	. . . . 5 |- ((x e. {A} /\ y e. {A}) -> (x _I y /\ x e. {A}))
32	19, 31	impbii 174	. . . 4 |- ((x _I y /\ x e. {A}) <-> (x e. {A} /\ y e. {A}))
33	5, 32	bitri 190	. . 3 |- ((<.x, y>. e. _I /\ x e. {A}) <-> (x e. {A} /\ y e. {A}))
34	7	opelres 4222	. . 3 |- (<.x, y>. e. ( _I |` {A}) <-> (<.x, y>. e. _I /\ x e. {A}))
35	7	opelxp 4036	. . 3 |- (<.x, y>. e. ({A} X. {A}) <-> (x e. {A} /\ y e. {A}))
36	33, 34, 35	3bitr4i 200	. 2 |- (<.x, y>. e. ( _I |` {A}) <-> <.x, y>. e. ({A} X. {A}))
37	1, 2, 36	eqrelriv 4080	1 |- ( _I |` {A}) = ({A} X. {A})

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298   e. wcel 1300  _Vcvv 2292  {csn 3044  <.cop 3046   class class class wbr 3338   _I cid 3582   X. cxp 3984   |` cres 3988

This theorem is referenced by:  invtrgrp 14979

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-res 4006

Copyright terms: Public domain