Metamath Proof Explorer


Theorem fsovrfovd

Description: The operator which gives a 1-to-1 a mapping to a subset and a reverse mapping from elements can be composed from the operator which gives a 1-to-1 mapping between relations and functions to subsets and the converse operator. (Contributed by RP, 15-May-2021)

Ref Expression
Hypotheses fsovd.fs O = a V , b V f 𝒫 b a y b x a | y f x
fsovd.a φ A V
fsovd.b φ B W
fsovd.rf R = a V , b V r 𝒫 a × b u a v b | u r v
fsovd.cnv C = a V , b V s 𝒫 a × b s -1
Assertion fsovrfovd φ A O B = B R A A C B A R B -1

Proof

Step Hyp Ref Expression
1 fsovd.fs O = a V , b V f 𝒫 b a y b x a | y f x
2 fsovd.a φ A V
3 fsovd.b φ B W
4 fsovd.rf R = a V , b V r 𝒫 a × b u a v b | u r v
5 fsovd.cnv C = a V , b V s 𝒫 a × b s -1
6 3 2 xpexd φ B × A V
7 6 adantr φ f 𝒫 B A B × A V
8 elmapi f 𝒫 B A f : A 𝒫 B
9 8 ffvelrnda f 𝒫 B A u A f u 𝒫 B
10 9 elpwid f 𝒫 B A u A f u B
11 10 sseld f 𝒫 B A u A v f u v B
12 11 impancom f 𝒫 B A v f u u A v B
13 12 pm4.71d f 𝒫 B A v f u u A u A v B
14 13 ex f 𝒫 B A v f u u A u A v B
15 14 pm5.32rd f 𝒫 B A u A v f u u A v B v f u
16 ancom u A v B v B u A
17 16 anbi1i u A v B v f u v B u A v f u
18 15 17 bitrdi f 𝒫 B A u A v f u v B u A v f u
19 18 opabbidv f 𝒫 B A v u | u A v f u = v u | v B u A v f u
20 opabssxp v u | v B u A v f u B × A
21 19 20 eqsstrdi f 𝒫 B A v u | u A v f u B × A
22 21 adantl φ f 𝒫 B A v u | u A v f u B × A
23 7 22 sselpwd φ f 𝒫 B A v u | u A v f u 𝒫 B × A
24 eqidd φ f 𝒫 B A v u | u A v f u = f 𝒫 B A v u | u A v f u
25 4 3 2 rfovd φ B R A = r 𝒫 B × A u B v A | u r v
26 breq r = t u r v u t v
27 26 rabbidv r = t v A | u r v = v A | u t v
28 27 mpteq2dv r = t u B v A | u r v = u B v A | u t v
29 breq1 u = c u t v c t v
30 29 rabbidv u = c v A | u t v = v A | c t v
31 breq2 v = d c t v c t d
32 31 cbvrabv v A | c t v = d A | c t d
33 30 32 eqtrdi u = c v A | u t v = d A | c t d
34 33 cbvmptv u B v A | u t v = c B d A | c t d
35 28 34 eqtrdi r = t u B v A | u r v = c B d A | c t d
36 35 cbvmptv r 𝒫 B × A u B v A | u r v = t 𝒫 B × A c B d A | c t d
37 25 36 eqtrdi φ B R A = t 𝒫 B × A c B d A | c t d
38 breq t = v u | u A v f u c t d c v u | u A v f u d
39 df-br c v u | u A v f u d c d v u | u A v f u
40 vex c V
41 vex d V
42 eleq1w v = c v f u c f u
43 42 anbi2d v = c u A v f u u A c f u
44 eleq1w u = d u A d A
45 fveq2 u = d f u = f d
46 45 eleq2d u = d c f u c f d
47 44 46 anbi12d u = d u A c f u d A c f d
48 40 41 43 47 opelopab c d v u | u A v f u d A c f d
49 39 48 bitri c v u | u A v f u d d A c f d
50 38 49 bitrdi t = v u | u A v f u c t d d A c f d
51 50 rabbidv t = v u | u A v f u d A | c t d = d A | d A c f d
52 51 mpteq2dv t = v u | u A v f u c B d A | c t d = c B d A | d A c f d
53 ibar d A c f d d A c f d
54 53 bicomd d A d A c f d c f d
55 54 rabbiia d A | d A c f d = d A | c f d
56 fveq2 d = x f d = f x
57 56 eleq2d d = x c f d c f x
58 57 cbvrabv d A | c f d = x A | c f x
59 55 58 eqtri d A | d A c f d = x A | c f x
60 59 mpteq2i c B d A | d A c f d = c B x A | c f x
61 eleq1w c = y c f x y f x
62 61 rabbidv c = y x A | c f x = x A | y f x
63 62 cbvmptv c B x A | c f x = y B x A | y f x
64 60 63 eqtri c B d A | d A c f d = y B x A | y f x
65 52 64 eqtrdi t = v u | u A v f u c B d A | c t d = y B x A | y f x
66 23 24 37 65 fmptco φ B R A f 𝒫 B A v u | u A v f u = f 𝒫 B A y B x A | y f x
67 2 3 xpexd φ A × B V
68 67 adantr φ f 𝒫 B A A × B V
69 15 opabbidv f 𝒫 B A u v | u A v f u = u v | u A v B v f u
70 opabssxp u v | u A v B v f u A × B
71 69 70 eqsstrdi f 𝒫 B A u v | u A v f u A × B
72 71 adantl φ f 𝒫 B A u v | u A v f u A × B
73 68 72 sselpwd φ f 𝒫 B A u v | u A v f u 𝒫 A × B
74 eqid A R B = A R B
75 4 2 3 74 rfovcnvd φ A R B -1 = f 𝒫 B A u v | u A v f u
76 5 a1i φ C = a V , b V s 𝒫 a × b s -1
77 xpeq12 a = A b = B a × b = A × B
78 77 pweqd a = A b = B 𝒫 a × b = 𝒫 A × B
79 78 mpteq1d a = A b = B s 𝒫 a × b s -1 = s 𝒫 A × B s -1
80 79 adantl φ a = A b = B s 𝒫 a × b s -1 = s 𝒫 A × B s -1
81 2 elexd φ A V
82 3 elexd φ B V
83 pwexg A × B V 𝒫 A × B V
84 mptexg 𝒫 A × B V s 𝒫 A × B s -1 V
85 67 83 84 3syl φ s 𝒫 A × B s -1 V
86 76 80 81 82 85 ovmpod φ A C B = s 𝒫 A × B s -1
87 cnveq s = u v | u A v f u s -1 = u v | u A v f u -1
88 cnvopab u v | u A v f u -1 = v u | u A v f u
89 87 88 eqtrdi s = u v | u A v f u s -1 = v u | u A v f u
90 73 75 86 89 fmptco φ A C B A R B -1 = f 𝒫 B A v u | u A v f u
91 90 coeq2d φ B R A A C B A R B -1 = B R A f 𝒫 B A v u | u A v f u
92 1 2 3 fsovd φ A O B = f 𝒫 B A y B x A | y f x
93 66 91 92 3eqtr4rd φ A O B = B R A A C B A R B -1