Proof of Theorem cnclsi
Step | Hyp | Ref
| Expression |
1 | | cntop1 21850 |
. . . . 5
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) |
2 | 1 | adantr 483 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝐽 ∈ Top) |
3 | | cnvimass 5951 |
. . . . 5
⊢ (◡𝐹 “ (𝐹 “ 𝑆)) ⊆ dom 𝐹 |
4 | | cnclsi.1 |
. . . . . . 7
⊢ 𝑋 = ∪
𝐽 |
5 | | eqid 2823 |
. . . . . . 7
⊢ ∪ 𝐾 =
∪ 𝐾 |
6 | 4, 5 | cnf 21856 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶∪ 𝐾) |
7 | 6 | adantr 483 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶∪ 𝐾) |
8 | 3, 7 | fssdm 6532 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (◡𝐹 “ (𝐹 “ 𝑆)) ⊆ 𝑋) |
9 | | simpr 487 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ 𝑋) |
10 | 7 | fdmd 6525 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → dom 𝐹 = 𝑋) |
11 | 9, 10 | sseqtrrd 4010 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ dom 𝐹) |
12 | | sseqin2 4194 |
. . . . . 6
⊢ (𝑆 ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ 𝑆) = 𝑆) |
13 | 11, 12 | sylib 220 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (dom 𝐹 ∩ 𝑆) = 𝑆) |
14 | | dminss 6012 |
. . . . 5
⊢ (dom
𝐹 ∩ 𝑆) ⊆ (◡𝐹 “ (𝐹 “ 𝑆)) |
15 | 13, 14 | eqsstrrdi 4024 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))) |
16 | 4 | clsss 21664 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ (◡𝐹 “ (𝐹 “ 𝑆)) ⊆ 𝑋 ∧ 𝑆 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))) → ((cls‘𝐽)‘𝑆) ⊆ ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆)))) |
17 | 2, 8, 15, 16 | syl3anc 1367 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆)))) |
18 | | imassrn 5942 |
. . . . 5
⊢ (𝐹 “ 𝑆) ⊆ ran 𝐹 |
19 | 7 | frnd 6523 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ran 𝐹 ⊆ ∪ 𝐾) |
20 | 18, 19 | sstrid 3980 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (𝐹 “ 𝑆) ⊆ ∪ 𝐾) |
21 | 5 | cncls2i 21880 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ (𝐹 “ 𝑆) ⊆ ∪ 𝐾) → ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆))) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆)))) |
22 | 20, 21 | syldan 593 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆))) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆)))) |
23 | 17, 22 | sstrd 3979 |
. 2
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆)))) |
24 | 7 | ffund 6520 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → Fun 𝐹) |
25 | 4 | clsss3 21669 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) |
26 | 1, 25 | sylan 582 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) |
27 | 26, 10 | sseqtrrd 4010 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ dom 𝐹) |
28 | | funimass3 6826 |
. . 3
⊢ ((Fun
𝐹 ∧ ((cls‘𝐽)‘𝑆) ⊆ dom 𝐹) → ((𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆)) ↔ ((cls‘𝐽)‘𝑆) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆))))) |
29 | 24, 27, 28 | syl2anc 586 |
. 2
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆)) ↔ ((cls‘𝐽)‘𝑆) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆))))) |
30 | 23, 29 | mpbird 259 |
1
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆))) |