Proof of Theorem qtopcld
Step | Hyp | Ref
| Expression |
1 | | qtoptopon 22448 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
2 | | topontop 21657 |
. . 3
⊢ ((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) → (𝐽 qTop 𝐹) ∈ Top) |
3 | | eqid 2738 |
. . . 4
⊢ ∪ (𝐽
qTop 𝐹) = ∪ (𝐽
qTop 𝐹) |
4 | 3 | iscld 21771 |
. . 3
⊢ ((𝐽 qTop 𝐹) ∈ Top → (𝐴 ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ (𝐴 ⊆ ∪ (𝐽 qTop 𝐹) ∧ (∪ (𝐽 qTop 𝐹) ∖ 𝐴) ∈ (𝐽 qTop 𝐹)))) |
5 | 1, 2, 4 | 3syl 18 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ (𝐴 ⊆ ∪ (𝐽 qTop 𝐹) ∧ (∪ (𝐽 qTop 𝐹) ∖ 𝐴) ∈ (𝐽 qTop 𝐹)))) |
6 | | toponuni 21658 |
. . . . 5
⊢ ((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹)) |
7 | 1, 6 | syl 17 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹)) |
8 | 7 | sseq2d 3907 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ⊆ 𝑌 ↔ 𝐴 ⊆ ∪ (𝐽 qTop 𝐹))) |
9 | 7 | difeq1d 4010 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝑌 ∖ 𝐴) = (∪ (𝐽 qTop 𝐹) ∖ 𝐴)) |
10 | 9 | eleq1d 2817 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → ((𝑌 ∖ 𝐴) ∈ (𝐽 qTop 𝐹) ↔ (∪
(𝐽 qTop 𝐹) ∖ 𝐴) ∈ (𝐽 qTop 𝐹))) |
11 | 8, 10 | anbi12d 634 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → ((𝐴 ⊆ 𝑌 ∧ (𝑌 ∖ 𝐴) ∈ (𝐽 qTop 𝐹)) ↔ (𝐴 ⊆ ∪ (𝐽 qTop 𝐹) ∧ (∪ (𝐽 qTop 𝐹) ∖ 𝐴) ∈ (𝐽 qTop 𝐹)))) |
12 | | elqtop3 22447 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → ((𝑌 ∖ 𝐴) ∈ (𝐽 qTop 𝐹) ↔ ((𝑌 ∖ 𝐴) ⊆ 𝑌 ∧ (◡𝐹 “ (𝑌 ∖ 𝐴)) ∈ 𝐽))) |
13 | 12 | adantr 484 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝑌 ∖ 𝐴) ∈ (𝐽 qTop 𝐹) ↔ ((𝑌 ∖ 𝐴) ⊆ 𝑌 ∧ (◡𝐹 “ (𝑌 ∖ 𝐴)) ∈ 𝐽))) |
14 | | difss 4020 |
. . . . . 6
⊢ (𝑌 ∖ 𝐴) ⊆ 𝑌 |
15 | 14 | biantrur 534 |
. . . . 5
⊢ ((◡𝐹 “ (𝑌 ∖ 𝐴)) ∈ 𝐽 ↔ ((𝑌 ∖ 𝐴) ⊆ 𝑌 ∧ (◡𝐹 “ (𝑌 ∖ 𝐴)) ∈ 𝐽)) |
16 | | fofun 6587 |
. . . . . . . . . 10
⊢ (𝐹:𝑋–onto→𝑌 → Fun 𝐹) |
17 | 16 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → Fun 𝐹) |
18 | | funcnvcnv 6400 |
. . . . . . . . 9
⊢ (Fun
𝐹 → Fun ◡◡𝐹) |
19 | | imadif 6417 |
. . . . . . . . 9
⊢ (Fun
◡◡𝐹 → (◡𝐹 “ (𝑌 ∖ 𝐴)) = ((◡𝐹 “ 𝑌) ∖ (◡𝐹 “ 𝐴))) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → (◡𝐹 “ (𝑌 ∖ 𝐴)) = ((◡𝐹 “ 𝑌) ∖ (◡𝐹 “ 𝐴))) |
21 | | fof 6586 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
22 | | fimacnv 6520 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑋⟶𝑌 → (◡𝐹 “ 𝑌) = 𝑋) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹:𝑋–onto→𝑌 → (◡𝐹 “ 𝑌) = 𝑋) |
24 | 23 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → (◡𝐹 “ 𝑌) = 𝑋) |
25 | | toponuni 21658 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
26 | 25 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝑋 = ∪ 𝐽) |
27 | 24, 26 | eqtrd 2773 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → (◡𝐹 “ 𝑌) = ∪ 𝐽) |
28 | 27 | difeq1d 4010 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → ((◡𝐹 “ 𝑌) ∖ (◡𝐹 “ 𝐴)) = (∪ 𝐽 ∖ (◡𝐹 “ 𝐴))) |
29 | 20, 28 | eqtrd 2773 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → (◡𝐹 “ (𝑌 ∖ 𝐴)) = (∪ 𝐽 ∖ (◡𝐹 “ 𝐴))) |
30 | 29 | eleq1d 2817 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → ((◡𝐹 “ (𝑌 ∖ 𝐴)) ∈ 𝐽 ↔ (∪ 𝐽 ∖ (◡𝐹 “ 𝐴)) ∈ 𝐽)) |
31 | | topontop 21657 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
32 | 31 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐽 ∈ Top) |
33 | | cnvimass 5917 |
. . . . . . . . 9
⊢ (◡𝐹 “ 𝐴) ⊆ dom 𝐹 |
34 | | fofn 6588 |
. . . . . . . . . . 11
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹 Fn 𝑋) |
35 | 34 | fndmd 6436 |
. . . . . . . . . 10
⊢ (𝐹:𝑋–onto→𝑌 → dom 𝐹 = 𝑋) |
36 | 35 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → dom 𝐹 = 𝑋) |
37 | 33, 36 | sseqtrid 3927 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → (◡𝐹 “ 𝐴) ⊆ 𝑋) |
38 | 37, 26 | sseqtrd 3915 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → (◡𝐹 “ 𝐴) ⊆ ∪ 𝐽) |
39 | | eqid 2738 |
. . . . . . . 8
⊢ ∪ 𝐽 =
∪ 𝐽 |
40 | 39 | iscld2 21772 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ (◡𝐹 “ 𝐴) ⊆ ∪ 𝐽) → ((◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽) ↔ (∪ 𝐽 ∖ (◡𝐹 “ 𝐴)) ∈ 𝐽)) |
41 | 32, 38, 40 | syl2anc 587 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → ((◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽) ↔ (∪ 𝐽 ∖ (◡𝐹 “ 𝐴)) ∈ 𝐽)) |
42 | 30, 41 | bitr4d 285 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → ((◡𝐹 “ (𝑌 ∖ 𝐴)) ∈ 𝐽 ↔ (◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽))) |
43 | 15, 42 | bitr3id 288 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → (((𝑌 ∖ 𝐴) ⊆ 𝑌 ∧ (◡𝐹 “ (𝑌 ∖ 𝐴)) ∈ 𝐽) ↔ (◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽))) |
44 | 13, 43 | bitrd 282 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝑌 ∖ 𝐴) ∈ (𝐽 qTop 𝐹) ↔ (◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽))) |
45 | 44 | pm5.32da 582 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → ((𝐴 ⊆ 𝑌 ∧ (𝑌 ∖ 𝐴) ∈ (𝐽 qTop 𝐹)) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽)))) |
46 | 5, 11, 45 | 3bitr2d 310 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽)))) |