Metamath Proof Explorer


Theorem fsovcnvlem

Description: The O operator, which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, gives a family of functions that include their own inverse. (Contributed by RP, 27-Apr-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
fsovfvd.g G = A O B
fsovcnvlem.h H = B O A
Assertion fsovcnvlem φ H G = I 𝒫 B A

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 fsovfvd.g G = A O B
5 fsovcnvlem.h H = B O A
6 ssrab2 x A | y f x A
7 6 a1i φ x A | y f x A
8 2 7 sselpwd φ x A | y f x 𝒫 A
9 8 adantr φ y B x A | y f x 𝒫 A
10 9 fmpttd φ y B x A | y f x : B 𝒫 A
11 2 pwexd φ 𝒫 A V
12 11 3 elmapd φ y B x A | y f x 𝒫 A B y B x A | y f x : B 𝒫 A
13 10 12 mpbird φ y B x A | y f x 𝒫 A B
14 13 adantr φ f 𝒫 B A y B x A | y f x 𝒫 A B
15 1 2 3 fsovd φ A O B = f 𝒫 B A y B x A | y f x
16 4 15 syl5eq φ G = f 𝒫 B A y B x A | y f x
17 oveq2 a = d 𝒫 b a = 𝒫 b d
18 rabeq a = d x a | y f x = x d | y f x
19 18 mpteq2dv a = d y b x a | y f x = y b x d | y f x
20 17 19 mpteq12dv a = d f 𝒫 b a y b x a | y f x = f 𝒫 b d y b x d | y f x
21 pweq b = c 𝒫 b = 𝒫 c
22 21 oveq1d b = c 𝒫 b d = 𝒫 c d
23 mpteq1 b = c y b x d | y f x = y c x d | y f x
24 22 23 mpteq12dv b = c f 𝒫 b d y b x d | y f x = f 𝒫 c d y c x d | y f x
25 20 24 cbvmpov a V , b V f 𝒫 b a y b x a | y f x = d V , c V f 𝒫 c d y c x d | y f x
26 eqid V = V
27 fveq1 f = g f x = g x
28 27 eleq2d f = g y f x y g x
29 28 rabbidv f = g x d | y f x = x d | y g x
30 29 mpteq2dv f = g y c x d | y f x = y c x d | y g x
31 30 cbvmptv f 𝒫 c d y c x d | y f x = g 𝒫 c d y c x d | y g x
32 eleq1w y = u y g x u g x
33 32 rabbidv y = u x d | y g x = x d | u g x
34 33 cbvmptv y c x d | y g x = u c x d | u g x
35 fveq2 x = v g x = g v
36 35 eleq2d x = v u g x u g v
37 36 cbvrabv x d | u g x = v d | u g v
38 37 mpteq2i u c x d | u g x = u c v d | u g v
39 34 38 eqtri y c x d | y g x = u c v d | u g v
40 39 mpteq2i g 𝒫 c d y c x d | y g x = g 𝒫 c d u c v d | u g v
41 31 40 eqtri f 𝒫 c d y c x d | y f x = g 𝒫 c d u c v d | u g v
42 26 26 41 mpoeq123i d V , c V f 𝒫 c d y c x d | y f x = d V , c V g 𝒫 c d u c v d | u g v
43 1 25 42 3eqtri O = d V , c V g 𝒫 c d u c v d | u g v
44 43 3 2 fsovd φ B O A = g 𝒫 A B u A v B | u g v
45 5 44 syl5eq φ H = g 𝒫 A B u A v B | u g v
46 fveq1 g = y B x A | y f x g v = y B x A | y f x v
47 46 eleq2d g = y B x A | y f x u g v u y B x A | y f x v
48 47 rabbidv g = y B x A | y f x v B | u g v = v B | u y B x A | y f x v
49 48 mpteq2dv g = y B x A | y f x u A v B | u g v = u A v B | u y B x A | y f x v
50 14 16 45 49 fmptco φ H G = f 𝒫 B A u A v B | u y B x A | y f x v
51 eqidd φ u A v B y B x A | y f x = y B x A | y f x
52 eleq1w y = v y f x v f x
53 52 rabbidv y = v x A | y f x = x A | v f x
54 53 adantl φ u A v B y = v x A | y f x = x A | v f x
55 simpr φ u A v B v B
56 rabexg A V x A | v f x V
57 2 56 syl φ x A | v f x V
58 57 ad2antrr φ u A v B x A | v f x V
59 51 54 55 58 fvmptd φ u A v B y B x A | y f x v = x A | v f x
60 59 eleq2d φ u A v B u y B x A | y f x v u x A | v f x
61 fveq2 x = u f x = f u
62 61 eleq2d x = u v f x v f u
63 62 elrab3 u A u x A | v f x v f u
64 63 ad2antlr φ u A v B u x A | v f x v f u
65 60 64 bitrd φ u A v B u y B x A | y f x v v f u
66 65 rabbidva φ u A v B | u y B x A | y f x v = v B | v f u
67 66 adantlr φ f 𝒫 B A u A v B | u y B x A | y f x v = v B | v f u
68 elmapi f 𝒫 B A f : A 𝒫 B
69 68 ad2antlr φ f 𝒫 B A u A f : A 𝒫 B
70 simpr φ f 𝒫 B A u A u A
71 69 70 ffvelrnd φ f 𝒫 B A u A f u 𝒫 B
72 71 elpwid φ f 𝒫 B A u A f u B
73 sseqin2 f u B B f u = f u
74 72 73 sylib φ f 𝒫 B A u A B f u = f u
75 dfin5 B f u = v B | v f u
76 74 75 eqtr3di φ f 𝒫 B A u A f u = v B | v f u
77 67 76 eqtr4d φ f 𝒫 B A u A v B | u y B x A | y f x v = f u
78 77 mpteq2dva φ f 𝒫 B A u A v B | u y B x A | y f x v = u A f u
79 68 feqmptd f 𝒫 B A f = u A f u
80 79 adantl φ f 𝒫 B A f = u A f u
81 78 80 eqtr4d φ f 𝒫 B A u A v B | u y B x A | y f x v = f
82 81 mpteq2dva φ f 𝒫 B A u A v B | u y B x A | y f x v = f 𝒫 B A f
83 mptresid I 𝒫 B A = f 𝒫 B A f
84 83 eqcomi f 𝒫 B A f = I 𝒫 B A
85 84 a1i φ f 𝒫 B A f = I 𝒫 B A
86 50 82 85 3eqtrd φ H G = I 𝒫 B A