Metamath Proof Explorer

Theorem supmullem1

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 supmullem1 
|- ( ph -> A. w e. C w <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) )

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 sselda 
 |-  ( ( ph /\ a e. A ) -> a e. RR )
15 14 adantrr 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> a e. RR )
16 suprcl 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )
17 12 16 syl 
 |-  ( ph -> sup ( A , RR , < ) e. RR )
18 17 adantr 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> sup ( A , RR , < ) e. RR )
19 2 simp3bi 
 |-  ( ph -> ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) )
20 19 simp1d 
 |-  ( ph -> B C_ RR )
21 20 sselda 
 |-  ( ( ph /\ b e. B ) -> b e. RR )
22 21 adantrl 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> b e. RR )
23 suprcl 
 |-  ( ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) -> sup ( B , RR , < ) e. RR )
24 19 23 syl 
 |-  ( ph -> sup ( B , RR , < ) e. RR )
25 24 adantr 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> sup ( B , RR , < ) e. RR )
26 simp1l 
 |-  ( ( ( 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 ) ) -> A. x e. A 0 <_ x )
27 2 26 sylbi 
 |-  ( ph -> A. x e. A 0 <_ x )
28 breq2 
 |-  ( x = a -> ( 0 <_ x <-> 0 <_ a ) )
29 28 rspccv 
 |-  ( A. x e. A 0 <_ x -> ( a e. A -> 0 <_ a ) )
30 27 29 syl 
 |-  ( ph -> ( a e. A -> 0 <_ a ) )
31 30 imp 
 |-  ( ( ph /\ a e. A ) -> 0 <_ a )
32 31 adantrr 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> 0 <_ a )
33 simp1r 
 |-  ( ( ( 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 ) ) -> A. x e. B 0 <_ x )
34 2 33 sylbi 
 |-  ( ph -> A. x e. B 0 <_ x )
35 breq2 
 |-  ( x = b -> ( 0 <_ x <-> 0 <_ b ) )
36 35 rspccv 
 |-  ( A. x e. B 0 <_ x -> ( b e. B -> 0 <_ b ) )
37 34 36 syl 
 |-  ( ph -> ( b e. B -> 0 <_ b ) )
38 37 imp 
 |-  ( ( ph /\ b e. B ) -> 0 <_ b )
39 38 adantrl 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> 0 <_ b )
40 suprub 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ a e. A ) -> a <_ sup ( A , RR , < ) )
41 12 40 sylan 
 |-  ( ( ph /\ a e. A ) -> a <_ sup ( A , RR , < ) )
42 41 adantrr 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> a <_ sup ( A , RR , < ) )
43 suprub 
 |-  ( ( ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) /\ b e. B ) -> b <_ sup ( B , RR , < ) )
44 19 43 sylan 
 |-  ( ( ph /\ b e. B ) -> b <_ sup ( B , RR , < ) )
45 44 adantrl 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> b <_ sup ( B , RR , < ) )
46 15 18 22 25 32 39 42 45 lemul12ad 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> ( a x. b ) <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) )
47 46 ex 
 |-  ( ph -> ( ( a e. A /\ b e. B ) -> ( a x. b ) <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) ) )
48 breq1 
 |-  ( w = ( a x. b ) -> ( w <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) <-> ( a x. b ) <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) ) )
49 48 biimprcd 
 |-  ( ( a x. b ) <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) -> ( w = ( a x. b ) -> w <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) ) )
50 47 49 syl6 
 |-  ( ph -> ( ( a e. A /\ b e. B ) -> ( w = ( a x. b ) -> w <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) ) ) )
51 50 rexlimdvv 
 |-  ( ph -> ( E. a e. A E. b e. B w = ( a x. b ) -> w <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) ) )
52 11 51 syl5bi 
 |-  ( ph -> ( w e. C -> w <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) ) )
53 52 ralrimiv 
 |-  ( ph -> A. w e. C w <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) )