Metamath Proof Explorer

Theorem supmullem2

Description: Lemma for supmul . (Contributed by Mario Carneiro, 5-Jul-2013)

Ref Expression
Hypotheses supmul.1 
|- C = { z | E. v e. A E. b e. B z = ( v x. b ) }
supmul.2 
|- ( ph <-> ( ( A. x e. A 0 <_ x /\ A. x e. B 0 <_ x ) /\ ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) )
Assertion supmullem2 
|- ( ph -> ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) )

Proof

Step Hyp Ref Expression
1 supmul.1 
 |-  C = { z | E. v e. A E. b e. B z = ( v x. b ) }
2 supmul.2 
 |-  ( ph <-> ( ( A. x e. A 0 <_ x /\ A. x e. B 0 <_ x ) /\ ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) )
3 vex 
 |-  w e. _V
4 oveq1 
 |-  ( v = a -> ( v x. b ) = ( a x. b ) )
5 4 eqeq2d 
 |-  ( v = a -> ( z = ( v x. b ) <-> z = ( a x. b ) ) )
6 5 rexbidv 
 |-  ( v = a -> ( E. b e. B z = ( v x. b ) <-> E. b e. B z = ( a x. b ) ) )
7 6 cbvrexvw 
 |-  ( E. v e. A E. b e. B z = ( v x. b ) <-> E. a e. A E. b e. B z = ( a x. b ) )
8 eqeq1 
 |-  ( z = w -> ( z = ( a x. b ) <-> w = ( a x. b ) ) )
9 8 2rexbidv 
 |-  ( z = w -> ( E. a e. A E. b e. B z = ( a x. b ) <-> E. a e. A E. b e. B w = ( a x. b ) ) )
10 7 9 syl5bb 
 |-  ( z = w -> ( E. v e. A E. b e. B z = ( v x. b ) <-> E. a e. A E. b e. B w = ( a x. b ) ) )
11 3 10 1 elab2 
 |-  ( w e. C <-> E. a e. A E. b e. B w = ( a x. b ) )
12 2 simp2bi 
 |-  ( ph -> ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) )
13 12 simp1d 
 |-  ( ph -> A C_ RR )
14 13 sseld 
 |-  ( ph -> ( a e. A -> a e. RR ) )
15 2 simp3bi 
 |-  ( ph -> ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) )
16 15 simp1d 
 |-  ( ph -> B C_ RR )
17 16 sseld 
 |-  ( ph -> ( b e. B -> b e. RR ) )
18 14 17 anim12d 
 |-  ( ph -> ( ( a e. A /\ b e. B ) -> ( a e. RR /\ b e. RR ) ) )
19 remulcl 
 |-  ( ( a e. RR /\ b e. RR ) -> ( a x. b ) e. RR )
20 18 19 syl6 
 |-  ( ph -> ( ( a e. A /\ b e. B ) -> ( a x. b ) e. RR ) )
21 eleq1a 
 |-  ( ( a x. b ) e. RR -> ( w = ( a x. b ) -> w e. RR ) )
22 20 21 syl6 
 |-  ( ph -> ( ( a e. A /\ b e. B ) -> ( w = ( a x. b ) -> w e. RR ) ) )
23 22 rexlimdvv 
 |-  ( ph -> ( E. a e. A E. b e. B w = ( a x. b ) -> w e. RR ) )
24 11 23 syl5bi 
 |-  ( ph -> ( w e. C -> w e. RR ) )
25 24 ssrdv 
 |-  ( ph -> C C_ RR )
26 12 simp2d 
 |-  ( ph -> A =/= (/) )
27 15 simp2d 
 |-  ( ph -> B =/= (/) )
28 ovex 
 |-  ( a x. b ) e. _V
29 28 isseti 
 |-  E. w w = ( a x. b )
30 29 rgenw 
 |-  A. b e. B E. w w = ( a x. b )
31 r19.2z 
 |-  ( ( B =/= (/) /\ A. b e. B E. w w = ( a x. b ) ) -> E. b e. B E. w w = ( a x. b ) )
32 27 30 31 sylancl 
 |-  ( ph -> E. b e. B E. w w = ( a x. b ) )
33 rexcom4 
 |-  ( E. b e. B E. w w = ( a x. b ) <-> E. w E. b e. B w = ( a x. b ) )
34 32 33 sylib 
 |-  ( ph -> E. w E. b e. B w = ( a x. b ) )
35 34 ralrimivw 
 |-  ( ph -> A. a e. A E. w E. b e. B w = ( a x. b ) )
36 r19.2z 
 |-  ( ( A =/= (/) /\ A. a e. A E. w E. b e. B w = ( a x. b ) ) -> E. a e. A E. w E. b e. B w = ( a x. b ) )
37 26 35 36 syl2anc 
 |-  ( ph -> E. a e. A E. w E. b e. B w = ( a x. b ) )
38 rexcom4 
 |-  ( E. a e. A E. w E. b e. B w = ( a x. b ) <-> E. w E. a e. A E. b e. B w = ( a x. b ) )
39 37 38 sylib 
 |-  ( ph -> E. w E. a e. A E. b e. B w = ( a x. b ) )
40 n0 
 |-  ( C =/= (/) <-> E. w w e. C )
41 11 exbii 
 |-  ( E. w w e. C <-> E. w E. a e. A E. b e. B w = ( a x. b ) )
42 40 41 bitri 
 |-  ( C =/= (/) <-> E. w E. a e. A E. b e. B w = ( a x. b ) )
43 39 42 sylibr 
 |-  ( ph -> C =/= (/) )
44 suprcl 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )
45 12 44 syl 
 |-  ( ph -> sup ( A , RR , < ) e. RR )
46 suprcl 
 |-  ( ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) -> sup ( B , RR , < ) e. RR )
47 15 46 syl 
 |-  ( ph -> sup ( B , RR , < ) e. RR )
48 45 47 remulcld 
 |-  ( ph -> ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) e. RR )
49 1 2 supmullem1 
 |-  ( ph -> A. w e. C w <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) )
50 brralrspcev 
 |-  ( ( ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) e. RR /\ A. w e. C w <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) ) -> E. x e. RR A. w e. C w <_ x )
51 48 49 50 syl2anc 
 |-  ( ph -> E. x e. RR A. w e. C w <_ x )
52 25 43 51 3jca 
 |-  ( ph -> ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) )