Proof of Theorem hoiqssbl
Step | Hyp | Ref
| Expression |
1 | | 0ex 5200 |
. . . . . . 7
⊢ ∅
∈ V |
2 | 1 | snid 4577 |
. . . . . 6
⊢ ∅
∈ {∅} |
3 | 2 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ ∈
{∅}) |
4 | | hoiqssbl.y |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ (ℝ ↑m 𝑋)) |
5 | 4 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝑌 ∈ (ℝ ↑m 𝑋)) |
6 | | oveq2 7221 |
. . . . . . . . . 10
⊢ (𝑋 = ∅ → (ℝ
↑m 𝑋) =
(ℝ ↑m ∅)) |
7 | | reex 10820 |
. . . . . . . . . . . 12
⊢ ℝ
∈ V |
8 | | mapdm0 8523 |
. . . . . . . . . . . 12
⊢ (ℝ
∈ V → (ℝ ↑m ∅) =
{∅}) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (ℝ
↑m ∅) = {∅} |
10 | 9 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑋 = ∅ → (ℝ
↑m ∅) = {∅}) |
11 | 6, 10 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝑋 = ∅ → (ℝ
↑m 𝑋) =
{∅}) |
12 | 11 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → (ℝ
↑m 𝑋) =
{∅}) |
13 | 5, 12 | eleqtrd 2840 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝑌 ∈ {∅}) |
14 | | 0fin 8849 |
. . . . . . . . . . . . 13
⊢ ∅
∈ Fin |
15 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(dist‘(ℝ^‘∅)) =
(dist‘(ℝ^‘∅)) |
16 | 15 | rrxmetfi 24309 |
. . . . . . . . . . . . 13
⊢ (∅
∈ Fin → (dist‘(ℝ^‘∅)) ∈
(Met‘(ℝ ↑m ∅))) |
17 | 14, 16 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(dist‘(ℝ^‘∅)) ∈ (Met‘(ℝ
↑m ∅)) |
18 | | metxmet 23232 |
. . . . . . . . . . . 12
⊢
((dist‘(ℝ^‘∅)) ∈ (Met‘(ℝ
↑m ∅)) → (dist‘(ℝ^‘∅))
∈ (∞Met‘(ℝ ↑m
∅))) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(dist‘(ℝ^‘∅)) ∈ (∞Met‘(ℝ
↑m ∅)) |
20 | 19 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 = ∅) →
(dist‘(ℝ^‘∅)) ∈ (∞Met‘(ℝ
↑m ∅))) |
21 | 3, 9 | eleqtrrdi 2849 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ ∈ (ℝ
↑m ∅)) |
22 | | hoiqssbl.e |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
23 | 22 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐸 ∈
ℝ+) |
24 | | blcntr 23311 |
. . . . . . . . . 10
⊢
(((dist‘(ℝ^‘∅)) ∈
(∞Met‘(ℝ ↑m ∅)) ∧ ∅ ∈
(ℝ ↑m ∅) ∧ 𝐸 ∈ ℝ+) → ∅
∈ (∅(ball‘(dist‘(ℝ^‘∅)))𝐸)) |
25 | 20, 21, 23, 24 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ ∈
(∅(ball‘(dist‘(ℝ^‘∅)))𝐸)) |
26 | | elsni 4558 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ {∅} → 𝑌 = ∅) |
27 | 13, 26 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝑌 = ∅) |
28 | 27 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ = 𝑌) |
29 | 28 | oveq1d 7228 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = ∅) →
(∅(ball‘(dist‘(ℝ^‘∅)))𝐸) = (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) |
30 | 25, 29 | eleqtrd 2840 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ ∈ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) |
31 | 30 | snssd 4722 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) |
32 | 13, 31 | jca 515 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) |
33 | | biidd 265 |
. . . . . . 7
⊢ (𝑑 = ∅ → ((𝑌 ∈ {∅} ∧
{∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) ↔ (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
34 | 33 | rspcev 3537 |
. . . . . 6
⊢ ((∅
∈ {∅} ∧ (𝑌
∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) → ∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) |
35 | 3, 32, 34 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) |
36 | | biidd 265 |
. . . . . 6
⊢ (𝑐 = ∅ → (∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧
{∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) ↔ ∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
37 | 36 | rspcev 3537 |
. . . . 5
⊢ ((∅
∈ {∅} ∧ ∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) → ∃𝑐 ∈ {∅}∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) |
38 | 3, 35, 37 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∃𝑐 ∈ {∅}∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) |
39 | | oveq2 7221 |
. . . . . . . . . 10
⊢ (𝑋 = ∅ → (ℚ
↑m 𝑋) =
(ℚ ↑m ∅)) |
40 | | qex 12557 |
. . . . . . . . . . . 12
⊢ ℚ
∈ V |
41 | | mapdm0 8523 |
. . . . . . . . . . . 12
⊢ (ℚ
∈ V → (ℚ ↑m ∅) =
{∅}) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (ℚ
↑m ∅) = {∅} |
43 | 42 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑋 = ∅ → (ℚ
↑m ∅) = {∅}) |
44 | 39, 43 | eqtr2d 2778 |
. . . . . . . . 9
⊢ (𝑋 = ∅ → {∅} =
(ℚ ↑m 𝑋)) |
45 | 44 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝑋 = ∅ → (ℚ
↑m 𝑋) =
{∅}) |
46 | 45 | eleq2d 2823 |
. . . . . . 7
⊢ (𝑋 = ∅ → (𝑐 ∈ (ℚ
↑m 𝑋)
↔ 𝑐 ∈
{∅})) |
47 | 45 | eleq2d 2823 |
. . . . . . . . 9
⊢ (𝑋 = ∅ → (𝑑 ∈ (ℚ
↑m 𝑋)
↔ 𝑑 ∈
{∅})) |
48 | 47 | anbi1d 633 |
. . . . . . . 8
⊢ (𝑋 = ∅ → ((𝑑 ∈ (ℚ
↑m 𝑋) ∧
(𝑌 ∈ {∅} ∧
{∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) ↔ (𝑑 ∈ {∅} ∧ (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))))) |
49 | 48 | rexbidv2 3214 |
. . . . . . 7
⊢ (𝑋 = ∅ → (∃𝑑 ∈ (ℚ
↑m 𝑋)(𝑌 ∈ {∅} ∧
{∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) ↔ ∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
50 | 46, 49 | anbi12d 634 |
. . . . . 6
⊢ (𝑋 = ∅ → ((𝑐 ∈ (ℚ
↑m 𝑋) ∧
∃𝑑 ∈ (ℚ
↑m 𝑋)(𝑌 ∈ {∅} ∧
{∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) ↔ (𝑐 ∈ {∅} ∧ ∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))))) |
51 | 50 | rexbidv2 3214 |
. . . . 5
⊢ (𝑋 = ∅ → (∃𝑐 ∈ (ℚ
↑m 𝑋)∃𝑑 ∈ (ℚ ↑m 𝑋)(𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) ↔ ∃𝑐 ∈ {∅}∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
52 | 51 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → (∃𝑐 ∈ (ℚ
↑m 𝑋)∃𝑑 ∈ (ℚ ↑m 𝑋)(𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) ↔ ∃𝑐 ∈ {∅}∃𝑑 ∈ {∅} (𝑌 ∈ {∅} ∧ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
53 | 38, 52 | mpbird 260 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∃𝑐 ∈ (ℚ ↑m 𝑋)∃𝑑 ∈ (ℚ ↑m 𝑋)(𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) |
54 | | ixpeq1 8589 |
. . . . . . . . 9
⊢ (𝑋 = ∅ → X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) = X𝑖 ∈ ∅ ((𝑐‘𝑖)[,)(𝑑‘𝑖))) |
55 | | ixp0x 8607 |
. . . . . . . . . 10
⊢ X𝑖 ∈
∅ ((𝑐‘𝑖)[,)(𝑑‘𝑖)) = {∅} |
56 | 55 | a1i 11 |
. . . . . . . . 9
⊢ (𝑋 = ∅ → X𝑖 ∈
∅ ((𝑐‘𝑖)[,)(𝑑‘𝑖)) = {∅}) |
57 | 54, 56 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝑋 = ∅ → X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) = {∅}) |
58 | 57 | eleq2d 2823 |
. . . . . . 7
⊢ (𝑋 = ∅ → (𝑌 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ↔ 𝑌 ∈ {∅})) |
59 | | 2fveq3 6722 |
. . . . . . . . . 10
⊢ (𝑋 = ∅ →
(dist‘(ℝ^‘𝑋)) =
(dist‘(ℝ^‘∅))) |
60 | 59 | fveq2d 6721 |
. . . . . . . . 9
⊢ (𝑋 = ∅ →
(ball‘(dist‘(ℝ^‘𝑋))) =
(ball‘(dist‘(ℝ^‘∅)))) |
61 | 60 | oveqd 7230 |
. . . . . . . 8
⊢ (𝑋 = ∅ → (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) = (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)) |
62 | 57, 61 | sseq12d 3934 |
. . . . . . 7
⊢ (𝑋 = ∅ → (X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) ↔ {∅} ⊆ (𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸))) |
63 | 58, 62 | anbi12d 634 |
. . . . . 6
⊢ (𝑋 = ∅ → ((𝑌 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)) ↔ (𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
64 | 63 | rexbidv 3216 |
. . . . 5
⊢ (𝑋 = ∅ → (∃𝑑 ∈ (ℚ
↑m 𝑋)(𝑌 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)) ↔ ∃𝑑 ∈ (ℚ ↑m 𝑋)(𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
65 | 64 | rexbidv 3216 |
. . . 4
⊢ (𝑋 = ∅ → (∃𝑐 ∈ (ℚ
↑m 𝑋)∃𝑑 ∈ (ℚ ↑m 𝑋)(𝑌 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)) ↔ ∃𝑐 ∈ (ℚ ↑m 𝑋)∃𝑑 ∈ (ℚ ↑m 𝑋)(𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
66 | 65 | adantl 485 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → (∃𝑐 ∈ (ℚ
↑m 𝑋)∃𝑑 ∈ (ℚ ↑m 𝑋)(𝑌 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)) ↔ ∃𝑐 ∈ (ℚ ↑m 𝑋)∃𝑑 ∈ (ℚ ↑m 𝑋)(𝑌 ∈ {∅} ∧ {∅} ⊆
(𝑌(ball‘(dist‘(ℝ^‘∅)))𝐸)))) |
67 | 53, 66 | mpbird 260 |
. 2
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∃𝑐 ∈ (ℚ ↑m 𝑋)∃𝑑 ∈ (ℚ ↑m 𝑋)(𝑌 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))) |
68 | | hoiqssbl.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ Fin) |
69 | 68 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ∈ Fin) |
70 | | neqne 2948 |
. . . 4
⊢ (¬
𝑋 = ∅ → 𝑋 ≠ ∅) |
71 | 70 | adantl 485 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅) |
72 | 4 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑌 ∈ (ℝ ↑m 𝑋)) |
73 | 22 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝐸 ∈
ℝ+) |
74 | 69, 71, 72, 73 | hoiqssbllem3 43837 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ∃𝑐 ∈ (ℚ ↑m 𝑋)∃𝑑 ∈ (ℚ ↑m 𝑋)(𝑌 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))) |
75 | 67, 74 | pm2.61dan 813 |
1
⊢ (𝜑 → ∃𝑐 ∈ (ℚ ↑m 𝑋)∃𝑑 ∈ (ℚ ↑m 𝑋)(𝑌 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))) |