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 e. _V , b e. _V |-> ( r e. ~P ( a X. b ) |-> ( x e. a |-> { y e. b | x r y } ) ) )
rfovd.a 
|- ( ph -> A e. V )
rfovd.b 
|- ( ph -> B e. W )
rfovcnvf1od.f 
|- F = ( A O B )
Assertion rfovcnvf1od 
|- ( ph -> ( F : ~P ( A X. B ) -1-1-onto-> ( ~P B ^m A ) /\ `' F = ( f e. ( ~P B ^m A ) |-> { <. x , y >. | ( x e. A /\ y e. ( f ` x ) ) } ) ) )

Proof

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