Step |
Hyp |
Ref |
Expression |
1 |
|
infrpgernmpt.x |
⊢ Ⅎ 𝑥 𝜑 |
2 |
|
infrpgernmpt.a |
⊢ ( 𝜑 → 𝐴 ≠ ∅ ) |
3 |
|
infrpgernmpt.b |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* ) |
4 |
|
infrpgernmpt.y |
⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ) |
5 |
|
infrpgernmpt.c |
⊢ ( 𝜑 → 𝐶 ∈ ℝ+ ) |
6 |
|
nfv |
⊢ Ⅎ 𝑤 𝜑 |
7 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
8 |
1 7 3
|
rnmptssd |
⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ* ) |
9 |
1 3 7 2
|
rnmptn0 |
⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ ) |
10 |
|
breq1 |
⊢ ( 𝑦 = 𝑤 → ( 𝑦 ≤ 𝐵 ↔ 𝑤 ≤ 𝐵 ) ) |
11 |
10
|
ralbidv |
⊢ ( 𝑦 = 𝑤 → ( ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 ) ) |
12 |
11
|
cbvrexvw |
⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 ) |
13 |
4 12
|
sylib |
⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 ) |
14 |
13
|
rnmptlb |
⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑧 ) |
15 |
6 8 9 14 5
|
infrpge |
⊢ ( 𝜑 → ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) |
16 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → 𝜑 ) |
17 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) |
18 |
|
vex |
⊢ 𝑤 ∈ V |
19 |
7
|
elrnmpt |
⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 ) ) |
20 |
18 19
|
ax-mp |
⊢ ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 ) |
21 |
20
|
biimpi |
⊢ ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 ) |
22 |
21
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 ) |
23 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑤 |
24 |
|
nfcv |
⊢ Ⅎ 𝑥 ≤ |
25 |
|
nfmpt1 |
⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
26 |
25
|
nfrn |
⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
27 |
|
nfcv |
⊢ Ⅎ 𝑥 ℝ* |
28 |
|
nfcv |
⊢ Ⅎ 𝑥 < |
29 |
26 27 28
|
nfinf |
⊢ Ⅎ 𝑥 inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) |
30 |
|
nfcv |
⊢ Ⅎ 𝑥 +𝑒 |
31 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐶 |
32 |
29 30 31
|
nfov |
⊢ Ⅎ 𝑥 ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) |
33 |
23 24 32
|
nfbr |
⊢ Ⅎ 𝑥 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) |
34 |
1 33
|
nfan |
⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) |
35 |
|
id |
⊢ ( 𝑤 = 𝐵 → 𝑤 = 𝐵 ) |
36 |
35
|
eqcomd |
⊢ ( 𝑤 = 𝐵 → 𝐵 = 𝑤 ) |
37 |
36
|
adantl |
⊢ ( ( 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ∧ 𝑤 = 𝐵 ) → 𝐵 = 𝑤 ) |
38 |
|
simpl |
⊢ ( ( 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ∧ 𝑤 = 𝐵 ) → 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) |
39 |
37 38
|
eqbrtrd |
⊢ ( ( 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ∧ 𝑤 = 𝐵 ) → 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) |
40 |
39
|
ex |
⊢ ( 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) → ( 𝑤 = 𝐵 → 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) ) |
41 |
40
|
a1d |
⊢ ( 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) → ( 𝑥 ∈ 𝐴 → ( 𝑤 = 𝐵 → 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) ) ) |
42 |
41
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → ( 𝑥 ∈ 𝐴 → ( 𝑤 = 𝐵 → 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) ) ) |
43 |
34 42
|
reximdai |
⊢ ( ( 𝜑 ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → ( ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) ) |
44 |
43
|
imp |
⊢ ( ( ( 𝜑 ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) ∧ ∃ 𝑥 ∈ 𝐴 𝑤 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) |
45 |
16 17 22 44
|
syl21anc |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) |
46 |
45
|
rexlimdva2 |
⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) ) |
47 |
15 46
|
mpd |
⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝐵 ≤ ( inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) +𝑒 𝐶 ) ) |