Metamath Proof Explorer


Theorem iss2

Description: A subclass of the identity relation is the intersection of identity relation with Cartesian product of the domain and range of the class. (Contributed by Peter Mazsa, 22-Jul-2019)

Ref Expression
Assertion iss2 AIA=IdomA×ranA

Proof

Step Hyp Ref Expression
1 ssel AIxyAxyI
2 vex xV
3 vex yV
4 2 3 opeldm xyAxdomA
5 1 4 jca2 AIxyAxyIxdomA
6 2 3 opelrn xyAyranA
7 1 6 jca2 AIxyAxyIyranA
8 5 7 jcad AIxyAxyIxdomAxyIyranA
9 anandi xyIxdomAyranAxyIxdomAxyIyranA
10 8 9 imbitrrdi AIxyAxyIxdomAyranA
11 df-br xIyxyI
12 3 ideq xIyx=y
13 11 12 bitr3i xyIx=y
14 2 eldm2 xdomAyxyA
15 opeq2 x=yxx=xy
16 15 eleq1d x=yxxAxyA
17 16 biimprcd xyAx=yxxA
18 13 17 biimtrid xyAxyIxxA
19 1 18 sylcom AIxyAxxA
20 19 exlimdv AIyxyAxxA
21 14 20 biimtrid AIxdomAxxA
22 16 imbi2d x=yxdomAxxAxdomAxyA
23 21 22 syl5ibcom AIx=yxdomAxyA
24 23 imp AIx=yxdomAxyA
25 24 adantrd AIx=yxdomAyranAxyA
26 25 ex AIx=yxdomAyranAxyA
27 13 26 biimtrid AIxyIxdomAyranAxyA
28 27 impd AIxyIxdomAyranAxyA
29 10 28 impbid AIxyAxyIxdomAyranA
30 opelinxp xyIdomA×ranAxdomAyranAxyI
31 30 biancomi xyIdomA×ranAxyIxdomAyranA
32 29 31 bitr4di AIxyAxyIdomA×ranA
33 32 alrimivv AIxyxyAxyIdomA×ranA
34 reli RelI
35 relss AIRelIRelA
36 34 35 mpi AIRelA
37 relinxp RelIdomA×ranA
38 eqrel RelARelIdomA×ranAA=IdomA×ranAxyxyAxyIdomA×ranA
39 36 37 38 sylancl AIA=IdomA×ranAxyxyAxyIdomA×ranA
40 33 39 mpbird AIA=IdomA×ranA
41 inss1 IdomA×ranAI
42 sseq1 A=IdomA×ranAAIIdomA×ranAI
43 41 42 mpbiri A=IdomA×ranAAI
44 40 43 impbii AIA=IdomA×ranA