Proof of Theorem ioorrnopnxrlem
| Step | Hyp | Ref
| Expression |
| 1 | | ioorrnopnxrlem.v |
. . . 4
⊢ 𝑉 = X𝑖 ∈ 𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖)) |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑉 = X𝑖 ∈ 𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖))) |
| 3 | | ioorrnopnxrlem.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ Fin) |
| 4 | | iftrue 4531 |
. . . . . . . 8
⊢ ((𝐴‘𝑖) = -∞ → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) = ((𝐹‘𝑖) − 1)) |
| 5 | 4 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) = ((𝐹‘𝑖) − 1)) |
| 6 | | ioorrnopnxrlem.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
| 7 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
| 8 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
| 9 | | fvixp2 45204 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
| 10 | 7, 8, 9 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
| 11 | 10 | elioored 45562 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ℝ) |
| 12 | | 1red 11262 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 1 ∈ ℝ) |
| 13 | 11, 12 | resubcld 11691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − 1) ∈ ℝ) |
| 14 | 13 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → ((𝐹‘𝑖) − 1) ∈ ℝ) |
| 15 | 5, 14 | eqeltrd 2841 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) ∈ ℝ) |
| 16 | | iffalse 4534 |
. . . . . . . 8
⊢ (¬
(𝐴‘𝑖) = -∞ → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) = (𝐴‘𝑖)) |
| 17 | 16 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) = (𝐴‘𝑖)) |
| 18 | | neqne 2948 |
. . . . . . . . 9
⊢ (¬
(𝐴‘𝑖) = -∞ → (𝐴‘𝑖) ≠ -∞) |
| 19 | 18 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) ≠ -∞) |
| 20 | | ioorrnopnxrlem.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴:𝑋⟶ℝ*) |
| 21 | 20 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈
ℝ*) |
| 22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) ≠ -∞) → (𝐴‘𝑖) ∈
ℝ*) |
| 23 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) ≠ -∞) → (𝐴‘𝑖) ≠ -∞) |
| 24 | | pnfxr 11315 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
| 25 | 24 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → +∞ ∈
ℝ*) |
| 26 | 11 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈
ℝ*) |
| 27 | | ioorrnopnxrlem.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵:𝑋⟶ℝ*) |
| 28 | 27 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈
ℝ*) |
| 29 | | ioogtlb 45508 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘𝑖) ∈ ℝ* ∧ (𝐵‘𝑖) ∈ ℝ* ∧ (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → (𝐴‘𝑖) < (𝐹‘𝑖)) |
| 30 | 21, 28, 10, 29 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) < (𝐹‘𝑖)) |
| 31 | 11 | ltpnfd 13163 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) < +∞) |
| 32 | 21, 26, 25, 30, 31 | xrlttrd 13201 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) < +∞) |
| 33 | 21, 25, 32 | xrltned 45368 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≠ +∞) |
| 34 | 33 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) ≠ -∞) → (𝐴‘𝑖) ≠ +∞) |
| 35 | 22, 23, 34 | xrred 45376 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) ≠ -∞) → (𝐴‘𝑖) ∈ ℝ) |
| 36 | 19, 35 | syldan 591 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) ∈ ℝ) |
| 37 | 17, 36 | eqeltrd 2841 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) ∈ ℝ) |
| 38 | 15, 37 | pm2.61dan 813 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) ∈ ℝ) |
| 39 | | ioorrnopnxrlem.l |
. . . . 5
⊢ 𝐿 = (𝑖 ∈ 𝑋 ↦ if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖))) |
| 40 | 38, 39 | fmptd 7134 |
. . . 4
⊢ (𝜑 → 𝐿:𝑋⟶ℝ) |
| 41 | | iftrue 4531 |
. . . . . . . 8
⊢ ((𝐵‘𝑖) = +∞ → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) = ((𝐹‘𝑖) + 1)) |
| 42 | 41 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) = ((𝐹‘𝑖) + 1)) |
| 43 | 11, 12 | readdcld 11290 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) + 1) ∈ ℝ) |
| 44 | 43 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → ((𝐹‘𝑖) + 1) ∈ ℝ) |
| 45 | 42, 44 | eqeltrd 2841 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) ∈ ℝ) |
| 46 | | iffalse 4534 |
. . . . . . . 8
⊢ (¬
(𝐵‘𝑖) = +∞ → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) = (𝐵‘𝑖)) |
| 47 | 46 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) = (𝐵‘𝑖)) |
| 48 | | neqne 2948 |
. . . . . . . . 9
⊢ (¬
(𝐵‘𝑖) = +∞ → (𝐵‘𝑖) ≠ +∞) |
| 49 | 48 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝐵‘𝑖) ≠ +∞) |
| 50 | 28 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) ≠ +∞) → (𝐵‘𝑖) ∈
ℝ*) |
| 51 | | mnfxr 11318 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
| 52 | 51 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → -∞ ∈
ℝ*) |
| 53 | 11 | mnfltd 13166 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → -∞ < (𝐹‘𝑖)) |
| 54 | | iooltub 45523 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘𝑖) ∈ ℝ* ∧ (𝐵‘𝑖) ∈ ℝ* ∧ (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → (𝐹‘𝑖) < (𝐵‘𝑖)) |
| 55 | 21, 28, 10, 54 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) < (𝐵‘𝑖)) |
| 56 | 52, 26, 28, 53, 55 | xrlttrd 13201 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → -∞ < (𝐵‘𝑖)) |
| 57 | 52, 28, 56 | xrgtned 45333 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ≠ -∞) |
| 58 | 57 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) ≠ +∞) → (𝐵‘𝑖) ≠ -∞) |
| 59 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) ≠ +∞) → (𝐵‘𝑖) ≠ +∞) |
| 60 | 50, 58, 59 | xrred 45376 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) ≠ +∞) → (𝐵‘𝑖) ∈ ℝ) |
| 61 | 49, 60 | syldan 591 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝐵‘𝑖) ∈ ℝ) |
| 62 | 47, 61 | eqeltrd 2841 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) ∈ ℝ) |
| 63 | 45, 62 | pm2.61dan 813 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) ∈ ℝ) |
| 64 | | ioorrnopnxrlem.r |
. . . . 5
⊢ 𝑅 = (𝑖 ∈ 𝑋 ↦ if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖))) |
| 65 | 63, 64 | fmptd 7134 |
. . . 4
⊢ (𝜑 → 𝑅:𝑋⟶ℝ) |
| 66 | 3, 40, 65 | ioorrnopn 46320 |
. . 3
⊢ (𝜑 → X𝑖 ∈
𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋))) |
| 67 | 2, 66 | eqeltrd 2841 |
. 2
⊢ (𝜑 → 𝑉 ∈ (TopOpen‘(ℝ^‘𝑋))) |
| 68 | 6 | elexd 3504 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ V) |
| 69 | | ixpfn 8943 |
. . . . . . 7
⊢ (𝐹 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) → 𝐹 Fn 𝑋) |
| 70 | 6, 69 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn 𝑋) |
| 71 | 40 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐿‘𝑖) ∈ ℝ) |
| 72 | 71 | rexrd 11311 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐿‘𝑖) ∈
ℝ*) |
| 73 | 65 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑅‘𝑖) ∈ ℝ) |
| 74 | 73 | rexrd 11311 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑅‘𝑖) ∈
ℝ*) |
| 75 | 39 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 = (𝑖 ∈ 𝑋 ↦ if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)))) |
| 76 | 38 | elexd 3504 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) ∈ V) |
| 77 | 75, 76 | fvmpt2d 7029 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐿‘𝑖) = if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖))) |
| 78 | 77 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐿‘𝑖) = if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖))) |
| 79 | 78, 5 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐿‘𝑖) = ((𝐹‘𝑖) − 1)) |
| 80 | 11 | ltm1d 12200 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − 1) < (𝐹‘𝑖)) |
| 81 | 80 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → ((𝐹‘𝑖) − 1) < (𝐹‘𝑖)) |
| 82 | 79, 81 | eqbrtrd 5165 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐿‘𝑖) < (𝐹‘𝑖)) |
| 83 | 77 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐿‘𝑖) = if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖))) |
| 84 | 83, 17 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐿‘𝑖) = (𝐴‘𝑖)) |
| 85 | 30 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) < (𝐹‘𝑖)) |
| 86 | 84, 85 | eqbrtrd 5165 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐿‘𝑖) < (𝐹‘𝑖)) |
| 87 | 82, 86 | pm2.61dan 813 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐿‘𝑖) < (𝐹‘𝑖)) |
| 88 | 11 | ltp1d 12198 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) < ((𝐹‘𝑖) + 1)) |
| 89 | 88 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝐹‘𝑖) < ((𝐹‘𝑖) + 1)) |
| 90 | 64 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 = (𝑖 ∈ 𝑋 ↦ if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)))) |
| 91 | 63 | elexd 3504 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) ∈ V) |
| 92 | 90, 91 | fvmpt2d 7029 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑅‘𝑖) = if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖))) |
| 93 | 92 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) = if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖))) |
| 94 | 93, 42 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) = ((𝐹‘𝑖) + 1)) |
| 95 | 94 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → ((𝐹‘𝑖) + 1) = (𝑅‘𝑖)) |
| 96 | 89, 95 | breqtrd 5169 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝐹‘𝑖) < (𝑅‘𝑖)) |
| 97 | 55 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝐹‘𝑖) < (𝐵‘𝑖)) |
| 98 | 92 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) = if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖))) |
| 99 | 98, 47 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) = (𝐵‘𝑖)) |
| 100 | 99 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝐵‘𝑖) = (𝑅‘𝑖)) |
| 101 | 97, 100 | breqtrd 5169 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝐹‘𝑖) < (𝑅‘𝑖)) |
| 102 | 96, 101 | pm2.61dan 813 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) < (𝑅‘𝑖)) |
| 103 | 72, 74, 11, 87, 102 | eliood 45511 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ((𝐿‘𝑖)(,)(𝑅‘𝑖))) |
| 104 | 103 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑖 ∈ 𝑋 (𝐹‘𝑖) ∈ ((𝐿‘𝑖)(,)(𝑅‘𝑖))) |
| 105 | 68, 70, 104 | 3jca 1129 |
. . . . 5
⊢ (𝜑 → (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝐹‘𝑖) ∈ ((𝐿‘𝑖)(,)(𝑅‘𝑖)))) |
| 106 | | elixp2 8941 |
. . . . 5
⊢ (𝐹 ∈ X𝑖 ∈
𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝐹‘𝑖) ∈ ((𝐿‘𝑖)(,)(𝑅‘𝑖)))) |
| 107 | 105, 106 | sylibr 234 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖))) |
| 108 | 107, 1 | eleqtrrdi 2852 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
| 109 | 21 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) ∈
ℝ*) |
| 110 | 72 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐿‘𝑖) ∈
ℝ*) |
| 111 | 15 | mnfltd 13166 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → -∞ < if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖))) |
| 112 | 111, 5 | breqtrd 5169 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → -∞ < ((𝐹‘𝑖) − 1)) |
| 113 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) = -∞) |
| 114 | 113, 79 | breq12d 5156 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → ((𝐴‘𝑖) < (𝐿‘𝑖) ↔ -∞ < ((𝐹‘𝑖) − 1))) |
| 115 | 112, 114 | mpbird 257 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) < (𝐿‘𝑖)) |
| 116 | 109, 110,
115 | xrltled 13192 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) ≤ (𝐿‘𝑖)) |
| 117 | 84 | eqcomd 2743 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) = (𝐿‘𝑖)) |
| 118 | 36, 117 | eqled 11364 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) ≤ (𝐿‘𝑖)) |
| 119 | 116, 118 | pm2.61dan 813 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ (𝐿‘𝑖)) |
| 120 | 74 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) ∈
ℝ*) |
| 121 | 28 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝐵‘𝑖) ∈
ℝ*) |
| 122 | 44 | ltpnfd 13163 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → ((𝐹‘𝑖) + 1) < +∞) |
| 123 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝐵‘𝑖) = +∞) |
| 124 | 94, 123 | breq12d 5156 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → ((𝑅‘𝑖) < (𝐵‘𝑖) ↔ ((𝐹‘𝑖) + 1) < +∞)) |
| 125 | 122, 124 | mpbird 257 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) < (𝐵‘𝑖)) |
| 126 | 120, 121,
125 | xrltled 13192 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) ≤ (𝐵‘𝑖)) |
| 127 | 73 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) ∈ ℝ) |
| 128 | 127, 99 | eqled 11364 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) ≤ (𝐵‘𝑖)) |
| 129 | 126, 128 | pm2.61dan 813 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑅‘𝑖) ≤ (𝐵‘𝑖)) |
| 130 | | ioossioo 13481 |
. . . . . . 7
⊢ ((((𝐴‘𝑖) ∈ ℝ* ∧ (𝐵‘𝑖) ∈ ℝ*) ∧ ((𝐴‘𝑖) ≤ (𝐿‘𝑖) ∧ (𝑅‘𝑖) ≤ (𝐵‘𝑖))) → ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ⊆ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
| 131 | 21, 28, 119, 129, 130 | syl22anc 839 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ⊆ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
| 132 | 131 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ⊆ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
| 133 | | ss2ixp 8950 |
. . . . 5
⊢
(∀𝑖 ∈
𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ⊆ ((𝐴‘𝑖)(,)(𝐵‘𝑖)) → X𝑖 ∈ 𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
| 134 | 132, 133 | syl 17 |
. . . 4
⊢ (𝜑 → X𝑖 ∈
𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
| 135 | 2, 134 | eqsstrd 4018 |
. . 3
⊢ (𝜑 → 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
| 136 | 108, 135 | jca 511 |
. 2
⊢ (𝜑 → (𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
| 137 | | eleq2 2830 |
. . . 4
⊢ (𝑣 = 𝑉 → (𝐹 ∈ 𝑣 ↔ 𝐹 ∈ 𝑉)) |
| 138 | | sseq1 4009 |
. . . 4
⊢ (𝑣 = 𝑉 → (𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ↔ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
| 139 | 137, 138 | anbi12d 632 |
. . 3
⊢ (𝑣 = 𝑉 → ((𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) ↔ (𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))))) |
| 140 | 139 | rspcev 3622 |
. 2
⊢ ((𝑉 ∈
(TopOpen‘(ℝ^‘𝑋)) ∧ (𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
| 141 | 67, 136, 140 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |