Proof of Theorem qtopcld
Step | Hyp | Ref
| Expression |
1 | | qtoptopon 21317 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
2 | | topontop 20541 |
. . 3
⊢ ((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) → (𝐽 qTop 𝐹) ∈ Top) |
3 | | eqid 2610 |
. . . 4
⊢ ∪ (𝐽
qTop 𝐹) = ∪ (𝐽
qTop 𝐹) |
4 | 3 | iscld 20641 |
. . 3
⊢ ((𝐽 qTop 𝐹) ∈ Top → (𝐴 ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ (𝐴 ⊆ ∪ (𝐽 qTop 𝐹) ∧ (∪ (𝐽 qTop 𝐹) ∖ 𝐴) ∈ (𝐽 qTop 𝐹)))) |
5 | 1, 2, 4 | 3syl 18 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ (𝐴 ⊆ ∪ (𝐽 qTop 𝐹) ∧ (∪ (𝐽 qTop 𝐹) ∖ 𝐴) ∈ (𝐽 qTop 𝐹)))) |
6 | | toponuni 20542 |
. . . . 5
⊢ ((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹)) |
7 | 1, 6 | syl 17 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹)) |
8 | 7 | sseq2d 3596 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ⊆ 𝑌 ↔ 𝐴 ⊆ ∪ (𝐽 qTop 𝐹))) |
9 | 7 | difeq1d 3689 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝑌 ∖ 𝐴) = (∪ (𝐽 qTop 𝐹) ∖ 𝐴)) |
10 | 9 | eleq1d 2672 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → ((𝑌 ∖ 𝐴) ∈ (𝐽 qTop 𝐹) ↔ (∪
(𝐽 qTop 𝐹) ∖ 𝐴) ∈ (𝐽 qTop 𝐹))) |
11 | 8, 10 | anbi12d 743 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → ((𝐴 ⊆ 𝑌 ∧ (𝑌 ∖ 𝐴) ∈ (𝐽 qTop 𝐹)) ↔ (𝐴 ⊆ ∪ (𝐽 qTop 𝐹) ∧ (∪ (𝐽 qTop 𝐹) ∖ 𝐴) ∈ (𝐽 qTop 𝐹)))) |
12 | | elqtop3 21316 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → ((𝑌 ∖ 𝐴) ∈ (𝐽 qTop 𝐹) ↔ ((𝑌 ∖ 𝐴) ⊆ 𝑌 ∧ (◡𝐹 “ (𝑌 ∖ 𝐴)) ∈ 𝐽))) |
13 | 12 | adantr 480 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝑌 ∖ 𝐴) ∈ (𝐽 qTop 𝐹) ↔ ((𝑌 ∖ 𝐴) ⊆ 𝑌 ∧ (◡𝐹 “ (𝑌 ∖ 𝐴)) ∈ 𝐽))) |
14 | | difss 3699 |
. . . . . 6
⊢ (𝑌 ∖ 𝐴) ⊆ 𝑌 |
15 | 14 | biantrur 526 |
. . . . 5
⊢ ((◡𝐹 “ (𝑌 ∖ 𝐴)) ∈ 𝐽 ↔ ((𝑌 ∖ 𝐴) ⊆ 𝑌 ∧ (◡𝐹 “ (𝑌 ∖ 𝐴)) ∈ 𝐽)) |
16 | | fofun 6029 |
. . . . . . . . . 10
⊢ (𝐹:𝑋–onto→𝑌 → Fun 𝐹) |
17 | 16 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → Fun 𝐹) |
18 | | funcnvcnv 5870 |
. . . . . . . . 9
⊢ (Fun
𝐹 → Fun ◡◡𝐹) |
19 | | imadif 5887 |
. . . . . . . . 9
⊢ (Fun
◡◡𝐹 → (◡𝐹 “ (𝑌 ∖ 𝐴)) = ((◡𝐹 “ 𝑌) ∖ (◡𝐹 “ 𝐴))) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → (◡𝐹 “ (𝑌 ∖ 𝐴)) = ((◡𝐹 “ 𝑌) ∖ (◡𝐹 “ 𝐴))) |
21 | | fof 6028 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
22 | | fimacnv 6255 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋⟶𝑌 → (◡𝐹 “ 𝑌) = 𝑋) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹:𝑋–onto→𝑌 → (◡𝐹 “ 𝑌) = 𝑋) |
24 | 23 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → (◡𝐹 “ 𝑌) = 𝑋) |
25 | | toponuni 20542 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
26 | 25 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝑋 = ∪ 𝐽) |
27 | 24, 26 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → (◡𝐹 “ 𝑌) = ∪ 𝐽) |
28 | 27 | difeq1d 3689 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → ((◡𝐹 “ 𝑌) ∖ (◡𝐹 “ 𝐴)) = (∪ 𝐽 ∖ (◡𝐹 “ 𝐴))) |
29 | 20, 28 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → (◡𝐹 “ (𝑌 ∖ 𝐴)) = (∪ 𝐽 ∖ (◡𝐹 “ 𝐴))) |
30 | 29 | eleq1d 2672 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → ((◡𝐹 “ (𝑌 ∖ 𝐴)) ∈ 𝐽 ↔ (∪ 𝐽 ∖ (◡𝐹 “ 𝐴)) ∈ 𝐽)) |
31 | | topontop 20541 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
32 | 31 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐽 ∈ Top) |
33 | | cnvimass 5404 |
. . . . . . . . 9
⊢ (◡𝐹 “ 𝐴) ⊆ dom 𝐹 |
34 | | fofn 6030 |
. . . . . . . . . . 11
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹 Fn 𝑋) |
35 | | fndm 5904 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋) |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
⊢ (𝐹:𝑋–onto→𝑌 → dom 𝐹 = 𝑋) |
37 | 36 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → dom 𝐹 = 𝑋) |
38 | 33, 37 | syl5sseq 3616 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → (◡𝐹 “ 𝐴) ⊆ 𝑋) |
39 | 38, 26 | sseqtrd 3604 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → (◡𝐹 “ 𝐴) ⊆ ∪ 𝐽) |
40 | | eqid 2610 |
. . . . . . . 8
⊢ ∪ 𝐽 =
∪ 𝐽 |
41 | 40 | iscld2 20642 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ (◡𝐹 “ 𝐴) ⊆ ∪ 𝐽) → ((◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽) ↔ (∪ 𝐽 ∖ (◡𝐹 “ 𝐴)) ∈ 𝐽)) |
42 | 32, 39, 41 | syl2anc 691 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → ((◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽) ↔ (∪ 𝐽 ∖ (◡𝐹 “ 𝐴)) ∈ 𝐽)) |
43 | 30, 42 | bitr4d 270 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → ((◡𝐹 “ (𝑌 ∖ 𝐴)) ∈ 𝐽 ↔ (◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽))) |
44 | 15, 43 | syl5bbr 273 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → (((𝑌 ∖ 𝐴) ⊆ 𝑌 ∧ (◡𝐹 “ (𝑌 ∖ 𝐴)) ∈ 𝐽) ↔ (◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽))) |
45 | 13, 44 | bitrd 267 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝑌 ∖ 𝐴) ∈ (𝐽 qTop 𝐹) ↔ (◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽))) |
46 | 45 | pm5.32da 671 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → ((𝐴 ⊆ 𝑌 ∧ (𝑌 ∖ 𝐴) ∈ (𝐽 qTop 𝐹)) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽)))) |
47 | 5, 11, 46 | 3bitr2d 295 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽)))) |