Step |
Hyp |
Ref |
Expression |
1 |
|
cncmpmax.1 |
⊢ 𝑇 = ∪ 𝐽 |
2 |
|
cncmpmax.2 |
⊢ 𝐾 = ( topGen ‘ ran (,) ) |
3 |
|
cncmpmax.3 |
⊢ ( 𝜑 → 𝐽 ∈ Comp ) |
4 |
|
cncmpmax.4 |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) |
5 |
|
cncmpmax.5 |
⊢ ( 𝜑 → 𝑇 ≠ ∅ ) |
6 |
1 2 3 4 5
|
evth |
⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑇 ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
7 |
|
eqid |
⊢ ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn 𝐾 ) |
8 |
2 1 7 4
|
fcnre |
⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ ) |
9 |
8
|
frnd |
⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ ) |
10 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) → ran 𝐹 ⊆ ℝ ) |
11 |
8
|
ffund |
⊢ ( 𝜑 → Fun 𝐹 ) |
12 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → Fun 𝐹 ) |
13 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ 𝑇 ) |
14 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → 𝐹 : 𝑇 ⟶ ℝ ) |
15 |
14
|
fdmd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → dom 𝐹 = 𝑇 ) |
16 |
13 15
|
eleqtrrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ dom 𝐹 ) |
17 |
|
fvelrn |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 ) |
18 |
12 16 17
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 ) |
19 |
18
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 ) |
20 |
|
ffn |
⊢ ( 𝐹 : 𝑇 ⟶ ℝ → 𝐹 Fn 𝑇 ) |
21 |
|
fvelrnb |
⊢ ( 𝐹 Fn 𝑇 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑠 ∈ 𝑇 ( 𝐹 ‘ 𝑠 ) = 𝑦 ) ) |
22 |
8 20 21
|
3syl |
⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑠 ∈ 𝑇 ( 𝐹 ‘ 𝑠 ) = 𝑦 ) ) |
23 |
22
|
biimpa |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → ∃ 𝑠 ∈ 𝑇 ( 𝐹 ‘ 𝑠 ) = 𝑦 ) |
24 |
|
df-rex |
⊢ ( ∃ 𝑠 ∈ 𝑇 ( 𝐹 ‘ 𝑠 ) = 𝑦 ↔ ∃ 𝑠 ( 𝑠 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑠 ) = 𝑦 ) ) |
25 |
23 24
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑠 ) = 𝑦 ) ) |
26 |
25
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑠 ) = 𝑦 ) ) |
27 |
|
simprr |
⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ ( 𝑠 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑠 ) = 𝑦 ) ) → ( 𝐹 ‘ 𝑠 ) = 𝑦 ) |
28 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ ( 𝑠 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑠 ) = 𝑦 ) ) → ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
29 |
|
simprl |
⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ ( 𝑠 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑠 ) = 𝑦 ) ) → 𝑠 ∈ 𝑇 ) |
30 |
|
fveq2 |
⊢ ( 𝑡 = 𝑠 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑠 ) ) |
31 |
30
|
breq1d |
⊢ ( 𝑡 = 𝑠 → ( ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑠 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) |
32 |
31
|
rspccva |
⊢ ( ( ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ 𝑠 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑠 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
33 |
28 29 32
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ ( 𝑠 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑠 ) = 𝑦 ) ) → ( 𝐹 ‘ 𝑠 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
34 |
27 33
|
eqbrtrrd |
⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ ( 𝑠 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑠 ) = 𝑦 ) ) → 𝑦 ≤ ( 𝐹 ‘ 𝑥 ) ) |
35 |
26 34
|
exlimddv |
⊢ ( ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ≤ ( 𝐹 ‘ 𝑥 ) ) |
36 |
35
|
ralrimiva |
⊢ ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ ( 𝐹 ‘ 𝑥 ) ) |
37 |
36
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ ( 𝐹 ‘ 𝑥 ) ) |
38 |
|
ubelsupr |
⊢ ( ( ran 𝐹 ⊆ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 ∧ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) = sup ( ran 𝐹 , ℝ , < ) ) |
39 |
10 19 37 38
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑥 ) = sup ( ran 𝐹 , ℝ , < ) ) |
40 |
39
|
eqcomd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) → sup ( ran 𝐹 , ℝ , < ) = ( 𝐹 ‘ 𝑥 ) ) |
41 |
40 19
|
eqeltrd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ) |
42 |
10 41
|
sseldd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ ) |
43 |
|
simplrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝑇 ) → ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
44 |
43 32
|
sylancom |
⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑠 ) ≤ ( 𝐹 ‘ 𝑥 ) ) |
45 |
40
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝑇 ) → sup ( ran 𝐹 , ℝ , < ) = ( 𝐹 ‘ 𝑥 ) ) |
46 |
44 45
|
breqtrrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑠 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑠 ) ≤ sup ( ran 𝐹 , ℝ , < ) ) |
47 |
46
|
ralrimiva |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) → ∀ 𝑠 ∈ 𝑇 ( 𝐹 ‘ 𝑠 ) ≤ sup ( ran 𝐹 , ℝ , < ) ) |
48 |
30
|
breq1d |
⊢ ( 𝑡 = 𝑠 → ( ( 𝐹 ‘ 𝑡 ) ≤ sup ( ran 𝐹 , ℝ , < ) ↔ ( 𝐹 ‘ 𝑠 ) ≤ sup ( ran 𝐹 , ℝ , < ) ) ) |
49 |
48
|
cbvralvw |
⊢ ( ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ sup ( ran 𝐹 , ℝ , < ) ↔ ∀ 𝑠 ∈ 𝑇 ( 𝐹 ‘ 𝑠 ) ≤ sup ( ran 𝐹 , ℝ , < ) ) |
50 |
47 49
|
sylibr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) → ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ sup ( ran 𝐹 , ℝ , < ) ) |
51 |
41 42 50
|
3jca |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) → ( sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ∧ sup ( ran 𝐹 , ℝ , < ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ sup ( ran 𝐹 , ℝ , < ) ) ) |
52 |
6 51
|
rexlimddv |
⊢ ( 𝜑 → ( sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ∧ sup ( ran 𝐹 , ℝ , < ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) ≤ sup ( ran 𝐹 , ℝ , < ) ) ) |