Metamath Proof Explorer


Theorem iss

Description: A subclass of the identity function is the identity function restricted to its domain. (Contributed by NM, 13-Dec-2003) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion iss A I A = I dom A

Proof

Step Hyp Ref Expression
1 vex x V
2 vex y V
3 1 2 opeldm x y A x dom A
4 3 a1i A I x y A x dom A
5 ssel A I x y A x y I
6 4 5 jcad A I x y A x dom A x y I
7 df-br x I y x y I
8 2 ideq x I y x = y
9 7 8 bitr3i x y I x = y
10 1 eldm2 x dom A y x y A
11 opeq2 x = y x x = x y
12 11 eleq1d x = y x x A x y A
13 12 biimprcd x y A x = y x x A
14 9 13 syl5bi x y A x y I x x A
15 5 14 sylcom A I x y A x x A
16 15 exlimdv A I y x y A x x A
17 10 16 syl5bi A I x dom A x x A
18 12 imbi2d x = y x dom A x x A x dom A x y A
19 17 18 syl5ibcom A I x = y x dom A x y A
20 9 19 syl5bi A I x y I x dom A x y A
21 20 impcomd A I x dom A x y I x y A
22 6 21 impbid A I x y A x dom A x y I
23 2 opelresi x y I dom A x dom A x y I
24 22 23 bitr4di A I x y A x y I dom A
25 24 alrimivv A I x y x y A x y I dom A
26 reli Rel I
27 relss A I Rel I Rel A
28 26 27 mpi A I Rel A
29 relres Rel I dom A
30 eqrel Rel A Rel I dom A A = I dom A x y x y A x y I dom A
31 28 29 30 sylancl A I A = I dom A x y x y A x y I dom A
32 25 31 mpbird A I A = I dom A
33 resss I dom A I
34 sseq1 A = I dom A A I I dom A I
35 33 34 mpbiri A = I dom A A I
36 32 35 impbii A I A = I dom A