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 4042 |
. . . . . . . 8
⊢ ((𝐴‘𝑖) = -∞ → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) = ((𝐹‘𝑖) − 1)) |
5 | 4 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) = ((𝐹‘𝑖) − 1)) |
6 | | ioossre 12106 |
. . . . . . . . . 10
⊢ ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ⊆ ℝ |
7 | | ioorrnopnxrlem.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
8 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
9 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
10 | | fvixp2 38384 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
11 | 8, 9, 10 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
12 | 6, 11 | sseldi 3566 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ℝ) |
13 | | 1red 9934 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 1 ∈ ℝ) |
14 | 12, 13 | resubcld 10337 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − 1) ∈ ℝ) |
15 | 14 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → ((𝐹‘𝑖) − 1) ∈ ℝ) |
16 | 5, 15 | eqeltrd 2688 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) ∈ ℝ) |
17 | | iffalse 4045 |
. . . . . . . 8
⊢ (¬
(𝐴‘𝑖) = -∞ → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) = (𝐴‘𝑖)) |
18 | 17 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) = (𝐴‘𝑖)) |
19 | | neqne 2790 |
. . . . . . . . 9
⊢ (¬
(𝐴‘𝑖) = -∞ → (𝐴‘𝑖) ≠ -∞) |
20 | 19 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) ≠ -∞) |
21 | | ioorrnopnxrlem.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴:𝑋⟶ℝ*) |
22 | 21 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈
ℝ*) |
23 | 22 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) ≠ -∞) → (𝐴‘𝑖) ∈
ℝ*) |
24 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) ≠ -∞) → (𝐴‘𝑖) ≠ -∞) |
25 | | pnfxr 9971 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
26 | 25 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → +∞ ∈
ℝ*) |
27 | 12 | rexrd 9968 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈
ℝ*) |
28 | | ioorrnopnxrlem.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵:𝑋⟶ℝ*) |
29 | 28 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈
ℝ*) |
30 | | ioogtlb 38564 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘𝑖) ∈ ℝ* ∧ (𝐵‘𝑖) ∈ ℝ* ∧ (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → (𝐴‘𝑖) < (𝐹‘𝑖)) |
31 | 22, 29, 11, 30 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) < (𝐹‘𝑖)) |
32 | 12 | ltpnfd 11831 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) < +∞) |
33 | 22, 27, 26, 31, 32 | xrlttrd 11866 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) < +∞) |
34 | 22, 26, 33 | xrltned 38514 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≠ +∞) |
35 | 34 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) ≠ -∞) → (𝐴‘𝑖) ≠ +∞) |
36 | 23, 24, 35 | xrred 38522 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) ≠ -∞) → (𝐴‘𝑖) ∈ ℝ) |
37 | 20, 36 | syldan 486 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) ∈ ℝ) |
38 | 18, 37 | eqeltrd 2688 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) ∈ ℝ) |
39 | 16, 38 | pm2.61dan 828 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) ∈ ℝ) |
40 | | ioorrnopnxrlem.l |
. . . . 5
⊢ 𝐿 = (𝑖 ∈ 𝑋 ↦ if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖))) |
41 | 39, 40 | fmptd 6292 |
. . . 4
⊢ (𝜑 → 𝐿:𝑋⟶ℝ) |
42 | | iftrue 4042 |
. . . . . . . 8
⊢ ((𝐵‘𝑖) = +∞ → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) = ((𝐹‘𝑖) + 1)) |
43 | 42 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) = ((𝐹‘𝑖) + 1)) |
44 | 12, 13 | readdcld 9948 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) + 1) ∈ ℝ) |
45 | 44 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → ((𝐹‘𝑖) + 1) ∈ ℝ) |
46 | 43, 45 | eqeltrd 2688 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) ∈ ℝ) |
47 | | iffalse 4045 |
. . . . . . . 8
⊢ (¬
(𝐵‘𝑖) = +∞ → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) = (𝐵‘𝑖)) |
48 | 47 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) = (𝐵‘𝑖)) |
49 | | neqne 2790 |
. . . . . . . . 9
⊢ (¬
(𝐵‘𝑖) = +∞ → (𝐵‘𝑖) ≠ +∞) |
50 | 49 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝐵‘𝑖) ≠ +∞) |
51 | 29 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) ≠ +∞) → (𝐵‘𝑖) ∈
ℝ*) |
52 | | mnfxr 9975 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
53 | 52 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → -∞ ∈
ℝ*) |
54 | 12 | mnfltd 11834 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → -∞ < (𝐹‘𝑖)) |
55 | | iooltub 38582 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘𝑖) ∈ ℝ* ∧ (𝐵‘𝑖) ∈ ℝ* ∧ (𝐹‘𝑖) ∈ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → (𝐹‘𝑖) < (𝐵‘𝑖)) |
56 | 22, 29, 11, 55 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) < (𝐵‘𝑖)) |
57 | 53, 27, 29, 54, 56 | xrlttrd 11866 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → -∞ < (𝐵‘𝑖)) |
58 | 53, 29, 57 | xrgtned 38479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ≠ -∞) |
59 | 58 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) ≠ +∞) → (𝐵‘𝑖) ≠ -∞) |
60 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) ≠ +∞) → (𝐵‘𝑖) ≠ +∞) |
61 | 51, 59, 60 | xrred 38522 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) ≠ +∞) → (𝐵‘𝑖) ∈ ℝ) |
62 | 50, 61 | syldan 486 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝐵‘𝑖) ∈ ℝ) |
63 | 48, 62 | eqeltrd 2688 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) ∈ ℝ) |
64 | 46, 63 | pm2.61dan 828 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) ∈ ℝ) |
65 | | ioorrnopnxrlem.r |
. . . . 5
⊢ 𝑅 = (𝑖 ∈ 𝑋 ↦ if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖))) |
66 | 64, 65 | fmptd 6292 |
. . . 4
⊢ (𝜑 → 𝑅:𝑋⟶ℝ) |
67 | 3, 41, 66 | ioorrnopn 39201 |
. . 3
⊢ (𝜑 → X𝑖 ∈
𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋))) |
68 | 2, 67 | eqeltrd 2688 |
. 2
⊢ (𝜑 → 𝑉 ∈ (TopOpen‘(ℝ^‘𝑋))) |
69 | 7 | elexd 3187 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ V) |
70 | | ixpfn 7800 |
. . . . . . 7
⊢ (𝐹 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) → 𝐹 Fn 𝑋) |
71 | 7, 70 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn 𝑋) |
72 | 41 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐿‘𝑖) ∈ ℝ) |
73 | 72 | rexrd 9968 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐿‘𝑖) ∈
ℝ*) |
74 | 66 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑅‘𝑖) ∈ ℝ) |
75 | 74 | rexrd 9968 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑅‘𝑖) ∈
ℝ*) |
76 | 40 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 = (𝑖 ∈ 𝑋 ↦ if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)))) |
77 | 39 | elexd 3187 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖)) ∈ V) |
78 | 76, 77 | fvmpt2d 6202 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐿‘𝑖) = if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖))) |
79 | 78 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐿‘𝑖) = if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖))) |
80 | 79, 5 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐿‘𝑖) = ((𝐹‘𝑖) − 1)) |
81 | 12 | ltm1d 10835 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐹‘𝑖) − 1) < (𝐹‘𝑖)) |
82 | 81 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → ((𝐹‘𝑖) − 1) < (𝐹‘𝑖)) |
83 | 80, 82 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐿‘𝑖) < (𝐹‘𝑖)) |
84 | 78 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐿‘𝑖) = if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖))) |
85 | 84, 18 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐿‘𝑖) = (𝐴‘𝑖)) |
86 | 31 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) < (𝐹‘𝑖)) |
87 | 85, 86 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐿‘𝑖) < (𝐹‘𝑖)) |
88 | 83, 87 | pm2.61dan 828 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐿‘𝑖) < (𝐹‘𝑖)) |
89 | 12 | ltp1d 10833 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) < ((𝐹‘𝑖) + 1)) |
90 | 89 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝐹‘𝑖) < ((𝐹‘𝑖) + 1)) |
91 | 65 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 = (𝑖 ∈ 𝑋 ↦ if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)))) |
92 | 64 | elexd 3187 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖)) ∈ V) |
93 | 91, 92 | fvmpt2d 6202 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑅‘𝑖) = if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖))) |
94 | 93 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) = if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖))) |
95 | 94, 43 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) = ((𝐹‘𝑖) + 1)) |
96 | 95 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → ((𝐹‘𝑖) + 1) = (𝑅‘𝑖)) |
97 | 90, 96 | breqtrd 4609 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝐹‘𝑖) < (𝑅‘𝑖)) |
98 | 56 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝐹‘𝑖) < (𝐵‘𝑖)) |
99 | 93 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) = if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖))) |
100 | 99, 48 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) = (𝐵‘𝑖)) |
101 | 100 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝐵‘𝑖) = (𝑅‘𝑖)) |
102 | 98, 101 | breqtrd 4609 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝐹‘𝑖) < (𝑅‘𝑖)) |
103 | 97, 102 | pm2.61dan 828 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) < (𝑅‘𝑖)) |
104 | 73, 75, 12, 88, 103 | eliood 38567 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐹‘𝑖) ∈ ((𝐿‘𝑖)(,)(𝑅‘𝑖))) |
105 | 104 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑖 ∈ 𝑋 (𝐹‘𝑖) ∈ ((𝐿‘𝑖)(,)(𝑅‘𝑖))) |
106 | 69, 71, 105 | 3jca 1235 |
. . . . 5
⊢ (𝜑 → (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝐹‘𝑖) ∈ ((𝐿‘𝑖)(,)(𝑅‘𝑖)))) |
107 | | elixp2 7798 |
. . . . 5
⊢ (𝐹 ∈ X𝑖 ∈
𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝐹‘𝑖) ∈ ((𝐿‘𝑖)(,)(𝑅‘𝑖)))) |
108 | 106, 107 | sylibr 223 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖))) |
109 | 108, 1 | syl6eleqr 2699 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
110 | 22 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) ∈
ℝ*) |
111 | 73 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐿‘𝑖) ∈
ℝ*) |
112 | 16 | mnfltd 11834 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → -∞ < if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖))) |
113 | 112, 5 | breqtrd 4609 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → -∞ < ((𝐹‘𝑖) − 1)) |
114 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) = -∞) |
115 | 114, 80 | breq12d 4596 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → ((𝐴‘𝑖) < (𝐿‘𝑖) ↔ -∞ < ((𝐹‘𝑖) − 1))) |
116 | 113, 115 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) < (𝐿‘𝑖)) |
117 | 110, 111,
116 | xrltled 38427 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) ≤ (𝐿‘𝑖)) |
118 | 85 | eqcomd 2616 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) = (𝐿‘𝑖)) |
119 | 37, 118 | eqled 10019 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐴‘𝑖) = -∞) → (𝐴‘𝑖) ≤ (𝐿‘𝑖)) |
120 | 117, 119 | pm2.61dan 828 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ (𝐿‘𝑖)) |
121 | 75 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) ∈
ℝ*) |
122 | 29 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝐵‘𝑖) ∈
ℝ*) |
123 | 45 | ltpnfd 11831 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → ((𝐹‘𝑖) + 1) < +∞) |
124 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝐵‘𝑖) = +∞) |
125 | 95, 124 | breq12d 4596 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → ((𝑅‘𝑖) < (𝐵‘𝑖) ↔ ((𝐹‘𝑖) + 1) < +∞)) |
126 | 123, 125 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) < (𝐵‘𝑖)) |
127 | 121, 122,
126 | xrltled 38427 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) ≤ (𝐵‘𝑖)) |
128 | 74 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) ∈ ℝ) |
129 | 128, 100 | eqled 10019 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ ¬ (𝐵‘𝑖) = +∞) → (𝑅‘𝑖) ≤ (𝐵‘𝑖)) |
130 | 127, 129 | pm2.61dan 828 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑅‘𝑖) ≤ (𝐵‘𝑖)) |
131 | | ioossioo 12136 |
. . . . . . 7
⊢ ((((𝐴‘𝑖) ∈ ℝ* ∧ (𝐵‘𝑖) ∈ ℝ*) ∧ ((𝐴‘𝑖) ≤ (𝐿‘𝑖) ∧ (𝑅‘𝑖) ≤ (𝐵‘𝑖))) → ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ⊆ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
132 | 22, 29, 120, 130, 131 | syl22anc 1319 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ⊆ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
133 | 132 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑖 ∈ 𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ⊆ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
134 | | ss2ixp 7807 |
. . . . 5
⊢
(∀𝑖 ∈
𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ⊆ ((𝐴‘𝑖)(,)(𝐵‘𝑖)) → X𝑖 ∈ 𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
135 | 133, 134 | syl 17 |
. . . 4
⊢ (𝜑 → X𝑖 ∈
𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
136 | 2, 135 | eqsstrd 3602 |
. . 3
⊢ (𝜑 → 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
137 | 109, 136 | jca 553 |
. 2
⊢ (𝜑 → (𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
138 | | eleq2 2677 |
. . . 4
⊢ (𝑣 = 𝑉 → (𝐹 ∈ 𝑣 ↔ 𝐹 ∈ 𝑉)) |
139 | | sseq1 3589 |
. . . 4
⊢ (𝑣 = 𝑉 → (𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ↔ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
140 | 138, 139 | anbi12d 743 |
. . 3
⊢ (𝑣 = 𝑉 → ((𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) ↔ (𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))))) |
141 | 140 | rspcev 3282 |
. 2
⊢ ((𝑉 ∈
(TopOpen‘(ℝ^‘𝑋)) ∧ (𝐹 ∈ 𝑉 ∧ 𝑉 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
142 | 68, 137, 141 | syl2anc 691 |
1
⊢ (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |