Proof of Theorem cnclsi
Step | Hyp | Ref
| Expression |
1 | | cntop1 20854 |
. . . . 5
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝐽 ∈ Top) |
3 | | cnvimass 5404 |
. . . . 5
⊢ (◡𝐹 “ (𝐹 “ 𝑆)) ⊆ dom 𝐹 |
4 | | cnclsi.1 |
. . . . . . . 8
⊢ 𝑋 = ∪
𝐽 |
5 | | eqid 2610 |
. . . . . . . 8
⊢ ∪ 𝐾 =
∪ 𝐾 |
6 | 4, 5 | cnf 20860 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶∪ 𝐾) |
7 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶∪ 𝐾) |
8 | | fdm 5964 |
. . . . . 6
⊢ (𝐹:𝑋⟶∪ 𝐾 → dom 𝐹 = 𝑋) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → dom 𝐹 = 𝑋) |
10 | 3, 9 | syl5sseq 3616 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (◡𝐹 “ (𝐹 “ 𝑆)) ⊆ 𝑋) |
11 | | simpr 476 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ 𝑋) |
12 | 11, 9 | sseqtr4d 3605 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ dom 𝐹) |
13 | | sseqin2 3779 |
. . . . . 6
⊢ (𝑆 ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ 𝑆) = 𝑆) |
14 | 12, 13 | sylib 207 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (dom 𝐹 ∩ 𝑆) = 𝑆) |
15 | | dminss 5466 |
. . . . 5
⊢ (dom
𝐹 ∩ 𝑆) ⊆ (◡𝐹 “ (𝐹 “ 𝑆)) |
16 | 14, 15 | syl6eqssr 3619 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))) |
17 | 4 | clsss 20668 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ (◡𝐹 “ (𝐹 “ 𝑆)) ⊆ 𝑋 ∧ 𝑆 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))) → ((cls‘𝐽)‘𝑆) ⊆ ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆)))) |
18 | 2, 10, 16, 17 | syl3anc 1318 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆)))) |
19 | | imassrn 5396 |
. . . . 5
⊢ (𝐹 “ 𝑆) ⊆ ran 𝐹 |
20 | | frn 5966 |
. . . . . 6
⊢ (𝐹:𝑋⟶∪ 𝐾 → ran 𝐹 ⊆ ∪ 𝐾) |
21 | 7, 20 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ran 𝐹 ⊆ ∪ 𝐾) |
22 | 19, 21 | syl5ss 3579 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (𝐹 “ 𝑆) ⊆ ∪ 𝐾) |
23 | 5 | cncls2i 20884 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ (𝐹 “ 𝑆) ⊆ ∪ 𝐾) → ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆))) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆)))) |
24 | 22, 23 | syldan 486 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆))) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆)))) |
25 | 18, 24 | sstrd 3578 |
. 2
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆)))) |
26 | | ffun 5961 |
. . . 4
⊢ (𝐹:𝑋⟶∪ 𝐾 → Fun 𝐹) |
27 | 7, 26 | syl 17 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → Fun 𝐹) |
28 | 4 | clsss3 20673 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) |
29 | 1, 28 | sylan 487 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) |
30 | 29, 9 | sseqtr4d 3605 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ dom 𝐹) |
31 | | funimass3 6241 |
. . 3
⊢ ((Fun
𝐹 ∧ ((cls‘𝐽)‘𝑆) ⊆ dom 𝐹) → ((𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆)) ↔ ((cls‘𝐽)‘𝑆) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆))))) |
32 | 27, 30, 31 | syl2anc 691 |
. 2
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆)) ↔ ((cls‘𝐽)‘𝑆) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆))))) |
33 | 25, 32 | mpbird 246 |
1
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆))) |