Step | Hyp | Ref
| Expression |
1 | | kgentop 21155 |
. . 3
⊢ (𝐽 ∈ ran 𝑘Gen →
𝐽 ∈
Top) |
2 | | qtopcmp.1 |
. . . 4
⊢ 𝑋 = ∪
𝐽 |
3 | 2 | qtoptop 21313 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top) |
4 | 1, 3 | sylan 487 |
. 2
⊢ ((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top) |
5 | | elssuni 4403 |
. . . . . . . 8
⊢ (𝑥 ∈
(𝑘Gen‘(𝐽 qTop
𝐹)) → 𝑥 ⊆ ∪ (𝑘Gen‘(𝐽 qTop 𝐹))) |
6 | 5 | adantl 481 |
. . . . . . 7
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → 𝑥 ⊆ ∪
(𝑘Gen‘(𝐽 qTop
𝐹))) |
7 | 4 | adantr 480 |
. . . . . . . 8
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → (𝐽 qTop 𝐹) ∈ Top) |
8 | | eqid 2610 |
. . . . . . . . 9
⊢ ∪ (𝐽
qTop 𝐹) = ∪ (𝐽
qTop 𝐹) |
9 | 8 | kgenuni 21152 |
. . . . . . . 8
⊢ ((𝐽 qTop 𝐹) ∈ Top → ∪ (𝐽
qTop 𝐹) = ∪ (𝑘Gen‘(𝐽 qTop 𝐹))) |
10 | 7, 9 | syl 17 |
. . . . . . 7
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → ∪
(𝐽 qTop 𝐹) = ∪
(𝑘Gen‘(𝐽 qTop
𝐹))) |
11 | 6, 10 | sseqtr4d 3605 |
. . . . . 6
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → 𝑥 ⊆ ∪ (𝐽 qTop 𝐹)) |
12 | | simpll 786 |
. . . . . . . 8
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → 𝐽 ∈ ran 𝑘Gen) |
13 | 12, 1 | syl 17 |
. . . . . . 7
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → 𝐽 ∈ Top) |
14 | | simplr 788 |
. . . . . . . 8
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → 𝐹 Fn 𝑋) |
15 | | dffn4 6034 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑋 ↔ 𝐹:𝑋–onto→ran 𝐹) |
16 | 14, 15 | sylib 207 |
. . . . . . 7
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → 𝐹:𝑋–onto→ran 𝐹) |
17 | 2 | qtopuni 21315 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐹:𝑋–onto→ran 𝐹) → ran 𝐹 = ∪ (𝐽 qTop 𝐹)) |
18 | 13, 16, 17 | syl2anc 691 |
. . . . . 6
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → ran 𝐹 = ∪ (𝐽 qTop 𝐹)) |
19 | 11, 18 | sseqtr4d 3605 |
. . . . 5
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → 𝑥 ⊆ ran 𝐹) |
20 | 2 | toptopon 20548 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
21 | 13, 20 | sylib 207 |
. . . . . . . 8
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → 𝐽 ∈ (TopOn‘𝑋)) |
22 | | qtopid 21318 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) |
23 | 21, 14, 22 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) |
24 | | kgencn3 21171 |
. . . . . . . 8
⊢ ((𝐽 ∈ ran 𝑘Gen ∧
(𝐽 qTop 𝐹) ∈ Top) → (𝐽 Cn (𝐽 qTop 𝐹)) = (𝐽 Cn (𝑘Gen‘(𝐽 qTop 𝐹)))) |
25 | 12, 7, 24 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → (𝐽 Cn (𝐽 qTop 𝐹)) = (𝐽 Cn (𝑘Gen‘(𝐽 qTop 𝐹)))) |
26 | 23, 25 | eleqtrd 2690 |
. . . . . 6
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → 𝐹 ∈ (𝐽 Cn (𝑘Gen‘(𝐽 qTop 𝐹)))) |
27 | | cnima 20879 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽 Cn (𝑘Gen‘(𝐽 qTop 𝐹))) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → (◡𝐹 “ 𝑥) ∈ 𝐽) |
28 | 26, 27 | sylancom 698 |
. . . . 5
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → (◡𝐹 “ 𝑥) ∈ 𝐽) |
29 | 2 | elqtop2 21314 |
. . . . . 6
⊢ ((𝐽 ∈ ran 𝑘Gen ∧
𝐹:𝑋–onto→ran 𝐹) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥 ⊆ ran 𝐹 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽))) |
30 | 12, 16, 29 | syl2anc 691 |
. . . . 5
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → (𝑥 ∈ (𝐽 qTop 𝐹) ↔ (𝑥 ⊆ ran 𝐹 ∧ (◡𝐹 “ 𝑥) ∈ 𝐽))) |
31 | 19, 28, 30 | mpbir2and 959 |
. . . 4
⊢ (((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) ∧ 𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹))) → 𝑥 ∈ (𝐽 qTop 𝐹)) |
32 | 31 | ex 449 |
. . 3
⊢ ((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) → (𝑥 ∈ (𝑘Gen‘(𝐽 qTop 𝐹)) → 𝑥 ∈ (𝐽 qTop 𝐹))) |
33 | 32 | ssrdv 3574 |
. 2
⊢ ((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) → (𝑘Gen‘(𝐽 qTop 𝐹)) ⊆ (𝐽 qTop 𝐹)) |
34 | | iskgen2 21161 |
. 2
⊢ ((𝐽 qTop 𝐹) ∈ ran 𝑘Gen ↔ ((𝐽 qTop 𝐹) ∈ Top ∧
(𝑘Gen‘(𝐽 qTop
𝐹)) ⊆ (𝐽 qTop 𝐹))) |
35 | 4, 33, 34 | sylanbrc 695 |
1
⊢ ((𝐽 ∈ ran 𝑘Gen ∧
𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ ran 𝑘Gen) |