| Step | Hyp | Ref
| Expression |
| 1 | | cntop2 23249 |
. . 3
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
| 2 | 1 | 3ad2ant3 1136 |
. 2
⊢ ((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Top) |
| 3 | | df-ne 2941 |
. . . . . . 7
⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅) |
| 4 | | eqid 2737 |
. . . . . . . . . . . 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 4204 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ 𝐾) |
| 9 | | cnima 23273 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑥 ∈ 𝐾) → (◡𝐹 “ 𝑥) ∈ 𝐽) |
| 10 | 6, 8, 9 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) ∈ 𝐽) |
| 11 | | elssuni 4937 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐾 → 𝑥 ⊆ ∪ 𝐾) |
| 12 | 8, 11 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ ∪ 𝐾) |
| 13 | | cnconn.2 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑌 = ∪
𝐾 |
| 14 | 12, 13 | sseqtrrdi 4025 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ 𝑌) |
| 15 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝐹:𝑋–onto→𝑌) |
| 16 | | forn 6823 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝑋–onto→𝑌 → ran 𝐹 = 𝑌) |
| 17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → ran 𝐹 = 𝑌) |
| 18 | 14, 17 | sseqtrrd 4021 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ ran 𝐹) |
| 19 | | df-rn 5696 |
. . . . . . . . . . . . . . . 16
⊢ ran 𝐹 = dom ◡𝐹 |
| 20 | 18, 19 | sseqtrdi 4024 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ dom ◡𝐹) |
| 21 | | sseqin2 4223 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ⊆ dom ◡𝐹 ↔ (dom ◡𝐹 ∩ 𝑥) = 𝑥) |
| 22 | 20, 21 | sylib 218 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (dom ◡𝐹 ∩ 𝑥) = 𝑥) |
| 23 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ≠ ∅) |
| 24 | 22, 23 | eqnetrd 3008 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (dom ◡𝐹 ∩ 𝑥) ≠ ∅) |
| 25 | | imadisj 6098 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐹 “ 𝑥) = ∅ ↔ (dom ◡𝐹 ∩ 𝑥) = ∅) |
| 26 | 25 | necon3bii 2993 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹 “ 𝑥) ≠ ∅ ↔ (dom ◡𝐹 ∩ 𝑥) ≠ ∅) |
| 27 | 24, 26 | sylibr 234 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) ≠ ∅) |
| 28 | 7 | elin2d 4205 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ (Clsd‘𝐾)) |
| 29 | | cnclima 23276 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑥 ∈ (Clsd‘𝐾)) → (◡𝐹 “ 𝑥) ∈ (Clsd‘𝐽)) |
| 30 | 6, 28, 29 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) ∈ (Clsd‘𝐽)) |
| 31 | 4, 5, 10, 27, 30 | connclo 23423 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) = ∪ 𝐽) |
| 32 | 4, 13 | cnf 23254 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶𝑌) |
| 33 | | fdm 6745 |
. . . . . . . . . . . 12
⊢ (𝐹:∪
𝐽⟶𝑌 → dom 𝐹 = ∪ 𝐽) |
| 34 | 6, 32, 33 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → dom 𝐹 = ∪ 𝐽) |
| 35 | | fof 6820 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
| 36 | | fdm 6745 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋) |
| 37 | 15, 35, 36 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → dom 𝐹 = 𝑋) |
| 38 | 31, 34, 37 | 3eqtr2d 2783 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) = 𝑋) |
| 39 | 38 | imaeq2d 6078 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹 “ (◡𝐹 “ 𝑥)) = (𝐹 “ 𝑋)) |
| 40 | | foimacnv 6865 |
. . . . . . . . . 10
⊢ ((𝐹:𝑋–onto→𝑌 ∧ 𝑥 ⊆ 𝑌) → (𝐹 “ (◡𝐹 “ 𝑥)) = 𝑥) |
| 41 | 15, 14, 40 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹 “ (◡𝐹 “ 𝑥)) = 𝑥) |
| 42 | | foima 6825 |
. . . . . . . . . 10
⊢ (𝐹:𝑋–onto→𝑌 → (𝐹 “ 𝑋) = 𝑌) |
| 43 | 15, 42 | syl 17 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹 “ 𝑋) = 𝑌) |
| 44 | 39, 41, 43 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 = 𝑌) |
| 45 | 44 | expr 456 |
. . . . . . 7
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → (𝑥 ≠ ∅ → 𝑥 = 𝑌)) |
| 46 | 3, 45 | biimtrrid 243 |
. . . . . 6
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → (¬ 𝑥 = ∅ → 𝑥 = 𝑌)) |
| 47 | 46 | orrd 864 |
. . . . 5
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → (𝑥 = ∅ ∨ 𝑥 = 𝑌)) |
| 48 | | vex 3484 |
. . . . . 6
⊢ 𝑥 ∈ V |
| 49 | 48 | elpr 4650 |
. . . . 5
⊢ (𝑥 ∈ {∅, 𝑌} ↔ (𝑥 = ∅ ∨ 𝑥 = 𝑌)) |
| 50 | 47, 49 | sylibr 234 |
. . . 4
⊢ (((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → 𝑥 ∈ {∅, 𝑌}) |
| 51 | 50 | ex 412 |
. . 3
⊢ ((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) → 𝑥 ∈ {∅, 𝑌})) |
| 52 | 51 | ssrdv 3989 |
. 2
⊢ ((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐾 ∩ (Clsd‘𝐾)) ⊆ {∅, 𝑌}) |
| 53 | 13 | isconn2 23422 |
. 2
⊢ (𝐾 ∈ Conn ↔ (𝐾 ∈ Top ∧ (𝐾 ∩ (Clsd‘𝐾)) ⊆ {∅, 𝑌})) |
| 54 | 2, 52, 53 | sylanbrc 583 |
1
⊢ ((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Conn) |