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 ( ๐ถ , โ , < ) ) |