Step |
Hyp |
Ref |
Expression |
1 |
|
evth2f.1 |
⊢ Ⅎ 𝑥 𝐹 |
2 |
|
evth2f.2 |
⊢ Ⅎ 𝑦 𝐹 |
3 |
|
evth2f.3 |
⊢ Ⅎ 𝑥 𝑋 |
4 |
|
evth2f.4 |
⊢ Ⅎ 𝑦 𝑋 |
5 |
|
evth2f.5 |
⊢ 𝑋 = ∪ 𝐽 |
6 |
|
evth2f.6 |
⊢ 𝐾 = ( topGen ‘ ran (,) ) |
7 |
|
evth2f.7 |
⊢ ( 𝜑 → 𝐽 ∈ Comp ) |
8 |
|
evth2f.8 |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) |
9 |
|
evth2f.9 |
⊢ ( 𝜑 → 𝑋 ≠ ∅ ) |
10 |
5 6 7 8 9
|
evth2 |
⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( 𝐹 ‘ 𝑎 ) ≤ ( 𝐹 ‘ 𝑏 ) ) |
11 |
|
nfcv |
⊢ Ⅎ 𝑎 𝑋 |
12 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑎 |
13 |
1 12
|
nffv |
⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑎 ) |
14 |
|
nfcv |
⊢ Ⅎ 𝑥 ≤ |
15 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑏 |
16 |
1 15
|
nffv |
⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑏 ) |
17 |
13 14 16
|
nfbr |
⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑎 ) ≤ ( 𝐹 ‘ 𝑏 ) |
18 |
3 17
|
nfralw |
⊢ Ⅎ 𝑥 ∀ 𝑏 ∈ 𝑋 ( 𝐹 ‘ 𝑎 ) ≤ ( 𝐹 ‘ 𝑏 ) |
19 |
|
nfv |
⊢ Ⅎ 𝑎 ∀ 𝑏 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑏 ) |
20 |
|
fveq2 |
⊢ ( 𝑎 = 𝑥 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑥 ) ) |
21 |
20
|
breq1d |
⊢ ( 𝑎 = 𝑥 → ( ( 𝐹 ‘ 𝑎 ) ≤ ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑏 ) ) ) |
22 |
21
|
ralbidv |
⊢ ( 𝑎 = 𝑥 → ( ∀ 𝑏 ∈ 𝑋 ( 𝐹 ‘ 𝑎 ) ≤ ( 𝐹 ‘ 𝑏 ) ↔ ∀ 𝑏 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑏 ) ) ) |
23 |
11 3 18 19 22
|
cbvrexfw |
⊢ ( ∃ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( 𝐹 ‘ 𝑎 ) ≤ ( 𝐹 ‘ 𝑏 ) ↔ ∃ 𝑥 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑏 ) ) |
24 |
|
nfcv |
⊢ Ⅎ 𝑏 𝑋 |
25 |
|
nfcv |
⊢ Ⅎ 𝑦 𝑥 |
26 |
2 25
|
nffv |
⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑥 ) |
27 |
|
nfcv |
⊢ Ⅎ 𝑦 ≤ |
28 |
|
nfcv |
⊢ Ⅎ 𝑦 𝑏 |
29 |
2 28
|
nffv |
⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑏 ) |
30 |
26 27 29
|
nfbr |
⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑏 ) |
31 |
|
nfv |
⊢ Ⅎ 𝑏 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) |
32 |
|
fveq2 |
⊢ ( 𝑏 = 𝑦 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑦 ) ) |
33 |
32
|
breq2d |
⊢ ( 𝑏 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) |
34 |
24 4 30 31 33
|
cbvralfw |
⊢ ( ∀ 𝑏 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑏 ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) |
35 |
34
|
rexbii |
⊢ ( ∃ 𝑥 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑏 ) ↔ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) |
36 |
23 35
|
bitri |
⊢ ( ∃ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( 𝐹 ‘ 𝑎 ) ≤ ( 𝐹 ‘ 𝑏 ) ↔ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) |
37 |
10 36
|
sylib |
⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) |