Metamath Proof Explorer

Theorem supmul

Description: The supremum function distributes over multiplication, in the sense that ( sup A ) x. ( sup B ) = sup ( A x. B ) , where A x. B is shorthand for { a x. b | a e. A , b e. B } and is defined as C below. We made use of this in our definition of multiplication in the Dedekind cut construction of the reals (see df-mp ). (Contributed by Mario Carneiro, 5-Jul-2013) (Revised by Mario Carneiro, 6-Sep-2014)

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 supmul 
|- ( ph -> ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) = sup ( C , 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 2 simp2bi 
 |-  ( ph -> ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) )
4 suprcl 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )
5 3 4 syl 
 |-  ( ph -> sup ( A , RR , < ) e. RR )
6 2 simp3bi 
 |-  ( ph -> ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) )
7 suprcl 
 |-  ( ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) -> sup ( B , RR , < ) e. RR )
8 6 7 syl 
 |-  ( ph -> sup ( B , RR , < ) e. RR )
9 recn 
 |-  ( sup ( A , RR , < ) e. RR -> sup ( A , RR , < ) e. CC )
10 recn 
 |-  ( sup ( B , RR , < ) e. RR -> sup ( B , RR , < ) e. CC )
11 mulcom 
 |-  ( ( sup ( A , RR , < ) e. CC /\ sup ( B , RR , < ) e. CC ) -> ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) = ( sup ( B , RR , < ) x. sup ( A , RR , < ) ) )
12 9 10 11 syl2an 
 |-  ( ( sup ( A , RR , < ) e. RR /\ sup ( B , RR , < ) e. RR ) -> ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) = ( sup ( B , RR , < ) x. sup ( A , RR , < ) ) )
13 5 8 12 syl2anc 
 |-  ( ph -> ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) = ( sup ( B , RR , < ) x. sup ( A , RR , < ) ) )
14 6 simp2d 
 |-  ( ph -> B =/= (/) )
15 n0 
 |-  ( B =/= (/) <-> E. b b e. B )
16 14 15 sylib 
 |-  ( ph -> E. b b e. B )
17 0red 
 |-  ( ( ph /\ b e. B ) -> 0 e. RR )
18 6 simp1d 
 |-  ( ph -> B C_ RR )
19 18 sselda 
 |-  ( ( ph /\ b e. B ) -> b e. RR )
20 8 adantr 
 |-  ( ( ph /\ b e. B ) -> sup ( B , RR , < ) e. RR )
21 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 )
22 2 21 sylbi 
 |-  ( ph -> A. x e. B 0 <_ x )
23 breq2 
 |-  ( x = b -> ( 0 <_ x <-> 0 <_ b ) )
24 23 rspccv 
 |-  ( A. x e. B 0 <_ x -> ( b e. B -> 0 <_ b ) )
25 22 24 syl 
 |-  ( ph -> ( b e. B -> 0 <_ b ) )
26 25 imp 
 |-  ( ( ph /\ b e. B ) -> 0 <_ b )
27 suprub 
 |-  ( ( ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) /\ b e. B ) -> b <_ sup ( B , RR , < ) )
28 6 27 sylan 
 |-  ( ( ph /\ b e. B ) -> b <_ sup ( B , RR , < ) )
29 17 19 20 26 28 letrd 
 |-  ( ( ph /\ b e. B ) -> 0 <_ sup ( B , RR , < ) )
30 16 29 exlimddv 
 |-  ( ph -> 0 <_ sup ( B , RR , < ) )
31 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 )
32 2 31 sylbi 
 |-  ( ph -> A. x e. A 0 <_ x )
33 eqid 
 |-  { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } = { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) }
34 biid 
 |-  ( ( ( sup ( B , RR , < ) e. RR /\ 0 <_ sup ( B , RR , < ) /\ A. x e. A 0 <_ x ) /\ ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) ) <-> ( ( sup ( B , RR , < ) e. RR /\ 0 <_ sup ( B , RR , < ) /\ A. x e. A 0 <_ x ) /\ ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) ) )
35 33 34 supmul1 
 |-  ( ( ( sup ( B , RR , < ) e. RR /\ 0 <_ sup ( B , RR , < ) /\ A. x e. A 0 <_ x ) /\ ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) ) -> ( sup ( B , RR , < ) x. sup ( A , RR , < ) ) = sup ( { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } , RR , < ) )
36 8 30 32 3 35 syl31anc 
 |-  ( ph -> ( sup ( B , RR , < ) x. sup ( A , RR , < ) ) = sup ( { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } , RR , < ) )
37 13 36 eqtrd 
 |-  ( ph -> ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) = sup ( { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } , RR , < ) )
38 vex 
 |-  w e. _V
39 eqeq1 
 |-  ( z = w -> ( z = ( sup ( B , RR , < ) x. a ) <-> w = ( sup ( B , RR , < ) x. a ) ) )
40 39 rexbidv 
 |-  ( z = w -> ( E. a e. A z = ( sup ( B , RR , < ) x. a ) <-> E. a e. A w = ( sup ( B , RR , < ) x. a ) ) )
41 38 40 elab 
 |-  ( w e. { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } <-> E. a e. A w = ( sup ( B , RR , < ) x. a ) )
42 8 adantr 
 |-  ( ( ph /\ a e. A ) -> sup ( B , RR , < ) e. RR )
43 3 simp1d 
 |-  ( ph -> A C_ RR )
44 43 sselda 
 |-  ( ( ph /\ a e. A ) -> a e. RR )
45 recn 
 |-  ( a e. RR -> a e. CC )
46 mulcom 
 |-  ( ( sup ( B , RR , < ) e. CC /\ a e. CC ) -> ( sup ( B , RR , < ) x. a ) = ( a x. sup ( B , RR , < ) ) )
47 10 45 46 syl2an 
 |-  ( ( sup ( B , RR , < ) e. RR /\ a e. RR ) -> ( sup ( B , RR , < ) x. a ) = ( a x. sup ( B , RR , < ) ) )
48 42 44 47 syl2anc 
 |-  ( ( ph /\ a e. A ) -> ( sup ( B , RR , < ) x. a ) = ( a x. sup ( B , RR , < ) ) )
49 breq2 
 |-  ( x = a -> ( 0 <_ x <-> 0 <_ a ) )
50 49 rspccv 
 |-  ( A. x e. A 0 <_ x -> ( a e. A -> 0 <_ a ) )
51 32 50 syl 
 |-  ( ph -> ( a e. A -> 0 <_ a ) )
52 51 imp 
 |-  ( ( ph /\ a e. A ) -> 0 <_ a )
53 22 adantr 
 |-  ( ( ph /\ a e. A ) -> A. x e. B 0 <_ x )
54 6 adantr 
 |-  ( ( ph /\ a e. A ) -> ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) )
55 eqid 
 |-  { z | E. b e. B z = ( a x. b ) } = { z | E. b e. B z = ( a x. b ) }
56 biid 
 |-  ( ( ( a e. RR /\ 0 <_ a /\ A. x e. B 0 <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) <-> ( ( a e. RR /\ 0 <_ a /\ A. x e. B 0 <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) )
57 55 56 supmul1 
 |-  ( ( ( a e. RR /\ 0 <_ a /\ A. x e. B 0 <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) -> ( a x. sup ( B , RR , < ) ) = sup ( { z | E. b e. B z = ( a x. b ) } , RR , < ) )
58 44 52 53 54 57 syl31anc 
 |-  ( ( ph /\ a e. A ) -> ( a x. sup ( B , RR , < ) ) = sup ( { z | E. b e. B z = ( a x. b ) } , RR , < ) )
59 eqeq1 
 |-  ( z = w -> ( z = ( a x. b ) <-> w = ( a x. b ) ) )
60 59 rexbidv 
 |-  ( z = w -> ( E. b e. B z = ( a x. b ) <-> E. b e. B w = ( a x. b ) ) )
61 38 60 elab 
 |-  ( w e. { z | E. b e. B z = ( a x. b ) } <-> E. b e. B w = ( a x. b ) )
62 rspe 
 |-  ( ( a e. A /\ E. b e. B w = ( a x. b ) ) -> E. a e. A E. b e. B w = ( a x. b ) )
63 oveq1 
 |-  ( v = a -> ( v x. b ) = ( a x. b ) )
64 63 eqeq2d 
 |-  ( v = a -> ( z = ( v x. b ) <-> z = ( a x. b ) ) )
65 64 rexbidv 
 |-  ( v = a -> ( E. b e. B z = ( v x. b ) <-> E. b e. B z = ( a x. b ) ) )
66 65 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 ) )
67 59 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 ) ) )
68 66 67 bitrid 
 |-  ( 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 ) ) )
69 38 68 1 elab2 
 |-  ( w e. C <-> E. a e. A E. b e. B w = ( a x. b ) )
70 62 69 sylibr 
 |-  ( ( a e. A /\ E. b e. B w = ( a x. b ) ) -> w e. C )
71 70 ex 
 |-  ( a e. A -> ( E. b e. B w = ( a x. b ) -> w e. C ) )
72 1 2 supmullem2 
 |-  ( ph -> ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) )
73 suprub 
 |-  ( ( ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) /\ w e. C ) -> w <_ sup ( C , RR , < ) )
74 73 ex 
 |-  ( ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) -> ( w e. C -> w <_ sup ( C , RR , < ) ) )
75 72 74 syl 
 |-  ( ph -> ( w e. C -> w <_ sup ( C , RR , < ) ) )
76 71 75 sylan9r 
 |-  ( ( ph /\ a e. A ) -> ( E. b e. B w = ( a x. b ) -> w <_ sup ( C , RR , < ) ) )
77 61 76 biimtrid 
 |-  ( ( ph /\ a e. A ) -> ( w e. { z | E. b e. B z = ( a x. b ) } -> w <_ sup ( C , RR , < ) ) )
78 77 ralrimiv 
 |-  ( ( ph /\ a e. A ) -> A. w e. { z | E. b e. B z = ( a x. b ) } w <_ sup ( C , RR , < ) )
79 44 adantr 
 |-  ( ( ( ph /\ a e. A ) /\ b e. B ) -> a e. RR )
80 19 adantlr 
 |-  ( ( ( ph /\ a e. A ) /\ b e. B ) -> b e. RR )
81 79 80 remulcld 
 |-  ( ( ( ph /\ a e. A ) /\ b e. B ) -> ( a x. b ) e. RR )
82 eleq1a 
 |-  ( ( a x. b ) e. RR -> ( z = ( a x. b ) -> z e. RR ) )
83 81 82 syl 
 |-  ( ( ( ph /\ a e. A ) /\ b e. B ) -> ( z = ( a x. b ) -> z e. RR ) )
84 83 rexlimdva 
 |-  ( ( ph /\ a e. A ) -> ( E. b e. B z = ( a x. b ) -> z e. RR ) )
85 84 abssdv 
 |-  ( ( ph /\ a e. A ) -> { z | E. b e. B z = ( a x. b ) } C_ RR )
86 ovex 
 |-  ( a x. b ) e. _V
87 86 isseti 
 |-  E. w w = ( a x. b )
88 87 rgenw 
 |-  A. b e. B E. w w = ( a x. b )
89 r19.2z 
 |-  ( ( B =/= (/) /\ A. b e. B E. w w = ( a x. b ) ) -> E. b e. B E. w w = ( a x. b ) )
90 14 88 89 sylancl 
 |-  ( ph -> E. b e. B E. w w = ( a x. b ) )
91 rexcom4 
 |-  ( E. b e. B E. w w = ( a x. b ) <-> E. w E. b e. B w = ( a x. b ) )
92 90 91 sylib 
 |-  ( ph -> E. w E. b e. B w = ( a x. b ) )
93 60 cbvexvw 
 |-  ( E. z E. b e. B z = ( a x. b ) <-> E. w E. b e. B w = ( a x. b ) )
94 92 93 sylibr 
 |-  ( ph -> E. z E. b e. B z = ( a x. b ) )
95 abn0 
 |-  ( { z | E. b e. B z = ( a x. b ) } =/= (/) <-> E. z E. b e. B z = ( a x. b ) )
96 94 95 sylibr 
 |-  ( ph -> { z | E. b e. B z = ( a x. b ) } =/= (/) )
97 96 adantr 
 |-  ( ( ph /\ a e. A ) -> { z | E. b e. B z = ( a x. b ) } =/= (/) )
98 suprcl 
 |-  ( ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) -> sup ( C , RR , < ) e. RR )
99 72 98 syl 
 |-  ( ph -> sup ( C , RR , < ) e. RR )
100 99 adantr 
 |-  ( ( ph /\ a e. A ) -> sup ( C , RR , < ) e. RR )
101 brralrspcev 
 |-  ( ( sup ( C , RR , < ) e. RR /\ A. w e. { z | E. b e. B z = ( a x. b ) } w <_ sup ( C , RR , < ) ) -> E. x e. RR A. w e. { z | E. b e. B z = ( a x. b ) } w <_ x )
102 100 78 101 syl2anc 
 |-  ( ( ph /\ a e. A ) -> E. x e. RR A. w e. { z | E. b e. B z = ( a x. b ) } w <_ x )
103 suprleub 
 |-  ( ( ( { z | E. b e. B z = ( a x. b ) } C_ RR /\ { z | E. b e. B z = ( a x. b ) } =/= (/) /\ E. x e. RR A. w e. { z | E. b e. B z = ( a x. b ) } w <_ x ) /\ sup ( C , RR , < ) e. RR ) -> ( sup ( { z | E. b e. B z = ( a x. b ) } , RR , < ) <_ sup ( C , RR , < ) <-> A. w e. { z | E. b e. B z = ( a x. b ) } w <_ sup ( C , RR , < ) ) )
104 85 97 102 100 103 syl31anc 
 |-  ( ( ph /\ a e. A ) -> ( sup ( { z | E. b e. B z = ( a x. b ) } , RR , < ) <_ sup ( C , RR , < ) <-> A. w e. { z | E. b e. B z = ( a x. b ) } w <_ sup ( C , RR , < ) ) )
105 78 104 mpbird 
 |-  ( ( ph /\ a e. A ) -> sup ( { z | E. b e. B z = ( a x. b ) } , RR , < ) <_ sup ( C , RR , < ) )
106 58 105 eqbrtrd 
 |-  ( ( ph /\ a e. A ) -> ( a x. sup ( B , RR , < ) ) <_ sup ( C , RR , < ) )
107 48 106 eqbrtrd 
 |-  ( ( ph /\ a e. A ) -> ( sup ( B , RR , < ) x. a ) <_ sup ( C , RR , < ) )
108 breq1 
 |-  ( w = ( sup ( B , RR , < ) x. a ) -> ( w <_ sup ( C , RR , < ) <-> ( sup ( B , RR , < ) x. a ) <_ sup ( C , RR , < ) ) )
109 107 108 syl5ibrcom 
 |-  ( ( ph /\ a e. A ) -> ( w = ( sup ( B , RR , < ) x. a ) -> w <_ sup ( C , RR , < ) ) )
110 109 rexlimdva 
 |-  ( ph -> ( E. a e. A w = ( sup ( B , RR , < ) x. a ) -> w <_ sup ( C , RR , < ) ) )
111 41 110 biimtrid 
 |-  ( ph -> ( w e. { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } -> w <_ sup ( C , RR , < ) ) )
112 111 ralrimiv 
 |-  ( ph -> A. w e. { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } w <_ sup ( C , RR , < ) )
113 42 44 remulcld 
 |-  ( ( ph /\ a e. A ) -> ( sup ( B , RR , < ) x. a ) e. RR )
114 eleq1a 
 |-  ( ( sup ( B , RR , < ) x. a ) e. RR -> ( z = ( sup ( B , RR , < ) x. a ) -> z e. RR ) )
115 113 114 syl 
 |-  ( ( ph /\ a e. A ) -> ( z = ( sup ( B , RR , < ) x. a ) -> z e. RR ) )
116 115 rexlimdva 
 |-  ( ph -> ( E. a e. A z = ( sup ( B , RR , < ) x. a ) -> z e. RR ) )
117 116 abssdv 
 |-  ( ph -> { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } C_ RR )
118 3 simp2d 
 |-  ( ph -> A =/= (/) )
119 ovex 
 |-  ( sup ( B , RR , < ) x. a ) e. _V
120 119 isseti 
 |-  E. z z = ( sup ( B , RR , < ) x. a )
121 120 rgenw 
 |-  A. a e. A E. z z = ( sup ( B , RR , < ) x. a )
122 r19.2z 
 |-  ( ( A =/= (/) /\ A. a e. A E. z z = ( sup ( B , RR , < ) x. a ) ) -> E. a e. A E. z z = ( sup ( B , RR , < ) x. a ) )
123 118 121 122 sylancl 
 |-  ( ph -> E. a e. A E. z z = ( sup ( B , RR , < ) x. a ) )
124 rexcom4 
 |-  ( E. a e. A E. z z = ( sup ( B , RR , < ) x. a ) <-> E. z E. a e. A z = ( sup ( B , RR , < ) x. a ) )
125 123 124 sylib 
 |-  ( ph -> E. z E. a e. A z = ( sup ( B , RR , < ) x. a ) )
126 abn0 
 |-  ( { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } =/= (/) <-> E. z E. a e. A z = ( sup ( B , RR , < ) x. a ) )
127 125 126 sylibr 
 |-  ( ph -> { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } =/= (/) )
128 brralrspcev 
 |-  ( ( sup ( C , RR , < ) e. RR /\ A. w e. { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } w <_ sup ( C , RR , < ) ) -> E. x e. RR A. w e. { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } w <_ x )
129 99 112 128 syl2anc 
 |-  ( ph -> E. x e. RR A. w e. { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } w <_ x )
130 suprleub 
 |-  ( ( ( { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } C_ RR /\ { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } =/= (/) /\ E. x e. RR A. w e. { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } w <_ x ) /\ sup ( C , RR , < ) e. RR ) -> ( sup ( { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } , RR , < ) <_ sup ( C , RR , < ) <-> A. w e. { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } w <_ sup ( C , RR , < ) ) )
131 117 127 129 99 130 syl31anc 
 |-  ( ph -> ( sup ( { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } , RR , < ) <_ sup ( C , RR , < ) <-> A. w e. { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } w <_ sup ( C , RR , < ) ) )
132 112 131 mpbird 
 |-  ( ph -> sup ( { z | E. a e. A z = ( sup ( B , RR , < ) x. a ) } , RR , < ) <_ sup ( C , RR , < ) )
133 37 132 eqbrtrd 
 |-  ( ph -> ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) <_ sup ( C , RR , < ) )
134 1 2 supmullem1 
 |-  ( ph -> A. w e. C w <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) )
135 5 8 remulcld 
 |-  ( ph -> ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) e. RR )
136 suprleub 
 |-  ( ( ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) /\ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) e. RR ) -> ( sup ( C , RR , < ) <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) <-> A. w e. C w <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) ) )
137 72 135 136 syl2anc 
 |-  ( ph -> ( sup ( C , RR , < ) <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) <-> A. w e. C w <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) ) )
138 134 137 mpbird 
 |-  ( ph -> sup ( C , RR , < ) <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) )
139 135 99 letri3d 
 |-  ( ph -> ( ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) = sup ( C , RR , < ) <-> ( ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) <_ sup ( C , RR , < ) /\ sup ( C , RR , < ) <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) ) ) )
140 133 138 139 mpbir2and 
 |-  ( ph -> ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) = sup ( C , RR , < ) )