Metamath Proof Explorer


Theorem cnvrcl0

Description: The converse of the reflexive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020)

Ref Expression
Assertion cnvrcl0 X V x | X x I dom x ran x x -1 = y | X -1 y I dom y ran y y

Proof

Step Hyp Ref Expression
1 cnvresid I dom y ran y -1 = I dom y ran y
2 cnvnonrel X X -1 -1 -1 =
3 cnv0 -1 =
4 2 3 eqtr4i X X -1 -1 -1 = -1
5 4 dmeqi dom X X -1 -1 -1 = dom -1
6 df-rn ran X X -1 -1 = dom X X -1 -1 -1
7 df-rn ran = dom -1
8 5 6 7 3eqtr4i ran X X -1 -1 = ran
9 0ss y -1
10 9 rnssi ran ran y -1
11 8 10 eqsstri ran X X -1 -1 ran y -1
12 ssequn2 ran X X -1 -1 ran y -1 ran y -1 ran X X -1 -1 = ran y -1
13 11 12 mpbi ran y -1 ran X X -1 -1 = ran y -1
14 rnun ran y -1 X X -1 -1 = ran y -1 ran X X -1 -1
15 dfdm4 dom y = ran y -1
16 13 14 15 3eqtr4ri dom y = ran y -1 X X -1 -1
17 4 rneqi ran X X -1 -1 -1 = ran -1
18 dfdm4 dom X X -1 -1 = ran X X -1 -1 -1
19 dfdm4 dom = ran -1
20 17 18 19 3eqtr4i dom X X -1 -1 = dom
21 dmss y -1 dom dom y -1
22 9 21 ax-mp dom dom y -1
23 20 22 eqsstri dom X X -1 -1 dom y -1
24 ssequn2 dom X X -1 -1 dom y -1 dom y -1 dom X X -1 -1 = dom y -1
25 23 24 mpbi dom y -1 dom X X -1 -1 = dom y -1
26 dmun dom y -1 X X -1 -1 = dom y -1 dom X X -1 -1
27 df-rn ran y = dom y -1
28 25 26 27 3eqtr4ri ran y = dom y -1 X X -1 -1
29 16 28 uneq12i dom y ran y = ran y -1 X X -1 -1 dom y -1 X X -1 -1
30 29 equncomi dom y ran y = dom y -1 X X -1 -1 ran y -1 X X -1 -1
31 30 reseq2i I dom y ran y = I dom y -1 X X -1 -1 ran y -1 X X -1 -1
32 1 31 eqtr2i I dom y -1 X X -1 -1 ran y -1 X X -1 -1 = I dom y ran y -1
33 cnvss I dom y ran y y I dom y ran y -1 y -1
34 32 33 eqsstrid I dom y ran y y I dom y -1 X X -1 -1 ran y -1 X X -1 -1 y -1
35 ssun1 y -1 y -1 X X -1 -1
36 34 35 sstrdi I dom y ran y y I dom y -1 X X -1 -1 ran y -1 X X -1 -1 y -1 X X -1 -1
37 dmeq x = y -1 X X -1 -1 dom x = dom y -1 X X -1 -1
38 rneq x = y -1 X X -1 -1 ran x = ran y -1 X X -1 -1
39 37 38 uneq12d x = y -1 X X -1 -1 dom x ran x = dom y -1 X X -1 -1 ran y -1 X X -1 -1
40 39 reseq2d x = y -1 X X -1 -1 I dom x ran x = I dom y -1 X X -1 -1 ran y -1 X X -1 -1
41 id x = y -1 X X -1 -1 x = y -1 X X -1 -1
42 40 41 sseq12d x = y -1 X X -1 -1 I dom x ran x x I dom y -1 X X -1 -1 ran y -1 X X -1 -1 y -1 X X -1 -1
43 36 42 syl5ibr x = y -1 X X -1 -1 I dom y ran y y I dom x ran x x
44 43 adantl X V x = y -1 X X -1 -1 I dom y ran y y I dom x ran x x
45 cnvresid I dom x ran x -1 = I dom x ran x
46 dfdm4 dom x = ran x -1
47 df-rn ran x = dom x -1
48 46 47 uneq12i dom x ran x = ran x -1 dom x -1
49 48 equncomi dom x ran x = dom x -1 ran x -1
50 49 reseq2i I dom x ran x = I dom x -1 ran x -1
51 45 50 eqtr2i I dom x -1 ran x -1 = I dom x ran x -1
52 cnvss I dom x ran x x I dom x ran x -1 x -1
53 51 52 eqsstrid I dom x ran x x I dom x -1 ran x -1 x -1
54 dmeq y = x -1 dom y = dom x -1
55 rneq y = x -1 ran y = ran x -1
56 54 55 uneq12d y = x -1 dom y ran y = dom x -1 ran x -1
57 56 reseq2d y = x -1 I dom y ran y = I dom x -1 ran x -1
58 id y = x -1 y = x -1
59 57 58 sseq12d y = x -1 I dom y ran y y I dom x -1 ran x -1 x -1
60 53 59 syl5ibr y = x -1 I dom x ran x x I dom y ran y y
61 60 adantl X V y = x -1 I dom x ran x x I dom y ran y y
62 dmeq x = X I dom X ran X dom x = dom X I dom X ran X
63 rneq x = X I dom X ran X ran x = ran X I dom X ran X
64 62 63 uneq12d x = X I dom X ran X dom x ran x = dom X I dom X ran X ran X I dom X ran X
65 64 reseq2d x = X I dom X ran X I dom x ran x = I dom X I dom X ran X ran X I dom X ran X
66 id x = X I dom X ran X x = X I dom X ran X
67 65 66 sseq12d x = X I dom X ran X I dom x ran x x I dom X I dom X ran X ran X I dom X ran X X I dom X ran X
68 ssun1 X X I dom X ran X
69 68 a1i X V X X I dom X ran X
70 dmexg X V dom X V
71 rnexg X V ran X V
72 unexg dom X V ran X V dom X ran X V
73 70 71 72 syl2anc X V dom X ran X V
74 73 resiexd X V I dom X ran X V
75 unexg X V I dom X ran X V X I dom X ran X V
76 74 75 mpdan X V X I dom X ran X V
77 dmun dom X I dom X ran X = dom X dom I dom X ran X
78 ssun1 dom X dom X ran X
79 dmresi dom I dom X ran X = dom X ran X
80 79 eqimssi dom I dom X ran X dom X ran X
81 78 80 unssi dom X dom I dom X ran X dom X ran X
82 77 81 eqsstri dom X I dom X ran X dom X ran X
83 rnun ran X I dom X ran X = ran X ran I dom X ran X
84 ssun2 ran X dom X ran X
85 rnresi ran I dom X ran X = dom X ran X
86 85 eqimssi ran I dom X ran X dom X ran X
87 84 86 unssi ran X ran I dom X ran X dom X ran X
88 83 87 eqsstri ran X I dom X ran X dom X ran X
89 82 88 pm3.2i dom X I dom X ran X dom X ran X ran X I dom X ran X dom X ran X
90 unss dom X I dom X ran X dom X ran X ran X I dom X ran X dom X ran X dom X I dom X ran X ran X I dom X ran X dom X ran X
91 ssres2 dom X I dom X ran X ran X I dom X ran X dom X ran X I dom X I dom X ran X ran X I dom X ran X I dom X ran X
92 90 91 sylbi dom X I dom X ran X dom X ran X ran X I dom X ran X dom X ran X I dom X I dom X ran X ran X I dom X ran X I dom X ran X
93 ssun4 I dom X I dom X ran X ran X I dom X ran X I dom X ran X I dom X I dom X ran X ran X I dom X ran X X I dom X ran X
94 89 92 93 mp2b I dom X I dom X ran X ran X I dom X ran X X I dom X ran X
95 94 a1i X V I dom X I dom X ran X ran X I dom X ran X X I dom X ran X
96 44 61 67 69 76 95 clcnvlem X V x | X x I dom x ran x x -1 = y | X -1 y I dom y ran y y