Metamath Proof Explorer

Theorem bropfvvvv

Description: If a binary relation holds for the result of an operation which is a function value, the involved classes are sets. (Contributed by AV, 31-Dec-2020) (Revised by AV, 16-Jan-2021)

Ref Expression
Hypotheses bropfvvvv.o 
|- O = ( a e. U |-> ( b e. V , c e. W |-> { <. d , e >. | ph } ) )
bropfvvvv.oo 
|- ( ( A e. U /\ B e. S /\ C e. T ) -> ( B ( O ` A ) C ) = { <. d , e >. | th } )
bropfvvvv.s 
|- ( a = A -> V = S )
bropfvvvv.t 
|- ( a = A -> W = T )
bropfvvvv.p 
|- ( a = A -> ( ph <-> ps ) )
Assertion bropfvvvv 
|- ( ( S e. X /\ T e. Y ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) )

Proof

Step Hyp Ref Expression
1 bropfvvvv.o 
 |-  O = ( a e. U |-> ( b e. V , c e. W |-> { <. d , e >. | ph } ) )
2 bropfvvvv.oo 
 |-  ( ( A e. U /\ B e. S /\ C e. T ) -> ( B ( O ` A ) C ) = { <. d , e >. | th } )
3 bropfvvvv.s 
 |-  ( a = A -> V = S )
4 bropfvvvv.t 
 |-  ( a = A -> W = T )
5 bropfvvvv.p 
 |-  ( a = A -> ( ph <-> ps ) )
6 brovpreldm 
 |-  ( D ( B ( O ` A ) C ) E -> <. B , C >. e. dom ( O ` A ) )
7 5 opabbidv 
 |-  ( a = A -> { <. d , e >. | ph } = { <. d , e >. | ps } )
8 3 4 7 mpoeq123dv 
 |-  ( a = A -> ( b e. V , c e. W |-> { <. d , e >. | ph } ) = ( b e. S , c e. T |-> { <. d , e >. | ps } ) )
9 8 1 fvmptg 
 |-  ( ( A e. U /\ ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V ) -> ( O ` A ) = ( b e. S , c e. T |-> { <. d , e >. | ps } ) )
10 9 dmeqd 
 |-  ( ( A e. U /\ ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V ) -> dom ( O ` A ) = dom ( b e. S , c e. T |-> { <. d , e >. | ps } ) )
11 10 eleq2d 
 |-  ( ( A e. U /\ ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V ) -> ( <. B , C >. e. dom ( O ` A ) <-> <. B , C >. e. dom ( b e. S , c e. T |-> { <. d , e >. | ps } ) ) )
12 dmoprabss 
 |-  dom { <. <. b , c >. , z >. | ( ( b e. S /\ c e. T ) /\ z = { <. d , e >. | ps } ) } C_ ( S X. T )
13 12 sseli 
 |-  ( <. B , C >. e. dom { <. <. b , c >. , z >. | ( ( b e. S /\ c e. T ) /\ z = { <. d , e >. | ps } ) } -> <. B , C >. e. ( S X. T ) )
14 1 2 bropfvvvvlem 
 |-  ( ( <. B , C >. e. ( S X. T ) /\ D ( B ( O ` A ) C ) E ) -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) )
15 14 ex 
 |-  ( <. B , C >. e. ( S X. T ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) )
16 13 15 syl 
 |-  ( <. B , C >. e. dom { <. <. b , c >. , z >. | ( ( b e. S /\ c e. T ) /\ z = { <. d , e >. | ps } ) } -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) )
17 df-mpo 
 |-  ( b e. S , c e. T |-> { <. d , e >. | ps } ) = { <. <. b , c >. , z >. | ( ( b e. S /\ c e. T ) /\ z = { <. d , e >. | ps } ) }
18 17 dmeqi 
 |-  dom ( b e. S , c e. T |-> { <. d , e >. | ps } ) = dom { <. <. b , c >. , z >. | ( ( b e. S /\ c e. T ) /\ z = { <. d , e >. | ps } ) }
19 16 18 eleq2s 
 |-  ( <. B , C >. e. dom ( b e. S , c e. T |-> { <. d , e >. | ps } ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) )
20 11 19 syl6bi 
 |-  ( ( A e. U /\ ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V ) -> ( <. B , C >. e. dom ( O ` A ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) ) )
21 20 com23 
 |-  ( ( A e. U /\ ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V ) -> ( D ( B ( O ` A ) C ) E -> ( <. B , C >. e. dom ( O ` A ) -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) ) )
22 21 a1d 
 |-  ( ( A e. U /\ ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V ) -> ( ( S e. X /\ T e. Y ) -> ( D ( B ( O ` A ) C ) E -> ( <. B , C >. e. dom ( O ` A ) -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) ) ) )
23 ianor 
 |-  ( -. ( A e. U /\ ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V ) <-> ( -. A e. U \/ -. ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V ) )
24 1 fvmptndm 
 |-  ( -. A e. U -> ( O ` A ) = (/) )
25 24 dmeqd 
 |-  ( -. A e. U -> dom ( O ` A ) = dom (/) )
26 25 eleq2d 
 |-  ( -. A e. U -> ( <. B , C >. e. dom ( O ` A ) <-> <. B , C >. e. dom (/) ) )
27 dm0 
 |-  dom (/) = (/)
28 27 eleq2i 
 |-  ( <. B , C >. e. dom (/) <-> <. B , C >. e. (/) )
29 26 28 bitrdi 
 |-  ( -. A e. U -> ( <. B , C >. e. dom ( O ` A ) <-> <. B , C >. e. (/) ) )
30 noel 
 |-  -. <. B , C >. e. (/)
31 30 pm2.21i 
 |-  ( <. B , C >. e. (/) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) )
32 29 31 syl6bi 
 |-  ( -. A e. U -> ( <. B , C >. e. dom ( O ` A ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) ) )
33 32 a1d 
 |-  ( -. A e. U -> ( ( S e. X /\ T e. Y ) -> ( <. B , C >. e. dom ( O ` A ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) ) ) )
34 notnotb 
 |-  ( A e. U <-> -. -. A e. U )
35 elex 
 |-  ( S e. X -> S e. _V )
36 elex 
 |-  ( T e. Y -> T e. _V )
37 35 36 anim12i 
 |-  ( ( S e. X /\ T e. Y ) -> ( S e. _V /\ T e. _V ) )
38 37 adantl 
 |-  ( ( A e. U /\ ( S e. X /\ T e. Y ) ) -> ( S e. _V /\ T e. _V ) )
39 mpoexga 
 |-  ( ( S e. _V /\ T e. _V ) -> ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V )
40 38 39 syl 
 |-  ( ( A e. U /\ ( S e. X /\ T e. Y ) ) -> ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V )
41 40 pm2.24d 
 |-  ( ( A e. U /\ ( S e. X /\ T e. Y ) ) -> ( -. ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V -> ( <. B , C >. e. dom ( O ` A ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) ) ) )
42 41 ex 
 |-  ( A e. U -> ( ( S e. X /\ T e. Y ) -> ( -. ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V -> ( <. B , C >. e. dom ( O ` A ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) ) ) ) )
43 42 com23 
 |-  ( A e. U -> ( -. ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V -> ( ( S e. X /\ T e. Y ) -> ( <. B , C >. e. dom ( O ` A ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) ) ) ) )
44 34 43 sylbir 
 |-  ( -. -. A e. U -> ( -. ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V -> ( ( S e. X /\ T e. Y ) -> ( <. B , C >. e. dom ( O ` A ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) ) ) ) )
45 44 imp 
 |-  ( ( -. -. A e. U /\ -. ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V ) -> ( ( S e. X /\ T e. Y ) -> ( <. B , C >. e. dom ( O ` A ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) ) ) )
46 33 45 jaoi3 
 |-  ( ( -. A e. U \/ -. ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V ) -> ( ( S e. X /\ T e. Y ) -> ( <. B , C >. e. dom ( O ` A ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) ) ) )
47 23 46 sylbi 
 |-  ( -. ( A e. U /\ ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V ) -> ( ( S e. X /\ T e. Y ) -> ( <. B , C >. e. dom ( O ` A ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) ) ) )
48 47 com34 
 |-  ( -. ( A e. U /\ ( b e. S , c e. T |-> { <. d , e >. | ps } ) e. _V ) -> ( ( S e. X /\ T e. Y ) -> ( D ( B ( O ` A ) C ) E -> ( <. B , C >. e. dom ( O ` A ) -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) ) ) )
49 22 48 pm2.61i 
 |-  ( ( S e. X /\ T e. Y ) -> ( D ( B ( O ` A ) C ) E -> ( <. B , C >. e. dom ( O ` A ) -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) ) )
50 6 49 mpdi 
 |-  ( ( S e. X /\ T e. Y ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) )