Metamath Proof Explorer


Theorem rfovcnvf1od

Description: Properties of the operator, ( A O B ) , which maps between relations and functions for relations between base sets, A and B . (Contributed by RP, 27-Apr-2021)

Ref Expression
Hypotheses rfovd.rf O = a V , b V r 𝒫 a × b x a y b | x r y
rfovd.a φ A V
rfovd.b φ B W
rfovcnvf1od.f F = A O B
Assertion rfovcnvf1od φ F : 𝒫 A × B 1-1 onto 𝒫 B A F -1 = f 𝒫 B A x y | x A y f x

Proof

Step Hyp Ref Expression
1 rfovd.rf O = a V , b V r 𝒫 a × b x a y b | x r y
2 rfovd.a φ A V
3 rfovd.b φ B W
4 rfovcnvf1od.f F = A O B
5 eqid r 𝒫 A × B x A y B | x r y = r 𝒫 A × B x A y B | x r y
6 ssrab2 y B | x r y B
7 6 a1i φ y B | x r y B
8 3 7 sselpwd φ y B | x r y 𝒫 B
9 8 adantr φ x A y B | x r y 𝒫 B
10 9 fmpttd φ x A y B | x r y : A 𝒫 B
11 3 pwexd φ 𝒫 B V
12 11 2 elmapd φ x A y B | x r y 𝒫 B A x A y B | x r y : A 𝒫 B
13 10 12 mpbird φ x A y B | x r y 𝒫 B A
14 13 adantr φ r 𝒫 A × B x A y B | x r y 𝒫 B A
15 2 3 xpexd φ A × B V
16 15 adantr φ f 𝒫 B A A × B V
17 11 2 elmapd φ f 𝒫 B A f : A 𝒫 B
18 17 biimpa φ f 𝒫 B A f : A 𝒫 B
19 18 ffvelrnda φ f 𝒫 B A x A f x 𝒫 B
20 19 ex φ f 𝒫 B A x A f x 𝒫 B
21 elpwi f x 𝒫 B f x B
22 21 sseld f x 𝒫 B y f x y B
23 20 22 syl6 φ f 𝒫 B A x A y f x y B
24 23 imdistand φ f 𝒫 B A x A y f x x A y B
25 trud x A y f x
26 24 25 jca2 φ f 𝒫 B A x A y f x x A y B
27 26 ssopab2dv φ f 𝒫 B A x y | x A y f x x y | x A y B
28 opabssxp x y | x A y B A × B
29 27 28 sstrdi φ f 𝒫 B A x y | x A y f x A × B
30 16 29 sselpwd φ f 𝒫 B A x y | x A y f x 𝒫 A × B
31 simplrr φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x f 𝒫 B A
32 elmapfn f 𝒫 B A f Fn A
33 31 32 syl φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x f Fn A
34 3 ad2antrr φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x B W
35 rabexg B W y B | x r y V
36 35 ralrimivw B W x A y B | x r y V
37 nfcv _ x A
38 37 fnmptf x A y B | x r y V x A y B | x r y Fn A
39 34 36 38 3syl φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x x A y B | x r y Fn A
40 dfin5 B f u = b B | b f u
41 simpllr φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A r 𝒫 A × B f 𝒫 B A
42 elmapi f 𝒫 B A f : A 𝒫 B
43 41 42 simpl2im φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A f : A 𝒫 B
44 simpr φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A u A
45 43 44 ffvelrnd φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A f u 𝒫 B
46 45 elpwid φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A f u B
47 sseqin2 f u B B f u = f u
48 46 47 sylib φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A B f u = f u
49 ibar u A b f u u A b f u
50 49 rabbidv u A b B | b f u = b B | u A b f u
51 50 adantl φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A b B | b f u = b B | u A b f u
52 40 48 51 3eqtr3a φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A f u = b B | u A b f u
53 breq2 y = b x r y x r b
54 53 cbvrabv y B | x r y = b B | x r b
55 breq1 x = a x r b a r b
56 df-br a r b a b r
57 55 56 bitrdi x = a x r b a b r
58 57 rabbidv x = a b B | x r b = b B | a b r
59 54 58 syl5eq x = a y B | x r y = b B | a b r
60 59 cbvmptv x A y B | x r y = a A b B | a b r
61 simpr φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A a = u a = u
62 61 opeq1d φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A a = u a b = u b
63 simpllr φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A a = u r = x y | x A y f x
64 62 63 eleq12d φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A a = u a b r u b x y | x A y f x
65 vex u V
66 vex b V
67 simpl x = u y = b x = u
68 67 eleq1d x = u y = b x A u A
69 simpr x = u y = b y = b
70 67 fveq2d x = u y = b f x = f u
71 69 70 eleq12d x = u y = b y f x b f u
72 68 71 anbi12d x = u y = b x A y f x u A b f u
73 65 66 72 opelopaba u b x y | x A y f x u A b f u
74 64 73 bitrdi φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A a = u a b r u A b f u
75 74 rabbidv φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A a = u b B | a b r = b B | u A b f u
76 3 ad3antrrr φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A B W
77 rabexg B W b B | u A b f u V
78 76 77 syl φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A b B | u A b f u V
79 60 75 44 78 fvmptd2 φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A x A y B | x r y u = b B | u A b f u
80 52 79 eqtr4d φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x u A f u = x A y B | x r y u
81 33 39 80 eqfnfvd φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x f = x A y B | x r y
82 simplrl φ r 𝒫 A × B f 𝒫 B A f = x A y B | x r y r 𝒫 A × B
83 82 elpwid φ r 𝒫 A × B f 𝒫 B A f = x A y B | x r y r A × B
84 xpss A × B V × V
85 83 84 sstrdi φ r 𝒫 A × B f 𝒫 B A f = x A y B | x r y r V × V
86 df-rel Rel r r V × V
87 85 86 sylibr φ r 𝒫 A × B f 𝒫 B A f = x A y B | x r y Rel r
88 relopabv Rel x y | x A y f x
89 88 a1i φ r 𝒫 A × B f 𝒫 B A f = x A y B | x r y Rel x y | x A y f x
90 simpl r 𝒫 A × B f 𝒫 B A r 𝒫 A × B
91 3 90 anim12i φ r 𝒫 A × B f 𝒫 B A B W r 𝒫 A × B
92 91 anim1i φ r 𝒫 A × B f 𝒫 B A f = x A y B | x r y B W r 𝒫 A × B f = x A y B | x r y
93 vex v V
94 simpl x = u y = v x = u
95 94 eleq1d x = u y = v x A u A
96 simpr x = u y = v y = v
97 94 fveq2d x = u y = v f x = f u
98 96 97 eleq12d x = u y = v y f x v f u
99 95 98 anbi12d x = u y = v x A y f x u A v f u
100 65 93 99 opelopaba u v x y | x A y f x u A v f u
101 breq2 b = v u r b u r v
102 df-br u r v u v r
103 101 102 bitrdi b = v u r b u v r
104 103 elrab v b B | u r b v B u v r
105 104 anbi2i u A v b B | u r b u A v B u v r
106 105 a1i B W r 𝒫 A × B f = x A y B | x r y u A v b B | u r b u A v B u v r
107 simplr B W r 𝒫 A × B f = x A y B | x r y u A f = x A y B | x r y
108 breq1 x = a x r y a r y
109 108 rabbidv x = a y B | x r y = y B | a r y
110 breq2 y = b a r y a r b
111 110 cbvrabv y B | a r y = b B | a r b
112 109 111 eqtrdi x = a y B | x r y = b B | a r b
113 112 cbvmptv x A y B | x r y = a A b B | a r b
114 107 113 eqtrdi B W r 𝒫 A × B f = x A y B | x r y u A f = a A b B | a r b
115 breq1 a = u a r b u r b
116 115 rabbidv a = u b B | a r b = b B | u r b
117 116 adantl B W r 𝒫 A × B f = x A y B | x r y u A a = u b B | a r b = b B | u r b
118 simpr B W r 𝒫 A × B f = x A y B | x r y u A u A
119 rabexg B W b B | u r b V
120 119 ad3antrrr B W r 𝒫 A × B f = x A y B | x r y u A b B | u r b V
121 114 117 118 120 fvmptd B W r 𝒫 A × B f = x A y B | x r y u A f u = b B | u r b
122 121 eleq2d B W r 𝒫 A × B f = x A y B | x r y u A v f u v b B | u r b
123 122 pm5.32da B W r 𝒫 A × B f = x A y B | x r y u A v f u u A v b B | u r b
124 simplr B W r 𝒫 A × B f = x A y B | x r y r 𝒫 A × B
125 124 elpwid B W r 𝒫 A × B f = x A y B | x r y r A × B
126 65 93 opeldm u v r u dom r
127 dmss r A × B dom r dom A × B
128 dmxpss dom A × B A
129 127 128 sstrdi r A × B dom r A
130 129 sseld r A × B u dom r u A
131 126 130 syl5 r A × B u v r u A
132 131 pm4.71rd r A × B u v r u A u v r
133 65 93 opelrn u v r v ran r
134 rnss r A × B ran r ran A × B
135 rnxpss ran A × B B
136 134 135 sstrdi r A × B ran r B
137 136 sseld r A × B v ran r v B
138 133 137 syl5 r A × B u v r v B
139 138 pm4.71rd r A × B u v r v B u v r
140 139 anbi2d r A × B u A u v r u A v B u v r
141 132 140 bitrd r A × B u v r u A v B u v r
142 125 141 syl B W r 𝒫 A × B f = x A y B | x r y u v r u A v B u v r
143 106 123 142 3bitr4d B W r 𝒫 A × B f = x A y B | x r y u A v f u u v r
144 100 143 bitr2id B W r 𝒫 A × B f = x A y B | x r y u v r u v x y | x A y f x
145 144 eqrelrdv2 Rel r Rel x y | x A y f x B W r 𝒫 A × B f = x A y B | x r y r = x y | x A y f x
146 87 89 92 145 syl21anc φ r 𝒫 A × B f 𝒫 B A f = x A y B | x r y r = x y | x A y f x
147 81 146 impbida φ r 𝒫 A × B f 𝒫 B A r = x y | x A y f x f = x A y B | x r y
148 5 14 30 147 f1ocnv2d φ r 𝒫 A × B x A y B | x r y : 𝒫 A × B 1-1 onto 𝒫 B A r 𝒫 A × B x A y B | x r y -1 = f 𝒫 B A x y | x A y f x
149 1 2 3 rfovd φ A O B = r 𝒫 A × B x A y B | x r y
150 4 149 syl5eq φ F = r 𝒫 A × B x A y B | x r y
151 f1oeq1 F = r 𝒫 A × B x A y B | x r y F : 𝒫 A × B 1-1 onto 𝒫 B A r 𝒫 A × B x A y B | x r y : 𝒫 A × B 1-1 onto 𝒫 B A
152 cnveq F = r 𝒫 A × B x A y B | x r y F -1 = r 𝒫 A × B x A y B | x r y -1
153 152 eqeq1d F = r 𝒫 A × B x A y B | x r y F -1 = f 𝒫 B A x y | x A y f x r 𝒫 A × B x A y B | x r y -1 = f 𝒫 B A x y | x A y f x
154 151 153 anbi12d F = r 𝒫 A × B x A y B | x r y F : 𝒫 A × B 1-1 onto 𝒫 B A F -1 = f 𝒫 B A x y | x A y f x r 𝒫 A × B x A y B | x r y : 𝒫 A × B 1-1 onto 𝒫 B A r 𝒫 A × B x A y B | x r y -1 = f 𝒫 B A x y | x A y f x
155 150 154 syl φ F : 𝒫 A × B 1-1 onto 𝒫 B A F -1 = f 𝒫 B A x y | x A y f x r 𝒫 A × B x A y B | x r y : 𝒫 A × B 1-1 onto 𝒫 B A r 𝒫 A × B x A y B | x r y -1 = f 𝒫 B A x y | x A y f x
156 148 155 mpbird φ F : 𝒫 A × B 1-1 onto 𝒫 B A F -1 = f 𝒫 B A x y | x A y f x