Step | Hyp | Ref
| Expression |
1 | | conntop 22168 |
. . 3
⊢ (𝐽 ∈ Conn → 𝐽 ∈ Top) |
2 | 1 | adantr 484 |
. 2
⊢ ((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
→ 𝐽 ∈
Top) |
3 | | eqid 2738 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 |
4 | | simpll 767 |
. . . . . 6
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ 𝐽 ∈
Conn) |
5 | | inss1 4119 |
. . . . . . 7
⊢ (𝐽 ∩ (Clsd‘𝐽)) ⊆ 𝐽 |
6 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
→ 𝐽 ∈
𝑛-Locally PConn) |
7 | 1 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
→ 𝐽 ∈
Top) |
8 | 3 | topopn 21657 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ Top → ∪ 𝐽
∈ 𝐽) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
→ ∪ 𝐽 ∈ 𝐽) |
10 | | simprr 773 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
→ 𝑧 ∈ ∪ 𝐽) |
11 | | nlly2i 22227 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ 𝑛-Locally PConn
∧ ∪ 𝐽 ∈ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽) → ∃𝑠 ∈ 𝒫 ∪ 𝐽∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn)) |
12 | 6, 9, 10, 11 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
→ ∃𝑠 ∈
𝒫 ∪ 𝐽∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn)) |
13 | | simprr1 1222 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ (𝑠 ∈ 𝒫
∪ 𝐽 ∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) → 𝑧 ∈ 𝑢) |
14 | | eqeq2 2750 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑤 → ((𝑓‘1) = 𝑦 ↔ (𝑓‘1) = 𝑤)) |
15 | 14 | anbi2d 632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑤 → (((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ ((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑤))) |
16 | 15 | rexbidv 3207 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑤 → (∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑤))) |
17 | 16 | elrab 3588 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ↔ (𝑤 ∈ ∪ 𝐽 ∧ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑤))) |
18 | 17 | simprbi 500 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑤)) |
19 | | simprr3 1224 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ (𝑠 ∈ 𝒫
∪ 𝐽 ∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) → (𝐽 ↾t 𝑠) ∈ PConn) |
20 | 19 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → (𝐽 ↾t 𝑠) ∈ PConn) |
21 | | simprr2 1223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ (𝑠 ∈ 𝒫
∪ 𝐽 ∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) → 𝑢 ⊆ 𝑠) |
22 | 21 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → 𝑢 ⊆ 𝑠) |
23 | | simprll 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → 𝑤 ∈ 𝑢) |
24 | 22, 23 | sseldd 3878 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → 𝑤 ∈ 𝑠) |
25 | 7 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → 𝐽 ∈ Top) |
26 | | elpwi 4497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑠 ∈ 𝒫 ∪ 𝐽
→ 𝑠 ⊆ ∪ 𝐽) |
27 | 26 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ (𝑠 ∈ 𝒫
∪ 𝐽 ∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) → 𝑠 ⊆ ∪ 𝐽) |
28 | 27 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → 𝑠 ⊆ ∪ 𝐽) |
29 | 3 | restuni 21913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐽 ∈ Top ∧ 𝑠 ⊆ ∪ 𝐽)
→ 𝑠 = ∪ (𝐽
↾t 𝑠)) |
30 | 25, 28, 29 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → 𝑠 = ∪ (𝐽 ↾t 𝑠)) |
31 | 24, 30 | eleqtrd 2835 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → 𝑤 ∈ ∪ (𝐽 ↾t 𝑠)) |
32 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → 𝑦 ∈ 𝑢) |
33 | 22, 32 | sseldd 3878 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → 𝑦 ∈ 𝑠) |
34 | 33, 30 | eleqtrd 2835 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → 𝑦 ∈ ∪ (𝐽 ↾t 𝑠)) |
35 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ∪ (𝐽
↾t 𝑠) =
∪ (𝐽 ↾t 𝑠) |
36 | 35 | pconncn 32757 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐽 ↾t 𝑠) ∈ PConn ∧ 𝑤 ∈ ∪ (𝐽
↾t 𝑠)
∧ 𝑦 ∈ ∪ (𝐽
↾t 𝑠))
→ ∃ℎ ∈ (II
Cn (𝐽 ↾t
𝑠))((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦)) |
37 | 20, 31, 34, 36 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → ∃ℎ ∈ (II Cn (𝐽 ↾t 𝑠))((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦)) |
38 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢) → 𝑔 ∈ (II Cn 𝐽)) |
39 | 38 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → 𝑔 ∈ (II Cn 𝐽)) |
40 | 25 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → 𝐽 ∈ Top) |
41 | | cnrest2r 22038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐽 ∈ Top → (II Cn (𝐽 ↾t 𝑠)) ⊆ (II Cn 𝐽)) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → (II Cn (𝐽 ↾t 𝑠)) ⊆ (II Cn 𝐽)) |
43 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → ℎ ∈ (II Cn (𝐽 ↾t 𝑠))) |
44 | 42, 43 | sseldd 3878 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → ℎ ∈ (II Cn 𝐽)) |
45 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢) → ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤)) |
46 | 45 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤)) |
47 | 46 | simprd 499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → (𝑔‘1) = 𝑤) |
48 | | simprrl 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → (ℎ‘0) = 𝑤) |
49 | 47, 48 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → (𝑔‘1) = (ℎ‘0)) |
50 | 39, 44, 49 | pcocn 23769 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → (𝑔(*𝑝‘𝐽)ℎ) ∈ (II Cn 𝐽)) |
51 | 39, 44 | pco0 23766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → ((𝑔(*𝑝‘𝐽)ℎ)‘0) = (𝑔‘0)) |
52 | 46 | simpld 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → (𝑔‘0) = 𝑥) |
53 | 51, 52 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → ((𝑔(*𝑝‘𝐽)ℎ)‘0) = 𝑥) |
54 | 39, 44 | pco1 23767 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → ((𝑔(*𝑝‘𝐽)ℎ)‘1) = (ℎ‘1)) |
55 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → (ℎ‘1) = 𝑦) |
56 | 54, 55 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → ((𝑔(*𝑝‘𝐽)ℎ)‘1) = 𝑦) |
57 | | fveq1 6673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓 = (𝑔(*𝑝‘𝐽)ℎ) → (𝑓‘0) = ((𝑔(*𝑝‘𝐽)ℎ)‘0)) |
58 | 57 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = (𝑔(*𝑝‘𝐽)ℎ) → ((𝑓‘0) = 𝑥 ↔ ((𝑔(*𝑝‘𝐽)ℎ)‘0) = 𝑥)) |
59 | | fveq1 6673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓 = (𝑔(*𝑝‘𝐽)ℎ) → (𝑓‘1) = ((𝑔(*𝑝‘𝐽)ℎ)‘1)) |
60 | 59 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = (𝑔(*𝑝‘𝐽)ℎ) → ((𝑓‘1) = 𝑦 ↔ ((𝑔(*𝑝‘𝐽)ℎ)‘1) = 𝑦)) |
61 | 58, 60 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = (𝑔(*𝑝‘𝐽)ℎ) → (((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ (((𝑔(*𝑝‘𝐽)ℎ)‘0) = 𝑥 ∧ ((𝑔(*𝑝‘𝐽)ℎ)‘1) = 𝑦))) |
62 | 61 | rspcev 3526 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑔(*𝑝‘𝐽)ℎ) ∈ (II Cn 𝐽) ∧ (((𝑔(*𝑝‘𝐽)ℎ)‘0) = 𝑥 ∧ ((𝑔(*𝑝‘𝐽)ℎ)‘1) = 𝑦)) → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
63 | 50, 53, 56, 62 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
64 | 37, 63 | rexlimddv 3201 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
65 | 64 | anassrs 471 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ (𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤)))) ∧ 𝑦 ∈ 𝑢) → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
66 | 65 | ralrimiva 3096 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ (𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤)))) → ∀𝑦 ∈ 𝑢 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
67 | 66 | anassrs 471 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ 𝑤 ∈ 𝑢) ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) → ∀𝑦 ∈ 𝑢 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
68 | 67 | rexlimdvaa 3195 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ 𝑤 ∈ 𝑢) → (∃𝑔 ∈ (II Cn 𝐽)((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤) → ∀𝑦 ∈ 𝑢 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦))) |
69 | 21 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ 𝑤 ∈ 𝑢) → 𝑢 ⊆ 𝑠) |
70 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ 𝑤 ∈ 𝑢) → 𝑠 ∈ 𝒫 ∪ 𝐽) |
71 | 70, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ 𝑤 ∈ 𝑢) → 𝑠 ⊆ ∪ 𝐽) |
72 | 69, 71 | sstrd 3887 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ 𝑤 ∈ 𝑢) → 𝑢 ⊆ ∪ 𝐽) |
73 | 68, 72 | jctild 529 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ 𝑤 ∈ 𝑢) → (∃𝑔 ∈ (II Cn 𝐽)((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤) → (𝑢 ⊆ ∪ 𝐽 ∧ ∀𝑦 ∈ 𝑢 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))) |
74 | | fveq1 6673 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑔 → (𝑓‘0) = (𝑔‘0)) |
75 | 74 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑔 → ((𝑓‘0) = 𝑥 ↔ (𝑔‘0) = 𝑥)) |
76 | | fveq1 6673 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑔 → (𝑓‘1) = (𝑔‘1)) |
77 | 76 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑔 → ((𝑓‘1) = 𝑤 ↔ (𝑔‘1) = 𝑤)) |
78 | 75, 77 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑔 → (((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑤) ↔ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) |
79 | 78 | cbvrexvw 3350 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑤) ↔ ∃𝑔 ∈ (II Cn 𝐽)((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤)) |
80 | | ssrab 3962 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ↔ (𝑢 ⊆ ∪ 𝐽 ∧ ∀𝑦 ∈ 𝑢 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦))) |
81 | 73, 79, 80 | 3imtr4g 299 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ 𝑤 ∈ 𝑢) → (∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑤) → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)})) |
82 | 18, 81 | syl5 34 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ 𝑤 ∈ 𝑢) → (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)})) |
83 | 82 | ralrimiva 3096 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ (𝑠 ∈ 𝒫
∪ 𝐽 ∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) → ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)})) |
84 | 13, 83 | jca 515 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ (𝑠 ∈ 𝒫
∪ 𝐽 ∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) → (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}))) |
85 | 84 | expr 460 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ 𝑠 ∈ 𝒫
∪ 𝐽) → ((𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn) → (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)})))) |
86 | 85 | reximdv 3183 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ 𝑠 ∈ 𝒫
∪ 𝐽) → (∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn) → ∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)})))) |
87 | 86 | rexlimdva 3194 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
→ (∃𝑠 ∈
𝒫 ∪ 𝐽∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn) → ∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)})))) |
88 | 12, 87 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
→ ∃𝑢 ∈
𝐽 (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}))) |
89 | 88 | anassrs 471 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
∧ 𝑧 ∈ ∪ 𝐽)
→ ∃𝑢 ∈
𝐽 (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}))) |
90 | 89 | ralrimiva 3096 |
. . . . . . . 8
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ ∀𝑧 ∈
∪ 𝐽∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}))) |
91 | 1 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ 𝐽 ∈
Top) |
92 | | ssrab2 3969 |
. . . . . . . . 9
⊢ {𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ⊆ ∪ 𝐽 |
93 | 3 | isclo2 21839 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ {𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ⊆ ∪ 𝐽) → ({𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ ∀𝑧 ∈ ∪ 𝐽∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)})))) |
94 | 91, 92, 93 | sylancl 589 |
. . . . . . . 8
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ ({𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ ∀𝑧 ∈ ∪ 𝐽∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)})))) |
95 | 90, 94 | mpbird 260 |
. . . . . . 7
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ {𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ∈ (𝐽 ∩ (Clsd‘𝐽))) |
96 | 5, 95 | sseldi 3875 |
. . . . . 6
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ {𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ∈ 𝐽) |
97 | | simpr 488 |
. . . . . . . 8
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ 𝑥 ∈ ∪ 𝐽) |
98 | | iitopon 23631 |
. . . . . . . . . 10
⊢ II ∈
(TopOn‘(0[,]1)) |
99 | 98 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ II ∈ (TopOn‘(0[,]1))) |
100 | 3 | toptopon 21668 |
. . . . . . . . . 10
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
101 | 91, 100 | sylib 221 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ 𝐽 ∈
(TopOn‘∪ 𝐽)) |
102 | | cnconst2 22034 |
. . . . . . . . 9
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝑥 ∈ ∪ 𝐽)
→ ((0[,]1) × {𝑥}) ∈ (II Cn 𝐽)) |
103 | 99, 101, 97, 102 | syl3anc 1372 |
. . . . . . . 8
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ ((0[,]1) × {𝑥}) ∈ (II Cn 𝐽)) |
104 | | 0elunit 12943 |
. . . . . . . . 9
⊢ 0 ∈
(0[,]1) |
105 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
106 | 105 | fvconst2 6976 |
. . . . . . . . 9
⊢ (0 ∈
(0[,]1) → (((0[,]1) × {𝑥})‘0) = 𝑥) |
107 | 104, 106 | mp1i 13 |
. . . . . . . 8
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ (((0[,]1) × {𝑥})‘0) = 𝑥) |
108 | | 1elunit 12944 |
. . . . . . . . 9
⊢ 1 ∈
(0[,]1) |
109 | 105 | fvconst2 6976 |
. . . . . . . . 9
⊢ (1 ∈
(0[,]1) → (((0[,]1) × {𝑥})‘1) = 𝑥) |
110 | 108, 109 | mp1i 13 |
. . . . . . . 8
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ (((0[,]1) × {𝑥})‘1) = 𝑥) |
111 | | eqeq2 2750 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ((𝑓‘1) = 𝑦 ↔ (𝑓‘1) = 𝑥)) |
112 | 111 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ ((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑥))) |
113 | | fveq1 6673 |
. . . . . . . . . . 11
⊢ (𝑓 = ((0[,]1) × {𝑥}) → (𝑓‘0) = (((0[,]1) × {𝑥})‘0)) |
114 | 113 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ (𝑓 = ((0[,]1) × {𝑥}) → ((𝑓‘0) = 𝑥 ↔ (((0[,]1) × {𝑥})‘0) = 𝑥)) |
115 | | fveq1 6673 |
. . . . . . . . . . 11
⊢ (𝑓 = ((0[,]1) × {𝑥}) → (𝑓‘1) = (((0[,]1) × {𝑥})‘1)) |
116 | 115 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ (𝑓 = ((0[,]1) × {𝑥}) → ((𝑓‘1) = 𝑥 ↔ (((0[,]1) × {𝑥})‘1) = 𝑥)) |
117 | 114, 116 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑓 = ((0[,]1) × {𝑥}) → (((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑥) ↔ ((((0[,]1) × {𝑥})‘0) = 𝑥 ∧ (((0[,]1) × {𝑥})‘1) = 𝑥))) |
118 | 112, 117 | rspc2ev 3538 |
. . . . . . . 8
⊢ ((𝑥 ∈ ∪ 𝐽
∧ ((0[,]1) × {𝑥})
∈ (II Cn 𝐽) ∧
((((0[,]1) × {𝑥})‘0) = 𝑥 ∧ (((0[,]1) × {𝑥})‘1) = 𝑥)) → ∃𝑦 ∈ ∪ 𝐽∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
119 | 97, 103, 107, 110, 118 | syl112anc 1375 |
. . . . . . 7
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ ∃𝑦 ∈
∪ 𝐽∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
120 | | rabn0 4274 |
. . . . . . 7
⊢ ({𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ≠ ∅ ↔ ∃𝑦 ∈ ∪ 𝐽∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
121 | 119, 120 | sylibr 237 |
. . . . . 6
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ {𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ≠ ∅) |
122 | | inss2 4120 |
. . . . . . 7
⊢ (𝐽 ∩ (Clsd‘𝐽)) ⊆ (Clsd‘𝐽) |
123 | 122, 95 | sseldi 3875 |
. . . . . 6
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ {𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ∈ (Clsd‘𝐽)) |
124 | 3, 4, 96, 121, 123 | connclo 22166 |
. . . . 5
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ {𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} = ∪ 𝐽) |
125 | 124 | eqcomd 2744 |
. . . 4
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ ∪ 𝐽 = {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}) |
126 | | rabid2 3284 |
. . . 4
⊢ (∪ 𝐽 =
{𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ↔ ∀𝑦 ∈ ∪ 𝐽∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
127 | 125, 126 | sylib 221 |
. . 3
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ ∀𝑦 ∈
∪ 𝐽∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
128 | 127 | ralrimiva 3096 |
. 2
⊢ ((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
→ ∀𝑥 ∈
∪ 𝐽∀𝑦 ∈ ∪ 𝐽∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
129 | 3 | ispconn 32756 |
. 2
⊢ (𝐽 ∈ PConn ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦))) |
130 | 2, 128, 129 | sylanbrc 586 |
1
⊢ ((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
→ 𝐽 ∈
PConn) |