Theorem iss 4254

Description: A subclass of the identity function is the identity function restricted to its domain. (The proof was shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
iss	|- (A C_ _I <-> A = ( _I |` dom A))

Proof of Theorem iss

Step	Hyp	Ref	Expression
1		ssel 2615	. . . . . . 7 |- (A C_ _I -> (<.x, y>. e. A -> <.x, y>. e. _I ))
2		visset 2295	. . . . . . . . 9 |- x e. _V
3	2	opeldm 4160	. . . . . . . 8 |- (<.x, y>. e. A -> x e. dom A)
4	3	a1i 8	. . . . . . 7 |- (A C_ _I -> (<.x, y>. e. A -> x e. dom A))
5	1, 4	jcad 661	. . . . . 6 |- (A C_ _I -> (<.x, y>. e. A -> (<.x, y>. e. _I /\ x e. dom A)))
6		opeq2 3159	. . . . . . . . . . 11 |- (x = y -> <.x, x>. = <.x, y>.)
7	6	eleq1d 1963	. . . . . . . . . 10 |- (x = y -> (<.x, x>. e. A <-> <.x, y>. e. A))
8	7	imbi2d 674	. . . . . . . . 9 |- (x = y -> ((x e. dom A -> <.x, x>. e. A) <-> (x e. dom A -> <.x, y>. e. A)))
9	7	biimprcd 173	. . . . . . . . . . . . 13 |- (<.x, y>. e. A -> (x = y -> <.x, x>. e. A))
10		df-br 3339	. . . . . . . . . . . . . 14 |- (x _I y <-> <.x, y>. e. _I )
11		visset 2295	. . . . . . . . . . . . . . 15 |- y e. _V
12	11	ideq 4116	. . . . . . . . . . . . . 14 |- (x _I y <-> x = y)
13	10, 12	bitr3i 192	. . . . . . . . . . . . 13 |- (<.x, y>. e. _I <-> x = y)
14	9, 13	syl5ib 223	. . . . . . . . . . . 12 |- (<.x, y>. e. A -> (<.x, y>. e. _I -> <.x, x>. e. A))
15	1, 14	sylcom 62	. . . . . . . . . . 11 |- (A C_ _I -> (<.x, y>. e. A -> <.x, x>. e. A))
16	15	19.23adv 1584	. . . . . . . . . 10 |- (A C_ _I -> (E.y<.x, y>. e. A -> <.x, x>. e. A))
17	2	eldm2 4154	. . . . . . . . . 10 |- (x e. dom A <-> E.y<.x, y>. e. A)
18	16, 17	syl5ib 223	. . . . . . . . 9 |- (A C_ _I -> (x e. dom A -> <.x, x>. e. A))
19	8, 18	syl5cbi 226	. . . . . . . 8 |- (A C_ _I -> (x = y -> (x e. dom A -> <.x, y>. e. A)))
20	19, 13	syl5ib 223	. . . . . . 7 |- (A C_ _I -> (<.x, y>. e. _I -> (x e. dom A -> <.x, y>. e. A)))
21	20	imp3a 388	. . . . . 6 |- (A C_ _I -> ((<.x, y>. e. _I /\ x e. dom A) -> <.x, y>. e. A))
22	5, 21	impbid 574	. . . . 5 |- (A C_ _I -> (<.x, y>. e. A <-> (<.x, y>. e. _I /\ x e. dom A)))
23	11	opelres 4222	. . . . 5 |- (<.x, y>. e. ( _I |` dom A) <-> (<.x, y>. e. _I /\ x e. dom A))
24	22, 23	syl6bbr 597	. . . 4 |- (A C_ _I -> (<.x, y>. e. A <-> <.x, y>. e. ( _I |` dom A)))
25	24	19.21aivv 1665	. . 3 |- (A C_ _I -> A.xA.y(<.x, y>. e. A <-> <.x, y>. e. ( _I |` dom A)))
26		eqrel 4077	. . . 4 |- ((Rel A /\ Rel ( _I |` dom A)) -> (A = ( _I |` dom A) <-> A.xA.y(<.x, y>. e. A <-> <.x, y>. e. ( _I |` dom A))))
27		reli 4105	. . . . 5 |- Rel _I
28		relss 4074	. . . . 5 |- (A C_ _I -> (Rel _I -> Rel A))
29	27, 28	mpi 55	. . . 4 |- (A C_ _I -> Rel A)
30		relres 4242	. . . 4 |- Rel ( _I |` dom A)
31	26, 29, 30	sylancl 525	. . 3 |- (A C_ _I -> (A = ( _I |` dom A) <-> A.xA.y(<.x, y>. e. A <-> <.x, y>. e. ( _I |` dom A))))
32	25, 31	mpbird 213	. 2 |- (A C_ _I -> A = ( _I |` dom A))
33		resss 4237	. . 3 |- ( _I |` dom A) C_ _I
34		sseq1 2637	. . 3 |- (A = ( _I |` dom A) -> (A C_ _I <-> ( _I |` dom A) C_ _I ))
35	33, 34	mpbiri 211	. 2 |- (A = ( _I |` dom A) -> A C_ _I )
36	32, 35	impbii 174	1 |- (A C_ _I <-> A = ( _I |` dom A))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326   C_ wss 2593  <.cop 3046   class class class wbr 3338   _I cid 3582  dom cdm 3986   |` cres 3988  Rel wrel 3991

This theorem is referenced by:  f1ococnv2 4662  cnvcan 15715

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-dm 4004  df-res 4006

Copyright terms: Public domain