Step | Hyp | Ref
| Expression |
1 | | p0ex 4853 |
. . . . . 6
⊢ {∅}
∈ V |
2 | 1 | prid2 4298 |
. . . . 5
⊢ {∅}
∈ {∅, {∅}} |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝑋 = ∅ → {∅}
∈ {∅, {∅}}) |
4 | | ixpeq1 7919 |
. . . . . 6
⊢ (𝑋 = ∅ → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) = X𝑖 ∈ ∅ ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
5 | | ixp0x 7936 |
. . . . . . 7
⊢ X𝑖 ∈
∅ ((𝐴‘𝑖)(,)(𝐵‘𝑖)) = {∅} |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (𝑋 = ∅ → X𝑖 ∈
∅ ((𝐴‘𝑖)(,)(𝐵‘𝑖)) = {∅}) |
7 | 4, 6 | eqtrd 2656 |
. . . . 5
⊢ (𝑋 = ∅ → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) = {∅}) |
8 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑋 = ∅ →
(ℝ^‘𝑋) =
(ℝ^‘∅)) |
9 | 8 | fveq2d 6195 |
. . . . . 6
⊢ (𝑋 = ∅ →
(TopOpen‘(ℝ^‘𝑋)) =
(TopOpen‘(ℝ^‘∅))) |
10 | | rrxtopn0b 40516 |
. . . . . . 7
⊢
(TopOpen‘(ℝ^‘∅)) = {∅,
{∅}} |
11 | 10 | a1i 11 |
. . . . . 6
⊢ (𝑋 = ∅ →
(TopOpen‘(ℝ^‘∅)) = {∅,
{∅}}) |
12 | 9, 11 | eqtrd 2656 |
. . . . 5
⊢ (𝑋 = ∅ →
(TopOpen‘(ℝ^‘𝑋)) = {∅, {∅}}) |
13 | 7, 12 | eleq12d 2695 |
. . . 4
⊢ (𝑋 = ∅ → (X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋)) ↔ {∅} ∈ {∅,
{∅}})) |
14 | 3, 13 | mpbird 247 |
. . 3
⊢ (𝑋 = ∅ → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋))) |
15 | 14 | adantl 482 |
. 2
⊢ ((𝜑 ∧ 𝑋 = ∅) → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋))) |
16 | | neqne 2802 |
. . . 4
⊢ (¬
𝑋 = ∅ → 𝑋 ≠ ∅) |
17 | 16 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅) |
18 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (𝐴‘𝑖) = (𝐴‘𝑗)) |
19 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (𝐵‘𝑖) = (𝐵‘𝑗)) |
20 | 18, 19 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → ((𝐴‘𝑖)(,)(𝐵‘𝑖)) = ((𝐴‘𝑗)(,)(𝐵‘𝑗))) |
21 | 20 | cbvixpv 7926 |
. . . . . . . . 9
⊢ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) = X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗)) |
22 | 21 | eleq2i 2693 |
. . . . . . . 8
⊢ (𝑓 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ↔ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) |
23 | 22 | biimpi 206 |
. . . . . . 7
⊢ (𝑓 ∈ X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) → 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) |
24 | 23 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) |
25 | | ioorrnopnxr.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ Fin) |
26 | 25 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) → 𝑋 ∈ Fin) |
27 | | ioorrnopnxr.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴:𝑋⟶ℝ*) |
28 | 27 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) → 𝐴:𝑋⟶ℝ*) |
29 | | ioorrnopnxr.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵:𝑋⟶ℝ*) |
30 | 29 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) → 𝐵:𝑋⟶ℝ*) |
31 | 22 | biimpri 218 |
. . . . . . . 8
⊢ (𝑓 ∈ X𝑗 ∈
𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗)) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
32 | 31 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) |
33 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑖 → (𝐴‘𝑗) = (𝐴‘𝑖)) |
34 | 33 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑗 = 𝑖 → ((𝐴‘𝑗) = -∞ ↔ (𝐴‘𝑖) = -∞)) |
35 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑖 → (𝑓‘𝑗) = (𝑓‘𝑖)) |
36 | 35 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑗 = 𝑖 → ((𝑓‘𝑗) − 1) = ((𝑓‘𝑖) − 1)) |
37 | 34, 36, 33 | ifbieq12d 4113 |
. . . . . . . 8
⊢ (𝑗 = 𝑖 → if((𝐴‘𝑗) = -∞, ((𝑓‘𝑗) − 1), (𝐴‘𝑗)) = if((𝐴‘𝑖) = -∞, ((𝑓‘𝑖) − 1), (𝐴‘𝑖))) |
38 | 37 | cbvmptv 4750 |
. . . . . . 7
⊢ (𝑗 ∈ 𝑋 ↦ if((𝐴‘𝑗) = -∞, ((𝑓‘𝑗) − 1), (𝐴‘𝑗))) = (𝑖 ∈ 𝑋 ↦ if((𝐴‘𝑖) = -∞, ((𝑓‘𝑖) − 1), (𝐴‘𝑖))) |
39 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑖 → (𝐵‘𝑗) = (𝐵‘𝑖)) |
40 | 39 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑗 = 𝑖 → ((𝐵‘𝑗) = +∞ ↔ (𝐵‘𝑖) = +∞)) |
41 | 35 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑗 = 𝑖 → ((𝑓‘𝑗) + 1) = ((𝑓‘𝑖) + 1)) |
42 | 40, 41, 39 | ifbieq12d 4113 |
. . . . . . . 8
⊢ (𝑗 = 𝑖 → if((𝐵‘𝑗) = +∞, ((𝑓‘𝑗) + 1), (𝐵‘𝑗)) = if((𝐵‘𝑖) = +∞, ((𝑓‘𝑖) + 1), (𝐵‘𝑖))) |
43 | 42 | cbvmptv 4750 |
. . . . . . 7
⊢ (𝑗 ∈ 𝑋 ↦ if((𝐵‘𝑗) = +∞, ((𝑓‘𝑗) + 1), (𝐵‘𝑗))) = (𝑖 ∈ 𝑋 ↦ if((𝐵‘𝑖) = +∞, ((𝑓‘𝑖) + 1), (𝐵‘𝑖))) |
44 | | eqid 2622 |
. . . . . . 7
⊢ X𝑖 ∈
𝑋 (((𝑗 ∈ 𝑋 ↦ if((𝐴‘𝑗) = -∞, ((𝑓‘𝑗) − 1), (𝐴‘𝑗)))‘𝑖)(,)((𝑗 ∈ 𝑋 ↦ if((𝐵‘𝑗) = +∞, ((𝑓‘𝑗) + 1), (𝐵‘𝑗)))‘𝑖)) = X𝑖 ∈ 𝑋 (((𝑗 ∈ 𝑋 ↦ if((𝐴‘𝑗) = -∞, ((𝑓‘𝑗) − 1), (𝐴‘𝑗)))‘𝑖)(,)((𝑗 ∈ 𝑋 ↦ if((𝐵‘𝑗) = +∞, ((𝑓‘𝑗) + 1), (𝐵‘𝑗)))‘𝑖)) |
45 | 26, 28, 30, 32, 38, 43, 44 | ioorrnopnxrlem 40526 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐴‘𝑗)(,)(𝐵‘𝑗))) → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
46 | 24, 45 | syldan 487 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
47 | 46 | ralrimiva 2966 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ∀𝑓 ∈ X
𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) |
48 | | eqid 2622 |
. . . . . . . 8
⊢
(TopOpen‘(ℝ^‘𝑋)) = (TopOpen‘(ℝ^‘𝑋)) |
49 | 48 | rrxtop 40509 |
. . . . . . 7
⊢ (𝑋 ∈ Fin →
(TopOpen‘(ℝ^‘𝑋)) ∈ Top) |
50 | 25, 49 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(TopOpen‘(ℝ^‘𝑋)) ∈ Top) |
51 | 50 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) →
(TopOpen‘(ℝ^‘𝑋)) ∈ Top) |
52 | | eltop2 20779 |
. . . . 5
⊢
((TopOpen‘(ℝ^‘𝑋)) ∈ Top → (X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋)) ↔ ∀𝑓 ∈ X 𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))))) |
53 | 51, 52 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋)) ↔ ∀𝑓 ∈ X 𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝑓 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))))) |
54 | 47, 53 | mpbird 247 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋))) |
55 | 17, 54 | syldan 487 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋))) |
56 | 15, 55 | pm2.61dan 832 |
1
⊢ (𝜑 → X𝑖 ∈
𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈
(TopOpen‘(ℝ^‘𝑋))) |