| Step |
Hyp |
Ref |
Expression |
| 1 |
|
conntop |
⊢ ( 𝐽 ∈ Conn → 𝐽 ∈ Top ) |
| 2 |
1
|
adantr |
⊢ ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) → 𝐽 ∈ Top ) |
| 3 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
| 4 |
|
simpll |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝐽 ∈ Conn ) |
| 5 |
|
inss1 |
⊢ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ⊆ 𝐽 |
| 6 |
|
simplr |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) → 𝐽 ∈ 𝑛-Locally PConn ) |
| 7 |
1
|
ad2antrr |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) → 𝐽 ∈ Top ) |
| 8 |
3
|
topopn |
⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽 ) |
| 9 |
7 8
|
syl |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ∪ 𝐽 ∈ 𝐽 ) |
| 10 |
|
simprr |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) → 𝑧 ∈ ∪ 𝐽 ) |
| 11 |
|
nlly2i |
⊢ ( ( 𝐽 ∈ 𝑛-Locally PConn ∧ ∪ 𝐽 ∈ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) → ∃ 𝑠 ∈ 𝒫 ∪ 𝐽 ∃ 𝑢 ∈ 𝐽 ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) |
| 12 |
6 9 10 11
|
syl3anc |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ∃ 𝑠 ∈ 𝒫 ∪ 𝐽 ∃ 𝑢 ∈ 𝐽 ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) |
| 13 |
|
simprr1 |
⊢ ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) → 𝑧 ∈ 𝑢 ) |
| 14 |
|
eqeq2 |
⊢ ( 𝑦 = 𝑤 → ( ( 𝑓 ‘ 1 ) = 𝑦 ↔ ( 𝑓 ‘ 1 ) = 𝑤 ) ) |
| 15 |
14
|
anbi2d |
⊢ ( 𝑦 = 𝑤 → ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑤 ) ) ) |
| 16 |
15
|
rexbidv |
⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑤 ) ) ) |
| 17 |
16
|
elrab |
⊢ ( 𝑤 ∈ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ↔ ( 𝑤 ∈ ∪ 𝐽 ∧ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑤 ) ) ) |
| 18 |
17
|
simprbi |
⊢ ( 𝑤 ∈ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } → ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑤 ) ) |
| 19 |
|
simprr3 |
⊢ ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) → ( 𝐽 ↾t 𝑠 ) ∈ PConn ) |
| 20 |
19
|
adantr |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) → ( 𝐽 ↾t 𝑠 ) ∈ PConn ) |
| 21 |
|
simprr2 |
⊢ ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) → 𝑢 ⊆ 𝑠 ) |
| 22 |
21
|
adantr |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) → 𝑢 ⊆ 𝑠 ) |
| 23 |
|
simprll |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) → 𝑤 ∈ 𝑢 ) |
| 24 |
22 23
|
sseldd |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) → 𝑤 ∈ 𝑠 ) |
| 25 |
7
|
ad2antrr |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) → 𝐽 ∈ Top ) |
| 26 |
|
elpwi |
⊢ ( 𝑠 ∈ 𝒫 ∪ 𝐽 → 𝑠 ⊆ ∪ 𝐽 ) |
| 27 |
26
|
ad2antrl |
⊢ ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) → 𝑠 ⊆ ∪ 𝐽 ) |
| 28 |
27
|
adantr |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) → 𝑠 ⊆ ∪ 𝐽 ) |
| 29 |
3
|
restuni |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑠 ⊆ ∪ 𝐽 ) → 𝑠 = ∪ ( 𝐽 ↾t 𝑠 ) ) |
| 30 |
25 28 29
|
syl2anc |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) → 𝑠 = ∪ ( 𝐽 ↾t 𝑠 ) ) |
| 31 |
24 30
|
eleqtrd |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) → 𝑤 ∈ ∪ ( 𝐽 ↾t 𝑠 ) ) |
| 32 |
|
simprr |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) → 𝑦 ∈ 𝑢 ) |
| 33 |
22 32
|
sseldd |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) → 𝑦 ∈ 𝑠 ) |
| 34 |
33 30
|
eleqtrd |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) → 𝑦 ∈ ∪ ( 𝐽 ↾t 𝑠 ) ) |
| 35 |
|
eqid |
⊢ ∪ ( 𝐽 ↾t 𝑠 ) = ∪ ( 𝐽 ↾t 𝑠 ) |
| 36 |
35
|
pconncn |
⊢ ( ( ( 𝐽 ↾t 𝑠 ) ∈ PConn ∧ 𝑤 ∈ ∪ ( 𝐽 ↾t 𝑠 ) ∧ 𝑦 ∈ ∪ ( 𝐽 ↾t 𝑠 ) ) → ∃ ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) |
| 37 |
20 31 34 36
|
syl3anc |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) → ∃ ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) |
| 38 |
|
simplrl |
⊢ ( ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) → 𝑔 ∈ ( II Cn 𝐽 ) ) |
| 39 |
38
|
ad2antlr |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → 𝑔 ∈ ( II Cn 𝐽 ) ) |
| 40 |
25
|
adantr |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → 𝐽 ∈ Top ) |
| 41 |
|
cnrest2r |
⊢ ( 𝐽 ∈ Top → ( II Cn ( 𝐽 ↾t 𝑠 ) ) ⊆ ( II Cn 𝐽 ) ) |
| 42 |
40 41
|
syl |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → ( II Cn ( 𝐽 ↾t 𝑠 ) ) ⊆ ( II Cn 𝐽 ) ) |
| 43 |
|
simprl |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ) |
| 44 |
42 43
|
sseldd |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → ℎ ∈ ( II Cn 𝐽 ) ) |
| 45 |
|
simplrr |
⊢ ( ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) → ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) |
| 46 |
45
|
ad2antlr |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) |
| 47 |
46
|
simprd |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → ( 𝑔 ‘ 1 ) = 𝑤 ) |
| 48 |
|
simprrl |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → ( ℎ ‘ 0 ) = 𝑤 ) |
| 49 |
47 48
|
eqtr4d |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → ( 𝑔 ‘ 1 ) = ( ℎ ‘ 0 ) ) |
| 50 |
39 44 49
|
pcocn |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) ∈ ( II Cn 𝐽 ) ) |
| 51 |
39 44
|
pco0 |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 0 ) = ( 𝑔 ‘ 0 ) ) |
| 52 |
46
|
simpld |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → ( 𝑔 ‘ 0 ) = 𝑥 ) |
| 53 |
51 52
|
eqtrd |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 0 ) = 𝑥 ) |
| 54 |
39 44
|
pco1 |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 1 ) = ( ℎ ‘ 1 ) ) |
| 55 |
|
simprrr |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → ( ℎ ‘ 1 ) = 𝑦 ) |
| 56 |
54 55
|
eqtrd |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 1 ) = 𝑦 ) |
| 57 |
|
fveq1 |
⊢ ( 𝑓 = ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) → ( 𝑓 ‘ 0 ) = ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 0 ) ) |
| 58 |
57
|
eqeq1d |
⊢ ( 𝑓 = ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) → ( ( 𝑓 ‘ 0 ) = 𝑥 ↔ ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 0 ) = 𝑥 ) ) |
| 59 |
|
fveq1 |
⊢ ( 𝑓 = ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) → ( 𝑓 ‘ 1 ) = ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 1 ) ) |
| 60 |
59
|
eqeq1d |
⊢ ( 𝑓 = ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) → ( ( 𝑓 ‘ 1 ) = 𝑦 ↔ ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 1 ) = 𝑦 ) ) |
| 61 |
58 60
|
anbi12d |
⊢ ( 𝑓 = ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) → ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ( ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 0 ) = 𝑥 ∧ ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 1 ) = 𝑦 ) ) ) |
| 62 |
61
|
rspcev |
⊢ ( ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) ∈ ( II Cn 𝐽 ) ∧ ( ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 0 ) = 𝑥 ∧ ( ( 𝑔 ( *𝑝 ‘ 𝐽 ) ℎ ) ‘ 1 ) = 𝑦 ) ) → ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 63 |
50 53 56 62
|
syl12anc |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( ℎ ∈ ( II Cn ( 𝐽 ↾t 𝑠 ) ) ∧ ( ( ℎ ‘ 0 ) = 𝑤 ∧ ( ℎ ‘ 1 ) = 𝑦 ) ) ) → ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 64 |
37 63
|
rexlimddv |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ∧ 𝑦 ∈ 𝑢 ) ) → ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 65 |
64
|
anassrs |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ) ∧ 𝑦 ∈ 𝑢 ) → ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 66 |
65
|
ralrimiva |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ ( 𝑤 ∈ 𝑢 ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) ) → ∀ 𝑦 ∈ 𝑢 ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 67 |
66
|
anassrs |
⊢ ( ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( 𝑔 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) → ∀ 𝑦 ∈ 𝑢 ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 68 |
67
|
rexlimdvaa |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ 𝑤 ∈ 𝑢 ) → ( ∃ 𝑔 ∈ ( II Cn 𝐽 ) ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) → ∀ 𝑦 ∈ 𝑢 ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) ) |
| 69 |
21
|
adantr |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ 𝑤 ∈ 𝑢 ) → 𝑢 ⊆ 𝑠 ) |
| 70 |
|
simplrl |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ 𝑤 ∈ 𝑢 ) → 𝑠 ∈ 𝒫 ∪ 𝐽 ) |
| 71 |
70 26
|
syl |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ 𝑤 ∈ 𝑢 ) → 𝑠 ⊆ ∪ 𝐽 ) |
| 72 |
69 71
|
sstrd |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ 𝑤 ∈ 𝑢 ) → 𝑢 ⊆ ∪ 𝐽 ) |
| 73 |
68 72
|
jctild |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ 𝑤 ∈ 𝑢 ) → ( ∃ 𝑔 ∈ ( II Cn 𝐽 ) ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) → ( 𝑢 ⊆ ∪ 𝐽 ∧ ∀ 𝑦 ∈ 𝑢 ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) ) ) |
| 74 |
|
fveq1 |
⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ 0 ) = ( 𝑔 ‘ 0 ) ) |
| 75 |
74
|
eqeq1d |
⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ‘ 0 ) = 𝑥 ↔ ( 𝑔 ‘ 0 ) = 𝑥 ) ) |
| 76 |
|
fveq1 |
⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ 1 ) = ( 𝑔 ‘ 1 ) ) |
| 77 |
76
|
eqeq1d |
⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ‘ 1 ) = 𝑤 ↔ ( 𝑔 ‘ 1 ) = 𝑤 ) ) |
| 78 |
75 77
|
anbi12d |
⊢ ( 𝑓 = 𝑔 → ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑤 ) ↔ ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) ) |
| 79 |
78
|
cbvrexvw |
⊢ ( ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑤 ) ↔ ∃ 𝑔 ∈ ( II Cn 𝐽 ) ( ( 𝑔 ‘ 0 ) = 𝑥 ∧ ( 𝑔 ‘ 1 ) = 𝑤 ) ) |
| 80 |
|
ssrab |
⊢ ( 𝑢 ⊆ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ↔ ( 𝑢 ⊆ ∪ 𝐽 ∧ ∀ 𝑦 ∈ 𝑢 ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) ) |
| 81 |
73 79 80
|
3imtr4g |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ 𝑤 ∈ 𝑢 ) → ( ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑤 ) → 𝑢 ⊆ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ) ) |
| 82 |
18 81
|
syl5 |
⊢ ( ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) ∧ 𝑤 ∈ 𝑢 ) → ( 𝑤 ∈ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } → 𝑢 ⊆ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ) ) |
| 83 |
82
|
ralrimiva |
⊢ ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) → ∀ 𝑤 ∈ 𝑢 ( 𝑤 ∈ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } → 𝑢 ⊆ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ) ) |
| 84 |
13 83
|
jca |
⊢ ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) ) ) → ( 𝑧 ∈ 𝑢 ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑤 ∈ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } → 𝑢 ⊆ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ) ) ) |
| 85 |
84
|
expr |
⊢ ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ 𝑠 ∈ 𝒫 ∪ 𝐽 ) → ( ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) → ( 𝑧 ∈ 𝑢 ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑤 ∈ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } → 𝑢 ⊆ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ) ) ) ) |
| 86 |
85
|
reximdv |
⊢ ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) ∧ 𝑠 ∈ 𝒫 ∪ 𝐽 ) → ( ∃ 𝑢 ∈ 𝐽 ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) → ∃ 𝑢 ∈ 𝐽 ( 𝑧 ∈ 𝑢 ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑤 ∈ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } → 𝑢 ⊆ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ) ) ) ) |
| 87 |
86
|
rexlimdva |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ( ∃ 𝑠 ∈ 𝒫 ∪ 𝐽 ∃ 𝑢 ∈ 𝐽 ( 𝑧 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝐽 ↾t 𝑠 ) ∈ PConn ) → ∃ 𝑢 ∈ 𝐽 ( 𝑧 ∈ 𝑢 ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑤 ∈ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } → 𝑢 ⊆ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ) ) ) ) |
| 88 |
12 87
|
mpd |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑧 ∈ ∪ 𝐽 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑧 ∈ 𝑢 ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑤 ∈ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } → 𝑢 ⊆ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ) ) ) |
| 89 |
88
|
anassrs |
⊢ ( ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑧 ∈ ∪ 𝐽 ) → ∃ 𝑢 ∈ 𝐽 ( 𝑧 ∈ 𝑢 ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑤 ∈ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } → 𝑢 ⊆ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ) ) ) |
| 90 |
89
|
ralrimiva |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ∀ 𝑧 ∈ ∪ 𝐽 ∃ 𝑢 ∈ 𝐽 ( 𝑧 ∈ 𝑢 ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑤 ∈ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } → 𝑢 ⊆ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ) ) ) |
| 91 |
1
|
ad2antrr |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝐽 ∈ Top ) |
| 92 |
|
ssrab2 |
⊢ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ⊆ ∪ 𝐽 |
| 93 |
3
|
isclo2 |
⊢ ( ( 𝐽 ∈ Top ∧ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ⊆ ∪ 𝐽 ) → ( { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ↔ ∀ 𝑧 ∈ ∪ 𝐽 ∃ 𝑢 ∈ 𝐽 ( 𝑧 ∈ 𝑢 ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑤 ∈ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } → 𝑢 ⊆ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ) ) ) ) |
| 94 |
91 92 93
|
sylancl |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ( { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ↔ ∀ 𝑧 ∈ ∪ 𝐽 ∃ 𝑢 ∈ 𝐽 ( 𝑧 ∈ 𝑢 ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑤 ∈ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } → 𝑢 ⊆ { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ) ) ) ) |
| 95 |
90 94
|
mpbird |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ) |
| 96 |
5 95
|
sselid |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ∈ 𝐽 ) |
| 97 |
|
simpr |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝑥 ∈ ∪ 𝐽 ) |
| 98 |
|
iitopon |
⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) |
| 99 |
98
|
a1i |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ) |
| 100 |
3
|
toptopon |
⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ) |
| 101 |
91 100
|
sylib |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ) |
| 102 |
|
cnconst2 |
⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ( 0 [,] 1 ) × { 𝑥 } ) ∈ ( II Cn 𝐽 ) ) |
| 103 |
99 101 97 102
|
syl3anc |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ( 0 [,] 1 ) × { 𝑥 } ) ∈ ( II Cn 𝐽 ) ) |
| 104 |
|
0elunit |
⊢ 0 ∈ ( 0 [,] 1 ) |
| 105 |
|
vex |
⊢ 𝑥 ∈ V |
| 106 |
105
|
fvconst2 |
⊢ ( 0 ∈ ( 0 [,] 1 ) → ( ( ( 0 [,] 1 ) × { 𝑥 } ) ‘ 0 ) = 𝑥 ) |
| 107 |
104 106
|
mp1i |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ( ( 0 [,] 1 ) × { 𝑥 } ) ‘ 0 ) = 𝑥 ) |
| 108 |
|
1elunit |
⊢ 1 ∈ ( 0 [,] 1 ) |
| 109 |
105
|
fvconst2 |
⊢ ( 1 ∈ ( 0 [,] 1 ) → ( ( ( 0 [,] 1 ) × { 𝑥 } ) ‘ 1 ) = 𝑥 ) |
| 110 |
108 109
|
mp1i |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ( ( 0 [,] 1 ) × { 𝑥 } ) ‘ 1 ) = 𝑥 ) |
| 111 |
|
eqeq2 |
⊢ ( 𝑦 = 𝑥 → ( ( 𝑓 ‘ 1 ) = 𝑦 ↔ ( 𝑓 ‘ 1 ) = 𝑥 ) ) |
| 112 |
111
|
anbi2d |
⊢ ( 𝑦 = 𝑥 → ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ↔ ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) ) ) |
| 113 |
|
fveq1 |
⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑥 } ) → ( 𝑓 ‘ 0 ) = ( ( ( 0 [,] 1 ) × { 𝑥 } ) ‘ 0 ) ) |
| 114 |
113
|
eqeq1d |
⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑥 } ) → ( ( 𝑓 ‘ 0 ) = 𝑥 ↔ ( ( ( 0 [,] 1 ) × { 𝑥 } ) ‘ 0 ) = 𝑥 ) ) |
| 115 |
|
fveq1 |
⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑥 } ) → ( 𝑓 ‘ 1 ) = ( ( ( 0 [,] 1 ) × { 𝑥 } ) ‘ 1 ) ) |
| 116 |
115
|
eqeq1d |
⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑥 } ) → ( ( 𝑓 ‘ 1 ) = 𝑥 ↔ ( ( ( 0 [,] 1 ) × { 𝑥 } ) ‘ 1 ) = 𝑥 ) ) |
| 117 |
114 116
|
anbi12d |
⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑥 } ) → ( ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ) ↔ ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ‘ 0 ) = 𝑥 ∧ ( ( ( 0 [,] 1 ) × { 𝑥 } ) ‘ 1 ) = 𝑥 ) ) ) |
| 118 |
112 117
|
rspc2ev |
⊢ ( ( 𝑥 ∈ ∪ 𝐽 ∧ ( ( 0 [,] 1 ) × { 𝑥 } ) ∈ ( II Cn 𝐽 ) ∧ ( ( ( ( 0 [,] 1 ) × { 𝑥 } ) ‘ 0 ) = 𝑥 ∧ ( ( ( 0 [,] 1 ) × { 𝑥 } ) ‘ 1 ) = 𝑥 ) ) → ∃ 𝑦 ∈ ∪ 𝐽 ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 119 |
97 103 107 110 118
|
syl112anc |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ∃ 𝑦 ∈ ∪ 𝐽 ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 120 |
|
rabn0 |
⊢ ( { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ≠ ∅ ↔ ∃ 𝑦 ∈ ∪ 𝐽 ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 121 |
119 120
|
sylibr |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ≠ ∅ ) |
| 122 |
|
inss2 |
⊢ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ⊆ ( Clsd ‘ 𝐽 ) |
| 123 |
122 95
|
sselid |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ∈ ( Clsd ‘ 𝐽 ) ) |
| 124 |
3 4 96 121 123
|
connclo |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } = ∪ 𝐽 ) |
| 125 |
124
|
eqcomd |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ∪ 𝐽 = { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ) |
| 126 |
|
rabid2 |
⊢ ( ∪ 𝐽 = { 𝑦 ∈ ∪ 𝐽 ∣ ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) } ↔ ∀ 𝑦 ∈ ∪ 𝐽 ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 127 |
125 126
|
sylib |
⊢ ( ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ∀ 𝑦 ∈ ∪ 𝐽 ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 128 |
127
|
ralrimiva |
⊢ ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) → ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) |
| 129 |
3
|
ispconn |
⊢ ( 𝐽 ∈ PConn ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) ) |
| 130 |
2 128 129
|
sylanbrc |
⊢ ( ( 𝐽 ∈ Conn ∧ 𝐽 ∈ 𝑛-Locally PConn ) → 𝐽 ∈ PConn ) |