Step | Hyp | Ref
| Expression |
1 | | cntop1 22497 |
. . . . 5
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) |
2 | 1 | adantr 481 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝐽 ∈ Top) |
3 | | cnvimass 6019 |
. . . . 5
⊢ (◡𝐹 “ (𝐹 “ 𝑆)) ⊆ dom 𝐹 |
4 | | cnclsi.1 |
. . . . . . 7
⊢ 𝑋 = ∪
𝐽 |
5 | | eqid 2736 |
. . . . . . 7
⊢ ∪ 𝐾 =
∪ 𝐾 |
6 | 4, 5 | cnf 22503 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶∪ 𝐾) |
7 | 6 | adantr 481 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶∪ 𝐾) |
8 | 3, 7 | fssdm 6671 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (◡𝐹 “ (𝐹 “ 𝑆)) ⊆ 𝑋) |
9 | | simpr 485 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ 𝑋) |
10 | 7 | fdmd 6662 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → dom 𝐹 = 𝑋) |
11 | 9, 10 | sseqtrrd 3973 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ dom 𝐹) |
12 | | sseqin2 4162 |
. . . . . 6
⊢ (𝑆 ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ 𝑆) = 𝑆) |
13 | 11, 12 | sylib 217 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (dom 𝐹 ∩ 𝑆) = 𝑆) |
14 | | dminss 6091 |
. . . . 5
⊢ (dom
𝐹 ∩ 𝑆) ⊆ (◡𝐹 “ (𝐹 “ 𝑆)) |
15 | 13, 14 | eqsstrrdi 3987 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))) |
16 | 4 | clsss 22311 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ (◡𝐹 “ (𝐹 “ 𝑆)) ⊆ 𝑋 ∧ 𝑆 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))) → ((cls‘𝐽)‘𝑆) ⊆ ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆)))) |
17 | 2, 8, 15, 16 | syl3anc 1370 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆)))) |
18 | | imassrn 6010 |
. . . . 5
⊢ (𝐹 “ 𝑆) ⊆ ran 𝐹 |
19 | 7 | frnd 6659 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ran 𝐹 ⊆ ∪ 𝐾) |
20 | 18, 19 | sstrid 3943 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (𝐹 “ 𝑆) ⊆ ∪ 𝐾) |
21 | 5 | cncls2i 22527 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ (𝐹 “ 𝑆) ⊆ ∪ 𝐾) → ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆))) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆)))) |
22 | 20, 21 | syldan 591 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆))) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆)))) |
23 | 17, 22 | sstrd 3942 |
. 2
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆)))) |
24 | 7 | ffund 6655 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → Fun 𝐹) |
25 | 4 | clsss3 22316 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) |
26 | 1, 25 | sylan 580 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) |
27 | 26, 10 | sseqtrrd 3973 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ dom 𝐹) |
28 | | funimass3 6987 |
. . 3
⊢ ((Fun
𝐹 ∧ ((cls‘𝐽)‘𝑆) ⊆ dom 𝐹) → ((𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆)) ↔ ((cls‘𝐽)‘𝑆) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆))))) |
29 | 24, 27, 28 | syl2anc 584 |
. 2
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆)) ↔ ((cls‘𝐽)‘𝑆) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆))))) |
30 | 23, 29 | mpbird 256 |
1
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆))) |