Proof of Theorem connima
Step | Hyp | Ref
| Expression |
1 | | connima.c |
. 2
⊢ (𝜑 → (𝐽 ↾t 𝐴) ∈ Conn) |
2 | | connima.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
3 | | connima.x |
. . . . . . 7
⊢ 𝑋 = ∪
𝐽 |
4 | | eqid 2622 |
. . . . . . 7
⊢ ∪ 𝐾 =
∪ 𝐾 |
5 | 3, 4 | cnf 21050 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶∪ 𝐾) |
6 | 2, 5 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹:𝑋⟶∪ 𝐾) |
7 | | ffun 6048 |
. . . . 5
⊢ (𝐹:𝑋⟶∪ 𝐾 → Fun 𝐹) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝜑 → Fun 𝐹) |
9 | | connima.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑋) |
10 | | fdm 6051 |
. . . . . 6
⊢ (𝐹:𝑋⟶∪ 𝐾 → dom 𝐹 = 𝑋) |
11 | 6, 10 | syl 17 |
. . . . 5
⊢ (𝜑 → dom 𝐹 = 𝑋) |
12 | 9, 11 | sseqtr4d 3642 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ dom 𝐹) |
13 | | fores 6124 |
. . . 4
⊢ ((Fun
𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴)) |
14 | 8, 12, 13 | syl2anc 693 |
. . 3
⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴)) |
15 | | cntop2 21045 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
16 | 2, 15 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ Top) |
17 | | imassrn 5477 |
. . . . . 6
⊢ (𝐹 “ 𝐴) ⊆ ran 𝐹 |
18 | | frn 6053 |
. . . . . . 7
⊢ (𝐹:𝑋⟶∪ 𝐾 → ran 𝐹 ⊆ ∪ 𝐾) |
19 | 6, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 ⊆ ∪ 𝐾) |
20 | 17, 19 | syl5ss 3614 |
. . . . 5
⊢ (𝜑 → (𝐹 “ 𝐴) ⊆ ∪ 𝐾) |
21 | 4 | restuni 20966 |
. . . . 5
⊢ ((𝐾 ∈ Top ∧ (𝐹 “ 𝐴) ⊆ ∪ 𝐾) → (𝐹 “ 𝐴) = ∪ (𝐾 ↾t (𝐹 “ 𝐴))) |
22 | 16, 20, 21 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝐹 “ 𝐴) = ∪ (𝐾 ↾t (𝐹 “ 𝐴))) |
23 | | foeq3 6113 |
. . . 4
⊢ ((𝐹 “ 𝐴) = ∪ (𝐾 ↾t (𝐹 “ 𝐴)) → ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ (𝐹 ↾ 𝐴):𝐴–onto→∪ (𝐾 ↾t (𝐹 “ 𝐴)))) |
24 | 22, 23 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ (𝐹 ↾ 𝐴):𝐴–onto→∪ (𝐾 ↾t (𝐹 “ 𝐴)))) |
25 | 14, 24 | mpbid 222 |
. 2
⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴–onto→∪ (𝐾 ↾t (𝐹 “ 𝐴))) |
26 | 3 | cnrest 21089 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) |
27 | 2, 9, 26 | syl2anc 693 |
. . 3
⊢ (𝜑 → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) |
28 | 4 | toptopon 20722 |
. . . . 5
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
29 | 16, 28 | sylib 208 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
30 | | df-ima 5127 |
. . . . 5
⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴) |
31 | | eqimss2 3658 |
. . . . 5
⊢ ((𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴) → ran (𝐹 ↾ 𝐴) ⊆ (𝐹 “ 𝐴)) |
32 | 30, 31 | mp1i 13 |
. . . 4
⊢ (𝜑 → ran (𝐹 ↾ 𝐴) ⊆ (𝐹 “ 𝐴)) |
33 | | cnrest2 21090 |
. . . 4
⊢ ((𝐾 ∈ (TopOn‘∪ 𝐾)
∧ ran (𝐹 ↾ 𝐴) ⊆ (𝐹 “ 𝐴) ∧ (𝐹 “ 𝐴) ⊆ ∪ 𝐾) → ((𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) ↔ (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn (𝐾 ↾t (𝐹 “ 𝐴))))) |
34 | 29, 32, 20, 33 | syl3anc 1326 |
. . 3
⊢ (𝜑 → ((𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) ↔ (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn (𝐾 ↾t (𝐹 “ 𝐴))))) |
35 | 27, 34 | mpbid 222 |
. 2
⊢ (𝜑 → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn (𝐾 ↾t (𝐹 “ 𝐴)))) |
36 | | eqid 2622 |
. . 3
⊢ ∪ (𝐾
↾t (𝐹
“ 𝐴)) = ∪ (𝐾
↾t (𝐹
“ 𝐴)) |
37 | 36 | cnconn 21225 |
. 2
⊢ (((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐹 ↾ 𝐴):𝐴–onto→∪ (𝐾 ↾t (𝐹 “ 𝐴)) ∧ (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn (𝐾 ↾t (𝐹 “ 𝐴)))) → (𝐾 ↾t (𝐹 “ 𝐴)) ∈ Conn) |
38 | 1, 25, 35, 37 | syl3anc 1326 |
1
⊢ (𝜑 → (𝐾 ↾t (𝐹 “ 𝐴)) ∈ Conn) |