Proof of Theorem iinhoiicclem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | iinhoiicclem.f | . . . 4
⊢ (𝜑 → 𝐹 ∈ ∩
𝑛 ∈ ℕ X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + (1 / 𝑛)))) | 
| 2 | 1 | elexd 3504 | . . 3
⊢ (𝜑 → 𝐹 ∈ V) | 
| 3 |  | 1nn 12277 | . . . . . . . . 9
⊢ 1 ∈
ℕ | 
| 4 | 3 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 1 ∈
ℕ) | 
| 5 |  | iinhoiicclem.k | . . . . . . . . 9
⊢
Ⅎ𝑘𝜑 | 
| 6 |  | iinhoiicclem.a | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) | 
| 7 |  | iinhoiicclem.b | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ) | 
| 8 |  | peano2re 11434 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ → (𝐵 + 1) ∈
ℝ) | 
| 9 | 7, 8 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵 + 1) ∈ ℝ) | 
| 10 | 9 | rexrd 11311 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵 + 1) ∈
ℝ*) | 
| 11 |  | icossre 13468 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 + 1) ∈
ℝ*) → (𝐴[,)(𝐵 + 1)) ⊆ ℝ) | 
| 12 | 6, 10, 11 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴[,)(𝐵 + 1)) ⊆ ℝ) | 
| 13 | 5, 12 | ixpssixp 45097 | . . . . . . . 8
⊢ (𝜑 → X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + 1)) ⊆ X𝑘 ∈ 𝑋 ℝ) | 
| 14 |  | oveq2 7439 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → (1 / 𝑛) = (1 / 1)) | 
| 15 |  | 1div1e1 11958 | . . . . . . . . . . . . . . 15
⊢ (1 / 1) =
1 | 
| 16 | 15 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → (1 / 1) =
1) | 
| 17 | 14, 16 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ (𝑛 = 1 → (1 / 𝑛) = 1) | 
| 18 | 17 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑛 = 1 → (𝐵 + (1 / 𝑛)) = (𝐵 + 1)) | 
| 19 | 18 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (𝑛 = 1 → (𝐴[,)(𝐵 + (1 / 𝑛))) = (𝐴[,)(𝐵 + 1))) | 
| 20 | 19 | ixpeq2dv 8953 | . . . . . . . . . 10
⊢ (𝑛 = 1 → X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) = X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) | 
| 21 | 20 | sseq1d 4015 | . . . . . . . . 9
⊢ (𝑛 = 1 → (X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 ℝ ↔ X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + 1)) ⊆ X𝑘 ∈ 𝑋 ℝ)) | 
| 22 | 21 | rspcev 3622 | . . . . . . . 8
⊢ ((1
∈ ℕ ∧ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1)) ⊆ X𝑘 ∈ 𝑋 ℝ) → ∃𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 ℝ) | 
| 23 | 4, 13, 22 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ∃𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 ℝ) | 
| 24 |  | iinss 5056 | . . . . . . 7
⊢
(∃𝑛 ∈
ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 ℝ → ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 ℝ) | 
| 25 | 23, 24 | syl 17 | . . . . . 6
⊢ (𝜑 → ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 ℝ) | 
| 26 | 25, 1 | sseldd 3984 | . . . . 5
⊢ (𝜑 → 𝐹 ∈ X𝑘 ∈ 𝑋 ℝ) | 
| 27 |  | elixpconstg 45094 | . . . . . 6
⊢ (𝐹 ∈ ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) → (𝐹 ∈ X𝑘 ∈ 𝑋 ℝ ↔ 𝐹:𝑋⟶ℝ)) | 
| 28 | 1, 27 | syl 17 | . . . . 5
⊢ (𝜑 → (𝐹 ∈ X𝑘 ∈ 𝑋 ℝ ↔ 𝐹:𝑋⟶ℝ)) | 
| 29 | 26, 28 | mpbid 232 | . . . 4
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) | 
| 30 | 29 | ffnd 6737 | . . 3
⊢ (𝜑 → 𝐹 Fn 𝑋) | 
| 31 | 29 | ffvelcdmda 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ ℝ) | 
| 32 | 6 | rexrd 11311 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈
ℝ*) | 
| 33 |  | ssid 4006 | . . . . . . . . . . . . 13
⊢ X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + 1)) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1)) | 
| 34 | 33 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + 1)) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) | 
| 35 | 20 | sseq1d 4015 | . . . . . . . . . . . . 13
⊢ (𝑛 = 1 → (X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1)) ↔ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1)) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1)))) | 
| 36 | 35 | rspcev 3622 | . . . . . . . . . . . 12
⊢ ((1
∈ ℕ ∧ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1)) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) → ∃𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) | 
| 37 | 4, 34, 36 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → ∃𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) | 
| 38 |  | iinss 5056 | . . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1)) → ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) | 
| 39 | 37, 38 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) | 
| 40 | 39, 1 | sseldd 3984 | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) | 
| 41 | 40 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + 1))) | 
| 42 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) | 
| 43 |  | fvixp2 45204 | . . . . . . . 8
⊢ ((𝐹 ∈ X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + 1)) ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + 1))) | 
| 44 | 41, 42, 43 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + 1))) | 
| 45 |  | icogelb 13438 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 + 1) ∈
ℝ* ∧ (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + 1))) → 𝐴 ≤ (𝐹‘𝑘)) | 
| 46 | 32, 10, 44, 45 | syl3anc 1373 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ≤ (𝐹‘𝑘)) | 
| 47 | 31 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) | 
| 48 | 7 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℝ) | 
| 49 |  | nnrecre 12308 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) | 
| 50 | 49 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈
ℝ) | 
| 51 | 48, 50 | readdcld 11290 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (𝐵 + (1 / 𝑛)) ∈ ℝ) | 
| 52 | 32 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → 𝐴 ∈
ℝ*) | 
| 53 |  | ressxr 11305 | . . . . . . . . . . 11
⊢ ℝ
⊆ ℝ* | 
| 54 | 53, 51 | sselid 3981 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (𝐵 + (1 / 𝑛)) ∈
ℝ*) | 
| 55 |  | eliin 4996 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ V → (𝐹 ∈ ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ↔ ∀𝑛 ∈ ℕ 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))))) | 
| 56 | 2, 55 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 ∈ ∩
𝑛 ∈ ℕ X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ↔ ∀𝑛 ∈ ℕ 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))))) | 
| 57 | 1, 56 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑛 ∈ ℕ 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛)))) | 
| 58 | 57 | r19.21bi 3251 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛)))) | 
| 59 |  | elixp2 8941 | . . . . . . . . . . . . . 14
⊢ (𝐹 ∈ X𝑘 ∈
𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + (1 / 𝑛))))) | 
| 60 | 58, 59 | sylib 218 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + (1 / 𝑛))))) | 
| 61 | 60 | simp3d 1145 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + (1 / 𝑛)))) | 
| 62 | 61 | r19.21bi 3251 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + (1 / 𝑛)))) | 
| 63 | 62 | an32s 652 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + (1 / 𝑛)))) | 
| 64 |  | icoltub 45521 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 + (1 / 𝑛)) ∈ ℝ*
∧ (𝐹‘𝑘) ∈ (𝐴[,)(𝐵 + (1 / 𝑛)))) → (𝐹‘𝑘) < (𝐵 + (1 / 𝑛))) | 
| 65 | 52, 54, 63, 64 | syl3anc 1373 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑘) < (𝐵 + (1 / 𝑛))) | 
| 66 | 47, 51, 65 | ltled 11409 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑘) ≤ (𝐵 + (1 / 𝑛))) | 
| 67 | 66 | ralrimiva 3146 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ∀𝑛 ∈ ℕ (𝐹‘𝑘) ≤ (𝐵 + (1 / 𝑛))) | 
| 68 |  | nfv 1914 | . . . . . . . 8
⊢
Ⅎ𝑛(𝜑 ∧ 𝑘 ∈ 𝑋) | 
| 69 | 53, 31 | sselid 3981 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈
ℝ*) | 
| 70 | 68, 69, 7 | xrralrecnnle 45394 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐹‘𝑘) ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (𝐹‘𝑘) ≤ (𝐵 + (1 / 𝑛)))) | 
| 71 | 67, 70 | mpbird 257 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ≤ 𝐵) | 
| 72 | 6, 7, 31, 46, 71 | eliccd 45517 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐹‘𝑘) ∈ (𝐴[,]𝐵)) | 
| 73 | 72 | ex 412 | . . . 4
⊢ (𝜑 → (𝑘 ∈ 𝑋 → (𝐹‘𝑘) ∈ (𝐴[,]𝐵))) | 
| 74 | 5, 73 | ralrimi 3257 | . . 3
⊢ (𝜑 → ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ (𝐴[,]𝐵)) | 
| 75 | 2, 30, 74 | 3jca 1129 | . 2
⊢ (𝜑 → (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ (𝐴[,]𝐵))) | 
| 76 |  | elixp2 8941 | . 2
⊢ (𝐹 ∈ X𝑘 ∈
𝑋 (𝐴[,]𝐵) ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝐹‘𝑘) ∈ (𝐴[,]𝐵))) | 
| 77 | 75, 76 | sylibr 234 | 1
⊢ (𝜑 → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,]𝐵)) |