Theorem cnclsi 23187

Description: Property of the image of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.)

Hypothesis

Ref	Expression
cnclsi.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
cnclsi	⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆)))

Proof of Theorem cnclsi

Step	Hyp	Ref	Expression
1		cntop1 23155	. . . . 5 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
2	1	adantr 480	. . . 4 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝐽 ∈ Top)
3		cnvimass 6030	. . . . 5 ⊢ (◡𝐹 “ (𝐹 “ 𝑆)) ⊆ dom 𝐹
4		cnclsi.1	. . . . . . 7 ⊢ 𝑋 = ∪ 𝐽
5		eqid 2731	. . . . . . 7 ⊢ ∪ 𝐾 = ∪ 𝐾
6	4, 5	cnf 23161	. . . . . 6 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶∪ 𝐾)
7	6	adantr 480	. . . . 5 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶∪ 𝐾)
8	3, 7	fssdm 6670	. . . 4 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (◡𝐹 “ (𝐹 “ 𝑆)) ⊆ 𝑋)
9		simpr 484	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ 𝑋)
10	7	fdmd 6661	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → dom 𝐹 = 𝑋)
11	9, 10	sseqtrrd 3967	. . . . . 6 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ dom 𝐹)
12		sseqin2 4170	. . . . . 6 ⊢ (𝑆 ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ 𝑆) = 𝑆)
13	11, 12	sylib 218	. . . . 5 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (dom 𝐹 ∩ 𝑆) = 𝑆)
14		dminss 6100	. . . . 5 ⊢ (dom 𝐹 ∩ 𝑆) ⊆ (◡𝐹 “ (𝐹 “ 𝑆))
15	13, 14	eqsstrrdi 3975	. . . 4 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (◡𝐹 “ (𝐹 “ 𝑆)))
16	4	clsss 22969	. . . 4 ⊢ ((𝐽 ∈ Top ∧ (◡𝐹 “ (𝐹 “ 𝑆)) ⊆ 𝑋 ∧ 𝑆 ⊆ (◡𝐹 “ (𝐹 “ 𝑆))) → ((cls‘𝐽)‘𝑆) ⊆ ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆))))
17	2, 8, 15, 16	syl3anc 1373	. . 3 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆))))
18		imassrn 6019	. . . . 5 ⊢ (𝐹 “ 𝑆) ⊆ ran 𝐹
19	7	frnd 6659	. . . . 5 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ran 𝐹 ⊆ ∪ 𝐾)
20	18, 19	sstrid 3941	. . . 4 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (𝐹 “ 𝑆) ⊆ ∪ 𝐾)
21	5	cncls2i 23185	. . . 4 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ (𝐹 “ 𝑆) ⊆ ∪ 𝐾) → ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆))) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆))))
22	20, 21	syldan 591	. . 3 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘(◡𝐹 “ (𝐹 “ 𝑆))) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆))))
23	17, 22	sstrd 3940	. 2 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ (◡𝐹 “ ((cls‘𝐾)‘(𝐹 “ 𝑆))))
24	7	ffund 6655	. . 3 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → Fun 𝐹)
25	4	clsss3 22974	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
26	1, 25	sylan 580	. . . 4 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
27	26, 10	sseqtrrd 3967	. . 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 257	1 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111   ∩ cin 3896   ⊆ wss 3897  ∪ cuni 4856  ^◡ccnv 5613  dom cdm 5614  ran crn 5615   “ cima 5617  Fun wfun 6475  ⟶wf 6477  ‘cfv 6481  (class class class)co 7346  Topctop 22808  clsccl 22933   Cn ccn 23139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-int 4896  df-iun 4941  df-iin 4942  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-map 8752  df-top 22809  df-topon 22826  df-cld 22934  df-cls 22936  df-cn 23142

This theorem is referenced by:  cncls  23189  hmeocls  23683  clsnsg  24025