| Step | Hyp | Ref
| Expression |
| 1 | | conntop 23425 |
. . 3
⊢ (𝐽 ∈ Conn → 𝐽 ∈ Top) |
| 2 | 1 | adantr 480 |
. 2
⊢ ((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
→ 𝐽 ∈
Top) |
| 3 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 4 | | simpll 767 |
. . . . . 6
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ 𝐽 ∈
Conn) |
| 5 | | inss1 4237 |
. . . . . . 7
⊢ (𝐽 ∩ (Clsd‘𝐽)) ⊆ 𝐽 |
| 6 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
→ 𝐽 ∈
𝑛-Locally PConn) |
| 7 | 1 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
→ 𝐽 ∈
Top) |
| 8 | 3 | topopn 22912 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ Top → ∪ 𝐽
∈ 𝐽) |
| 9 | 7, 8 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
→ ∪ 𝐽 ∈ 𝐽) |
| 10 | | simprr 773 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
→ 𝑧 ∈ ∪ 𝐽) |
| 11 | | nlly2i 23484 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ 𝑛-Locally PConn
∧ ∪ 𝐽 ∈ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽) → ∃𝑠 ∈ 𝒫 ∪ 𝐽∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn)) |
| 12 | 6, 9, 10, 11 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
→ ∃𝑠 ∈
𝒫 ∪ 𝐽∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn)) |
| 13 | | simprr1 1222 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ (𝑠 ∈ 𝒫
∪ 𝐽 ∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) → 𝑧 ∈ 𝑢) |
| 14 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑤 → ((𝑓‘1) = 𝑦 ↔ (𝑓‘1) = 𝑤)) |
| 15 | 14 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑤 → (((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ ((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑤))) |
| 16 | 15 | rexbidv 3179 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑤 → (∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑤))) |
| 17 | 16 | elrab 3692 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ↔ (𝑤 ∈ ∪ 𝐽 ∧ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑤))) |
| 18 | 17 | simprbi 496 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑤)) |
| 19 | | simprr3 1224 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ (𝑠 ∈ 𝒫
∪ 𝐽 ∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) → (𝐽 ↾t 𝑠) ∈ PConn) |
| 20 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → (𝐽 ↾t 𝑠) ∈ PConn) |
| 21 | | simprr2 1223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ (𝑠 ∈ 𝒫
∪ 𝐽 ∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) → 𝑢 ⊆ 𝑠) |
| 22 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3984 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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 4607 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑠 ∈ 𝒫 ∪ 𝐽
→ 𝑠 ⊆ ∪ 𝐽) |
| 27 | 26 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ (𝑠 ∈ 𝒫
∪ 𝐽 ∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) → 𝑠 ⊆ ∪ 𝐽) |
| 28 | 27 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → 𝑠 ⊆ ∪ 𝐽) |
| 29 | 3 | restuni 23170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐽 ∈ Top ∧ 𝑠 ⊆ ∪ 𝐽)
→ 𝑠 = ∪ (𝐽
↾t 𝑠)) |
| 30 | 25, 28, 29 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → 𝑠 = ∪ (𝐽 ↾t 𝑠)) |
| 31 | 24, 30 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 3984 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → 𝑦 ∈ 𝑠) |
| 34 | 33, 30 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → 𝑦 ∈ ∪ (𝐽 ↾t 𝑠)) |
| 35 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ∪ (𝐽
↾t 𝑠) =
∪ (𝐽 ↾t 𝑠) |
| 36 | 35 | pconncn 35229 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐽 ↾t 𝑠) ∈ PConn ∧ 𝑤 ∈ ∪ (𝐽
↾t 𝑠)
∧ 𝑦 ∈ ∪ (𝐽
↾t 𝑠))
→ ∃ℎ ∈ (II
Cn (𝐽 ↾t
𝑠))((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦)) |
| 37 | 20, 31, 34, 36 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 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 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → 𝐽 ∈ Top) |
| 41 | | cnrest2r 23295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3984 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2780 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → (𝑔‘1) = (ℎ‘0)) |
| 50 | 39, 44, 49 | pcocn 25050 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → (𝑔(*𝑝‘𝐽)ℎ) ∈ (II Cn 𝐽)) |
| 51 | 39, 44 | pco0 25047 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → ((𝑔(*𝑝‘𝐽)ℎ)‘0) = (𝑔‘0)) |
| 52 | 46 | simpld 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → (𝑔‘0) = 𝑥) |
| 53 | 51, 52 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → ((𝑔(*𝑝‘𝐽)ℎ)‘0) = 𝑥) |
| 54 | 39, 44 | pco1 25048 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → ((𝑔(*𝑝‘𝐽)ℎ)‘1) = 𝑦) |
| 57 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓 = (𝑔(*𝑝‘𝐽)ℎ) → (𝑓‘0) = ((𝑔(*𝑝‘𝐽)ℎ)‘0)) |
| 58 | 57 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = (𝑔(*𝑝‘𝐽)ℎ) → ((𝑓‘0) = 𝑥 ↔ ((𝑔(*𝑝‘𝐽)ℎ)‘0) = 𝑥)) |
| 59 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓 = (𝑔(*𝑝‘𝐽)ℎ) → (𝑓‘1) = ((𝑔(*𝑝‘𝐽)ℎ)‘1)) |
| 60 | 59 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = (𝑔(*𝑝‘𝐽)ℎ) → ((𝑓‘1) = 𝑦 ↔ ((𝑔(*𝑝‘𝐽)ℎ)‘1) = 𝑦)) |
| 61 | 58, 60 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = (𝑔(*𝑝‘𝐽)ℎ) → (((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ (((𝑔(*𝑝‘𝐽)ℎ)‘0) = 𝑥 ∧ ((𝑔(*𝑝‘𝐽)ℎ)‘1) = 𝑦))) |
| 62 | 61 | rspcev 3622 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑔(*𝑝‘𝐽)ℎ) ∈ (II Cn 𝐽) ∧ (((𝑔(*𝑝‘𝐽)ℎ)‘0) = 𝑥 ∧ ((𝑔(*𝑝‘𝐽)ℎ)‘1) = 𝑦)) → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 63 | 50, 53, 56, 62 | syl12anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) ∧ (ℎ ∈ (II Cn (𝐽 ↾t 𝑠)) ∧ ((ℎ‘0) = 𝑤 ∧ (ℎ‘1) = 𝑦))) → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 64 | 37, 63 | rexlimddv 3161 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ ((𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) ∧ 𝑦 ∈ 𝑢)) → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 65 | 64 | anassrs 467 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ (𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤)))) ∧ 𝑦 ∈ 𝑢) → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 66 | 65 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ (𝑤 ∈ 𝑢 ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤)))) → ∀𝑦 ∈ 𝑢 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 67 | 66 | anassrs 467 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ 𝑤 ∈ 𝑢) ∧ (𝑔 ∈ (II Cn 𝐽) ∧ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) → ∀𝑦 ∈ 𝑢 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 68 | 67 | rexlimdvaa 3156 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ 𝑤 ∈ 𝑢) → (∃𝑔 ∈ (II Cn 𝐽)((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤) → ∀𝑦 ∈ 𝑢 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦))) |
| 69 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 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 3994 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ 𝑤 ∈ 𝑢) → 𝑢 ⊆ ∪ 𝐽) |
| 73 | 68, 72 | jctild 525 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐽 ∈ Conn
∧ 𝐽 ∈
𝑛-Locally PConn) ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽)) ∧ (𝑠 ∈ 𝒫 ∪ 𝐽
∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) ∧ 𝑤 ∈ 𝑢) → (∃𝑔 ∈ (II Cn 𝐽)((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤) → (𝑢 ⊆ ∪ 𝐽 ∧ ∀𝑦 ∈ 𝑢 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))) |
| 74 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑔 → (𝑓‘0) = (𝑔‘0)) |
| 75 | 74 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑔 → ((𝑓‘0) = 𝑥 ↔ (𝑔‘0) = 𝑥)) |
| 76 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑔 → (𝑓‘1) = (𝑔‘1)) |
| 77 | 76 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑔 → ((𝑓‘1) = 𝑤 ↔ (𝑔‘1) = 𝑤)) |
| 78 | 75, 77 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑔 → (((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑤) ↔ ((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤))) |
| 79 | 78 | cbvrexvw 3238 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑤) ↔ ∃𝑔 ∈ (II Cn 𝐽)((𝑔‘0) = 𝑥 ∧ (𝑔‘1) = 𝑤)) |
| 80 | | ssrab 4073 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ↔ (𝑢 ⊆ ∪ 𝐽 ∧ ∀𝑦 ∈ 𝑢 ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦))) |
| 81 | 73, 79, 80 | 3imtr4g 296 |
. . . . . . . . . . . . . . . . 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 3146 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ (𝑠 ∈ 𝒫
∪ 𝐽 ∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) → ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)})) |
| 84 | 13, 83 | jca 511 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ (𝑠 ∈ 𝒫
∪ 𝐽 ∧ (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn))) → (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}))) |
| 85 | 84 | expr 456 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ 𝑠 ∈ 𝒫
∪ 𝐽) → ((𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn) → (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)})))) |
| 86 | 85 | reximdv 3170 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ (𝑥 ∈ ∪ 𝐽
∧ 𝑧 ∈ ∪ 𝐽))
∧ 𝑠 ∈ 𝒫
∪ 𝐽) → (∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ PConn) → ∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)})))) |
| 87 | 86 | rexlimdva 3155 |
. . . . . . . . . . 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 467 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
∧ 𝑧 ∈ ∪ 𝐽)
→ ∃𝑢 ∈
𝐽 (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}))) |
| 90 | 89 | ralrimiva 3146 |
. . . . . . . 8
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ ∀𝑧 ∈
∪ 𝐽∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}))) |
| 91 | 1 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ 𝐽 ∈
Top) |
| 92 | | ssrab2 4080 |
. . . . . . . . 9
⊢ {𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ⊆ ∪ 𝐽 |
| 93 | 3 | isclo2 23096 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ {𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ⊆ ∪ 𝐽) → ({𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ ∀𝑧 ∈ ∪ 𝐽∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)})))) |
| 94 | 91, 92, 93 | sylancl 586 |
. . . . . . . 8
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ ({𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ ∀𝑧 ∈ ∪ 𝐽∃𝑢 ∈ 𝐽 (𝑧 ∈ 𝑢 ∧ ∀𝑤 ∈ 𝑢 (𝑤 ∈ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} → 𝑢 ⊆ {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)})))) |
| 95 | 90, 94 | mpbird 257 |
. . . . . . 7
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ {𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ∈ (𝐽 ∩ (Clsd‘𝐽))) |
| 96 | 5, 95 | sselid 3981 |
. . . . . 6
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ {𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ∈ 𝐽) |
| 97 | | simpr 484 |
. . . . . . . 8
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ 𝑥 ∈ ∪ 𝐽) |
| 98 | | iitopon 24905 |
. . . . . . . . . 10
⊢ II ∈
(TopOn‘(0[,]1)) |
| 99 | 98 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ II ∈ (TopOn‘(0[,]1))) |
| 100 | 3 | toptopon 22923 |
. . . . . . . . . 10
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
| 101 | 91, 100 | sylib 218 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ 𝐽 ∈
(TopOn‘∪ 𝐽)) |
| 102 | | cnconst2 23291 |
. . . . . . . . 9
⊢ ((II
∈ (TopOn‘(0[,]1)) ∧ 𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝑥 ∈ ∪ 𝐽)
→ ((0[,]1) × {𝑥}) ∈ (II Cn 𝐽)) |
| 103 | 99, 101, 97, 102 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ ((0[,]1) × {𝑥}) ∈ (II Cn 𝐽)) |
| 104 | | 0elunit 13509 |
. . . . . . . . 9
⊢ 0 ∈
(0[,]1) |
| 105 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 106 | 105 | fvconst2 7224 |
. . . . . . . . 9
⊢ (0 ∈
(0[,]1) → (((0[,]1) × {𝑥})‘0) = 𝑥) |
| 107 | 104, 106 | mp1i 13 |
. . . . . . . 8
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ (((0[,]1) × {𝑥})‘0) = 𝑥) |
| 108 | | 1elunit 13510 |
. . . . . . . . 9
⊢ 1 ∈
(0[,]1) |
| 109 | 105 | fvconst2 7224 |
. . . . . . . . 9
⊢ (1 ∈
(0[,]1) → (((0[,]1) × {𝑥})‘1) = 𝑥) |
| 110 | 108, 109 | mp1i 13 |
. . . . . . . 8
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ (((0[,]1) × {𝑥})‘1) = 𝑥) |
| 111 | | eqeq2 2749 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ((𝑓‘1) = 𝑦 ↔ (𝑓‘1) = 𝑥)) |
| 112 | 111 | anbi2d 630 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ ((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑥))) |
| 113 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (𝑓 = ((0[,]1) × {𝑥}) → (𝑓‘0) = (((0[,]1) × {𝑥})‘0)) |
| 114 | 113 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑓 = ((0[,]1) × {𝑥}) → ((𝑓‘0) = 𝑥 ↔ (((0[,]1) × {𝑥})‘0) = 𝑥)) |
| 115 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (𝑓 = ((0[,]1) × {𝑥}) → (𝑓‘1) = (((0[,]1) × {𝑥})‘1)) |
| 116 | 115 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑓 = ((0[,]1) × {𝑥}) → ((𝑓‘1) = 𝑥 ↔ (((0[,]1) × {𝑥})‘1) = 𝑥)) |
| 117 | 114, 116 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑓 = ((0[,]1) × {𝑥}) → (((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑥) ↔ ((((0[,]1) × {𝑥})‘0) = 𝑥 ∧ (((0[,]1) × {𝑥})‘1) = 𝑥))) |
| 118 | 112, 117 | rspc2ev 3635 |
. . . . . . . 8
⊢ ((𝑥 ∈ ∪ 𝐽
∧ ((0[,]1) × {𝑥})
∈ (II Cn 𝐽) ∧
((((0[,]1) × {𝑥})‘0) = 𝑥 ∧ (((0[,]1) × {𝑥})‘1) = 𝑥)) → ∃𝑦 ∈ ∪ 𝐽∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 119 | 97, 103, 107, 110, 118 | syl112anc 1376 |
. . . . . . 7
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ ∃𝑦 ∈
∪ 𝐽∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 120 | | rabn0 4389 |
. . . . . . 7
⊢ ({𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ≠ ∅ ↔ ∃𝑦 ∈ ∪ 𝐽∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 121 | 119, 120 | sylibr 234 |
. . . . . 6
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ {𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ≠ ∅) |
| 122 | | inss2 4238 |
. . . . . . 7
⊢ (𝐽 ∩ (Clsd‘𝐽)) ⊆ (Clsd‘𝐽) |
| 123 | 122, 95 | sselid 3981 |
. . . . . 6
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ {𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ∈ (Clsd‘𝐽)) |
| 124 | 3, 4, 96, 121, 123 | connclo 23423 |
. . . . 5
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ {𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} = ∪ 𝐽) |
| 125 | 124 | eqcomd 2743 |
. . . 4
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ ∪ 𝐽 = {𝑦 ∈ ∪ 𝐽 ∣ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}) |
| 126 | | rabid2 3470 |
. . . 4
⊢ (∪ 𝐽 =
{𝑦 ∈ ∪ 𝐽
∣ ∃𝑓 ∈ (II
Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)} ↔ ∀𝑦 ∈ ∪ 𝐽∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 127 | 125, 126 | sylib 218 |
. . 3
⊢ (((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
∧ 𝑥 ∈ ∪ 𝐽)
→ ∀𝑦 ∈
∪ 𝐽∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 128 | 127 | ralrimiva 3146 |
. 2
⊢ ((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
→ ∀𝑥 ∈
∪ 𝐽∀𝑦 ∈ ∪ 𝐽∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)) |
| 129 | 3 | ispconn 35228 |
. 2
⊢ (𝐽 ∈ PConn ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦))) |
| 130 | 2, 128, 129 | sylanbrc 583 |
1
⊢ ((𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn)
→ 𝐽 ∈
PConn) |