Step | Hyp | Ref
| Expression |
1 | | cntop2 20855 |
. . 3
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
2 | 1 | 3ad2ant3 1077 |
. 2
⊢ ((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Top) |
3 | | df-ne 2782 |
. . . . . . 7
⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅) |
4 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ∪ 𝐽 =
∪ 𝐽 |
5 | | simpl1 1057 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝐽 ∈ Con) |
6 | | simpl3 1059 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
7 | | inss1 3795 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∩ (Clsd‘𝐾)) ⊆ 𝐾 |
8 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) |
9 | 7, 8 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ 𝐾) |
10 | | cnima 20879 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑥 ∈ 𝐾) → (◡𝐹 “ 𝑥) ∈ 𝐽) |
11 | 6, 9, 10 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) ∈ 𝐽) |
12 | | elssuni 4403 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐾 → 𝑥 ⊆ ∪ 𝐾) |
13 | 9, 12 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ ∪ 𝐾) |
14 | | cnconn.2 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑌 = ∪
𝐾 |
15 | 13, 14 | syl6sseqr 3615 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ 𝑌) |
16 | | simpl2 1058 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝐹:𝑋–onto→𝑌) |
17 | | forn 6031 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝑋–onto→𝑌 → ran 𝐹 = 𝑌) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → ran 𝐹 = 𝑌) |
19 | 15, 18 | sseqtr4d 3605 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ ran 𝐹) |
20 | | df-rn 5049 |
. . . . . . . . . . . . . . . 16
⊢ ran 𝐹 = dom ◡𝐹 |
21 | 19, 20 | syl6sseq 3614 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ⊆ dom ◡𝐹) |
22 | | sseqin2 3779 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ⊆ dom ◡𝐹 ↔ (dom ◡𝐹 ∩ 𝑥) = 𝑥) |
23 | 21, 22 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (dom ◡𝐹 ∩ 𝑥) = 𝑥) |
24 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ≠ ∅) |
25 | 23, 24 | eqnetrd 2849 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (dom ◡𝐹 ∩ 𝑥) ≠ ∅) |
26 | | imadisj 5403 |
. . . . . . . . . . . . . 14
⊢ ((◡𝐹 “ 𝑥) = ∅ ↔ (dom ◡𝐹 ∩ 𝑥) = ∅) |
27 | 26 | necon3bii 2834 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹 “ 𝑥) ≠ ∅ ↔ (dom ◡𝐹 ∩ 𝑥) ≠ ∅) |
28 | 25, 27 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) ≠ ∅) |
29 | | inss2 3796 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∩ (Clsd‘𝐾)) ⊆ (Clsd‘𝐾) |
30 | 29, 8 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ (Clsd‘𝐾)) |
31 | | cnclima 20882 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑥 ∈ (Clsd‘𝐾)) → (◡𝐹 “ 𝑥) ∈ (Clsd‘𝐽)) |
32 | 6, 30, 31 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) ∈ (Clsd‘𝐽)) |
33 | 4, 5, 11, 28, 32 | conclo 21028 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) = ∪ 𝐽) |
34 | 4, 14 | cnf 20860 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶𝑌) |
35 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝐹:∪
𝐽⟶𝑌 → dom 𝐹 = ∪ 𝐽) |
36 | 6, 34, 35 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → dom 𝐹 = ∪ 𝐽) |
37 | | fof 6028 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
38 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋) |
39 | 16, 37, 38 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → dom 𝐹 = 𝑋) |
40 | 33, 36, 39 | 3eqtr2d 2650 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (◡𝐹 “ 𝑥) = 𝑋) |
41 | 40 | imaeq2d 5385 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹 “ (◡𝐹 “ 𝑥)) = (𝐹 “ 𝑋)) |
42 | | foimacnv 6067 |
. . . . . . . . . 10
⊢ ((𝐹:𝑋–onto→𝑌 ∧ 𝑥 ⊆ 𝑌) → (𝐹 “ (◡𝐹 “ 𝑥)) = 𝑥) |
43 | 16, 15, 42 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹 “ (◡𝐹 “ 𝑥)) = 𝑥) |
44 | | foima 6033 |
. . . . . . . . . 10
⊢ (𝐹:𝑋–onto→𝑌 → (𝐹 “ 𝑋) = 𝑌) |
45 | 16, 44 | syl 17 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → (𝐹 “ 𝑋) = 𝑌) |
46 | 41, 43, 45 | 3eqtr3d 2652 |
. . . . . . . 8
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) ∧ 𝑥 ≠ ∅)) → 𝑥 = 𝑌) |
47 | 46 | expr 641 |
. . . . . . 7
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → (𝑥 ≠ ∅ → 𝑥 = 𝑌)) |
48 | 3, 47 | syl5bir 232 |
. . . . . 6
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → (¬ 𝑥 = ∅ → 𝑥 = 𝑌)) |
49 | 48 | orrd 392 |
. . . . 5
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → (𝑥 = ∅ ∨ 𝑥 = 𝑌)) |
50 | | vex 3176 |
. . . . . 6
⊢ 𝑥 ∈ V |
51 | 50 | elpr 4146 |
. . . . 5
⊢ (𝑥 ∈ {∅, 𝑌} ↔ (𝑥 = ∅ ∨ 𝑥 = 𝑌)) |
52 | 49, 51 | sylibr 223 |
. . . 4
⊢ (((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾))) → 𝑥 ∈ {∅, 𝑌}) |
53 | 52 | ex 449 |
. . 3
⊢ ((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝑥 ∈ (𝐾 ∩ (Clsd‘𝐾)) → 𝑥 ∈ {∅, 𝑌})) |
54 | 53 | ssrdv 3574 |
. 2
⊢ ((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐾 ∩ (Clsd‘𝐾)) ⊆ {∅, 𝑌}) |
55 | 14 | iscon2 21027 |
. 2
⊢ (𝐾 ∈ Con ↔ (𝐾 ∈ Top ∧ (𝐾 ∩ (Clsd‘𝐾)) ⊆ {∅, 𝑌})) |
56 | 2, 54, 55 | sylanbrc 695 |
1
⊢ ((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Con) |