cmpcld

Description: A closed subset of a compact space is compact. (Contributed by Jeff Hankins, 29-Jun-2009)

		Ref	Expression
	Assertion	cmpcld	$⊢ (J \in Comp \land S \in Clsd (J)) \to J ↾_{𝑡} S \in Comp$

Proof

Step	Hyp	Ref	Expression
1		velpw	$⊢ s \in 𝒫 J \leftrightarrow s \subseteq J$
2		simp1l	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to J \in Comp$
3		simp2	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to s \subseteq J$
4		eqid	$⊢ ⋃ J = ⋃ J$
5	4	cldopn	$⊢ S \in Clsd (J) \to ⋃ J ∖ S \in J$
6	5	adantl	$⊢ (J \in Comp \land S \in Clsd (J)) \to ⋃ J ∖ S \in J$
7	6	3ad2ant1	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to ⋃ J ∖ S \in J$
8	7	snssd	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to \{⋃ J ∖ S\} \subseteq J$
9	3 8	unssd	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to s \cup \{⋃ J ∖ S\} \subseteq J$
10		simp3	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to S \subseteq ⋃ s$
11		uniss	$⊢ s \subseteq J \to ⋃ s \subseteq ⋃ J$
12	11	3ad2ant2	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to ⋃ s \subseteq ⋃ J$
13	10 12	sstrd	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to S \subseteq ⋃ J$
14		undif	$⊢ S \subseteq ⋃ J \leftrightarrow S \cup (⋃ J ∖ S) = ⋃ J$
15	13 14	sylib	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to S \cup (⋃ J ∖ S) = ⋃ J$
16		unss1	$⊢ S \subseteq ⋃ s \to S \cup (⋃ J ∖ S) \subseteq ⋃ s \cup (⋃ J ∖ S)$
17	16	3ad2ant3	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to S \cup (⋃ J ∖ S) \subseteq ⋃ s \cup (⋃ J ∖ S)$
18	15 17	eqsstrrd	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to ⋃ J \subseteq ⋃ s \cup (⋃ J ∖ S)$
19		difss	$⊢ ⋃ J ∖ S \subseteq ⋃ J$
20		unss	$⊢ (⋃ s \subseteq ⋃ J \land ⋃ J ∖ S \subseteq ⋃ J) \leftrightarrow ⋃ s \cup (⋃ J ∖ S) \subseteq ⋃ J$
21	12 19 20	sylanblc	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to ⋃ s \cup (⋃ J ∖ S) \subseteq ⋃ J$
22	18 21	eqssd	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to ⋃ J = ⋃ s \cup (⋃ J ∖ S)$
23		uniexg	$⊢ J \in Comp \to ⋃ J \in V$
24	23	ad2antrr	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J) \to ⋃ J \in V$
25	24	3adant3	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to ⋃ J \in V$
26		difexg	$⊢ ⋃ J \in V \to ⋃ J ∖ S \in V$
27		unisng	$⊢ ⋃ J ∖ S \in V \to ⋃ \{⋃ J ∖ S\} = ⋃ J ∖ S$
28	25 26 27	3syl	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to ⋃ \{⋃ J ∖ S\} = ⋃ J ∖ S$
29	28	uneq2d	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to ⋃ s \cup ⋃ \{⋃ J ∖ S\} = ⋃ s \cup (⋃ J ∖ S)$
30	22 29	eqtr4d	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to ⋃ J = ⋃ s \cup ⋃ \{⋃ J ∖ S\}$
31		uniun	$⊢ ⋃ (s \cup \{⋃ J ∖ S\}) = ⋃ s \cup ⋃ \{⋃ J ∖ S\}$
32	30 31	eqtr4di	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to ⋃ J = ⋃ (s \cup \{⋃ J ∖ S\})$
33	4	cmpcov	$⊢ (J \in Comp \land s \cup \{⋃ J ∖ S\} \subseteq J \land ⋃ J = ⋃ (s \cup \{⋃ J ∖ S\})) \to \exists u \in (𝒫 (s \cup \{⋃ J ∖ S\}) \cap Fin) ⋃ J = ⋃ u$
34	2 9 32 33	syl3anc	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to \exists u \in (𝒫 (s \cup \{⋃ J ∖ S\}) \cap Fin) ⋃ J = ⋃ u$
35		elfpw	$⊢ u \in (𝒫 (s \cup \{⋃ J ∖ S\}) \cap Fin) \leftrightarrow (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin)$
36		simp2l	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \to u \subseteq s \cup \{⋃ J ∖ S\}$
37		uncom	$⊢ s \cup \{⋃ J ∖ S\} = \{⋃ J ∖ S\} \cup s$
38	36 37	sseqtrdi	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \to u \subseteq \{⋃ J ∖ S\} \cup s$
39		ssundif	$⊢ u \subseteq \{⋃ J ∖ S\} \cup s \leftrightarrow u ∖ \{⋃ J ∖ S\} \subseteq s$
40	38 39	sylib	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \to u ∖ \{⋃ J ∖ S\} \subseteq s$
41		diffi	$⊢ u \in Fin \to u ∖ \{⋃ J ∖ S\} \in Fin$
42	41	ad2antll	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin)) \to u ∖ \{⋃ J ∖ S\} \in Fin$
43	42	3adant3	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \to u ∖ \{⋃ J ∖ S\} \in Fin$
44		elfpw	$⊢ u ∖ \{⋃ J ∖ S\} \in (𝒫 s \cap Fin) \leftrightarrow (u ∖ \{⋃ J ∖ S\} \subseteq s \land u ∖ \{⋃ J ∖ S\} \in Fin)$
45	40 43 44	sylanbrc	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \to u ∖ \{⋃ J ∖ S\} \in (𝒫 s \cap Fin)$
46	10	3ad2ant1	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \to S \subseteq ⋃ s$
47	12	3ad2ant1	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \to ⋃ s \subseteq ⋃ J$
48		simp3	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \to ⋃ J = ⋃ u$
49	47 48	sseqtrd	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \to ⋃ s \subseteq ⋃ u$
50	46 49	sstrd	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \to S \subseteq ⋃ u$
51	50	sselda	$⊢ ((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \to v \in ⋃ u$
52		eluni	$⊢ v \in ⋃ u \leftrightarrow \exists w (v \in w \land w \in u)$
53	51 52	sylib	$⊢ ((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \to \exists w (v \in w \land w \in u)$
54		simpl	$⊢ (v \in w \land w \in u) \to v \in w$
55	54	a1i	$⊢ ((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \to ((v \in w \land w \in u) \to v \in w)$
56		simpr	$⊢ (v \in w \land w \in u) \to w \in u$
57	56	a1i	$⊢ ((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \to ((v \in w \land w \in u) \to w \in u)$
58		elndif	$⊢ v \in S \to \neg v \in (⋃ J ∖ S)$
59	58	ad2antlr	$⊢ (((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \land v \in w) \to \neg v \in (⋃ J ∖ S)$
60		eleq2	$⊢ w = ⋃ J ∖ S \to (v \in w \leftrightarrow v \in (⋃ J ∖ S))$
61	60	biimpd	$⊢ w = ⋃ J ∖ S \to (v \in w \to v \in (⋃ J ∖ S))$
62	61	a1i	$⊢ ((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \to (w = ⋃ J ∖ S \to (v \in w \to v \in (⋃ J ∖ S)))$
63	62	com23	$⊢ ((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \to (v \in w \to (w = ⋃ J ∖ S \to v \in (⋃ J ∖ S)))$
64	63	imp	$⊢ (((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \land v \in w) \to (w = ⋃ J ∖ S \to v \in (⋃ J ∖ S))$
65	59 64	mtod	$⊢ (((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \land v \in w) \to \neg w = ⋃ J ∖ S$
66	65	ex	$⊢ ((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \to (v \in w \to \neg w = ⋃ J ∖ S)$
67	66	adantrd	$⊢ ((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \to ((v \in w \land w \in u) \to \neg w = ⋃ J ∖ S)$
68		velsn	$⊢ w \in \{⋃ J ∖ S\} \leftrightarrow w = ⋃ J ∖ S$
69	68	notbii	$⊢ \neg w \in \{⋃ J ∖ S\} \leftrightarrow \neg w = ⋃ J ∖ S$
70	67 69	syl6ibr	$⊢ ((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \to ((v \in w \land w \in u) \to \neg w \in \{⋃ J ∖ S\})$
71	57 70	jcad	$⊢ ((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \to ((v \in w \land w \in u) \to (w \in u \land \neg w \in \{⋃ J ∖ S\}))$
72		eldif	$⊢ w \in (u ∖ \{⋃ J ∖ S\}) \leftrightarrow (w \in u \land \neg w \in \{⋃ J ∖ S\})$
73	71 72	syl6ibr	$⊢ ((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \to ((v \in w \land w \in u) \to w \in (u ∖ \{⋃ J ∖ S\}))$
74	55 73	jcad	$⊢ ((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \to ((v \in w \land w \in u) \to (v \in w \land w \in (u ∖ \{⋃ J ∖ S\})))$
75	74	eximdv	$⊢ ((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \to (\exists w (v \in w \land w \in u) \to \exists w (v \in w \land w \in (u ∖ \{⋃ J ∖ S\})))$
76	53 75	mpd	$⊢ ((((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \land v \in S) \to \exists w (v \in w \land w \in (u ∖ \{⋃ J ∖ S\}))$
77	76	ex	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \to (v \in S \to \exists w (v \in w \land w \in (u ∖ \{⋃ J ∖ S\})))$
78		eluni	$⊢ v \in ⋃ (u ∖ \{⋃ J ∖ S\}) \leftrightarrow \exists w (v \in w \land w \in (u ∖ \{⋃ J ∖ S\}))$
79	77 78	syl6ibr	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \to (v \in S \to v \in ⋃ (u ∖ \{⋃ J ∖ S\}))$
80	79	ssrdv	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \to S \subseteq ⋃ (u ∖ \{⋃ J ∖ S\})$
81		unieq	$⊢ t = u ∖ \{⋃ J ∖ S\} \to ⋃ t = ⋃ (u ∖ \{⋃ J ∖ S\})$
82	81	sseq2d	$⊢ t = u ∖ \{⋃ J ∖ S\} \to (S \subseteq ⋃ t \leftrightarrow S \subseteq ⋃ (u ∖ \{⋃ J ∖ S\}))$
83	82	rspcev	$⊢ (u ∖ \{⋃ J ∖ S\} \in (𝒫 s \cap Fin) \land S \subseteq ⋃ (u ∖ \{⋃ J ∖ S\})) \to \exists t \in (𝒫 s \cap Fin) S \subseteq ⋃ t$
84	45 80 83	syl2anc	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land (u \subseteq s \cup \{⋃ J ∖ S\} \land u \in Fin) \land ⋃ J = ⋃ u) \to \exists t \in (𝒫 s \cap Fin) S \subseteq ⋃ t$
85	35 84	syl3an2b	$⊢ (((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \land u \in (𝒫 (s \cup \{⋃ J ∖ S\}) \cap Fin) \land ⋃ J = ⋃ u) \to \exists t \in (𝒫 s \cap Fin) S \subseteq ⋃ t$
86	85	rexlimdv3a	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to (\exists u \in (𝒫 (s \cup \{⋃ J ∖ S\}) \cap Fin) ⋃ J = ⋃ u \to \exists t \in (𝒫 s \cap Fin) S \subseteq ⋃ t)$
87	34 86	mpd	$⊢ ((J \in Comp \land S \in Clsd (J)) \land s \subseteq J \land S \subseteq ⋃ s) \to \exists t \in (𝒫 s \cap Fin) S \subseteq ⋃ t$
88	87	3exp	$⊢ (J \in Comp \land S \in Clsd (J)) \to (s \subseteq J \to (S \subseteq ⋃ s \to \exists t \in (𝒫 s \cap Fin) S \subseteq ⋃ t))$
89	1 88	syl5bi	$⊢ (J \in Comp \land S \in Clsd (J)) \to (s \in 𝒫 J \to (S \subseteq ⋃ s \to \exists t \in (𝒫 s \cap Fin) S \subseteq ⋃ t))$
90	89	ralrimiv	$⊢ (J \in Comp \land S \in Clsd (J)) \to \forall s \in 𝒫 J (S \subseteq ⋃ s \to \exists t \in (𝒫 s \cap Fin) S \subseteq ⋃ t)$
91		cmptop	$⊢ J \in Comp \to J \in Top$
92	4	cldss	$⊢ S \in Clsd (J) \to S \subseteq ⋃ J$
93	4	cmpsub	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (J ↾_{𝑡} S \in Comp \leftrightarrow \forall s \in 𝒫 J (S \subseteq ⋃ s \to \exists t \in (𝒫 s \cap Fin) S \subseteq ⋃ t))$
94	91 92 93	syl2an	$⊢ (J \in Comp \land S \in Clsd (J)) \to (J ↾_{𝑡} S \in Comp \leftrightarrow \forall s \in 𝒫 J (S \subseteq ⋃ s \to \exists t \in (𝒫 s \cap Fin) S \subseteq ⋃ t))$
95	90 94	mpbird	$⊢ (J \in Comp \land S \in Clsd (J)) \to J ↾_{𝑡} S \in Comp$

Metamath Proof Explorer

Theorem cmpcld

Proof