Step | Hyp | Ref
| Expression |
1 | | nnn0 39595 |
. . . . . 6
⊢ ℕ
≠ ∅ |
2 | | iunconst 4529 |
. . . . . 6
⊢ (ℕ
≠ ∅ → ∪ 𝑛 ∈ ℕ {∅} =
{∅}) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ ∪ 𝑛 ∈ ℕ {∅} =
{∅} |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝑋 = ∅ → ∪ 𝑛 ∈ ℕ {∅} =
{∅}) |
5 | | ixpeq1 7919 |
. . . . . . 7
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = X𝑘 ∈ ∅ ((𝐴 + (1 / 𝑛))[,)𝐵)) |
6 | | ixp0x 7936 |
. . . . . . . 8
⊢ X𝑘 ∈
∅ ((𝐴 + (1 / 𝑛))[,)𝐵) = {∅} |
7 | 6 | a1i 11 |
. . . . . . 7
⊢ (𝑋 = ∅ → X𝑘 ∈
∅ ((𝐴 + (1 / 𝑛))[,)𝐵) = {∅}) |
8 | 5, 7 | eqtrd 2656 |
. . . . . 6
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = {∅}) |
9 | 8 | adantr 481 |
. . . . 5
⊢ ((𝑋 = ∅ ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = {∅}) |
10 | 9 | iuneq2dv 4542 |
. . . 4
⊢ (𝑋 = ∅ → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = ∪
𝑛 ∈ ℕ
{∅}) |
11 | | ixpeq1 7919 |
. . . . 5
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 (𝐴(,)𝐵) = X𝑘 ∈ ∅ (𝐴(,)𝐵)) |
12 | | ixp0x 7936 |
. . . . . 6
⊢ X𝑘 ∈
∅ (𝐴(,)𝐵) = {∅} |
13 | 12 | a1i 11 |
. . . . 5
⊢ (𝑋 = ∅ → X𝑘 ∈
∅ (𝐴(,)𝐵) = {∅}) |
14 | 11, 13 | eqtrd 2656 |
. . . 4
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 (𝐴(,)𝐵) = {∅}) |
15 | 4, 10, 14 | 3eqtr4d 2666 |
. . 3
⊢ (𝑋 = ∅ → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
16 | 15 | adantl 482 |
. 2
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
17 | | iunhoiioo.k |
. . . . . . . 8
⊢
Ⅎ𝑘𝜑 |
18 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑘 𝑛 ∈ ℕ |
19 | 17, 18 | nfan 1828 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ 𝑛 ∈ ℕ) |
20 | | iunhoiioo.a |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) |
21 | 20 | rexrd 10089 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈
ℝ*) |
22 | 21 | adantlr 751 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈
ℝ*) |
23 | | iunhoiioo.b |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈
ℝ*) |
24 | 23 | adantlr 751 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈
ℝ*) |
25 | 20 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) |
26 | | nnrp 11842 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
27 | 26 | ad2antlr 763 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝑛 ∈ ℝ+) |
28 | 27 | rpreccld 11882 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈
ℝ+) |
29 | 25, 28 | ltaddrpd 11905 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐴 < (𝐴 + (1 / 𝑛))) |
30 | | xrleid 11983 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ*
→ 𝐵 ≤ 𝐵) |
31 | 23, 30 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ≤ 𝐵) |
32 | 31 | adantlr 751 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐵 ≤ 𝐵) |
33 | | icossioo 12264 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < (𝐴 + (1 / 𝑛)) ∧ 𝐵 ≤ 𝐵)) → ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ (𝐴(,)𝐵)) |
34 | 22, 24, 29, 32, 33 | syl22anc 1327 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ (𝐴(,)𝐵)) |
35 | 19, 34 | ixpssixp 39269 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
36 | 35 | ralrimiva 2966 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
37 | | iunss 4561 |
. . . . 5
⊢ (∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ X𝑘 ∈ 𝑋 (𝐴(,)𝐵) ↔ ∀𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
38 | 36, 37 | sylibr 224 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
39 | 38 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
40 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑘 ¬ 𝑋 = ∅ |
41 | 17, 40 | nfan 1828 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ ¬ 𝑋 = ∅) |
42 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑘𝑓 |
43 | | nfixp1 7928 |
. . . . . . . 8
⊢
Ⅎ𝑘X𝑘 ∈
𝑋 (𝐴(,)𝐵) |
44 | 42, 43 | nfel 2777 |
. . . . . . 7
⊢
Ⅎ𝑘 𝑓 ∈ X𝑘 ∈
𝑋 (𝐴(,)𝐵) |
45 | 41, 44 | nfan 1828 |
. . . . . 6
⊢
Ⅎ𝑘((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
46 | | iunhoiioo.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ Fin) |
47 | 46 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) → 𝑋 ∈ Fin) |
48 | | neqne 2802 |
. . . . . . 7
⊢ (¬
𝑋 = ∅ → 𝑋 ≠ ∅) |
49 | 48 | ad2antlr 763 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) → 𝑋 ≠ ∅) |
50 | 20 | ad4ant14 1293 |
. . . . . 6
⊢ ((((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) |
51 | 23 | ad4ant14 1293 |
. . . . . 6
⊢ ((((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈
ℝ*) |
52 | | simpr 477 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) → 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
53 | | eqid 2622 |
. . . . . 6
⊢ inf(ran
(𝑘 ∈ 𝑋 ↦ ((𝑓‘𝑘) − 𝐴)), ℝ, < ) = inf(ran (𝑘 ∈ 𝑋 ↦ ((𝑓‘𝑘) − 𝐴)), ℝ, < ) |
54 | 45, 47, 49, 50, 51, 52, 53 | iunhoiioolem 40889 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) → 𝑓 ∈ ∪
𝑛 ∈ ℕ X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵)) |
55 | 54 | ralrimiva 2966 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∀𝑓 ∈ X
𝑘 ∈ 𝑋 (𝐴(,)𝐵)𝑓 ∈ ∪
𝑛 ∈ ℕ X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵)) |
56 | | dfss3 3592 |
. . . 4
⊢ (X𝑘 ∈
𝑋 (𝐴(,)𝐵) ⊆ ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ↔ ∀𝑓 ∈ X 𝑘 ∈ 𝑋 (𝐴(,)𝐵)𝑓 ∈ ∪
𝑛 ∈ ℕ X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵)) |
57 | 55, 56 | sylibr 224 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → X𝑘 ∈
𝑋 (𝐴(,)𝐵) ⊆ ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵)) |
58 | 39, 57 | eqssd 3620 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
59 | 16, 58 | pm2.61dan 832 |
1
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |