Proof of Theorem sepfsepc
| Step | Hyp | Ref
| Expression |
| 1 | | sepfsepc.1 |
. 2
⊢ (𝜑 → ∃𝑓 ∈ (𝐽 Cn II)(𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) |
| 2 | | simpl 482 |
. . . . 5
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) → 𝑓 ∈ (𝐽 Cn II)) |
| 3 | | 0re 11263 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
| 4 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 5 | | 0le0 12367 |
. . . . . . . 8
⊢ 0 ≤
0 |
| 6 | | 3re 12346 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
| 7 | | 3ne0 12372 |
. . . . . . . . . 10
⊢ 3 ≠
0 |
| 8 | 6, 7 | rereccli 12032 |
. . . . . . . . 9
⊢ (1 / 3)
∈ ℝ |
| 9 | | 1lt3 12439 |
. . . . . . . . . . 11
⊢ 1 <
3 |
| 10 | | recgt1i 12165 |
. . . . . . . . . . 11
⊢ ((3
∈ ℝ ∧ 1 < 3) → (0 < (1 / 3) ∧ (1 / 3) <
1)) |
| 11 | 6, 9, 10 | mp2an 692 |
. . . . . . . . . 10
⊢ (0 <
(1 / 3) ∧ (1 / 3) < 1) |
| 12 | 11 | simpri 485 |
. . . . . . . . 9
⊢ (1 / 3)
< 1 |
| 13 | 8, 4, 12 | ltleii 11384 |
. . . . . . . 8
⊢ (1 / 3)
≤ 1 |
| 14 | | iccss 13455 |
. . . . . . . 8
⊢ (((0
∈ ℝ ∧ 1 ∈ ℝ) ∧ (0 ≤ 0 ∧ (1 / 3) ≤ 1))
→ (0[,](1 / 3)) ⊆ (0[,]1)) |
| 15 | 3, 4, 5, 13, 14 | mp4an 693 |
. . . . . . 7
⊢ (0[,](1 /
3)) ⊆ (0[,]1) |
| 16 | | i0oii 48817 |
. . . . . . . . 9
⊢ ((1 / 3)
≤ 1 → (0[,)(1 / 3)) ∈ II) |
| 17 | 13, 16 | ax-mp 5 |
. . . . . . . 8
⊢ (0[,)(1 /
3)) ∈ II |
| 18 | 11 | simpli 483 |
. . . . . . . . . 10
⊢ 0 < (1
/ 3) |
| 19 | 8 | rexri 11319 |
. . . . . . . . . . . . 13
⊢ (1 / 3)
∈ ℝ* |
| 20 | | elico2 13451 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ (1 / 3) ∈ ℝ*) → (0 ∈
(0[,)(1 / 3)) ↔ (0 ∈ ℝ ∧ 0 ≤ 0 ∧ 0 < (1 /
3)))) |
| 21 | 3, 19, 20 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (0 ∈
(0[,)(1 / 3)) ↔ (0 ∈ ℝ ∧ 0 ≤ 0 ∧ 0 < (1 /
3))) |
| 22 | 21 | biimpri 228 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 0 ≤ 0 ∧ 0 < (1 / 3)) → 0 ∈ (0[,)(1 /
3))) |
| 23 | 22 | snssd 4809 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 0 ≤ 0 ∧ 0 < (1 / 3)) → {0} ⊆ (0[,)(1
/ 3))) |
| 24 | 3, 5, 18, 23 | mp3an 1463 |
. . . . . . . . 9
⊢ {0}
⊆ (0[,)(1 / 3)) |
| 25 | | icossicc 13476 |
. . . . . . . . 9
⊢ (0[,)(1 /
3)) ⊆ (0[,](1 / 3)) |
| 26 | 24, 25 | pm3.2i 470 |
. . . . . . . 8
⊢ ({0}
⊆ (0[,)(1 / 3)) ∧ (0[,)(1 / 3)) ⊆ (0[,](1 /
3))) |
| 27 | | sseq2 4010 |
. . . . . . . . . 10
⊢ (𝑔 = (0[,)(1 / 3)) → ({0}
⊆ 𝑔 ↔ {0}
⊆ (0[,)(1 / 3)))) |
| 28 | | sseq1 4009 |
. . . . . . . . . 10
⊢ (𝑔 = (0[,)(1 / 3)) → (𝑔 ⊆ (0[,](1 / 3)) ↔
(0[,)(1 / 3)) ⊆ (0[,](1 / 3)))) |
| 29 | 27, 28 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑔 = (0[,)(1 / 3)) → (({0}
⊆ 𝑔 ∧ 𝑔 ⊆ (0[,](1 / 3))) ↔
({0} ⊆ (0[,)(1 / 3)) ∧ (0[,)(1 / 3)) ⊆ (0[,](1 /
3))))) |
| 30 | 29 | rspcev 3622 |
. . . . . . . 8
⊢ (((0[,)(1
/ 3)) ∈ II ∧ ({0} ⊆ (0[,)(1 / 3)) ∧ (0[,)(1 / 3)) ⊆
(0[,](1 / 3)))) → ∃𝑔 ∈ II ({0} ⊆ 𝑔 ∧ 𝑔 ⊆ (0[,](1 / 3)))) |
| 31 | 17, 26, 30 | mp2an 692 |
. . . . . . 7
⊢
∃𝑔 ∈ II
({0} ⊆ 𝑔 ∧ 𝑔 ⊆ (0[,](1 /
3))) |
| 32 | | iitop 24906 |
. . . . . . . 8
⊢ II ∈
Top |
| 33 | 24, 25 | sstri 3993 |
. . . . . . . . 9
⊢ {0}
⊆ (0[,](1 / 3)) |
| 34 | 33, 15 | sstri 3993 |
. . . . . . . 8
⊢ {0}
⊆ (0[,]1) |
| 35 | | iiuni 24907 |
. . . . . . . . 9
⊢ (0[,]1) =
∪ II |
| 36 | 35 | isnei 23111 |
. . . . . . . 8
⊢ ((II
∈ Top ∧ {0} ⊆ (0[,]1)) → ((0[,](1 / 3)) ∈
((nei‘II)‘{0}) ↔ ((0[,](1 / 3)) ⊆ (0[,]1) ∧
∃𝑔 ∈ II ({0}
⊆ 𝑔 ∧ 𝑔 ⊆ (0[,](1 /
3)))))) |
| 37 | 32, 34, 36 | mp2an 692 |
. . . . . . 7
⊢ ((0[,](1
/ 3)) ∈ ((nei‘II)‘{0}) ↔ ((0[,](1 / 3)) ⊆ (0[,]1)
∧ ∃𝑔 ∈ II
({0} ⊆ 𝑔 ∧ 𝑔 ⊆ (0[,](1 /
3))))) |
| 38 | 15, 31, 37 | mpbir2an 711 |
. . . . . 6
⊢ (0[,](1 /
3)) ∈ ((nei‘II)‘{0}) |
| 39 | 38 | a1i 11 |
. . . . 5
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) → (0[,](1 / 3)) ∈
((nei‘II)‘{0})) |
| 40 | | simprl 771 |
. . . . 5
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) → 𝑆 ⊆ (◡𝑓 “ {0})) |
| 41 | 2, 39, 40 | cnneiima 48814 |
. . . 4
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) → (◡𝑓 “ (0[,](1 / 3))) ∈
((nei‘𝐽)‘𝑆)) |
| 42 | | halfge0 12483 |
. . . . . . . 8
⊢ 0 ≤ (1
/ 2) |
| 43 | | 1le1 11891 |
. . . . . . . 8
⊢ 1 ≤
1 |
| 44 | | iccss 13455 |
. . . . . . . 8
⊢ (((0
∈ ℝ ∧ 1 ∈ ℝ) ∧ (0 ≤ (1 / 2) ∧ 1 ≤ 1))
→ ((1 / 2)[,]1) ⊆ (0[,]1)) |
| 45 | 3, 4, 42, 43, 44 | mp4an 693 |
. . . . . . 7
⊢ ((1 /
2)[,]1) ⊆ (0[,]1) |
| 46 | | io1ii 48818 |
. . . . . . . . 9
⊢ (0 ≤
(1 / 2) → ((1 / 2)(,]1) ∈ II) |
| 47 | 42, 46 | ax-mp 5 |
. . . . . . . 8
⊢ ((1 /
2)(,]1) ∈ II |
| 48 | | halflt1 12484 |
. . . . . . . . . 10
⊢ (1 / 2)
< 1 |
| 49 | | halfre 12480 |
. . . . . . . . . . . . . 14
⊢ (1 / 2)
∈ ℝ |
| 50 | 49 | rexri 11319 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
∈ ℝ* |
| 51 | | elioc2 13450 |
. . . . . . . . . . . . 13
⊢ (((1 / 2)
∈ ℝ* ∧ 1 ∈ ℝ) → (1 ∈ ((1 /
2)(,]1) ↔ (1 ∈ ℝ ∧ (1 / 2) < 1 ∧ 1 ≤
1))) |
| 52 | 50, 4, 51 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (1 ∈
((1 / 2)(,]1) ↔ (1 ∈ ℝ ∧ (1 / 2) < 1 ∧ 1 ≤
1)) |
| 53 | 52 | biimpri 228 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ (1 / 2) < 1 ∧ 1 ≤ 1) → 1 ∈ ((1 /
2)(,]1)) |
| 54 | 53 | snssd 4809 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (1 / 2) < 1 ∧ 1 ≤ 1) → {1} ⊆ ((1 /
2)(,]1)) |
| 55 | 4, 48, 43, 54 | mp3an 1463 |
. . . . . . . . 9
⊢ {1}
⊆ ((1 / 2)(,]1) |
| 56 | | iocssicc 13477 |
. . . . . . . . 9
⊢ ((1 /
2)(,]1) ⊆ ((1 / 2)[,]1) |
| 57 | 55, 56 | pm3.2i 470 |
. . . . . . . 8
⊢ ({1}
⊆ ((1 / 2)(,]1) ∧ ((1 / 2)(,]1) ⊆ ((1 /
2)[,]1)) |
| 58 | | sseq2 4010 |
. . . . . . . . . 10
⊢ (ℎ = ((1 / 2)(,]1) → ({1}
⊆ ℎ ↔ {1} ⊆
((1 / 2)(,]1))) |
| 59 | | sseq1 4009 |
. . . . . . . . . 10
⊢ (ℎ = ((1 / 2)(,]1) → (ℎ ⊆ ((1 / 2)[,]1) ↔ ((1
/ 2)(,]1) ⊆ ((1 / 2)[,]1))) |
| 60 | 58, 59 | anbi12d 632 |
. . . . . . . . 9
⊢ (ℎ = ((1 / 2)(,]1) → (({1}
⊆ ℎ ∧ ℎ ⊆ ((1 / 2)[,]1)) ↔
({1} ⊆ ((1 / 2)(,]1) ∧ ((1 / 2)(,]1) ⊆ ((1 /
2)[,]1)))) |
| 61 | 60 | rspcev 3622 |
. . . . . . . 8
⊢ ((((1 /
2)(,]1) ∈ II ∧ ({1} ⊆ ((1 / 2)(,]1) ∧ ((1 / 2)(,]1) ⊆
((1 / 2)[,]1))) → ∃ℎ ∈ II ({1} ⊆ ℎ ∧ ℎ ⊆ ((1 / 2)[,]1))) |
| 62 | 47, 57, 61 | mp2an 692 |
. . . . . . 7
⊢
∃ℎ ∈ II
({1} ⊆ ℎ ∧ ℎ ⊆ ((1 /
2)[,]1)) |
| 63 | 55, 56 | sstri 3993 |
. . . . . . . . 9
⊢ {1}
⊆ ((1 / 2)[,]1) |
| 64 | 63, 45 | sstri 3993 |
. . . . . . . 8
⊢ {1}
⊆ (0[,]1) |
| 65 | 35 | isnei 23111 |
. . . . . . . 8
⊢ ((II
∈ Top ∧ {1} ⊆ (0[,]1)) → (((1 / 2)[,]1) ∈
((nei‘II)‘{1}) ↔ (((1 / 2)[,]1) ⊆ (0[,]1) ∧
∃ℎ ∈ II ({1}
⊆ ℎ ∧ ℎ ⊆ ((1 /
2)[,]1))))) |
| 66 | 32, 64, 65 | mp2an 692 |
. . . . . . 7
⊢ (((1 /
2)[,]1) ∈ ((nei‘II)‘{1}) ↔ (((1 / 2)[,]1) ⊆ (0[,]1)
∧ ∃ℎ ∈ II
({1} ⊆ ℎ ∧ ℎ ⊆ ((1 /
2)[,]1)))) |
| 67 | 45, 62, 66 | mpbir2an 711 |
. . . . . 6
⊢ ((1 /
2)[,]1) ∈ ((nei‘II)‘{1}) |
| 68 | 67 | a1i 11 |
. . . . 5
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) → ((1 / 2)[,]1) ∈
((nei‘II)‘{1})) |
| 69 | | simprr 773 |
. . . . 5
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) → 𝑇 ⊆ (◡𝑓 “ {1})) |
| 70 | 2, 68, 69 | cnneiima 48814 |
. . . 4
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) → (◡𝑓 “ ((1 / 2)[,]1)) ∈
((nei‘𝐽)‘𝑇)) |
| 71 | | icccldii 48816 |
. . . . . 6
⊢ ((0 ≤
0 ∧ (1 / 3) ≤ 1) → (0[,](1 / 3)) ∈
(Clsd‘II)) |
| 72 | 5, 13, 71 | mp2an 692 |
. . . . 5
⊢ (0[,](1 /
3)) ∈ (Clsd‘II) |
| 73 | | cnclima 23276 |
. . . . 5
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (0[,](1 / 3)) ∈
(Clsd‘II)) → (◡𝑓 “ (0[,](1 / 3))) ∈
(Clsd‘𝐽)) |
| 74 | 2, 72, 73 | sylancl 586 |
. . . 4
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) → (◡𝑓 “ (0[,](1 / 3))) ∈
(Clsd‘𝐽)) |
| 75 | | icccldii 48816 |
. . . . . 6
⊢ ((0 ≤
(1 / 2) ∧ 1 ≤ 1) → ((1 / 2)[,]1) ∈
(Clsd‘II)) |
| 76 | 42, 43, 75 | mp2an 692 |
. . . . 5
⊢ ((1 /
2)[,]1) ∈ (Clsd‘II) |
| 77 | | cnclima 23276 |
. . . . 5
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ ((1 / 2)[,]1) ∈
(Clsd‘II)) → (◡𝑓 “ ((1 / 2)[,]1)) ∈
(Clsd‘𝐽)) |
| 78 | 2, 76, 77 | sylancl 586 |
. . . 4
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) → (◡𝑓 “ ((1 / 2)[,]1)) ∈
(Clsd‘𝐽)) |
| 79 | | eqid 2737 |
. . . . . . . 8
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 80 | 79, 35 | cnf 23254 |
. . . . . . 7
⊢ (𝑓 ∈ (𝐽 Cn II) → 𝑓:∪ 𝐽⟶(0[,]1)) |
| 81 | 80 | ffund 6740 |
. . . . . 6
⊢ (𝑓 ∈ (𝐽 Cn II) → Fun 𝑓) |
| 82 | 2, 81 | syl 17 |
. . . . 5
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) → Fun 𝑓) |
| 83 | | 0xr 11308 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
| 84 | | 1xr 11320 |
. . . . . . 7
⊢ 1 ∈
ℝ* |
| 85 | | 2lt3 12438 |
. . . . . . . 8
⊢ 2 <
3 |
| 86 | | 2re 12340 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
| 87 | | 2pos 12369 |
. . . . . . . . 9
⊢ 0 <
2 |
| 88 | | 3pos 12371 |
. . . . . . . . 9
⊢ 0 <
3 |
| 89 | 86, 6, 87, 88 | ltrecii 12184 |
. . . . . . . 8
⊢ (2 < 3
↔ (1 / 3) < (1 / 2)) |
| 90 | 85, 89 | mpbi 230 |
. . . . . . 7
⊢ (1 / 3)
< (1 / 2) |
| 91 | | iccdisj2 48795 |
. . . . . . 7
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ (1 / 3)
< (1 / 2)) → ((0[,](1 / 3)) ∩ ((1 / 2)[,]1)) =
∅) |
| 92 | 83, 84, 90, 91 | mp3an 1463 |
. . . . . 6
⊢ ((0[,](1
/ 3)) ∩ ((1 / 2)[,]1)) = ∅ |
| 93 | 92 | a1i 11 |
. . . . 5
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) → ((0[,](1 / 3)) ∩
((1 / 2)[,]1)) = ∅) |
| 94 | | ssidd 4007 |
. . . . 5
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) → (◡𝑓 “ (0[,](1 / 3))) ⊆ (◡𝑓 “ (0[,](1 / 3)))) |
| 95 | | ssidd 4007 |
. . . . 5
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) → (◡𝑓 “ ((1 / 2)[,]1)) ⊆ (◡𝑓 “ ((1 / 2)[,]1))) |
| 96 | 82, 93, 94, 95 | predisj 48730 |
. . . 4
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) → ((◡𝑓 “ (0[,](1 / 3))) ∩ (◡𝑓 “ ((1 / 2)[,]1))) =
∅) |
| 97 | | eleq1 2829 |
. . . . . 6
⊢ (𝑛 = (◡𝑓 “ (0[,](1 / 3))) → (𝑛 ∈ (Clsd‘𝐽) ↔ (◡𝑓 “ (0[,](1 / 3))) ∈
(Clsd‘𝐽))) |
| 98 | | ineq1 4213 |
. . . . . . 7
⊢ (𝑛 = (◡𝑓 “ (0[,](1 / 3))) → (𝑛 ∩ 𝑚) = ((◡𝑓 “ (0[,](1 / 3))) ∩ 𝑚)) |
| 99 | 98 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑛 = (◡𝑓 “ (0[,](1 / 3))) → ((𝑛 ∩ 𝑚) = ∅ ↔ ((◡𝑓 “ (0[,](1 / 3))) ∩ 𝑚) = ∅)) |
| 100 | 97, 99 | 3anbi13d 1440 |
. . . . 5
⊢ (𝑛 = (◡𝑓 “ (0[,](1 / 3))) → ((𝑛 ∈ (Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ (𝑛 ∩ 𝑚) = ∅) ↔ ((◡𝑓 “ (0[,](1 / 3))) ∈
(Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ ((◡𝑓 “ (0[,](1 / 3))) ∩ 𝑚) = ∅))) |
| 101 | | eleq1 2829 |
. . . . . 6
⊢ (𝑚 = (◡𝑓 “ ((1 / 2)[,]1)) → (𝑚 ∈ (Clsd‘𝐽) ↔ (◡𝑓 “ ((1 / 2)[,]1)) ∈
(Clsd‘𝐽))) |
| 102 | | ineq2 4214 |
. . . . . . 7
⊢ (𝑚 = (◡𝑓 “ ((1 / 2)[,]1)) → ((◡𝑓 “ (0[,](1 / 3))) ∩ 𝑚) = ((◡𝑓 “ (0[,](1 / 3))) ∩ (◡𝑓 “ ((1 / 2)[,]1)))) |
| 103 | 102 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑚 = (◡𝑓 “ ((1 / 2)[,]1)) → (((◡𝑓 “ (0[,](1 / 3))) ∩ 𝑚) = ∅ ↔ ((◡𝑓 “ (0[,](1 / 3))) ∩ (◡𝑓 “ ((1 / 2)[,]1))) =
∅)) |
| 104 | 101, 103 | 3anbi23d 1441 |
. . . . 5
⊢ (𝑚 = (◡𝑓 “ ((1 / 2)[,]1)) → (((◡𝑓 “ (0[,](1 / 3))) ∈
(Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ ((◡𝑓 “ (0[,](1 / 3))) ∩ 𝑚) = ∅) ↔ ((◡𝑓 “ (0[,](1 / 3))) ∈
(Clsd‘𝐽) ∧ (◡𝑓 “ ((1 / 2)[,]1)) ∈
(Clsd‘𝐽) ∧
((◡𝑓 “ (0[,](1 / 3))) ∩ (◡𝑓 “ ((1 / 2)[,]1))) =
∅))) |
| 105 | 100, 104 | rspc2ev 3635 |
. . . 4
⊢ (((◡𝑓 “ (0[,](1 / 3))) ∈
((nei‘𝐽)‘𝑆) ∧ (◡𝑓 “ ((1 / 2)[,]1)) ∈
((nei‘𝐽)‘𝑇) ∧ ((◡𝑓 “ (0[,](1 / 3))) ∈
(Clsd‘𝐽) ∧ (◡𝑓 “ ((1 / 2)[,]1)) ∈
(Clsd‘𝐽) ∧
((◡𝑓 “ (0[,](1 / 3))) ∩ (◡𝑓 “ ((1 / 2)[,]1))) = ∅)) →
∃𝑛 ∈
((nei‘𝐽)‘𝑆)∃𝑚 ∈ ((nei‘𝐽)‘𝑇)(𝑛 ∈ (Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ (𝑛 ∩ 𝑚) = ∅)) |
| 106 | 41, 70, 74, 78, 96, 105 | syl113anc 1384 |
. . 3
⊢ ((𝑓 ∈ (𝐽 Cn II) ∧ (𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1}))) → ∃𝑛 ∈ ((nei‘𝐽)‘𝑆)∃𝑚 ∈ ((nei‘𝐽)‘𝑇)(𝑛 ∈ (Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ (𝑛 ∩ 𝑚) = ∅)) |
| 107 | 106 | rexlimiva 3147 |
. 2
⊢
(∃𝑓 ∈
(𝐽 Cn II)(𝑆 ⊆ (◡𝑓 “ {0}) ∧ 𝑇 ⊆ (◡𝑓 “ {1})) → ∃𝑛 ∈ ((nei‘𝐽)‘𝑆)∃𝑚 ∈ ((nei‘𝐽)‘𝑇)(𝑛 ∈ (Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ (𝑛 ∩ 𝑚) = ∅)) |
| 108 | 1, 107 | syl 17 |
1
⊢ (𝜑 → ∃𝑛 ∈ ((nei‘𝐽)‘𝑆)∃𝑚 ∈ ((nei‘𝐽)‘𝑇)(𝑛 ∈ (Clsd‘𝐽) ∧ 𝑚 ∈ (Clsd‘𝐽) ∧ (𝑛 ∩ 𝑚) = ∅)) |