Proof of Theorem hoiqssbl
Step | Hyp | Ref
| Expression |
1 | | 0ex 4718 |
. . . . . . 7
⊢ ∅
∈ V |
2 | 1 | snid 4155 |
. . . . . 6
⊢ ∅
∈ {∅} |
3 | 2 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ ∈
{∅}) |
4 | | hoiqssbl.y |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ (ℝ ↑𝑚
𝑋)) |
5 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝑌 ∈ (ℝ ↑𝑚
𝑋)) |
6 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑋 = ∅ → (ℝ
↑𝑚 𝑋) = (ℝ ↑𝑚
∅)) |
7 | | reex 9906 |
. . . . . . . . . . . 12
⊢ ℝ
∈ V |
8 | | mapdm0 38378 |
. . . . . . . . . . . 12
⊢ (ℝ
∈ V → (ℝ ↑𝑚 ∅) =
{∅}) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (ℝ
↑𝑚 ∅) = {∅} |
10 | 9 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑋 = ∅ → (ℝ
↑𝑚 ∅) = {∅}) |
11 | 6, 10 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝑋 = ∅ → (ℝ
↑𝑚 𝑋) = {∅}) |
12 | 11 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → (ℝ
↑𝑚 𝑋) = {∅}) |
13 | 5, 12 | eleqtrd 2690 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝑌 ∈ {∅}) |
14 | | 0fin 8073 |
. . . . . . . . . . . . 13
⊢ ∅
∈ Fin |
15 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(dist‘(ℝ^‘∅)) =
(dist‘(ℝ^‘∅)) |
16 | 15 | rrxmetfi 39183 |
. . . . . . . . . . . . 13
⊢ (∅
∈ Fin → (dist‘(ℝ^‘∅)) ∈
(Met‘(ℝ ↑𝑚 ∅))) |
17 | 14, 16 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(dist‘(ℝ^‘∅)) ∈ (Met‘(ℝ
↑𝑚 ∅)) |
18 | | metxmet 21949 |
. . . . . . . . . . . 12
⊢
((dist‘(ℝ^‘∅)) ∈ (Met‘(ℝ
↑𝑚 ∅)) →
(dist‘(ℝ^‘∅)) ∈ (∞Met‘(ℝ
↑𝑚 ∅))) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(dist‘(ℝ^‘∅)) ∈ (∞Met‘(ℝ
↑𝑚 ∅)) |
20 | 19 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 = ∅) →
(dist‘(ℝ^‘∅)) ∈ (∞Met‘(ℝ
↑𝑚 ∅))) |
21 | 3, 9 | syl6eleqr 2699 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ ∈ (ℝ
↑𝑚 ∅)) |
22 | | hoiqssbl.e |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
23 | 22 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐸 ∈
ℝ+) |
24 | | blcntr 22028 |
. . . . . . . . . 10
⊢
(((dist‘(ℝ^‘∅)) ∈
(∞Met‘(ℝ ↑𝑚 ∅)) ∧ ∅
∈ (ℝ ↑𝑚 ∅) ∧ 𝐸 ∈ ℝ+) → ∅
∈ (∅(ball‘(dist‘(ℝ^‘∅)))𝐸)) |
25 | 20, 21, 23, 24 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ ∈
(∅(ball‘(dist‘(ℝ^‘∅)))𝐸)) |
26 | | elsni 4142 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ {∅} → 𝑌 = ∅) |
27 | 13, 26 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝑌 = ∅) |
28 | 27 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ = 𝑌) |
29 | 28 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = ∅) →
(∅(ball‘(dist‘(ℝ^‘∅)))𝐸) = (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) |
30 | 25, 29 | eleqtrd 2690 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ ∈ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) |
31 | 30 | snssd 4281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) |
32 | 13, 31 | jca 553 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) |
33 | | biidd 251 |
. . . . . . 7
⊢ (𝑑 = ∅ → ((𝑌 ∈ {∅} ∧
{∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) ↔ (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
34 | 33 | rspcev 3282 |
. . . . . 6
⊢ ((∅
∈ {∅} ∧ (𝑌
∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) → ∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) |
35 | 3, 32, 34 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) |
36 | | biidd 251 |
. . . . . 6
⊢ (𝑐 = ∅ → (∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧
{∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) ↔ ∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
37 | 36 | rspcev 3282 |
. . . . 5
⊢ ((∅
∈ {∅} ∧ ∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) → ∃𝑐 ∈ {∅}∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) |
38 | 3, 35, 37 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∃𝑐 ∈ {∅}∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) |
39 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑋 = ∅ → (ℚ
↑𝑚 𝑋) = (ℚ ↑𝑚
∅)) |
40 | | qex 11676 |
. . . . . . . . . . . 12
⊢ ℚ
∈ V |
41 | | mapdm0 38378 |
. . . . . . . . . . . 12
⊢ (ℚ
∈ V → (ℚ ↑𝑚 ∅) =
{∅}) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (ℚ
↑𝑚 ∅) = {∅} |
43 | 42 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑋 = ∅ → (ℚ
↑𝑚 ∅) = {∅}) |
44 | 39, 43 | eqtr2d 2645 |
. . . . . . . . 9
⊢ (𝑋 = ∅ → {∅} =
(ℚ ↑𝑚 𝑋)) |
45 | 44 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑋 = ∅ → (ℚ
↑𝑚 𝑋) = {∅}) |
46 | 45 | eleq2d 2673 |
. . . . . . 7
⊢ (𝑋 = ∅ → (𝑐 ∈ (ℚ
↑𝑚 𝑋) ↔ 𝑐 ∈ {∅})) |
47 | 45 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝑋 = ∅ → (𝑑 ∈ (ℚ
↑𝑚 𝑋) ↔ 𝑑 ∈ {∅})) |
48 | 47 | anbi1d 737 |
. . . . . . . 8
⊢ (𝑋 = ∅ → ((𝑑 ∈ (ℚ
↑𝑚 𝑋) ∧ (𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) ↔ (𝑑 ∈ {∅} ∧ (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))))) |
49 | 48 | rexbidv2 3030 |
. . . . . . 7
⊢ (𝑋 = ∅ → (∃𝑑 ∈ (ℚ
↑𝑚 𝑋)(𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) ↔ ∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
50 | 46, 49 | anbi12d 743 |
. . . . . 6
⊢ (𝑋 = ∅ → ((𝑐 ∈ (ℚ
↑𝑚 𝑋) ∧ ∃𝑑 ∈ (ℚ ↑𝑚
𝑋)(𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) ↔ (𝑐 ∈ {∅} ∧ ∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))))) |
51 | 50 | rexbidv2 3030 |
. . . . 5
⊢ (𝑋 = ∅ → (∃𝑐 ∈ (ℚ
↑𝑚 𝑋)∃𝑑 ∈ (ℚ ↑𝑚
𝑋)(𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) ↔ ∃𝑐 ∈ {∅}∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
52 | 51 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → (∃𝑐 ∈ (ℚ
↑𝑚 𝑋)∃𝑑 ∈ (ℚ ↑𝑚
𝑋)(𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) ↔ ∃𝑐 ∈ {∅}∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
53 | 38, 52 | mpbird 246 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∃𝑐 ∈ (ℚ ↑𝑚
𝑋)∃𝑑 ∈ (ℚ ↑𝑚
𝑋)(𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) |
54 | | ixpeq1 7805 |
. . . . . . . . 9
⊢ (𝑋 = ∅ → X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) = X𝑖 ∈ ∅ ((𝑐‘𝑖)[,)(𝑑‘𝑖))) |
55 | | ixp0x 7822 |
. . . . . . . . . 10
⊢ X𝑖 ∈
∅ ((𝑐‘𝑖)[,)(𝑑‘𝑖)) = {∅} |
56 | 55 | a1i 11 |
. . . . . . . . 9
⊢ (𝑋 = ∅ → X𝑖 ∈
∅ ((𝑐‘𝑖)[,)(𝑑‘𝑖)) = {∅}) |
57 | 54, 56 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝑋 = ∅ → X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) = {∅}) |
58 | 57 | eleq2d 2673 |
. . . . . . 7
⊢ (𝑋 = ∅ → (𝑌 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ↔ 𝑌 ∈ {∅})) |
59 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ →
(ℝ^‘𝑋) =
(ℝ^‘∅)) |
60 | 59 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑋 = ∅ →
(dist‘(ℝ^‘𝑋)) =
(dist‘(ℝ^‘∅))) |
61 | 60 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑋 = ∅ →
(ball‘(dist‘(ℝ^‘𝑋))) =
(ball‘(dist‘(ℝ^‘∅)))) |
62 | 61 | oveqd 6566 |
. . . . . . . 8
⊢ (𝑋 = ∅ → (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) = (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) |
63 | 57, 62 | sseq12d 3597 |
. . . . . . 7
⊢ (𝑋 = ∅ → (X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) ↔ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) |
64 | 58, 63 | anbi12d 743 |
. . . . . 6
⊢ (𝑋 = ∅ → ((𝑌 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)) ↔ (𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
65 | 64 | rexbidv 3034 |
. . . . 5
⊢ (𝑋 = ∅ → (∃𝑑 ∈ (ℚ
↑𝑚 𝑋)(𝑌 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)) ↔ ∃𝑑 ∈ (ℚ ↑𝑚
𝑋)(𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
66 | 65 | rexbidv 3034 |
. . . 4
⊢ (𝑋 = ∅ → (∃𝑐 ∈ (ℚ
↑𝑚 𝑋)∃𝑑 ∈ (ℚ ↑𝑚
𝑋)(𝑌 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)) ↔ ∃𝑐 ∈ (ℚ ↑𝑚
𝑋)∃𝑑 ∈ (ℚ ↑𝑚
𝑋)(𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
67 | 66 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → (∃𝑐 ∈ (ℚ
↑𝑚 𝑋)∃𝑑 ∈ (ℚ ↑𝑚
𝑋)(𝑌 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)) ↔ ∃𝑐 ∈ (ℚ ↑𝑚
𝑋)∃𝑑 ∈ (ℚ ↑𝑚
𝑋)(𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
68 | 53, 67 | mpbird 246 |
. 2
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∃𝑐 ∈ (ℚ ↑𝑚
𝑋)∃𝑑 ∈ (ℚ ↑𝑚
𝑋)(𝑌 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))) |
69 | | hoiqssbl.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ Fin) |
70 | 69 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ∈ Fin) |
71 | | neqne 2790 |
. . . 4
⊢ (¬
𝑋 = ∅ → 𝑋 ≠ ∅) |
72 | 71 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅) |
73 | 4 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑌 ∈ (ℝ ↑𝑚
𝑋)) |
74 | 22 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝐸 ∈
ℝ+) |
75 | 70, 72, 73, 74 | hoiqssbllem3 39514 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∃𝑐 ∈ (ℚ ↑𝑚
𝑋)∃𝑑 ∈ (ℚ ↑𝑚
𝑋)(𝑌 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))) |
76 | 68, 75 | pm2.61dan 828 |
1
⊢ (𝜑 → ∃𝑐 ∈ (ℚ ↑𝑚
𝑋)∃𝑑 ∈ (ℚ ↑𝑚
𝑋)(𝑌 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))) |