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 e. _V , b e. _V |-> ( f e. ( ~P b ^m a ) |-> ( y e. b |-> { x e. a | y e. ( f ` x ) } ) ) )
fsovd.a 
|- ( ph -> A e. V )
fsovd.b 
|- ( ph -> B e. W )
fsovd.rf 
|- R = ( a e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> ( u e. a |-> { v e. b | u r v } ) ) )
fsovd.cnv 
|- C = ( a e. _V , b e. _V |-> ( s e. ~P ( a X. b ) |-> `' s ) )
Assertion fsovrfovd 
|- ( ph -> ( A O B ) = ( ( B R A ) o. ( ( A C B ) o. `' ( A R B ) ) ) )

Proof

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