cmpcld - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cmpcld		Structured version Visualization version GIF version

Theorem cmpcld 23350

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

**Assertion**
Ref	Expression
cmpcld	⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝐽 ↾_t 𝑆) ∈ Comp)

Proof of Theorem cmpcld Dummy variables 𝑡 𝑠 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		velpw 4609	. . . 4 ⊢ (𝑠 ∈ 𝒫 𝐽 ↔ 𝑠 ⊆ 𝐽)
2		simp1l 1194	. . . . . . 7 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝐽 ∈ Comp)
3		simp2 1134	. . . . . . . 8 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝑠 ⊆ 𝐽)
4		eqid 2725	. . . . . . . . . . . 12 ⊢ ∪ 𝐽 = ∪ 𝐽
5	4	cldopn 22979	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (Clsd‘𝐽) → (∪ 𝐽 ∖ 𝑆) ∈ 𝐽)
6	5	adantl 480	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ∖ 𝑆) ∈ 𝐽)
7	6	3ad2ant1 1130	. . . . . . . . 9 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∪ 𝐽 ∖ 𝑆) ∈ 𝐽)
8	7	snssd 4814	. . . . . . . 8 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → {(∪ 𝐽 ∖ 𝑆)} ⊆ 𝐽)
9	3, 8	unssd 4184	. . . . . . 7 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ⊆ 𝐽)
10		simp3 1135	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝑆 ⊆ ∪ 𝑠)
11		uniss 4917	. . . . . . . . . . . . . 14 ⊢ (𝑠 ⊆ 𝐽 → ∪ 𝑠 ⊆ ∪ 𝐽)
12	11	3ad2ant2 1131	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝑠 ⊆ ∪ 𝐽)
13	10, 12	sstrd 3987	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → 𝑆 ⊆ ∪ 𝐽)
14		undif 4483	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ ∪ 𝐽 ↔ (𝑆 ∪ (∪ 𝐽 ∖ 𝑆)) = ∪ 𝐽)
15	13, 14	sylib 217	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (𝑆 ∪ (∪ 𝐽 ∖ 𝑆)) = ∪ 𝐽)
16		unss1 4177	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ ∪ 𝑠 → (𝑆 ∪ (∪ 𝐽 ∖ 𝑆)) ⊆ (∪ 𝑠 ∪ (∪ 𝐽 ∖ 𝑆)))
17	16	3ad2ant3 1132	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (𝑆 ∪ (∪ 𝐽 ∖ 𝑆)) ⊆ (∪ 𝑠 ∪ (∪ 𝐽 ∖ 𝑆)))
18	15, 17	eqsstrrd 4016	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽 ⊆ (∪ 𝑠 ∪ (∪ 𝐽 ∖ 𝑆)))
19		difss 4128	. . . . . . . . . . 11 ⊢ (∪ 𝐽 ∖ 𝑆) ⊆ ∪ 𝐽
20		unss 4182	. . . . . . . . . . 11 ⊢ ((∪ 𝑠 ⊆ ∪ 𝐽 ∧ (∪ 𝐽 ∖ 𝑆) ⊆ ∪ 𝐽) ↔ (∪ 𝑠 ∪ (∪ 𝐽 ∖ 𝑆)) ⊆ ∪ 𝐽)
21	12, 19, 20	sylanblc 587	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∪ 𝑠 ∪ (∪ 𝐽 ∖ 𝑆)) ⊆ ∪ 𝐽)
22	18, 21	eqssd 3994	. . . . . . . . 9 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽 = (∪ 𝑠 ∪ (∪ 𝐽 ∖ 𝑆)))
23		uniexg 7746	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ Comp → ∪ 𝐽 ∈ V)
24	23	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽) → ∪ 𝐽 ∈ V)
25	24	3adant3 1129	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽 ∈ V)
26		difexg 5330	. . . . . . . . . . 11 ⊢ (∪ 𝐽 ∈ V → (∪ 𝐽 ∖ 𝑆) ∈ V)
27		unisng 4929	. . . . . . . . . . 11 ⊢ ((∪ 𝐽 ∖ 𝑆) ∈ V → ∪ {(∪ 𝐽 ∖ 𝑆)} = (∪ 𝐽 ∖ 𝑆))
28	25, 26, 27	3syl 18	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ {(∪ 𝐽 ∖ 𝑆)} = (∪ 𝐽 ∖ 𝑆))
29	28	uneq2d 4160	. . . . . . . . 9 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∪ 𝑠 ∪ ∪ {(∪ 𝐽 ∖ 𝑆)}) = (∪ 𝑠 ∪ (∪ 𝐽 ∖ 𝑆)))
30	22, 29	eqtr4d 2768	. . . . . . . 8 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽 = (∪ 𝑠 ∪ ∪ {(∪ 𝐽 ∖ 𝑆)}))
31		uniun 4934	. . . . . . . 8 ⊢ ∪ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) = (∪ 𝑠 ∪ ∪ {(∪ 𝐽 ∖ 𝑆)})
32	30, 31	eqtr4di 2783	. . . . . . 7 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∪ 𝐽 = ∪ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}))
33	4	cmpcov 23337	. . . . . . 7 ⊢ ((𝐽 ∈ Comp ∧ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)})) → ∃𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∩ Fin)∪ 𝐽 = ∪ 𝑢)
34	2, 9, 32, 33	syl3anc 1368	. . . . . 6 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∃𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∩ Fin)∪ 𝐽 = ∪ 𝑢)
35		elfpw 9380	. . . . . . . 8 ⊢ (𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∩ Fin) ↔ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin))
36		simp2l 1196	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) → 𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}))
37		uncom 4150	. . . . . . . . . . . 12 ⊢ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) = ({(∪ 𝐽 ∖ 𝑆)} ∪ 𝑠)
38	36, 37	sseqtrdi 4027	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) → 𝑢 ⊆ ({(∪ 𝐽 ∖ 𝑆)} ∪ 𝑠))
39		ssundif 4489	. . . . . . . . . . 11 ⊢ (𝑢 ⊆ ({(∪ 𝐽 ∖ 𝑆)} ∪ 𝑠) ↔ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ⊆ 𝑠)
40	38, 39	sylib 217	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ⊆ 𝑠)
41		diffi 9204	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ Fin → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ Fin)
42	41	ad2antll 727	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin)) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ Fin)
43	42	3adant3 1129	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ Fin)
44		elfpw 9380	. . . . . . . . . 10 ⊢ ((𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ (𝒫 𝑠 ∩ Fin) ↔ ((𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ⊆ 𝑠 ∧ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ Fin))
45	40, 43, 44	sylanbrc 581	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) → (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ (𝒫 𝑠 ∩ Fin))
46	10	3ad2ant1 1130	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) → 𝑆 ⊆ ∪ 𝑠)
47	12	3ad2ant1 1130	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) → ∪ 𝑠 ⊆ ∪ 𝐽)
48		simp3 1135	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) → ∪ 𝐽 = ∪ 𝑢)
49	47, 48	sseqtrd 4017	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) → ∪ 𝑠 ⊆ ∪ 𝑢)
50	46, 49	sstrd 3987	. . . . . . . . . . . . . . 15 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) → 𝑆 ⊆ ∪ 𝑢)
51	50	sselda 3976	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → 𝑣 ∈ ∪ 𝑢)
52		eluni 4912	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ∪ 𝑢 ↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢))
53	51, 52	sylib 217	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢))
54		simpl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑣 ∈ 𝑤)
55	54	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑣 ∈ 𝑤))
56		simpr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑤 ∈ 𝑢)
57	56	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑤 ∈ 𝑢))
58		elndif 4125	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ 𝑆 → ¬ 𝑣 ∈ (∪ 𝐽 ∖ 𝑆))
59	58	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) ∧ 𝑣 ∈ 𝑤) → ¬ 𝑣 ∈ (∪ 𝐽 ∖ 𝑆))
60		eleq2 2814	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (∪ 𝐽 ∖ 𝑆) → (𝑣 ∈ 𝑤 ↔ 𝑣 ∈ (∪ 𝐽 ∖ 𝑆)))
61	60	biimpd 228	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (∪ 𝐽 ∖ 𝑆) → (𝑣 ∈ 𝑤 → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆)))
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (𝑤 = (∪ 𝐽 ∖ 𝑆) → (𝑣 ∈ 𝑤 → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆))))
63	62	com23 86	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (𝑣 ∈ 𝑤 → (𝑤 = (∪ 𝐽 ∖ 𝑆) → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆))))
64	63	imp 405	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) ∧ 𝑣 ∈ 𝑤) → (𝑤 = (∪ 𝐽 ∖ 𝑆) → 𝑣 ∈ (∪ 𝐽 ∖ 𝑆)))
65	59, 64	mtod 197	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) ∧ 𝑣 ∈ 𝑤) → ¬ 𝑤 = (∪ 𝐽 ∖ 𝑆))
66	65	ex 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (𝑣 ∈ 𝑤 → ¬ 𝑤 = (∪ 𝐽 ∖ 𝑆)))
67	66	adantrd 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → ¬ 𝑤 = (∪ 𝐽 ∖ 𝑆)))
68		velsn 4646	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ {(∪ 𝐽 ∖ 𝑆)} ↔ 𝑤 = (∪ 𝐽 ∖ 𝑆))
69	68	notbii 319	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑤 ∈ {(∪ 𝐽 ∖ 𝑆)} ↔ ¬ 𝑤 = (∪ 𝐽 ∖ 𝑆))
70	67, 69	imbitrrdi 251	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → ¬ 𝑤 ∈ {(∪ 𝐽 ∖ 𝑆)}))
71	57, 70	jcad 511	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → (𝑤 ∈ 𝑢 ∧ ¬ 𝑤 ∈ {(∪ 𝐽 ∖ 𝑆)})))
72		eldif 3954	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ↔ (𝑤 ∈ 𝑢 ∧ ¬ 𝑤 ∈ {(∪ 𝐽 ∖ 𝑆)}))
73	71, 72	imbitrrdi 251	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)})))
74	55, 73	jcad 511	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → (𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}))))
75	74	eximdv 1912	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑢) → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}))))
76	53, 75	mpd 15	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) ∧ 𝑣 ∈ 𝑆) → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)})))
77	76	ex 411	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) → (𝑣 ∈ 𝑆 → ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}))))
78		eluni 4912	. . . . . . . . . . 11 ⊢ (𝑣 ∈ ∪ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)})))
79	77, 78	imbitrrdi 251	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) → (𝑣 ∈ 𝑆 → 𝑣 ∈ ∪ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)})))
80	79	ssrdv 3982	. . . . . . . . 9 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) → 𝑆 ⊆ ∪ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}))
81		unieq 4920	. . . . . . . . . . 11 ⊢ (𝑡 = (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) → ∪ 𝑡 = ∪ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}))
82	81	sseq2d 4009	. . . . . . . . . 10 ⊢ (𝑡 = (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) → (𝑆 ⊆ ∪ 𝑡 ↔ 𝑆 ⊆ ∪ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)})))
83	82	rspcev 3606	. . . . . . . . 9 ⊢ (((𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)}) ∈ (𝒫 𝑠 ∩ Fin) ∧ 𝑆 ⊆ ∪ (𝑢 ∖ {(∪ 𝐽 ∖ 𝑆)})) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡)
84	45, 80, 83	syl2anc 582	. . . . . . . 8 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ (𝑢 ⊆ (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∧ 𝑢 ∈ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡)
85	35, 84	syl3an2b 1401	. . . . . . 7 ⊢ ((((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) ∧ 𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∩ Fin) ∧ ∪ 𝐽 = ∪ 𝑢) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡)
86	85	rexlimdv3a 3148	. . . . . 6 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → (∃𝑢 ∈ (𝒫 (𝑠 ∪ {(∪ 𝐽 ∖ 𝑆)}) ∩ Fin)∪ 𝐽 = ∪ 𝑢 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡))
87	34, 86	mpd 15	. . . . 5 ⊢ (((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑠 ⊆ 𝐽 ∧ 𝑆 ⊆ ∪ 𝑠) → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡)
88	87	3exp 1116	. . . 4 ⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑠 ⊆ 𝐽 → (𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡)))
89	1, 88	biimtrid 241	. . 3 ⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑠 ∈ 𝒫 𝐽 → (𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡)))
90	89	ralrimiv 3134	. 2 ⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∀𝑠 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡))
91		cmptop 23343	. . 3 ⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top)
92	4	cldss 22977	. . 3 ⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ ∪ 𝐽)
93	4	cmpsub 23348	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽) → ((𝐽 ↾_t 𝑆) ∈ Comp ↔ ∀𝑠 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡)))
94	91, 92, 93	syl2an 594	. 2 ⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((𝐽 ↾_t 𝑆) ∈ Comp ↔ ∀𝑠 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)𝑆 ⊆ ∪ 𝑡)))
95	90, 94	mpbird 256	1 ⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝐽 ↾_t 𝑆) ∈ Comp)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∃wex 1773 ∈ wcel 2098 ∀wral 3050 ∃wrex 3059 Vcvv 3461 ∖ cdif 3941 ∪ cun 3942 ∩ cin 3943 ⊆ wss 3944 𝒫 cpw 4604 {csn 4630 ∪ cuni 4909 ‘cfv 6549 (class class class)co 7419 Fincfn 8964 ↾_t crest 17405 Topctop 22839 Clsdccld 22964 Compccmp 23334

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 ax-un 7741

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-ral 3051 df-rex 3060 df-reu 3364 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3964 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-int 4951 df-iun 4999 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-ord 6374 df-on 6375 df-lim 6376 df-suc 6377 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-fo 6555 df-f1o 6556 df-fv 6557 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7872 df-1st 7994 df-2nd 7995 df-1o 8487 df-er 8725 df-en 8965 df-dom 8966 df-fin 8968 df-fi 9436 df-rest 17407 df-topgen 17428 df-top 22840 df-topon 22857 df-bases 22893 df-cld 22967 df-cmp 23335

This theorem is referenced by: hausllycmp 23442 cldllycmp 23443 txkgen 23600 cmphaushmeo 23748 cnheiborlem 24924 cmpcmet 25291 stoweidlem28 45554 stoweidlem50 45576 stoweidlem57 45583

W3C validator