Step | Hyp | Ref
| Expression |
1 | | f1ocnv 6673 |
. . . . . . . . 9
⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌–1-1-onto→𝑋) |
2 | | f1ofun 6663 |
. . . . . . . . 9
⊢ (◡𝐹:𝑌–1-1-onto→𝑋 → Fun ◡𝐹) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝐹:𝑋–1-1-onto→𝑌 → Fun ◡𝐹) |
4 | 3 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → Fun ◡𝐹) |
5 | | simpr 488 |
. . . . . . . 8
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → 𝑥 ⊆ 𝑌) |
6 | | df-rn 5562 |
. . . . . . . . 9
⊢ ran 𝐹 = dom ◡𝐹 |
7 | | f1ofo 6668 |
. . . . . . . . . . 11
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋–onto→𝑌) |
8 | 7 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → 𝐹:𝑋–onto→𝑌) |
9 | | forn 6636 |
. . . . . . . . . 10
⊢ (𝐹:𝑋–onto→𝑌 → ran 𝐹 = 𝑌) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → ran 𝐹 = 𝑌) |
11 | 6, 10 | eqtr3id 2792 |
. . . . . . . 8
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → dom ◡𝐹 = 𝑌) |
12 | 5, 11 | sseqtrrd 3942 |
. . . . . . 7
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → 𝑥 ⊆ dom ◡𝐹) |
13 | | funimass4 6777 |
. . . . . . 7
⊢ ((Fun
◡𝐹 ∧ 𝑥 ⊆ dom ◡𝐹) → ((◡𝐹 “ 𝑥) ⊆ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ↔ ∀𝑦 ∈ 𝑥 (◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))) |
14 | 4, 12, 13 | syl2anc 587 |
. . . . . 6
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → ((◡𝐹 “ 𝑥) ⊆ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ↔ ∀𝑦 ∈ 𝑥 (◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))) |
15 | | dfss3 3888 |
. . . . . . 7
⊢ (𝑥 ⊆ ∪ ((𝐽
qTop 𝐹) ∩ 𝒫
𝑥) ↔ ∀𝑦 ∈ 𝑥 𝑦 ∈ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)) |
16 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)) |
17 | 16 | elin1d 4112 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑧 ∈ (𝐽 qTop 𝐹)) |
18 | | qtopcmp.1 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑋 = ∪
𝐽 |
19 | 18 | elqtop2 22598 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–onto→𝑌) → (𝑧 ∈ (𝐽 qTop 𝐹) ↔ (𝑧 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑧) ∈ 𝐽))) |
20 | 7, 19 | sylan2 596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑧 ∈ (𝐽 qTop 𝐹) ↔ (𝑧 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑧) ∈ 𝐽))) |
21 | 20 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (𝑧 ∈ (𝐽 qTop 𝐹) ↔ (𝑧 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑧) ∈ 𝐽))) |
22 | 17, 21 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (𝑧 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑧) ∈ 𝐽)) |
23 | 22 | simprd 499 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (◡𝐹 “ 𝑧) ∈ 𝐽) |
24 | 16 | elin2d 4113 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑧 ∈ 𝒫 𝑥) |
25 | 24 | elpwid 4524 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑧 ⊆ 𝑥) |
26 | | imass2 5970 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ⊆ 𝑥 → (◡𝐹 “ 𝑧) ⊆ (◡𝐹 “ 𝑥)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (◡𝐹 “ 𝑧) ⊆ (◡𝐹 “ 𝑥)) |
28 | 23, 27 | elpwd 4521 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (◡𝐹 “ 𝑧) ∈ 𝒫 (◡𝐹 “ 𝑥)) |
29 | 23, 28 | elind 4108 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (◡𝐹 “ 𝑧) ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))) |
30 | | simp-4r 784 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝐹:𝑋–1-1-onto→𝑌) |
31 | 30, 1 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → ◡𝐹:𝑌–1-1-onto→𝑋) |
32 | | f1ofn 6662 |
. . . . . . . . . . . . . 14
⊢ (◡𝐹:𝑌–1-1-onto→𝑋 → ◡𝐹 Fn 𝑌) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → ◡𝐹 Fn 𝑌) |
34 | 5 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑥 ⊆ 𝑌) |
35 | 25, 34 | sstrd 3911 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑧 ⊆ 𝑌) |
36 | | simprr 773 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑦 ∈ 𝑧) |
37 | | fnfvima 7049 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹 Fn 𝑌 ∧ 𝑧 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑧) → (◡𝐹‘𝑦) ∈ (◡𝐹 “ 𝑧)) |
38 | 33, 35, 36, 37 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (◡𝐹‘𝑦) ∈ (◡𝐹 “ 𝑧)) |
39 | | eleq2 2826 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (◡𝐹 “ 𝑧) → ((◡𝐹‘𝑦) ∈ 𝑤 ↔ (◡𝐹‘𝑦) ∈ (◡𝐹 “ 𝑧))) |
40 | 39 | rspcev 3537 |
. . . . . . . . . . . 12
⊢ (((◡𝐹 “ 𝑧) ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ (◡𝐹 “ 𝑧)) → ∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤) |
41 | 29, 38, 40 | syl2anc 587 |
. . . . . . . . . . 11
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → ∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤) |
42 | 41 | rexlimdvaa 3204 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧 → ∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤)) |
43 | | simp-4r 784 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝐹:𝑋–1-1-onto→𝑌) |
44 | | f1ofun 6663 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝑋–1-1-onto→𝑌 → Fun 𝐹) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → Fun 𝐹) |
46 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))) |
47 | 46 | elin2d 4113 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑤 ∈ 𝒫 (◡𝐹 “ 𝑥)) |
48 | 47 | elpwid 4524 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑤 ⊆ (◡𝐹 “ 𝑥)) |
49 | | funimass2 6463 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐹 ∧ 𝑤 ⊆ (◡𝐹 “ 𝑥)) → (𝐹 “ 𝑤) ⊆ 𝑥) |
50 | 45, 48, 49 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹 “ 𝑤) ⊆ 𝑥) |
51 | 5 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑥 ⊆ 𝑌) |
52 | 50, 51 | sstrd 3911 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹 “ 𝑤) ⊆ 𝑌) |
53 | | f1of1 6660 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋–1-1→𝑌) |
54 | 43, 53 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝐹:𝑋–1-1→𝑌) |
55 | 46 | elin1d 4112 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑤 ∈ 𝐽) |
56 | | elssuni 4851 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽) |
57 | 56, 18 | sseqtrrdi 3952 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ 𝑋) |
58 | 55, 57 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑤 ⊆ 𝑋) |
59 | | f1imacnv 6677 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝑋–1-1→𝑌 ∧ 𝑤 ⊆ 𝑋) → (◡𝐹 “ (𝐹 “ 𝑤)) = 𝑤) |
60 | 54, 58, 59 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (◡𝐹 “ (𝐹 “ 𝑤)) = 𝑤) |
61 | 60, 55 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (◡𝐹 “ (𝐹 “ 𝑤)) ∈ 𝐽) |
62 | 18 | elqtop2 22598 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–onto→𝑌) → ((𝐹 “ 𝑤) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹 “ 𝑤) ⊆ 𝑌 ∧ (◡𝐹 “ (𝐹 “ 𝑤)) ∈ 𝐽))) |
63 | 7, 62 | sylan2 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → ((𝐹 “ 𝑤) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹 “ 𝑤) ⊆ 𝑌 ∧ (◡𝐹 “ (𝐹 “ 𝑤)) ∈ 𝐽))) |
64 | 63 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → ((𝐹 “ 𝑤) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹 “ 𝑤) ⊆ 𝑌 ∧ (◡𝐹 “ (𝐹 “ 𝑤)) ∈ 𝐽))) |
65 | 52, 61, 64 | mpbir2and 713 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹 “ 𝑤) ∈ (𝐽 qTop 𝐹)) |
66 | | vex 3412 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
67 | 66 | elpw2 5238 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 “ 𝑤) ∈ 𝒫 𝑥 ↔ (𝐹 “ 𝑤) ⊆ 𝑥) |
68 | 50, 67 | sylibr 237 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹 “ 𝑤) ∈ 𝒫 𝑥) |
69 | 65, 68 | elind 4108 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹 “ 𝑤) ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)) |
70 | 5 | sselda 3901 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑌) |
71 | 70 | adantr 484 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑦 ∈ 𝑌) |
72 | | f1ocnvfv2 7088 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ 𝑦 ∈ 𝑌) → (𝐹‘(◡𝐹‘𝑦)) = 𝑦) |
73 | 43, 71, 72 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹‘(◡𝐹‘𝑦)) = 𝑦) |
74 | | f1ofn 6662 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹 Fn 𝑋) |
75 | 74 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → 𝐹 Fn 𝑋) |
76 | 75 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝐹 Fn 𝑋) |
77 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (◡𝐹‘𝑦) ∈ 𝑤) |
78 | | fnfvima 7049 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn 𝑋 ∧ 𝑤 ⊆ 𝑋 ∧ (◡𝐹‘𝑦) ∈ 𝑤) → (𝐹‘(◡𝐹‘𝑦)) ∈ (𝐹 “ 𝑤)) |
79 | 76, 58, 77, 78 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹‘(◡𝐹‘𝑦)) ∈ (𝐹 “ 𝑤)) |
80 | 73, 79 | eqeltrrd 2839 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑦 ∈ (𝐹 “ 𝑤)) |
81 | | eleq2 2826 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐹 “ 𝑤) → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ (𝐹 “ 𝑤))) |
82 | 81 | rspcev 3537 |
. . . . . . . . . . . 12
⊢ (((𝐹 “ 𝑤) ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ (𝐹 “ 𝑤)) → ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧) |
83 | 69, 80, 82 | syl2anc 587 |
. . . . . . . . . . 11
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧) |
84 | 83 | rexlimdvaa 3204 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤 → ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧)) |
85 | 42, 84 | impbid 215 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧 ↔ ∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤)) |
86 | | eluni2 4823 |
. . . . . . . . 9
⊢ (𝑦 ∈ ∪ ((𝐽
qTop 𝐹) ∩ 𝒫
𝑥) ↔ ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧) |
87 | | eluni2 4823 |
. . . . . . . . 9
⊢ ((◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ↔ ∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤) |
88 | 85, 86, 87 | 3bitr4g 317 |
. . . . . . . 8
⊢ ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (𝑦 ∈ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ (◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))) |
89 | 88 | ralbidva 3117 |
. . . . . . 7
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → (∀𝑦 ∈ 𝑥 𝑦 ∈ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ ∀𝑦 ∈ 𝑥 (◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))) |
90 | 15, 89 | syl5bb 286 |
. . . . . 6
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → (𝑥 ⊆ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ ∀𝑦 ∈ 𝑥 (◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))) |
91 | 14, 90 | bitr4d 285 |
. . . . 5
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → ((◡𝐹 “ 𝑥) ⊆ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ↔ 𝑥 ⊆ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥))) |
92 | | eltg 21854 |
. . . . . 6
⊢ (𝐽 ∈ TopBases → ((◡𝐹 “ 𝑥) ∈ (topGen‘𝐽) ↔ (◡𝐹 “ 𝑥) ⊆ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))) |
93 | 92 | ad2antrr 726 |
. . . . 5
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → ((◡𝐹 “ 𝑥) ∈ (topGen‘𝐽) ↔ (◡𝐹 “ 𝑥) ⊆ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))) |
94 | | ovex 7246 |
. . . . . 6
⊢ (𝐽 qTop 𝐹) ∈ V |
95 | | eltg 21854 |
. . . . . 6
⊢ ((𝐽 qTop 𝐹) ∈ V → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) ↔ 𝑥 ⊆ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥))) |
96 | 94, 95 | mp1i 13 |
. . . . 5
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) ↔ 𝑥 ⊆ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥))) |
97 | 91, 93, 96 | 3bitr4d 314 |
. . . 4
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → ((◡𝐹 “ 𝑥) ∈ (topGen‘𝐽) ↔ 𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)))) |
98 | 97 | pm5.32da 582 |
. . 3
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → ((𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ (topGen‘𝐽)) ↔ (𝑥 ⊆ 𝑌 ∧ 𝑥 ∈ (topGen‘(𝐽 qTop 𝐹))))) |
99 | | tgtopon 21868 |
. . . . . 6
⊢ (𝐽 ∈ TopBases →
(topGen‘𝐽) ∈
(TopOn‘∪ 𝐽)) |
100 | 99 | adantr 484 |
. . . . 5
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (topGen‘𝐽) ∈ (TopOn‘∪ 𝐽)) |
101 | 18 | fveq2i 6720 |
. . . . 5
⊢
(TopOn‘𝑋) =
(TopOn‘∪ 𝐽) |
102 | 100, 101 | eleqtrrdi 2849 |
. . . 4
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (topGen‘𝐽) ∈ (TopOn‘𝑋)) |
103 | 7 | adantl 485 |
. . . 4
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → 𝐹:𝑋–onto→𝑌) |
104 | | elqtop3 22600 |
. . . 4
⊢
(((topGen‘𝐽)
∈ (TopOn‘𝑋)
∧ 𝐹:𝑋–onto→𝑌) → (𝑥 ∈ ((topGen‘𝐽) qTop 𝐹) ↔ (𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ (topGen‘𝐽)))) |
105 | 102, 103,
104 | syl2anc 587 |
. . 3
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑥 ∈ ((topGen‘𝐽) qTop 𝐹) ↔ (𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ (topGen‘𝐽)))) |
106 | | unitg 21864 |
. . . . . . . . 9
⊢ ((𝐽 qTop 𝐹) ∈ V → ∪ (topGen‘(𝐽 qTop 𝐹)) = ∪ (𝐽 qTop 𝐹)) |
107 | 94, 106 | ax-mp 5 |
. . . . . . . 8
⊢ ∪ (topGen‘(𝐽 qTop 𝐹)) = ∪ (𝐽 qTop 𝐹) |
108 | 18 | elqtop2 22598 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–onto→𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽))) |
109 | 7, 108 | sylan2 596 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽))) |
110 | | simpl 486 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽) → 𝑥 ⊆ 𝑌) |
111 | | velpw 4518 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 𝑌 ↔ 𝑥 ⊆ 𝑌) |
112 | 110, 111 | sylibr 237 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽) → 𝑥 ∈ 𝒫 𝑌) |
113 | 109, 112 | syl6bi 256 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) → 𝑥 ∈ 𝒫 𝑌)) |
114 | 113 | ssrdv 3907 |
. . . . . . . . 9
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝐽 qTop 𝐹) ⊆ 𝒫 𝑌) |
115 | | sspwuni 5008 |
. . . . . . . . 9
⊢ ((𝐽 qTop 𝐹) ⊆ 𝒫 𝑌 ↔ ∪ (𝐽 qTop 𝐹) ⊆ 𝑌) |
116 | 114, 115 | sylib 221 |
. . . . . . . 8
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → ∪ (𝐽
qTop 𝐹) ⊆ 𝑌) |
117 | 107, 116 | eqsstrid 3949 |
. . . . . . 7
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → ∪ (topGen‘(𝐽 qTop 𝐹)) ⊆ 𝑌) |
118 | | sspwuni 5008 |
. . . . . . 7
⊢
((topGen‘(𝐽
qTop 𝐹)) ⊆ 𝒫
𝑌 ↔ ∪ (topGen‘(𝐽 qTop 𝐹)) ⊆ 𝑌) |
119 | 117, 118 | sylibr 237 |
. . . . . 6
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (topGen‘(𝐽 qTop 𝐹)) ⊆ 𝒫 𝑌) |
120 | 119 | sseld 3900 |
. . . . 5
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) → 𝑥 ∈ 𝒫 𝑌)) |
121 | 120, 111 | syl6ib 254 |
. . . 4
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) → 𝑥 ⊆ 𝑌)) |
122 | 121 | pm4.71rd 566 |
. . 3
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) ↔ (𝑥 ⊆ 𝑌 ∧ 𝑥 ∈ (topGen‘(𝐽 qTop 𝐹))))) |
123 | 98, 105, 122 | 3bitr4d 314 |
. 2
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑥 ∈ ((topGen‘𝐽) qTop 𝐹) ↔ 𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)))) |
124 | 123 | eqrdv 2735 |
1
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → ((topGen‘𝐽) qTop 𝐹) = (topGen‘(𝐽 qTop 𝐹))) |