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 A I A = I dom A × ran A

Proof

Step Hyp Ref Expression
1 ssel A I x y A x y I
2 vex x V
3 vex y V
4 2 3 opeldm x y A x dom A
5 1 4 jca2 A I x y A x y I x dom A
6 2 3 opelrn x y A y ran A
7 1 6 jca2 A I x y A x y I y ran A
8 5 7 jcad A I x y A x y I x dom A x y I y ran A
9 anandi x y I x dom A y ran A x y I x dom A x y I y ran A
10 8 9 syl6ibr A I x y A x y I x dom A y ran A
11 df-br x I y x y I
12 3 ideq x I y x = y
13 11 12 bitr3i x y I x = y
14 2 eldm2 x dom A y x y A
15 opeq2 x = y x x = x y
16 15 eleq1d x = y x x A x y A
17 16 biimprcd x y A x = y x x A
18 13 17 syl5bi x y A x y I x x A
19 1 18 sylcom A I x y A x x A
20 19 exlimdv A I y x y A x x A
21 14 20 syl5bi A I x dom A x x A
22 16 imbi2d x = y x dom A x x A x dom A x y A
23 21 22 syl5ibcom A I x = y x dom A x y A
24 23 imp A I x = y x dom A x y A
25 24 adantrd A I x = y x dom A y ran A x y A
26 25 ex A I x = y x dom A y ran A x y A
27 13 26 syl5bi A I x y I x dom A y ran A x y A
28 27 impd A I x y I x dom A y ran A x y A
29 10 28 impbid A I x y A x y I x dom A y ran A
30 opelinxp x y I dom A × ran A x dom A y ran A x y I
31 30 biancomi x y I dom A × ran A x y I x dom A y ran A
32 29 31 bitr4di A I x y A x y I dom A × ran A
33 32 alrimivv A I x y x y A x y I dom A × ran A
34 reli Rel I
35 relss A I Rel I Rel A
36 34 35 mpi A I Rel A
37 relinxp Rel I dom A × ran A
38 eqrel Rel A Rel I dom A × ran A A = I dom A × ran A x y x y A x y I dom A × ran A
39 36 37 38 sylancl A I A = I dom A × ran A x y x y A x y I dom A × ran A
40 33 39 mpbird A I A = I dom A × ran A
41 inss1 I dom A × ran A I
42 sseq1 A = I dom A × ran A A I I dom A × ran A I
43 41 42 mpbiri A = I dom A × ran A A I
44 40 43 impbii A I A = I dom A × ran A