clsf2 - Mathbox for Richard Penner

	Mathbox for Richard Penner		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > clsf2		Structured version Visualization version GIF version

Theorem clsf2 41203

Description: The closure function is a map from the powerset of the base set to itself. This is less precise than clsf 21749. (Contributed by RP, 22-Apr-2021.)

**Hypotheses**
Ref	Expression
clselmap.x	⊢ 𝑋 = ∪ 𝐽
clselmap.k	⊢ 𝐾 = (cls‘𝐽)

**Assertion**
Ref	Expression
clsf2	⊢ (𝐽 ∈ Top → 𝐾:𝒫 𝑋⟶𝒫 𝑋)

**Proof of Theorem clsf2**
Step	Hyp	Ref	Expression
1		clselmap.x	. . . 4 ⊢ 𝑋 = ∪ 𝐽
2	1	clsf 21749	. . 3 ⊢ (𝐽 ∈ Top → (cls‘𝐽):𝒫 𝑋⟶(Clsd‘𝐽))
3		clselmap.k	. . . . 5 ⊢ 𝐾 = (cls‘𝐽)
4	3	feq1i 6490	. . . 4 ⊢ (𝐾:𝒫 𝑋⟶(Clsd‘𝐽) ↔ (cls‘𝐽):𝒫 𝑋⟶(Clsd‘𝐽))
5		df-f 6340	. . . 4 ⊢ (𝐾:𝒫 𝑋⟶(Clsd‘𝐽) ↔ (𝐾 Fn 𝒫 𝑋 ∧ ran 𝐾 ⊆ (Clsd‘𝐽)))
6	4, 5	sylbb1 240	. . 3 ⊢ ((cls‘𝐽):𝒫 𝑋⟶(Clsd‘𝐽) → (𝐾 Fn 𝒫 𝑋 ∧ ran 𝐾 ⊆ (Clsd‘𝐽)))
7	1	cldss2 21731	. . . . 5 ⊢ (Clsd‘𝐽) ⊆ 𝒫 𝑋
8		sstr2 3900	. . . . 5 ⊢ (ran 𝐾 ⊆ (Clsd‘𝐽) → ((Clsd‘𝐽) ⊆ 𝒫 𝑋 → ran 𝐾 ⊆ 𝒫 𝑋))
9	7, 8	mpi 20	. . . 4 ⊢ (ran 𝐾 ⊆ (Clsd‘𝐽) → ran 𝐾 ⊆ 𝒫 𝑋)
10	9	anim2i 620	. . 3 ⊢ ((𝐾 Fn 𝒫 𝑋 ∧ ran 𝐾 ⊆ (Clsd‘𝐽)) → (𝐾 Fn 𝒫 𝑋 ∧ ran 𝐾 ⊆ 𝒫 𝑋))
11	2, 6, 10	3syl 18	. 2 ⊢ (𝐽 ∈ Top → (𝐾 Fn 𝒫 𝑋 ∧ ran 𝐾 ⊆ 𝒫 𝑋))
12		df-f 6340	. 2 ⊢ (𝐾:𝒫 𝑋⟶𝒫 𝑋 ↔ (𝐾 Fn 𝒫 𝑋 ∧ ran 𝐾 ⊆ 𝒫 𝑋))
13	11, 12	sylibr 237	1 ⊢ (𝐽 ∈ Top → 𝐾:𝒫 𝑋⟶𝒫 𝑋)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1539 ∈ wcel 2112 ⊆ wss 3859 𝒫 cpw 4495 ∪ cuni 4799 ran crn 5526 Fn wfn 6331 ⟶wf 6332 ‘cfv 6336 Topctop 21594 Clsdccld 21717 clsccl 21719

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-rep 5157 ax-sep 5170 ax-nul 5177 ax-pow 5235 ax-pr 5299 ax-un 7460

This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2902 df-ne 2953 df-ral 3076 df-rex 3077 df-reu 3078 df-rab 3080 df-v 3412 df-sbc 3698 df-csb 3807 df-dif 3862 df-un 3864 df-in 3866 df-ss 3876 df-nul 4227 df-if 4422 df-pw 4497 df-sn 4524 df-pr 4526 df-op 4530 df-uni 4800 df-int 4840 df-iun 4886 df-iin 4887 df-br 5034 df-opab 5096 df-mpt 5114 df-id 5431 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-iota 6295 df-fun 6338 df-fn 6339 df-f 6340 df-f1 6341 df-fo 6342 df-f1o 6343 df-fv 6344 df-top 21595 df-cld 21720 df-cls 21722

This theorem is referenced by: clselmap 41204

W3C validator