| Step | Hyp | Ref
| Expression |
| 1 | | nnn0 45389 |
. . . . . 6
⊢ ℕ
≠ ∅ |
| 2 | | iunconst 5001 |
. . . . . 6
⊢ (ℕ
≠ ∅ → ∪ 𝑛 ∈ ℕ {∅} =
{∅}) |
| 3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ ∪ 𝑛 ∈ ℕ {∅} =
{∅} |
| 4 | 3 | a1i 11 |
. . . 4
⊢ (𝑋 = ∅ → ∪ 𝑛 ∈ ℕ {∅} =
{∅}) |
| 5 | | ixpeq1 8948 |
. . . . . . 7
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = X𝑘 ∈ ∅ ((𝐴 + (1 / 𝑛))[,)𝐵)) |
| 6 | | ixp0x 8966 |
. . . . . . . 8
⊢ X𝑘 ∈
∅ ((𝐴 + (1 / 𝑛))[,)𝐵) = {∅} |
| 7 | 6 | a1i 11 |
. . . . . . 7
⊢ (𝑋 = ∅ → X𝑘 ∈
∅ ((𝐴 + (1 / 𝑛))[,)𝐵) = {∅}) |
| 8 | 5, 7 | eqtrd 2777 |
. . . . . 6
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = {∅}) |
| 9 | 8 | adantr 480 |
. . . . 5
⊢ ((𝑋 = ∅ ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = {∅}) |
| 10 | 9 | iuneq2dv 5016 |
. . . 4
⊢ (𝑋 = ∅ → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = ∪
𝑛 ∈ ℕ
{∅}) |
| 11 | | ixpeq1 8948 |
. . . . 5
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 (𝐴(,)𝐵) = X𝑘 ∈ ∅ (𝐴(,)𝐵)) |
| 12 | | ixp0x 8966 |
. . . . . 6
⊢ X𝑘 ∈
∅ (𝐴(,)𝐵) = {∅} |
| 13 | 12 | a1i 11 |
. . . . 5
⊢ (𝑋 = ∅ → X𝑘 ∈
∅ (𝐴(,)𝐵) = {∅}) |
| 14 | 11, 13 | eqtrd 2777 |
. . . 4
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 (𝐴(,)𝐵) = {∅}) |
| 15 | 4, 10, 14 | 3eqtr4d 2787 |
. . 3
⊢ (𝑋 = ∅ → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
| 16 | 15 | adantl 481 |
. 2
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
| 17 | | iunhoiioo.k |
. . . . . . . 8
⊢
Ⅎ𝑘𝜑 |
| 18 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑘 𝑛 ∈ ℕ |
| 19 | 17, 18 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ 𝑛 ∈ ℕ) |
| 20 | | iunhoiioo.a |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) |
| 21 | 20 | rexrd 11311 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈
ℝ*) |
| 22 | 21 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈
ℝ*) |
| 23 | | iunhoiioo.b |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈
ℝ*) |
| 24 | 23 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈
ℝ*) |
| 25 | 20 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) |
| 26 | | nnrp 13046 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
| 27 | 26 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝑛 ∈ ℝ+) |
| 28 | 27 | rpreccld 13087 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈
ℝ+) |
| 29 | 25, 28 | ltaddrpd 13110 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐴 < (𝐴 + (1 / 𝑛))) |
| 30 | 23 | xrleidd 13194 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ≤ 𝐵) |
| 31 | 30 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝐵 ≤ 𝐵) |
| 32 | | icossioo 13480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 < (𝐴 + (1 / 𝑛)) ∧ 𝐵 ≤ 𝐵)) → ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ (𝐴(,)𝐵)) |
| 33 | 22, 24, 29, 31, 32 | syl22anc 839 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ (𝐴(,)𝐵)) |
| 34 | 19, 33 | ixpssixp 45097 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
| 35 | 34 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
| 36 | | iunss 5045 |
. . . . 5
⊢ (∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ X𝑘 ∈ 𝑋 (𝐴(,)𝐵) ↔ ∀𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
| 37 | 35, 36 | sylibr 234 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
| 38 | 37 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) ⊆ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
| 39 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑘 ¬ 𝑋 = ∅ |
| 40 | 17, 39 | nfan 1899 |
. . . . 5
⊢
Ⅎ𝑘(𝜑 ∧ ¬ 𝑋 = ∅) |
| 41 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑘𝑓 |
| 42 | | nfixp1 8958 |
. . . . . 6
⊢
Ⅎ𝑘X𝑘 ∈
𝑋 (𝐴(,)𝐵) |
| 43 | 41, 42 | nfel 2920 |
. . . . 5
⊢
Ⅎ𝑘 𝑓 ∈ X𝑘 ∈
𝑋 (𝐴(,)𝐵) |
| 44 | 40, 43 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑘((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
| 45 | | iunhoiioo.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) |
| 46 | 45 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) → 𝑋 ∈ Fin) |
| 47 | | neqne 2948 |
. . . . 5
⊢ (¬
𝑋 = ∅ → 𝑋 ≠ ∅) |
| 48 | 47 | ad2antlr 727 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) → 𝑋 ≠ ∅) |
| 49 | 20 | ad4ant14 752 |
. . . 4
⊢ ((((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) |
| 50 | 23 | ad4ant14 752 |
. . . 4
⊢ ((((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈
ℝ*) |
| 51 | | simpr 484 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) → 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
| 52 | | eqid 2737 |
. . . 4
⊢ inf(ran
(𝑘 ∈ 𝑋 ↦ ((𝑓‘𝑘) − 𝐴)), ℝ, < ) = inf(ran (𝑘 ∈ 𝑋 ↦ ((𝑓‘𝑘) − 𝐴)), ℝ, < ) |
| 53 | 44, 46, 48, 49, 50, 51, 52 | iunhoiioolem 46690 |
. . 3
⊢ (((𝜑 ∧ ¬ 𝑋 = ∅) ∧ 𝑓 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) → 𝑓 ∈ ∪
𝑛 ∈ ℕ X𝑘 ∈
𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵)) |
| 54 | 38, 53 | eqelssd 4005 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |
| 55 | 16, 54 | pm2.61dan 813 |
1
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) |