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 โŠข ๐ถ = { ๐‘ง โˆฃ โˆƒ ๐‘ฃ โˆˆ ๐ด โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘ฃ ยท ๐‘ ) }
supmul.2 โŠข ( ๐œ‘ โ†” ( ( โˆ€ ๐‘ฅ โˆˆ ๐ด 0 โ‰ค ๐‘ฅ โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต 0 โ‰ค ๐‘ฅ ) โˆง ( ๐ด โŠ† โ„ โˆง ๐ด โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ด ๐‘ฆ โ‰ค ๐‘ฅ ) โˆง ( ๐ต โŠ† โ„ โˆง ๐ต โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ต ๐‘ฆ โ‰ค ๐‘ฅ ) ) )
Assertion supmul ( ๐œ‘ โ†’ ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) = sup ( ๐ถ , โ„ , < ) )

Proof

Step Hyp Ref Expression
1 supmul.1 โŠข ๐ถ = { ๐‘ง โˆฃ โˆƒ ๐‘ฃ โˆˆ ๐ด โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘ฃ ยท ๐‘ ) }
2 supmul.2 โŠข ( ๐œ‘ โ†” ( ( โˆ€ ๐‘ฅ โˆˆ ๐ด 0 โ‰ค ๐‘ฅ โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต 0 โ‰ค ๐‘ฅ ) โˆง ( ๐ด โŠ† โ„ โˆง ๐ด โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ด ๐‘ฆ โ‰ค ๐‘ฅ ) โˆง ( ๐ต โŠ† โ„ โˆง ๐ต โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ต ๐‘ฆ โ‰ค ๐‘ฅ ) ) )
3 2 simp2bi โŠข ( ๐œ‘ โ†’ ( ๐ด โŠ† โ„ โˆง ๐ด โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ด ๐‘ฆ โ‰ค ๐‘ฅ ) )
4 suprcl โŠข ( ( ๐ด โŠ† โ„ โˆง ๐ด โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ด ๐‘ฆ โ‰ค ๐‘ฅ ) โ†’ sup ( ๐ด , โ„ , < ) โˆˆ โ„ )
5 3 4 syl โŠข ( ๐œ‘ โ†’ sup ( ๐ด , โ„ , < ) โˆˆ โ„ )
6 2 simp3bi โŠข ( ๐œ‘ โ†’ ( ๐ต โŠ† โ„ โˆง ๐ต โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ต ๐‘ฆ โ‰ค ๐‘ฅ ) )
7 suprcl โŠข ( ( ๐ต โŠ† โ„ โˆง ๐ต โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ต ๐‘ฆ โ‰ค ๐‘ฅ ) โ†’ sup ( ๐ต , โ„ , < ) โˆˆ โ„ )
8 6 7 syl โŠข ( ๐œ‘ โ†’ sup ( ๐ต , โ„ , < ) โˆˆ โ„ )
9 recn โŠข ( sup ( ๐ด , โ„ , < ) โˆˆ โ„ โ†’ sup ( ๐ด , โ„ , < ) โˆˆ โ„‚ )
10 recn โŠข ( sup ( ๐ต , โ„ , < ) โˆˆ โ„ โ†’ sup ( ๐ต , โ„ , < ) โˆˆ โ„‚ )
11 mulcom โŠข ( ( sup ( ๐ด , โ„ , < ) โˆˆ โ„‚ โˆง sup ( ๐ต , โ„ , < ) โˆˆ โ„‚ ) โ†’ ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) = ( sup ( ๐ต , โ„ , < ) ยท sup ( ๐ด , โ„ , < ) ) )
12 9 10 11 syl2an โŠข ( ( sup ( ๐ด , โ„ , < ) โˆˆ โ„ โˆง sup ( ๐ต , โ„ , < ) โˆˆ โ„ ) โ†’ ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) = ( sup ( ๐ต , โ„ , < ) ยท sup ( ๐ด , โ„ , < ) ) )
13 5 8 12 syl2anc โŠข ( ๐œ‘ โ†’ ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) = ( sup ( ๐ต , โ„ , < ) ยท sup ( ๐ด , โ„ , < ) ) )
14 6 simp2d โŠข ( ๐œ‘ โ†’ ๐ต โ‰  โˆ… )
15 n0 โŠข ( ๐ต โ‰  โˆ… โ†” โˆƒ ๐‘ ๐‘ โˆˆ ๐ต )
16 14 15 sylib โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘ ๐‘ โˆˆ ๐ต )
17 0red โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ ๐ต ) โ†’ 0 โˆˆ โ„ )
18 6 simp1d โŠข ( ๐œ‘ โ†’ ๐ต โŠ† โ„ )
19 18 sselda โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ ๐ต ) โ†’ ๐‘ โˆˆ โ„ )
20 8 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ ๐ต ) โ†’ sup ( ๐ต , โ„ , < ) โˆˆ โ„ )
21 simp1r โŠข ( ( ( โˆ€ ๐‘ฅ โˆˆ ๐ด 0 โ‰ค ๐‘ฅ โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต 0 โ‰ค ๐‘ฅ ) โˆง ( ๐ด โŠ† โ„ โˆง ๐ด โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ด ๐‘ฆ โ‰ค ๐‘ฅ ) โˆง ( ๐ต โŠ† โ„ โˆง ๐ต โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ต ๐‘ฆ โ‰ค ๐‘ฅ ) ) โ†’ โˆ€ ๐‘ฅ โˆˆ ๐ต 0 โ‰ค ๐‘ฅ )
22 2 21 sylbi โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ ๐ต 0 โ‰ค ๐‘ฅ )
23 breq2 โŠข ( ๐‘ฅ = ๐‘ โ†’ ( 0 โ‰ค ๐‘ฅ โ†” 0 โ‰ค ๐‘ ) )
24 23 rspccv โŠข ( โˆ€ ๐‘ฅ โˆˆ ๐ต 0 โ‰ค ๐‘ฅ โ†’ ( ๐‘ โˆˆ ๐ต โ†’ 0 โ‰ค ๐‘ ) )
25 22 24 syl โŠข ( ๐œ‘ โ†’ ( ๐‘ โˆˆ ๐ต โ†’ 0 โ‰ค ๐‘ ) )
26 25 imp โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ ๐ต ) โ†’ 0 โ‰ค ๐‘ )
27 suprub โŠข ( ( ( ๐ต โŠ† โ„ โˆง ๐ต โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ต ๐‘ฆ โ‰ค ๐‘ฅ ) โˆง ๐‘ โˆˆ ๐ต ) โ†’ ๐‘ โ‰ค sup ( ๐ต , โ„ , < ) )
28 6 27 sylan โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ ๐ต ) โ†’ ๐‘ โ‰ค sup ( ๐ต , โ„ , < ) )
29 17 19 20 26 28 letrd โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ ๐ต ) โ†’ 0 โ‰ค sup ( ๐ต , โ„ , < ) )
30 16 29 exlimddv โŠข ( ๐œ‘ โ†’ 0 โ‰ค sup ( ๐ต , โ„ , < ) )
31 simp1l โŠข ( ( ( โˆ€ ๐‘ฅ โˆˆ ๐ด 0 โ‰ค ๐‘ฅ โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต 0 โ‰ค ๐‘ฅ ) โˆง ( ๐ด โŠ† โ„ โˆง ๐ด โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ด ๐‘ฆ โ‰ค ๐‘ฅ ) โˆง ( ๐ต โŠ† โ„ โˆง ๐ต โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ต ๐‘ฆ โ‰ค ๐‘ฅ ) ) โ†’ โˆ€ ๐‘ฅ โˆˆ ๐ด 0 โ‰ค ๐‘ฅ )
32 2 31 sylbi โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ ๐ด 0 โ‰ค ๐‘ฅ )
33 eqid โŠข { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } = { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) }
34 biid โŠข ( ( ( sup ( ๐ต , โ„ , < ) โˆˆ โ„ โˆง 0 โ‰ค sup ( ๐ต , โ„ , < ) โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด 0 โ‰ค ๐‘ฅ ) โˆง ( ๐ด โŠ† โ„ โˆง ๐ด โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ด ๐‘ฆ โ‰ค ๐‘ฅ ) ) โ†” ( ( sup ( ๐ต , โ„ , < ) โˆˆ โ„ โˆง 0 โ‰ค sup ( ๐ต , โ„ , < ) โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด 0 โ‰ค ๐‘ฅ ) โˆง ( ๐ด โŠ† โ„ โˆง ๐ด โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ด ๐‘ฆ โ‰ค ๐‘ฅ ) ) )
35 33 34 supmul1 โŠข ( ( ( sup ( ๐ต , โ„ , < ) โˆˆ โ„ โˆง 0 โ‰ค sup ( ๐ต , โ„ , < ) โˆง โˆ€ ๐‘ฅ โˆˆ ๐ด 0 โ‰ค ๐‘ฅ ) โˆง ( ๐ด โŠ† โ„ โˆง ๐ด โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ด ๐‘ฆ โ‰ค ๐‘ฅ ) ) โ†’ ( sup ( ๐ต , โ„ , < ) ยท sup ( ๐ด , โ„ , < ) ) = sup ( { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } , โ„ , < ) )
36 8 30 32 3 35 syl31anc โŠข ( ๐œ‘ โ†’ ( sup ( ๐ต , โ„ , < ) ยท sup ( ๐ด , โ„ , < ) ) = sup ( { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } , โ„ , < ) )
37 13 36 eqtrd โŠข ( ๐œ‘ โ†’ ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) = sup ( { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } , โ„ , < ) )
38 vex โŠข ๐‘ค โˆˆ V
39 eqeq1 โŠข ( ๐‘ง = ๐‘ค โ†’ ( ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) โ†” ๐‘ค = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) ) )
40 39 rexbidv โŠข ( ๐‘ง = ๐‘ค โ†’ ( โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) โ†” โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ค = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) ) )
41 38 40 elab โŠข ( ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } โ†” โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ค = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) )
42 8 adantr โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ sup ( ๐ต , โ„ , < ) โˆˆ โ„ )
43 3 simp1d โŠข ( ๐œ‘ โ†’ ๐ด โŠ† โ„ )
44 43 sselda โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ ๐‘Ž โˆˆ โ„ )
45 recn โŠข ( ๐‘Ž โˆˆ โ„ โ†’ ๐‘Ž โˆˆ โ„‚ )
46 mulcom โŠข ( ( sup ( ๐ต , โ„ , < ) โˆˆ โ„‚ โˆง ๐‘Ž โˆˆ โ„‚ ) โ†’ ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) = ( ๐‘Ž ยท sup ( ๐ต , โ„ , < ) ) )
47 10 45 46 syl2an โŠข ( ( sup ( ๐ต , โ„ , < ) โˆˆ โ„ โˆง ๐‘Ž โˆˆ โ„ ) โ†’ ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) = ( ๐‘Ž ยท sup ( ๐ต , โ„ , < ) ) )
48 42 44 47 syl2anc โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) = ( ๐‘Ž ยท sup ( ๐ต , โ„ , < ) ) )
49 breq2 โŠข ( ๐‘ฅ = ๐‘Ž โ†’ ( 0 โ‰ค ๐‘ฅ โ†” 0 โ‰ค ๐‘Ž ) )
50 49 rspccv โŠข ( โˆ€ ๐‘ฅ โˆˆ ๐ด 0 โ‰ค ๐‘ฅ โ†’ ( ๐‘Ž โˆˆ ๐ด โ†’ 0 โ‰ค ๐‘Ž ) )
51 32 50 syl โŠข ( ๐œ‘ โ†’ ( ๐‘Ž โˆˆ ๐ด โ†’ 0 โ‰ค ๐‘Ž ) )
52 51 imp โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ 0 โ‰ค ๐‘Ž )
53 22 adantr โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ โˆ€ ๐‘ฅ โˆˆ ๐ต 0 โ‰ค ๐‘ฅ )
54 6 adantr โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ ( ๐ต โŠ† โ„ โˆง ๐ต โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ต ๐‘ฆ โ‰ค ๐‘ฅ ) )
55 eqid โŠข { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } = { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) }
56 biid โŠข ( ( ( ๐‘Ž โˆˆ โ„ โˆง 0 โ‰ค ๐‘Ž โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต 0 โ‰ค ๐‘ฅ ) โˆง ( ๐ต โŠ† โ„ โˆง ๐ต โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ต ๐‘ฆ โ‰ค ๐‘ฅ ) ) โ†” ( ( ๐‘Ž โˆˆ โ„ โˆง 0 โ‰ค ๐‘Ž โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต 0 โ‰ค ๐‘ฅ ) โˆง ( ๐ต โŠ† โ„ โˆง ๐ต โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ต ๐‘ฆ โ‰ค ๐‘ฅ ) ) )
57 55 56 supmul1 โŠข ( ( ( ๐‘Ž โˆˆ โ„ โˆง 0 โ‰ค ๐‘Ž โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต 0 โ‰ค ๐‘ฅ ) โˆง ( ๐ต โŠ† โ„ โˆง ๐ต โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ฆ โˆˆ ๐ต ๐‘ฆ โ‰ค ๐‘ฅ ) ) โ†’ ( ๐‘Ž ยท sup ( ๐ต , โ„ , < ) ) = sup ( { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } , โ„ , < ) )
58 44 52 53 54 57 syl31anc โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ ( ๐‘Ž ยท sup ( ๐ต , โ„ , < ) ) = sup ( { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } , โ„ , < ) )
59 eqeq1 โŠข ( ๐‘ง = ๐‘ค โ†’ ( ๐‘ง = ( ๐‘Ž ยท ๐‘ ) โ†” ๐‘ค = ( ๐‘Ž ยท ๐‘ ) ) )
60 59 rexbidv โŠข ( ๐‘ง = ๐‘ค โ†’ ( โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) โ†” โˆƒ ๐‘ โˆˆ ๐ต ๐‘ค = ( ๐‘Ž ยท ๐‘ ) ) )
61 38 60 elab โŠข ( ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } โ†” โˆƒ ๐‘ โˆˆ ๐ต ๐‘ค = ( ๐‘Ž ยท ๐‘ ) )
62 rspe โŠข ( ( ๐‘Ž โˆˆ ๐ด โˆง โˆƒ ๐‘ โˆˆ ๐ต ๐‘ค = ( ๐‘Ž ยท ๐‘ ) ) โ†’ โˆƒ ๐‘Ž โˆˆ ๐ด โˆƒ ๐‘ โˆˆ ๐ต ๐‘ค = ( ๐‘Ž ยท ๐‘ ) )
63 oveq1 โŠข ( ๐‘ฃ = ๐‘Ž โ†’ ( ๐‘ฃ ยท ๐‘ ) = ( ๐‘Ž ยท ๐‘ ) )
64 63 eqeq2d โŠข ( ๐‘ฃ = ๐‘Ž โ†’ ( ๐‘ง = ( ๐‘ฃ ยท ๐‘ ) โ†” ๐‘ง = ( ๐‘Ž ยท ๐‘ ) ) )
65 64 rexbidv โŠข ( ๐‘ฃ = ๐‘Ž โ†’ ( โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘ฃ ยท ๐‘ ) โ†” โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) ) )
66 65 cbvrexvw โŠข ( โˆƒ ๐‘ฃ โˆˆ ๐ด โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘ฃ ยท ๐‘ ) โ†” โˆƒ ๐‘Ž โˆˆ ๐ด โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) )
67 59 2rexbidv โŠข ( ๐‘ง = ๐‘ค โ†’ ( โˆƒ ๐‘Ž โˆˆ ๐ด โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) โ†” โˆƒ ๐‘Ž โˆˆ ๐ด โˆƒ ๐‘ โˆˆ ๐ต ๐‘ค = ( ๐‘Ž ยท ๐‘ ) ) )
68 66 67 syl5bb โŠข ( ๐‘ง = ๐‘ค โ†’ ( โˆƒ ๐‘ฃ โˆˆ ๐ด โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘ฃ ยท ๐‘ ) โ†” โˆƒ ๐‘Ž โˆˆ ๐ด โˆƒ ๐‘ โˆˆ ๐ต ๐‘ค = ( ๐‘Ž ยท ๐‘ ) ) )
69 38 68 1 elab2 โŠข ( ๐‘ค โˆˆ ๐ถ โ†” โˆƒ ๐‘Ž โˆˆ ๐ด โˆƒ ๐‘ โˆˆ ๐ต ๐‘ค = ( ๐‘Ž ยท ๐‘ ) )
70 62 69 sylibr โŠข ( ( ๐‘Ž โˆˆ ๐ด โˆง โˆƒ ๐‘ โˆˆ ๐ต ๐‘ค = ( ๐‘Ž ยท ๐‘ ) ) โ†’ ๐‘ค โˆˆ ๐ถ )
71 70 ex โŠข ( ๐‘Ž โˆˆ ๐ด โ†’ ( โˆƒ ๐‘ โˆˆ ๐ต ๐‘ค = ( ๐‘Ž ยท ๐‘ ) โ†’ ๐‘ค โˆˆ ๐ถ ) )
72 1 2 supmullem2 โŠข ( ๐œ‘ โ†’ ( ๐ถ โŠ† โ„ โˆง ๐ถ โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ค โˆˆ ๐ถ ๐‘ค โ‰ค ๐‘ฅ ) )
73 suprub โŠข ( ( ( ๐ถ โŠ† โ„ โˆง ๐ถ โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ค โˆˆ ๐ถ ๐‘ค โ‰ค ๐‘ฅ ) โˆง ๐‘ค โˆˆ ๐ถ ) โ†’ ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) )
74 73 ex โŠข ( ( ๐ถ โŠ† โ„ โˆง ๐ถ โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ค โˆˆ ๐ถ ๐‘ค โ‰ค ๐‘ฅ ) โ†’ ( ๐‘ค โˆˆ ๐ถ โ†’ ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) ) )
75 72 74 syl โŠข ( ๐œ‘ โ†’ ( ๐‘ค โˆˆ ๐ถ โ†’ ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) ) )
76 71 75 sylan9r โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ ( โˆƒ ๐‘ โˆˆ ๐ต ๐‘ค = ( ๐‘Ž ยท ๐‘ ) โ†’ ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) ) )
77 61 76 syl5bi โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ ( ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } โ†’ ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) ) )
78 77 ralrimiv โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ โˆ€ ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) )
79 44 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โˆง ๐‘ โˆˆ ๐ต ) โ†’ ๐‘Ž โˆˆ โ„ )
80 19 adantlr โŠข ( ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โˆง ๐‘ โˆˆ ๐ต ) โ†’ ๐‘ โˆˆ โ„ )
81 79 80 remulcld โŠข ( ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โˆง ๐‘ โˆˆ ๐ต ) โ†’ ( ๐‘Ž ยท ๐‘ ) โˆˆ โ„ )
82 eleq1a โŠข ( ( ๐‘Ž ยท ๐‘ ) โˆˆ โ„ โ†’ ( ๐‘ง = ( ๐‘Ž ยท ๐‘ ) โ†’ ๐‘ง โˆˆ โ„ ) )
83 81 82 syl โŠข ( ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โˆง ๐‘ โˆˆ ๐ต ) โ†’ ( ๐‘ง = ( ๐‘Ž ยท ๐‘ ) โ†’ ๐‘ง โˆˆ โ„ ) )
84 83 rexlimdva โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ ( โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) โ†’ ๐‘ง โˆˆ โ„ ) )
85 84 abssdv โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } โŠ† โ„ )
86 ovex โŠข ( ๐‘Ž ยท ๐‘ ) โˆˆ V
87 86 isseti โŠข โˆƒ ๐‘ค ๐‘ค = ( ๐‘Ž ยท ๐‘ )
88 87 rgenw โŠข โˆ€ ๐‘ โˆˆ ๐ต โˆƒ ๐‘ค ๐‘ค = ( ๐‘Ž ยท ๐‘ )
89 r19.2z โŠข ( ( ๐ต โ‰  โˆ… โˆง โˆ€ ๐‘ โˆˆ ๐ต โˆƒ ๐‘ค ๐‘ค = ( ๐‘Ž ยท ๐‘ ) ) โ†’ โˆƒ ๐‘ โˆˆ ๐ต โˆƒ ๐‘ค ๐‘ค = ( ๐‘Ž ยท ๐‘ ) )
90 14 88 89 sylancl โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘ โˆˆ ๐ต โˆƒ ๐‘ค ๐‘ค = ( ๐‘Ž ยท ๐‘ ) )
91 rexcom4 โŠข ( โˆƒ ๐‘ โˆˆ ๐ต โˆƒ ๐‘ค ๐‘ค = ( ๐‘Ž ยท ๐‘ ) โ†” โˆƒ ๐‘ค โˆƒ ๐‘ โˆˆ ๐ต ๐‘ค = ( ๐‘Ž ยท ๐‘ ) )
92 90 91 sylib โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘ค โˆƒ ๐‘ โˆˆ ๐ต ๐‘ค = ( ๐‘Ž ยท ๐‘ ) )
93 60 cbvexvw โŠข ( โˆƒ ๐‘ง โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) โ†” โˆƒ ๐‘ค โˆƒ ๐‘ โˆˆ ๐ต ๐‘ค = ( ๐‘Ž ยท ๐‘ ) )
94 92 93 sylibr โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘ง โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) )
95 abn0 โŠข ( { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } โ‰  โˆ… โ†” โˆƒ ๐‘ง โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) )
96 94 95 sylibr โŠข ( ๐œ‘ โ†’ { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } โ‰  โˆ… )
97 96 adantr โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } โ‰  โˆ… )
98 suprcl โŠข ( ( ๐ถ โŠ† โ„ โˆง ๐ถ โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ค โˆˆ ๐ถ ๐‘ค โ‰ค ๐‘ฅ ) โ†’ sup ( ๐ถ , โ„ , < ) โˆˆ โ„ )
99 72 98 syl โŠข ( ๐œ‘ โ†’ sup ( ๐ถ , โ„ , < ) โˆˆ โ„ )
100 99 adantr โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ sup ( ๐ถ , โ„ , < ) โˆˆ โ„ )
101 brralrspcev โŠข ( ( sup ( ๐ถ , โ„ , < ) โˆˆ โ„ โˆง โˆ€ ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } ๐‘ค โ‰ค ๐‘ฅ )
102 100 78 101 syl2anc โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } ๐‘ค โ‰ค ๐‘ฅ )
103 suprleub โŠข ( ( ( { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } โŠ† โ„ โˆง { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } ๐‘ค โ‰ค ๐‘ฅ ) โˆง sup ( ๐ถ , โ„ , < ) โˆˆ โ„ ) โ†’ ( sup ( { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } , โ„ , < ) โ‰ค sup ( ๐ถ , โ„ , < ) โ†” โˆ€ ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) ) )
104 85 97 102 100 103 syl31anc โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ ( sup ( { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } , โ„ , < ) โ‰ค sup ( ๐ถ , โ„ , < ) โ†” โˆ€ ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) ) )
105 78 104 mpbird โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ sup ( { ๐‘ง โˆฃ โˆƒ ๐‘ โˆˆ ๐ต ๐‘ง = ( ๐‘Ž ยท ๐‘ ) } , โ„ , < ) โ‰ค sup ( ๐ถ , โ„ , < ) )
106 58 105 eqbrtrd โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ ( ๐‘Ž ยท sup ( ๐ต , โ„ , < ) ) โ‰ค sup ( ๐ถ , โ„ , < ) )
107 48 106 eqbrtrd โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) โ‰ค sup ( ๐ถ , โ„ , < ) )
108 breq1 โŠข ( ๐‘ค = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) โ†’ ( ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) โ†” ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) โ‰ค sup ( ๐ถ , โ„ , < ) ) )
109 107 108 syl5ibrcom โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ ( ๐‘ค = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) โ†’ ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) ) )
110 109 rexlimdva โŠข ( ๐œ‘ โ†’ ( โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ค = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) โ†’ ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) ) )
111 41 110 syl5bi โŠข ( ๐œ‘ โ†’ ( ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } โ†’ ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) ) )
112 111 ralrimiv โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) )
113 42 44 remulcld โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) โˆˆ โ„ )
114 eleq1a โŠข ( ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) โˆˆ โ„ โ†’ ( ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) โ†’ ๐‘ง โˆˆ โ„ ) )
115 113 114 syl โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ด ) โ†’ ( ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) โ†’ ๐‘ง โˆˆ โ„ ) )
116 115 rexlimdva โŠข ( ๐œ‘ โ†’ ( โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) โ†’ ๐‘ง โˆˆ โ„ ) )
117 116 abssdv โŠข ( ๐œ‘ โ†’ { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } โŠ† โ„ )
118 3 simp2d โŠข ( ๐œ‘ โ†’ ๐ด โ‰  โˆ… )
119 ovex โŠข ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) โˆˆ V
120 119 isseti โŠข โˆƒ ๐‘ง ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž )
121 120 rgenw โŠข โˆ€ ๐‘Ž โˆˆ ๐ด โˆƒ ๐‘ง ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž )
122 r19.2z โŠข ( ( ๐ด โ‰  โˆ… โˆง โˆ€ ๐‘Ž โˆˆ ๐ด โˆƒ ๐‘ง ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) ) โ†’ โˆƒ ๐‘Ž โˆˆ ๐ด โˆƒ ๐‘ง ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) )
123 118 121 122 sylancl โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘Ž โˆˆ ๐ด โˆƒ ๐‘ง ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) )
124 rexcom4 โŠข ( โˆƒ ๐‘Ž โˆˆ ๐ด โˆƒ ๐‘ง ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) โ†” โˆƒ ๐‘ง โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) )
125 123 124 sylib โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘ง โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) )
126 abn0 โŠข ( { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } โ‰  โˆ… โ†” โˆƒ ๐‘ง โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) )
127 125 126 sylibr โŠข ( ๐œ‘ โ†’ { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } โ‰  โˆ… )
128 brralrspcev โŠข ( ( sup ( ๐ถ , โ„ , < ) โˆˆ โ„ โˆง โˆ€ ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } ๐‘ค โ‰ค ๐‘ฅ )
129 99 112 128 syl2anc โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } ๐‘ค โ‰ค ๐‘ฅ )
130 suprleub โŠข ( ( ( { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } โŠ† โ„ โˆง { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } ๐‘ค โ‰ค ๐‘ฅ ) โˆง sup ( ๐ถ , โ„ , < ) โˆˆ โ„ ) โ†’ ( sup ( { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } , โ„ , < ) โ‰ค sup ( ๐ถ , โ„ , < ) โ†” โˆ€ ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) ) )
131 117 127 129 99 130 syl31anc โŠข ( ๐œ‘ โ†’ ( sup ( { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } , โ„ , < ) โ‰ค sup ( ๐ถ , โ„ , < ) โ†” โˆ€ ๐‘ค โˆˆ { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } ๐‘ค โ‰ค sup ( ๐ถ , โ„ , < ) ) )
132 112 131 mpbird โŠข ( ๐œ‘ โ†’ sup ( { ๐‘ง โˆฃ โˆƒ ๐‘Ž โˆˆ ๐ด ๐‘ง = ( sup ( ๐ต , โ„ , < ) ยท ๐‘Ž ) } , โ„ , < ) โ‰ค sup ( ๐ถ , โ„ , < ) )
133 37 132 eqbrtrd โŠข ( ๐œ‘ โ†’ ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) โ‰ค sup ( ๐ถ , โ„ , < ) )
134 1 2 supmullem1 โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ค โˆˆ ๐ถ ๐‘ค โ‰ค ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) )
135 5 8 remulcld โŠข ( ๐œ‘ โ†’ ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) โˆˆ โ„ )
136 suprleub โŠข ( ( ( ๐ถ โŠ† โ„ โˆง ๐ถ โ‰  โˆ… โˆง โˆƒ ๐‘ฅ โˆˆ โ„ โˆ€ ๐‘ค โˆˆ ๐ถ ๐‘ค โ‰ค ๐‘ฅ ) โˆง ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) โˆˆ โ„ ) โ†’ ( sup ( ๐ถ , โ„ , < ) โ‰ค ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) โ†” โˆ€ ๐‘ค โˆˆ ๐ถ ๐‘ค โ‰ค ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) ) )
137 72 135 136 syl2anc โŠข ( ๐œ‘ โ†’ ( sup ( ๐ถ , โ„ , < ) โ‰ค ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) โ†” โˆ€ ๐‘ค โˆˆ ๐ถ ๐‘ค โ‰ค ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) ) )
138 134 137 mpbird โŠข ( ๐œ‘ โ†’ sup ( ๐ถ , โ„ , < ) โ‰ค ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) )
139 135 99 letri3d โŠข ( ๐œ‘ โ†’ ( ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) = sup ( ๐ถ , โ„ , < ) โ†” ( ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) โ‰ค sup ( ๐ถ , โ„ , < ) โˆง sup ( ๐ถ , โ„ , < ) โ‰ค ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) ) ) )
140 133 138 139 mpbir2and โŠข ( ๐œ‘ โ†’ ( sup ( ๐ด , โ„ , < ) ยท sup ( ๐ต , โ„ , < ) ) = sup ( ๐ถ , โ„ , < ) )