Step | Hyp | Ref
| Expression |
1 | | f1ocnv 6062 |
. . . . . . . . 9
⊢ (𝐹:𝑋–1-1-onto→𝑌 → ◡𝐹:𝑌–1-1-onto→𝑋) |
2 | | f1ofun 6052 |
. . . . . . . . 9
⊢ (◡𝐹:𝑌–1-1-onto→𝑋 → Fun ◡𝐹) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝐹:𝑋–1-1-onto→𝑌 → Fun ◡𝐹) |
4 | 3 | ad2antlr 759 |
. . . . . . 7
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → Fun ◡𝐹) |
5 | | simpr 476 |
. . . . . . . 8
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → 𝑥 ⊆ 𝑌) |
6 | | df-rn 5049 |
. . . . . . . . 9
⊢ ran 𝐹 = dom ◡𝐹 |
7 | | f1ofo 6057 |
. . . . . . . . . . 11
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋–onto→𝑌) |
8 | 7 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → 𝐹:𝑋–onto→𝑌) |
9 | | forn 6031 |
. . . . . . . . . 10
⊢ (𝐹:𝑋–onto→𝑌 → ran 𝐹 = 𝑌) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → ran 𝐹 = 𝑌) |
11 | 6, 10 | syl5eqr 2658 |
. . . . . . . 8
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → dom ◡𝐹 = 𝑌) |
12 | 5, 11 | sseqtr4d 3605 |
. . . . . . 7
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → 𝑥 ⊆ dom ◡𝐹) |
13 | | funimass4 6157 |
. . . . . . 7
⊢ ((Fun
◡𝐹 ∧ 𝑥 ⊆ dom ◡𝐹) → ((◡𝐹 “ 𝑥) ⊆ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ↔ ∀𝑦 ∈ 𝑥 (◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))) |
14 | 4, 12, 13 | syl2anc 691 |
. . . . . 6
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → ((◡𝐹 “ 𝑥) ⊆ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ↔ ∀𝑦 ∈ 𝑥 (◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))) |
15 | | dfss3 3558 |
. . . . . . 7
⊢ (𝑥 ⊆ ∪ ((𝐽
qTop 𝐹) ∩ 𝒫
𝑥) ↔ ∀𝑦 ∈ 𝑥 𝑦 ∈ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)) |
16 | | inss1 3795 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ⊆ (𝐽 qTop 𝐹) |
17 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)) |
18 | 16, 17 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑧 ∈ (𝐽 qTop 𝐹)) |
19 | | qtopcmp.1 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑋 = ∪
𝐽 |
20 | 19 | elqtop2 21314 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–onto→𝑌) → (𝑧 ∈ (𝐽 qTop 𝐹) ↔ (𝑧 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑧) ∈ 𝐽))) |
21 | 7, 20 | sylan2 490 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑧 ∈ (𝐽 qTop 𝐹) ↔ (𝑧 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑧) ∈ 𝐽))) |
22 | 21 | ad3antrrr 762 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (𝑧 ∈ (𝐽 qTop 𝐹) ↔ (𝑧 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑧) ∈ 𝐽))) |
23 | 18, 22 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (𝑧 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑧) ∈ 𝐽)) |
24 | 23 | simprd 478 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (◡𝐹 “ 𝑧) ∈ 𝐽) |
25 | | inss2 3796 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ⊆ 𝒫 𝑥 |
26 | 25, 17 | sseldi 3566 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑧 ∈ 𝒫 𝑥) |
27 | 26 | elpwid 4118 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑧 ⊆ 𝑥) |
28 | | imass2 5420 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ⊆ 𝑥 → (◡𝐹 “ 𝑧) ⊆ (◡𝐹 “ 𝑥)) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (◡𝐹 “ 𝑧) ⊆ (◡𝐹 “ 𝑥)) |
30 | | elpwg 4116 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐹 “ 𝑧) ∈ 𝐽 → ((◡𝐹 “ 𝑧) ∈ 𝒫 (◡𝐹 “ 𝑥) ↔ (◡𝐹 “ 𝑧) ⊆ (◡𝐹 “ 𝑥))) |
31 | 24, 30 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → ((◡𝐹 “ 𝑧) ∈ 𝒫 (◡𝐹 “ 𝑥) ↔ (◡𝐹 “ 𝑧) ⊆ (◡𝐹 “ 𝑥))) |
32 | 29, 31 | mpbird 246 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (◡𝐹 “ 𝑧) ∈ 𝒫 (◡𝐹 “ 𝑥)) |
33 | 24, 32 | elind 3760 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (◡𝐹 “ 𝑧) ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))) |
34 | | simp-4r 803 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝐹:𝑋–1-1-onto→𝑌) |
35 | 34, 1 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → ◡𝐹:𝑌–1-1-onto→𝑋) |
36 | | f1ofn 6051 |
. . . . . . . . . . . . . 14
⊢ (◡𝐹:𝑌–1-1-onto→𝑋 → ◡𝐹 Fn 𝑌) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → ◡𝐹 Fn 𝑌) |
38 | 5 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑥 ⊆ 𝑌) |
39 | 27, 38 | sstrd 3578 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑧 ⊆ 𝑌) |
40 | | simprr 792 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → 𝑦 ∈ 𝑧) |
41 | | fnfvima 6400 |
. . . . . . . . . . . . 13
⊢ ((◡𝐹 Fn 𝑌 ∧ 𝑧 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑧) → (◡𝐹‘𝑦) ∈ (◡𝐹 “ 𝑧)) |
42 | 37, 39, 40, 41 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → (◡𝐹‘𝑦) ∈ (◡𝐹 “ 𝑧)) |
43 | | eleq2 2677 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (◡𝐹 “ 𝑧) → ((◡𝐹‘𝑦) ∈ 𝑤 ↔ (◡𝐹‘𝑦) ∈ (◡𝐹 “ 𝑧))) |
44 | 43 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ (((◡𝐹 “ 𝑧) ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ (◡𝐹 “ 𝑧)) → ∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤) |
45 | 33, 42, 44 | syl2anc 691 |
. . . . . . . . . . 11
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ 𝑧)) → ∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤) |
46 | 45 | rexlimdvaa 3014 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧 → ∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤)) |
47 | | simp-4r 803 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝐹:𝑋–1-1-onto→𝑌) |
48 | | f1ofun 6052 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝑋–1-1-onto→𝑌 → Fun 𝐹) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → Fun 𝐹) |
50 | | inss2 3796 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ⊆ 𝒫 (◡𝐹 “ 𝑥) |
51 | | simprl 790 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))) |
52 | 50, 51 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑤 ∈ 𝒫 (◡𝐹 “ 𝑥)) |
53 | 52 | elpwid 4118 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑤 ⊆ (◡𝐹 “ 𝑥)) |
54 | | funimass2 5886 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐹 ∧ 𝑤 ⊆ (◡𝐹 “ 𝑥)) → (𝐹 “ 𝑤) ⊆ 𝑥) |
55 | 49, 53, 54 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹 “ 𝑤) ⊆ 𝑥) |
56 | 5 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑥 ⊆ 𝑌) |
57 | 55, 56 | sstrd 3578 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹 “ 𝑤) ⊆ 𝑌) |
58 | | f1of1 6049 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹:𝑋–1-1→𝑌) |
59 | 47, 58 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝐹:𝑋–1-1→𝑌) |
60 | | inss1 3795 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ⊆ 𝐽 |
61 | 60, 51 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑤 ∈ 𝐽) |
62 | | elssuni 4403 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽) |
63 | 62, 19 | syl6sseqr 3615 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ 𝑋) |
64 | 61, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑤 ⊆ 𝑋) |
65 | | f1imacnv 6066 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝑋–1-1→𝑌 ∧ 𝑤 ⊆ 𝑋) → (◡𝐹 “ (𝐹 “ 𝑤)) = 𝑤) |
66 | 59, 64, 65 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (◡𝐹 “ (𝐹 “ 𝑤)) = 𝑤) |
67 | 66, 61 | eqeltrd 2688 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (◡𝐹 “ (𝐹 “ 𝑤)) ∈ 𝐽) |
68 | 19 | elqtop2 21314 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–onto→𝑌) → ((𝐹 “ 𝑤) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹 “ 𝑤) ⊆ 𝑌 ∧ (◡𝐹 “ (𝐹 “ 𝑤)) ∈ 𝐽))) |
69 | 7, 68 | sylan2 490 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → ((𝐹 “ 𝑤) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹 “ 𝑤) ⊆ 𝑌 ∧ (◡𝐹 “ (𝐹 “ 𝑤)) ∈ 𝐽))) |
70 | 69 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → ((𝐹 “ 𝑤) ∈ (𝐽 qTop 𝐹) ↔ ((𝐹 “ 𝑤) ⊆ 𝑌 ∧ (◡𝐹 “ (𝐹 “ 𝑤)) ∈ 𝐽))) |
71 | 57, 67, 70 | mpbir2and 959 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹 “ 𝑤) ∈ (𝐽 qTop 𝐹)) |
72 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
73 | 72 | elpw2 4755 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 “ 𝑤) ∈ 𝒫 𝑥 ↔ (𝐹 “ 𝑤) ⊆ 𝑥) |
74 | 55, 73 | sylibr 223 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹 “ 𝑤) ∈ 𝒫 𝑥) |
75 | 71, 74 | elind 3760 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹 “ 𝑤) ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)) |
76 | 5 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑌) |
77 | 76 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑦 ∈ 𝑌) |
78 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝑋–1-1-onto→𝑌 ∧ 𝑦 ∈ 𝑌) → (𝐹‘(◡𝐹‘𝑦)) = 𝑦) |
79 | 47, 77, 78 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹‘(◡𝐹‘𝑦)) = 𝑦) |
80 | | f1ofn 6051 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑋–1-1-onto→𝑌 → 𝐹 Fn 𝑋) |
81 | 80 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → 𝐹 Fn 𝑋) |
82 | 81 | ad3antrrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝐹 Fn 𝑋) |
83 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (◡𝐹‘𝑦) ∈ 𝑤) |
84 | | fnfvima 6400 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn 𝑋 ∧ 𝑤 ⊆ 𝑋 ∧ (◡𝐹‘𝑦) ∈ 𝑤) → (𝐹‘(◡𝐹‘𝑦)) ∈ (𝐹 “ 𝑤)) |
85 | 82, 64, 83, 84 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → (𝐹‘(◡𝐹‘𝑦)) ∈ (𝐹 “ 𝑤)) |
86 | 79, 85 | eqeltrrd 2689 |
. . . . . . . . . . . 12
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → 𝑦 ∈ (𝐹 “ 𝑤)) |
87 | | eleq2 2677 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐹 “ 𝑤) → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ (𝐹 “ 𝑤))) |
88 | 87 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ (((𝐹 “ 𝑤) ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ∧ 𝑦 ∈ (𝐹 “ 𝑤)) → ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧) |
89 | 75, 86, 88 | syl2anc 691 |
. . . . . . . . . . 11
⊢
(((((𝐽 ∈
TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) ∧ (𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ∧ (◡𝐹‘𝑦) ∈ 𝑤)) → ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧) |
90 | 89 | rexlimdvaa 3014 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤 → ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧)) |
91 | 46, 90 | impbid 201 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧 ↔ ∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤)) |
92 | | eluni2 4376 |
. . . . . . . . 9
⊢ (𝑦 ∈ ∪ ((𝐽
qTop 𝐹) ∩ 𝒫
𝑥) ↔ ∃𝑧 ∈ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥)𝑦 ∈ 𝑧) |
93 | | eluni2 4376 |
. . . . . . . . 9
⊢ ((◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ↔ ∃𝑤 ∈ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥))(◡𝐹‘𝑦) ∈ 𝑤) |
94 | 91, 92, 93 | 3bitr4g 302 |
. . . . . . . 8
⊢ ((((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (𝑦 ∈ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ (◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))) |
95 | 94 | ralbidva 2968 |
. . . . . . 7
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → (∀𝑦 ∈ 𝑥 𝑦 ∈ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ ∀𝑦 ∈ 𝑥 (◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))) |
96 | 15, 95 | syl5bb 271 |
. . . . . 6
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → (𝑥 ⊆ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥) ↔ ∀𝑦 ∈ 𝑥 (◡𝐹‘𝑦) ∈ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))) |
97 | 14, 96 | bitr4d 270 |
. . . . 5
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → ((◡𝐹 “ 𝑥) ⊆ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)) ↔ 𝑥 ⊆ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥))) |
98 | | eltg 20572 |
. . . . . 6
⊢ (𝐽 ∈ TopBases → ((◡𝐹 “ 𝑥) ∈ (topGen‘𝐽) ↔ (◡𝐹 “ 𝑥) ⊆ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))) |
99 | 98 | ad2antrr 758 |
. . . . 5
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → ((◡𝐹 “ 𝑥) ∈ (topGen‘𝐽) ↔ (◡𝐹 “ 𝑥) ⊆ ∪ (𝐽 ∩ 𝒫 (◡𝐹 “ 𝑥)))) |
100 | | ovex 6577 |
. . . . . 6
⊢ (𝐽 qTop 𝐹) ∈ V |
101 | | eltg 20572 |
. . . . . 6
⊢ ((𝐽 qTop 𝐹) ∈ V → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) ↔ 𝑥 ⊆ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥))) |
102 | 100, 101 | mp1i 13 |
. . . . 5
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) ↔ 𝑥 ⊆ ∪ ((𝐽 qTop 𝐹) ∩ 𝒫 𝑥))) |
103 | 97, 99, 102 | 3bitr4d 299 |
. . . 4
⊢ (((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) ∧ 𝑥 ⊆ 𝑌) → ((◡𝐹 “ 𝑥) ∈ (topGen‘𝐽) ↔ 𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)))) |
104 | 103 | pm5.32da 671 |
. . 3
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → ((𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ (topGen‘𝐽)) ↔ (𝑥 ⊆ 𝑌 ∧ 𝑥 ∈ (topGen‘(𝐽 qTop 𝐹))))) |
105 | | tgtopon 20586 |
. . . . . 6
⊢ (𝐽 ∈ TopBases →
(topGen‘𝐽) ∈
(TopOn‘∪ 𝐽)) |
106 | 105 | adantr 480 |
. . . . 5
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (topGen‘𝐽) ∈ (TopOn‘∪ 𝐽)) |
107 | 19 | fveq2i 6106 |
. . . . 5
⊢
(TopOn‘𝑋) =
(TopOn‘∪ 𝐽) |
108 | 106, 107 | syl6eleqr 2699 |
. . . 4
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (topGen‘𝐽) ∈ (TopOn‘𝑋)) |
109 | 7 | adantl 481 |
. . . 4
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → 𝐹:𝑋–onto→𝑌) |
110 | | elqtop3 21316 |
. . . 4
⊢
(((topGen‘𝐽)
∈ (TopOn‘𝑋)
∧ 𝐹:𝑋–onto→𝑌) → (𝑥 ∈ ((topGen‘𝐽) qTop 𝐹) ↔ (𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ (topGen‘𝐽)))) |
111 | 108, 109,
110 | syl2anc 691 |
. . 3
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑥 ∈ ((topGen‘𝐽) qTop 𝐹) ↔ (𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ (topGen‘𝐽)))) |
112 | | unitg 20582 |
. . . . . . . . 9
⊢ ((𝐽 qTop 𝐹) ∈ V → ∪ (topGen‘(𝐽 qTop 𝐹)) = ∪ (𝐽 qTop 𝐹)) |
113 | 100, 112 | ax-mp 5 |
. . . . . . . 8
⊢ ∪ (topGen‘(𝐽 qTop 𝐹)) = ∪ (𝐽 qTop 𝐹) |
114 | 19 | elqtop2 21314 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–onto→𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽))) |
115 | 7, 114 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽))) |
116 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽) → 𝑥 ⊆ 𝑌) |
117 | | selpw 4115 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 𝑌 ↔ 𝑥 ⊆ 𝑌) |
118 | 116, 117 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽) → 𝑥 ∈ 𝒫 𝑌) |
119 | 115, 118 | syl6bi 242 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑥 ∈ (𝐽 qTop 𝐹) → 𝑥 ∈ 𝒫 𝑌)) |
120 | 119 | ssrdv 3574 |
. . . . . . . . 9
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝐽 qTop 𝐹) ⊆ 𝒫 𝑌) |
121 | | sspwuni 4547 |
. . . . . . . . 9
⊢ ((𝐽 qTop 𝐹) ⊆ 𝒫 𝑌 ↔ ∪ (𝐽 qTop 𝐹) ⊆ 𝑌) |
122 | 120, 121 | sylib 207 |
. . . . . . . 8
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → ∪ (𝐽
qTop 𝐹) ⊆ 𝑌) |
123 | 113, 122 | syl5eqss 3612 |
. . . . . . 7
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → ∪ (topGen‘(𝐽 qTop 𝐹)) ⊆ 𝑌) |
124 | | sspwuni 4547 |
. . . . . . 7
⊢
((topGen‘(𝐽
qTop 𝐹)) ⊆ 𝒫
𝑌 ↔ ∪ (topGen‘(𝐽 qTop 𝐹)) ⊆ 𝑌) |
125 | 123, 124 | sylibr 223 |
. . . . . 6
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (topGen‘(𝐽 qTop 𝐹)) ⊆ 𝒫 𝑌) |
126 | 125 | sseld 3567 |
. . . . 5
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) → 𝑥 ∈ 𝒫 𝑌)) |
127 | 126, 117 | syl6ib 240 |
. . . 4
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) → 𝑥 ⊆ 𝑌)) |
128 | 127 | pm4.71rd 665 |
. . 3
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)) ↔ (𝑥 ⊆ 𝑌 ∧ 𝑥 ∈ (topGen‘(𝐽 qTop 𝐹))))) |
129 | 104, 111,
128 | 3bitr4d 299 |
. 2
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝑥 ∈ ((topGen‘𝐽) qTop 𝐹) ↔ 𝑥 ∈ (topGen‘(𝐽 qTop 𝐹)))) |
130 | 129 | eqrdv 2608 |
1
⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → ((topGen‘𝐽) qTop 𝐹) = (topGen‘(𝐽 qTop 𝐹))) |