Proof of Theorem cnclsi
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cntop1 23249 | . . . . 5
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) | 
| 2 | 1 | adantr 480 | . . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝐽 ∈ Top) | 
| 3 |  | cnvimass 6099 | . . . . 5
⊢ (◡𝐹 “ (𝐹 “ 𝑆)) ⊆ dom 𝐹 | 
| 4 |  | cnclsi.1 | . . . . . . 7
⊢ 𝑋 = ∪
𝐽 | 
| 5 |  | eqid 2736 | . . . . . . 7
⊢ ∪ 𝐾 =
∪ 𝐾 | 
| 6 | 4, 5 | cnf 23255 | . . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶∪ 𝐾) | 
| 7 | 6 | adantr 480 | . . . . 5
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶∪ 𝐾) | 
| 8 | 3, 7 | fssdm 6754 | . . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (◡𝐹 “ (𝐹 “ 𝑆)) ⊆ 𝑋) | 
| 9 |  | simpr 484 | . . . . . . 7
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ 𝑋) | 
| 10 | 7 | fdmd 6745 | . . . . . . 7
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → dom 𝐹 = 𝑋) | 
| 11 | 9, 10 | sseqtrrd 4020 | . . . . . 6
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ dom 𝐹) | 
| 12 |  | sseqin2 4222 | . . . . . 6
⊢ (𝑆 ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ 𝑆) = 𝑆) | 
| 13 | 11, 12 | sylib 218 | . . . . 5
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (dom 𝐹 ∩ 𝑆) = 𝑆) | 
| 14 |  | dminss 6172 | . . . . 5
⊢ (dom
𝐹 ∩ 𝑆) ⊆ (◡𝐹 “ (𝐹 “ 𝑆)) | 
| 15 | 13, 14 | eqsstrrdi 4028 | . . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))) | 
| 16 | 4 | clsss 23063 | . . . 4
⊢ ((𝐽 ∈ Top ∧ (◡𝐹 “ (𝐹 “ 𝑆)) ⊆ 𝑋 ∧ 𝑆 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))) → ((cls‘𝐽)‘𝑆) ⊆ ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆)))) | 
| 17 | 2, 8, 15, 16 | syl3anc 1372 | . . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆)))) | 
| 18 |  | imassrn 6088 | . . . . 5
⊢ (𝐹 “ 𝑆) ⊆ ran 𝐹 | 
| 19 | 7 | frnd 6743 | . . . . 5
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ran 𝐹 ⊆ ∪ 𝐾) | 
| 20 | 18, 19 | sstrid 3994 | . . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (𝐹 “ 𝑆) ⊆ ∪ 𝐾) | 
| 21 | 5 | cncls2i 23279 | . . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ (𝐹 “ 𝑆) ⊆ ∪ 𝐾) → ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆))) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆)))) | 
| 22 | 20, 21 | syldan 591 | . . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆))) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆)))) | 
| 23 | 17, 22 | sstrd 3993 | . 2
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆)))) | 
| 24 | 7 | ffund 6739 | . . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → Fun 𝐹) | 
| 25 | 4 | clsss3 23068 | . . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) | 
| 26 | 1, 25 | sylan 580 | . . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) | 
| 27 | 26, 10 | sseqtrrd 4020 | . . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ dom 𝐹) | 
| 28 |  | funimass3 7073 | . . 3
⊢ ((Fun
𝐹 ∧ ((cls‘𝐽)‘𝑆) ⊆ dom 𝐹) → ((𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆)) ↔ ((cls‘𝐽)‘𝑆) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆))))) | 
| 29 | 24, 27, 28 | syl2anc 584 | . 2
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆)) ↔ ((cls‘𝐽)‘𝑆) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆))))) | 
| 30 | 23, 29 | mpbird 257 | 1
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆))) |