Step | Hyp | Ref
| Expression |
1 | | cntop2 21992 |
. . 3
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
2 | 1 | 3ad2ant3 1136 |
. 2
⊢ ((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Top) |
3 | | df-ne 2935 |
. . . . . . 7
⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅) |
4 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ ∪ 𝐽 =
∪ 𝐽 |
5 | | simpl1 1192 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝐽 ∈ Conn) |
6 | | simpl3 1194 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
7 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) |
8 | 7 | elin1d 4088 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ 𝐾) |
9 | | cnima 22016 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑥 ∈ 𝐾) → (◡𝐹 “ 𝑥) ∈ 𝐽) |
10 | 6, 8, 9 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) ∈ 𝐽) |
11 | | elssuni 4828 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐾 → 𝑥 ⊆ ∪ 𝐾) |
12 | 8, 11 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ ∪ 𝐾) |
13 | | cnconn.2 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑌 = ∪
𝐾 |
14 | 12, 13 | sseqtrrdi 3928 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ 𝑌) |
15 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝐹:𝑋–onto→𝑌) |
16 | | forn 6595 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝑋–onto→𝑌 → ran 𝐹 = 𝑌) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → ran 𝐹 = 𝑌) |
18 | 14, 17 | sseqtrrd 3918 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ ran 𝐹) |
19 | | df-rn 5536 |
. . . . . . . . . . . . . . . 16
⊢ ran 𝐹 = dom ◡𝐹 |
20 | 18, 19 | sseqtrdi 3927 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ dom ◡𝐹) |
21 | | sseqin2 4106 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ⊆ dom ◡𝐹 ↔ (dom ◡𝐹 ∩ 𝑥) = 𝑥) |
22 | 20, 21 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (dom ◡𝐹 ∩ 𝑥) = 𝑥) |
23 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ≠ ∅) |
24 | 22, 23 | eqnetrd 3001 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (dom ◡𝐹 ∩ 𝑥) ≠ ∅) |
25 | | imadisj 5922 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐹 “ 𝑥) = ∅ ↔ (dom ◡𝐹 ∩ 𝑥) = ∅) |
26 | 25 | necon3bii 2986 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹 “ 𝑥) ≠ ∅ ↔ (dom ◡𝐹 ∩ 𝑥) ≠ ∅) |
27 | 24, 26 | sylibr 237 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) ≠ ∅) |
28 | 7 | elin2d 4089 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ (Clsd‘𝐾)) |
29 | | cnclima 22019 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑥 ∈ (Clsd‘𝐾)) → (◡𝐹 “ 𝑥) ∈ (Clsd‘𝐽)) |
30 | 6, 28, 29 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) ∈ (Clsd‘𝐽)) |
31 | 4, 5, 10, 27, 30 | connclo 22166 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) = ∪ 𝐽) |
32 | 4, 13 | cnf 21997 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶𝑌) |
33 | | fdm 6513 |
. . . . . . . . . . . 12
⊢ (𝐹:∪
𝐽⟶𝑌 → dom 𝐹 = ∪ 𝐽) |
34 | 6, 32, 33 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → dom 𝐹 = ∪ 𝐽) |
35 | | fof 6592 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
36 | | fdm 6513 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋) |
37 | 15, 35, 36 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → dom 𝐹 = 𝑋) |
38 | 31, 34, 37 | 3eqtr2d 2779 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) = 𝑋) |
39 | 38 | imaeq2d 5903 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹 “ (◡𝐹 “ 𝑥)) = (𝐹 “ 𝑋)) |
40 | | foimacnv 6635 |
. . . . . . . . . 10
⊢ ((𝐹:𝑋–onto→𝑌 ∧ 𝑥 ⊆ 𝑌) → (𝐹 “ (◡𝐹 “ 𝑥)) = 𝑥) |
41 | 15, 14, 40 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹 “ (◡𝐹 “ 𝑥)) = 𝑥) |
42 | | foima 6597 |
. . . . . . . . . 10
⊢ (𝐹:𝑋–onto→𝑌 → (𝐹 “ 𝑋) = 𝑌) |
43 | 15, 42 | syl 17 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹 “ 𝑋) = 𝑌) |
44 | 39, 41, 43 | 3eqtr3d 2781 |
. . . . . . . 8
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 = 𝑌) |
45 | 44 | expr 460 |
. . . . . . 7
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → (𝑥 ≠ ∅ → 𝑥 = 𝑌)) |
46 | 3, 45 | syl5bir 246 |
. . . . . 6
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → (¬ 𝑥 = ∅ → 𝑥 = 𝑌)) |
47 | 46 | orrd 862 |
. . . . 5
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → (𝑥 = ∅ ∨ 𝑥 = 𝑌)) |
48 | | vex 3402 |
. . . . . 6
⊢ 𝑥 ∈ V |
49 | 48 | elpr 4539 |
. . . . 5
⊢ (𝑥 ∈ {∅, 𝑌} ↔ (𝑥 = ∅ ∨ 𝑥 = 𝑌)) |
50 | 47, 49 | sylibr 237 |
. . . 4
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → 𝑥 ∈ {∅, 𝑌}) |
51 | 50 | ex 416 |
. . 3
⊢ ((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) → 𝑥 ∈ {∅, 𝑌})) |
52 | 51 | ssrdv 3883 |
. 2
⊢ ((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐾 ∩ (Clsd‘𝐾)) ⊆ {∅, 𝑌}) |
53 | 13 | isconn2 22165 |
. 2
⊢ (𝐾 ∈ Conn ↔ (𝐾 ∈ Top ∧ (𝐾 ∩ (Clsd‘𝐾)) ⊆ {∅, 𝑌})) |
54 | 2, 52, 53 | sylanbrc 586 |
1
⊢ ((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Conn) |