Metamath Proof Explorer


Theorem dfrcl2

Description: Reflexive closure of a relation as union with restricted identity relation. (Contributed by RP, 6-Jun-2020)

Ref Expression
Assertion dfrcl2 r* = x V I dom x ran x x

Proof

Step Hyp Ref Expression
1 df-rcl r* = x V z | x z I dom z ran z z
2 rabab z V | x z I dom z ran z z = z | x z I dom z ran z z
3 2 eqcomi z | x z I dom z ran z z = z V | x z I dom z ran z z
4 3 inteqi z | x z I dom z ran z z = z V | x z I dom z ran z z
5 4 a1i x V z | x z I dom z ran z z = z V | x z I dom z ran z z
6 vex x V
7 6 dmex dom x V
8 6 rnex ran x V
9 7 8 unex dom x ran x V
10 resiexg dom x ran x V I dom x ran x V
11 9 10 ax-mp I dom x ran x V
12 11 6 unex I dom x ran x x V
13 12 a1i x V I dom x ran x x V
14 ssun2 x I dom x ran x x
15 dmun dom I dom x ran x x = dom I dom x ran x dom x
16 dmresi dom I dom x ran x = dom x ran x
17 16 uneq1i dom I dom x ran x dom x = dom x ran x dom x
18 un23 dom x ran x dom x = dom x dom x ran x
19 unidm dom x dom x = dom x
20 19 uneq1i dom x dom x ran x = dom x ran x
21 18 20 eqtri dom x ran x dom x = dom x ran x
22 15 17 21 3eqtri dom I dom x ran x x = dom x ran x
23 rnun ran I dom x ran x x = ran I dom x ran x ran x
24 rnresi ran I dom x ran x = dom x ran x
25 24 uneq1i ran I dom x ran x ran x = dom x ran x ran x
26 unass dom x ran x ran x = dom x ran x ran x
27 unidm ran x ran x = ran x
28 27 uneq2i dom x ran x ran x = dom x ran x
29 26 28 eqtri dom x ran x ran x = dom x ran x
30 23 25 29 3eqtri ran I dom x ran x x = dom x ran x
31 22 30 uneq12i dom I dom x ran x x ran I dom x ran x x = dom x ran x dom x ran x
32 unidm dom x ran x dom x ran x = dom x ran x
33 31 32 eqtri dom I dom x ran x x ran I dom x ran x x = dom x ran x
34 33 reseq2i I dom I dom x ran x x ran I dom x ran x x = I dom x ran x
35 ssun1 I dom x ran x I dom x ran x x
36 34 35 eqsstri I dom I dom x ran x x ran I dom x ran x x I dom x ran x x
37 14 36 pm3.2i x I dom x ran x x I dom I dom x ran x x ran I dom x ran x x I dom x ran x x
38 dmeq z = I dom x ran x x dom z = dom I dom x ran x x
39 rneq z = I dom x ran x x ran z = ran I dom x ran x x
40 38 39 uneq12d z = I dom x ran x x dom z ran z = dom I dom x ran x x ran I dom x ran x x
41 40 reseq2d z = I dom x ran x x I dom z ran z = I dom I dom x ran x x ran I dom x ran x x
42 id z = I dom x ran x x z = I dom x ran x x
43 41 42 sseq12d z = I dom x ran x x I dom z ran z z I dom I dom x ran x x ran I dom x ran x x I dom x ran x x
44 43 cleq2lem z = I dom x ran x x x z I dom z ran z z x I dom x ran x x I dom I dom x ran x x ran I dom x ran x x I dom x ran x x
45 44 intminss I dom x ran x x V x I dom x ran x x I dom I dom x ran x x ran I dom x ran x x I dom x ran x x z V | x z I dom z ran z z I dom x ran x x
46 13 37 45 sylancl x V z V | x z I dom z ran z z I dom x ran x x
47 5 46 eqsstrd x V z | x z I dom z ran z z I dom x ran x x
48 dmss x z dom x dom z
49 rnss x z ran x ran z
50 unss12 dom x dom z ran x ran z dom x ran x dom z ran z
51 48 49 50 syl2anc x z dom x ran x dom z ran z
52 dfss dom x ran x dom z ran z dom x ran x = dom x ran x dom z ran z
53 51 52 sylib x z dom x ran x = dom x ran x dom z ran z
54 incom dom x ran x dom z ran z = dom z ran z dom x ran x
55 53 54 syl6eq x z dom x ran x = dom z ran z dom x ran x
56 55 reseq2d x z I dom x ran x = I dom z ran z dom x ran x
57 resres I dom z ran z dom x ran x = I dom z ran z dom x ran x
58 56 57 syl6eqr x z I dom x ran x = I dom z ran z dom x ran x
59 resss I dom z ran z dom x ran x I dom z ran z
60 59 a1i x z I dom z ran z dom x ran x I dom z ran z
61 58 60 eqsstrd x z I dom x ran x I dom z ran z
62 61 adantr x z I dom z ran z z I dom x ran x I dom z ran z
63 simpr x z I dom z ran z z I dom z ran z z
64 62 63 sstrd x z I dom z ran z z I dom x ran x z
65 simpl x z I dom z ran z z x z
66 64 65 unssd x z I dom z ran z z I dom x ran x x z
67 66 ax-gen z x z I dom z ran z z I dom x ran x x z
68 67 a1i x V z x z I dom z ran z z I dom x ran x x z
69 ssintab I dom x ran x x z | x z I dom z ran z z z x z I dom z ran z z I dom x ran x x z
70 68 69 sylibr x V I dom x ran x x z | x z I dom z ran z z
71 47 70 eqssd x V z | x z I dom z ran z z = I dom x ran x x
72 71 mpteq2ia x V z | x z I dom z ran z z = x V I dom x ran x x
73 1 72 eqtri r* = x V I dom x ran x x