Step | Hyp | Ref
| Expression |
1 | | kqval.2 |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) |
2 | 1 | kqffn 22876 |
. . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋) |
3 | | elpreima 6935 |
. . . . . 6
⊢ (𝐹 Fn 𝑋 → (𝑧 ∈ (◡𝐹 “ (𝐹 “ 𝑈)) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ (𝐹 “ 𝑈)))) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝑧 ∈ (◡𝐹 “ (𝐹 “ 𝑈)) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ (𝐹 “ 𝑈)))) |
5 | 4 | adantr 481 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝑧 ∈ (◡𝐹 “ (𝐹 “ 𝑈)) ↔ (𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ (𝐹 “ 𝑈)))) |
6 | | noel 4264 |
. . . . . . . 8
⊢ ¬
(𝐹‘𝑧) ∈ ∅ |
7 | | elin 3903 |
. . . . . . . . 9
⊢ ((𝐹‘𝑧) ∈ ((𝐹 “ 𝑈) ∩ (𝐹 “ (𝑋 ∖ 𝑈))) ↔ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑈) ∧ (𝐹‘𝑧) ∈ (𝐹 “ (𝑋 ∖ 𝑈)))) |
8 | | incom 4135 |
. . . . . . . . . . 11
⊢ ((𝐹 “ 𝑈) ∩ (𝐹 “ (𝑋 ∖ 𝑈))) = ((𝐹 “ (𝑋 ∖ 𝑈)) ∩ (𝐹 “ 𝑈)) |
9 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∪ 𝐽 =
∪ 𝐽 |
10 | 9 | cldss 22180 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑈 ∈ (Clsd‘𝐽) → 𝑈 ⊆ ∪ 𝐽) |
11 | 10 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → 𝑈 ⊆ ∪ 𝐽) |
12 | | fndm 6536 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋) |
13 | 2, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐽 ∈ (TopOn‘𝑋) → dom 𝐹 = 𝑋) |
14 | | toponuni 22063 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
15 | 13, 14 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐽 ∈ (TopOn‘𝑋) → dom 𝐹 = ∪ 𝐽) |
16 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → dom 𝐹 = ∪ 𝐽) |
17 | 11, 16 | sseqtrrd 3962 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → 𝑈 ⊆ dom 𝐹) |
18 | 13 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → dom 𝐹 = 𝑋) |
19 | 17, 18 | sseqtrd 3961 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → 𝑈 ⊆ 𝑋) |
20 | 19 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → 𝑈 ⊆ 𝑋) |
21 | | dfss4 4192 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑈)) = 𝑈) |
22 | 20, 21 | sylib 217 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → (𝑋 ∖ (𝑋 ∖ 𝑈)) = 𝑈) |
23 | 22 | imaeq2d 5969 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → (𝐹 “ (𝑋 ∖ (𝑋 ∖ 𝑈))) = (𝐹 “ 𝑈)) |
24 | 23 | ineq2d 4146 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → ((𝐹 “ (𝑋 ∖ 𝑈)) ∩ (𝐹 “ (𝑋 ∖ (𝑋 ∖ 𝑈)))) = ((𝐹 “ (𝑋 ∖ 𝑈)) ∩ (𝐹 “ 𝑈))) |
25 | | simpll 764 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
26 | 14 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → 𝑋 = ∪ 𝐽) |
27 | 26 | difeq1d 4056 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑈) = (∪ 𝐽 ∖ 𝑈)) |
28 | 9 | cldopn 22182 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 ∈ (Clsd‘𝐽) → (∪ 𝐽
∖ 𝑈) ∈ 𝐽) |
29 | 28 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (∪
𝐽 ∖ 𝑈) ∈ 𝐽) |
30 | 27, 29 | eqeltrd 2839 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑈) ∈ 𝐽) |
31 | 30 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → (𝑋 ∖ 𝑈) ∈ 𝐽) |
32 | 1 | kqdisj 22883 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋 ∖ 𝑈) ∈ 𝐽) → ((𝐹 “ (𝑋 ∖ 𝑈)) ∩ (𝐹 “ (𝑋 ∖ (𝑋 ∖ 𝑈)))) = ∅) |
33 | 25, 31, 32 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → ((𝐹 “ (𝑋 ∖ 𝑈)) ∩ (𝐹 “ (𝑋 ∖ (𝑋 ∖ 𝑈)))) = ∅) |
34 | 24, 33 | eqtr3d 2780 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → ((𝐹 “ (𝑋 ∖ 𝑈)) ∩ (𝐹 “ 𝑈)) = ∅) |
35 | 8, 34 | eqtrid 2790 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → ((𝐹 “ 𝑈) ∩ (𝐹 “ (𝑋 ∖ 𝑈))) = ∅) |
36 | 35 | eleq2d 2824 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ ((𝐹 “ 𝑈) ∩ (𝐹 “ (𝑋 ∖ 𝑈))) ↔ (𝐹‘𝑧) ∈ ∅)) |
37 | 7, 36 | bitr3id 285 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → (((𝐹‘𝑧) ∈ (𝐹 “ 𝑈) ∧ (𝐹‘𝑧) ∈ (𝐹 “ (𝑋 ∖ 𝑈))) ↔ (𝐹‘𝑧) ∈ ∅)) |
38 | 6, 37 | mtbiri 327 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → ¬ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑈) ∧ (𝐹‘𝑧) ∈ (𝐹 “ (𝑋 ∖ 𝑈)))) |
39 | | imnan 400 |
. . . . . . 7
⊢ (((𝐹‘𝑧) ∈ (𝐹 “ 𝑈) → ¬ (𝐹‘𝑧) ∈ (𝐹 “ (𝑋 ∖ 𝑈))) ↔ ¬ ((𝐹‘𝑧) ∈ (𝐹 “ 𝑈) ∧ (𝐹‘𝑧) ∈ (𝐹 “ (𝑋 ∖ 𝑈)))) |
40 | 38, 39 | sylibr 233 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ (𝐹 “ 𝑈) → ¬ (𝐹‘𝑧) ∈ (𝐹 “ (𝑋 ∖ 𝑈)))) |
41 | | eldif 3897 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑋 ∖ 𝑈) ↔ (𝑧 ∈ 𝑋 ∧ ¬ 𝑧 ∈ 𝑈)) |
42 | 41 | baibr 537 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑋 → (¬ 𝑧 ∈ 𝑈 ↔ 𝑧 ∈ (𝑋 ∖ 𝑈))) |
43 | 42 | adantl 482 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → (¬ 𝑧 ∈ 𝑈 ↔ 𝑧 ∈ (𝑋 ∖ 𝑈))) |
44 | | simpr 485 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
45 | 1 | kqfvima 22881 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋 ∖ 𝑈) ∈ 𝐽 ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (𝑋 ∖ 𝑈) ↔ (𝐹‘𝑧) ∈ (𝐹 “ (𝑋 ∖ 𝑈)))) |
46 | 25, 31, 44, 45 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → (𝑧 ∈ (𝑋 ∖ 𝑈) ↔ (𝐹‘𝑧) ∈ (𝐹 “ (𝑋 ∖ 𝑈)))) |
47 | 43, 46 | bitrd 278 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → (¬ 𝑧 ∈ 𝑈 ↔ (𝐹‘𝑧) ∈ (𝐹 “ (𝑋 ∖ 𝑈)))) |
48 | 47 | con1bid 356 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → (¬ (𝐹‘𝑧) ∈ (𝐹 “ (𝑋 ∖ 𝑈)) ↔ 𝑧 ∈ 𝑈)) |
49 | 40, 48 | sylibd 238 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ (𝐹 “ 𝑈) → 𝑧 ∈ 𝑈)) |
50 | 49 | expimpd 454 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → ((𝑧 ∈ 𝑋 ∧ (𝐹‘𝑧) ∈ (𝐹 “ 𝑈)) → 𝑧 ∈ 𝑈)) |
51 | 5, 50 | sylbid 239 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝑧 ∈ (◡𝐹 “ (𝐹 “ 𝑈)) → 𝑧 ∈ 𝑈)) |
52 | 51 | ssrdv 3927 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (◡𝐹 “ (𝐹 “ 𝑈)) ⊆ 𝑈) |
53 | | sseqin2 4149 |
. . . 4
⊢ (𝑈 ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ 𝑈) = 𝑈) |
54 | 17, 53 | sylib 217 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (dom 𝐹 ∩ 𝑈) = 𝑈) |
55 | | dminss 6056 |
. . 3
⊢ (dom
𝐹 ∩ 𝑈) ⊆ (◡𝐹 “ (𝐹 “ 𝑈)) |
56 | 54, 55 | eqsstrrdi 3976 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → 𝑈 ⊆ (◡𝐹 “ (𝐹 “ 𝑈))) |
57 | 52, 56 | eqssd 3938 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (◡𝐹 “ (𝐹 “ 𝑈)) = 𝑈) |