Step | Hyp | Ref
| Expression |
1 | | cntop2 21045 |
. . 3
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
2 | 1 | 3ad2ant3 1084 |
. 2
⊢ ((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Top) |
3 | | df-ne 2795 |
. . . . . . 7
⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅) |
4 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ ∪ 𝐽 =
∪ 𝐽 |
5 | | simpl1 1064 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝐽 ∈ Conn) |
6 | | simpl3 1066 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
7 | | inss1 3833 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∩ (Clsd‘𝐾)) ⊆ 𝐾 |
8 | | simprl 794 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) |
9 | 7, 8 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ 𝐾) |
10 | | cnima 21069 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑥 ∈ 𝐾) → (◡𝐹 “ 𝑥) ∈ 𝐽) |
11 | 6, 9, 10 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) ∈ 𝐽) |
12 | | elssuni 4467 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐾 → 𝑥 ⊆ ∪ 𝐾) |
13 | 9, 12 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ ∪ 𝐾) |
14 | | cnconn.2 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑌 = ∪
𝐾 |
15 | 13, 14 | syl6sseqr 3652 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ 𝑌) |
16 | | simpl2 1065 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝐹:𝑋–onto→𝑌) |
17 | | forn 6118 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝑋–onto→𝑌 → ran 𝐹 = 𝑌) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → ran 𝐹 = 𝑌) |
19 | 15, 18 | sseqtr4d 3642 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ ran 𝐹) |
20 | | df-rn 5125 |
. . . . . . . . . . . . . . . 16
⊢ ran 𝐹 = dom ◡𝐹 |
21 | 19, 20 | syl6sseq 3651 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ dom ◡𝐹) |
22 | | sseqin2 3817 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ⊆ dom ◡𝐹 ↔ (dom ◡𝐹 ∩ 𝑥) = 𝑥) |
23 | 21, 22 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (dom ◡𝐹 ∩ 𝑥) = 𝑥) |
24 | | simprr 796 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ≠ ∅) |
25 | 23, 24 | eqnetrd 2861 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (dom ◡𝐹 ∩ 𝑥) ≠ ∅) |
26 | | imadisj 5484 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐹 “ 𝑥) = ∅ ↔ (dom ◡𝐹 ∩ 𝑥) = ∅) |
27 | 26 | necon3bii 2846 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹 “ 𝑥) ≠ ∅ ↔ (dom ◡𝐹 ∩ 𝑥) ≠ ∅) |
28 | 25, 27 | sylibr 224 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) ≠ ∅) |
29 | | inss2 3834 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∩ (Clsd‘𝐾)) ⊆ (Clsd‘𝐾) |
30 | 29, 8 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ (Clsd‘𝐾)) |
31 | | cnclima 21072 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑥 ∈ (Clsd‘𝐾)) → (◡𝐹 “ 𝑥) ∈ (Clsd‘𝐽)) |
32 | 6, 30, 31 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) ∈ (Clsd‘𝐽)) |
33 | 4, 5, 11, 28, 32 | connclo 21218 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) = ∪ 𝐽) |
34 | 4, 14 | cnf 21050 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶𝑌) |
35 | | fdm 6051 |
. . . . . . . . . . . 12
⊢ (𝐹:∪
𝐽⟶𝑌 → dom 𝐹 = ∪ 𝐽) |
36 | 6, 34, 35 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → dom 𝐹 = ∪ 𝐽) |
37 | | fof 6115 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
38 | | fdm 6051 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋) |
39 | 16, 37, 38 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → dom 𝐹 = 𝑋) |
40 | 33, 36, 39 | 3eqtr2d 2662 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) = 𝑋) |
41 | 40 | imaeq2d 5466 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹 “ (◡𝐹 “ 𝑥)) = (𝐹 “ 𝑋)) |
42 | | foimacnv 6154 |
. . . . . . . . . 10
⊢ ((𝐹:𝑋–onto→𝑌 ∧ 𝑥 ⊆ 𝑌) → (𝐹 “ (◡𝐹 “ 𝑥)) = 𝑥) |
43 | 16, 15, 42 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹 “ (◡𝐹 “ 𝑥)) = 𝑥) |
44 | | foima 6120 |
. . . . . . . . . 10
⊢ (𝐹:𝑋–onto→𝑌 → (𝐹 “ 𝑋) = 𝑌) |
45 | 16, 44 | syl 17 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹 “ 𝑋) = 𝑌) |
46 | 41, 43, 45 | 3eqtr3d 2664 |
. . . . . . . 8
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 = 𝑌) |
47 | 46 | expr 643 |
. . . . . . 7
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → (𝑥 ≠ ∅ → 𝑥 = 𝑌)) |
48 | 3, 47 | syl5bir 233 |
. . . . . 6
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → (¬ 𝑥 = ∅ → 𝑥 = 𝑌)) |
49 | 48 | orrd 393 |
. . . . 5
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → (𝑥 = ∅ ∨ 𝑥 = 𝑌)) |
50 | | vex 3203 |
. . . . . 6
⊢ 𝑥 ∈ V |
51 | 50 | elpr 4198 |
. . . . 5
⊢ (𝑥 ∈ {∅, 𝑌} ↔ (𝑥 = ∅ ∨ 𝑥 = 𝑌)) |
52 | 49, 51 | sylibr 224 |
. . . 4
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → 𝑥 ∈ {∅, 𝑌}) |
53 | 52 | ex 450 |
. . 3
⊢ ((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) → 𝑥 ∈ {∅, 𝑌})) |
54 | 53 | ssrdv 3609 |
. 2
⊢ ((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐾 ∩ (Clsd‘𝐾)) ⊆ {∅, 𝑌}) |
55 | 14 | isconn2 21217 |
. 2
⊢ (𝐾 ∈ Conn ↔ (𝐾 ∈ Top ∧ (𝐾 ∩ (Clsd‘𝐾)) ⊆ {∅, 𝑌})) |
56 | 2, 54, 55 | sylanbrc 698 |
1
⊢ ((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Conn) |