This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bropfvvvvlem

Description: Lemma for bropfvvvv . (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 } )
Assertion 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 ) ) )

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 opelxp 
 |-  ( <. B , C >. e. ( S X. T ) <-> ( B e. S /\ C e. T ) )
4 brne0 
 |-  ( D ( B ( O ` A ) C ) E -> ( B ( O ` A ) C ) =/= (/) )
5 2 3expb 
 |-  ( ( A e. U /\ ( B e. S /\ C e. T ) ) -> ( B ( O ` A ) C ) = { <. d , e >. | th } )
6 5 breqd 
 |-  ( ( A e. U /\ ( B e. S /\ C e. T ) ) -> ( D ( B ( O ` A ) C ) E <-> D { <. d , e >. | th } E ) )
7 brabv 
 |-  ( D { <. d , e >. | th } E -> ( D e. _V /\ E e. _V ) )
8 7 anim2i 
 |-  ( ( A e. U /\ D { <. d , e >. | th } E ) -> ( A e. U /\ ( D e. _V /\ E e. _V ) ) )
9 8 ex 
 |-  ( A e. U -> ( D { <. d , e >. | th } E -> ( A e. U /\ ( D e. _V /\ E e. _V ) ) ) )
10 9 adantr 
 |-  ( ( A e. U /\ ( B e. S /\ C e. T ) ) -> ( D { <. d , e >. | th } E -> ( A e. U /\ ( D e. _V /\ E e. _V ) ) ) )
11 6 10 sylbid 
 |-  ( ( A e. U /\ ( B e. S /\ C e. T ) ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( D e. _V /\ E e. _V ) ) ) )
12 11 ex 
 |-  ( A e. U -> ( ( B e. S /\ C e. T ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( D e. _V /\ E e. _V ) ) ) ) )
13 12 com23 
 |-  ( A e. U -> ( D ( B ( O ` A ) C ) E -> ( ( B e. S /\ C e. T ) -> ( A e. U /\ ( D e. _V /\ E e. _V ) ) ) ) )
14 13 a1d 
 |-  ( A e. U -> ( ( B ( O ` A ) C ) =/= (/) -> ( D ( B ( O ` A ) C ) E -> ( ( B e. S /\ C e. T ) -> ( A e. U /\ ( D e. _V /\ E e. _V ) ) ) ) ) )
15 1 fvmptndm 
 |-  ( -. A e. U -> ( O ` A ) = (/) )
16 df-ov 
 |-  ( B ( O ` A ) C ) = ( ( O ` A ) ` <. B , C >. )
17 fveq1 
 |-  ( ( O ` A ) = (/) -> ( ( O ` A ) ` <. B , C >. ) = ( (/) ` <. B , C >. ) )
18 16 17 eqtrid 
 |-  ( ( O ` A ) = (/) -> ( B ( O ` A ) C ) = ( (/) ` <. B , C >. ) )
19 0fv 
 |-  ( (/) ` <. B , C >. ) = (/)
20 18 19 eqtrdi 
 |-  ( ( O ` A ) = (/) -> ( B ( O ` A ) C ) = (/) )
21 eqneqall 
 |-  ( ( B ( O ` A ) C ) = (/) -> ( ( B ( O ` A ) C ) =/= (/) -> ( D ( B ( O ` A ) C ) E -> ( ( B e. S /\ C e. T ) -> ( A e. U /\ ( D e. _V /\ E e. _V ) ) ) ) ) )
22 15 20 21 3syl 
 |-  ( -. A e. U -> ( ( B ( O ` A ) C ) =/= (/) -> ( D ( B ( O ` A ) C ) E -> ( ( B e. S /\ C e. T ) -> ( A e. U /\ ( D e. _V /\ E e. _V ) ) ) ) ) )
23 14 22 pm2.61i 
 |-  ( ( B ( O ` A ) C ) =/= (/) -> ( D ( B ( O ` A ) C ) E -> ( ( B e. S /\ C e. T ) -> ( A e. U /\ ( D e. _V /\ E e. _V ) ) ) ) )
24 4 23 mpcom 
 |-  ( D ( B ( O ` A ) C ) E -> ( ( B e. S /\ C e. T ) -> ( A e. U /\ ( D e. _V /\ E e. _V ) ) ) )
25 24 com12 
 |-  ( ( B e. S /\ C e. T ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( D e. _V /\ E e. _V ) ) ) )
26 25 anc2ri 
 |-  ( ( B e. S /\ C e. T ) -> ( D ( B ( O ` A ) C ) E -> ( ( A e. U /\ ( D e. _V /\ E e. _V ) ) /\ ( B e. S /\ C e. T ) ) ) )
27 3anan32 
 |-  ( ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) <-> ( ( A e. U /\ ( D e. _V /\ E e. _V ) ) /\ ( B e. S /\ C e. T ) ) )
28 26 27 imbitrrdi 
 |-  ( ( B e. S /\ C e. T ) -> ( D ( B ( O ` A ) C ) E -> ( A e. U /\ ( B e. S /\ C e. T ) /\ ( D e. _V /\ E e. _V ) ) ) )
29 3 28 sylbi 
 |-  ( <. 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 ) ) ) )
30 29 imp 
 |-  ( ( <. 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 ) ) )