cmpsub

Description: Two equivalent ways of describing a compact subset of a topological space. Inspired by Sue E. Goodman'sBeginning Topology. (Contributed by Jeff Hankins, 22-Jun-2009) (Revised by Mario Carneiro, 15-Dec-2013)

		Ref	Expression
	Hypothesis	cmpsub.1	$⊢ X = ⋃ J$
	Assertion	cmpsub	$⊢ (J \in Top \land S \subseteq X) \to (J ↾_{𝑡} S \in Comp \leftrightarrow \forall c \in 𝒫 J (S \subseteq ⋃ c \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d))$

Proof

Step	Hyp	Ref	Expression
1		cmpsub.1	$⊢ X = ⋃ J$
2		eqid	$⊢ ⋃ (J ↾_{𝑡} S) = ⋃ (J ↾_{𝑡} S)$
3	2	iscmp	$⊢ J ↾_{𝑡} S \in Comp \leftrightarrow (J ↾_{𝑡} S \in Top \land \forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
4		id	$⊢ S \subseteq X \to S \subseteq X$
5	1	topopn	$⊢ J \in Top \to X \in J$
6		ssexg	$⊢ (S \subseteq X \land X \in J) \to S \in V$
7	4 5 6	syl2anr	$⊢ (J \in Top \land S \subseteq X) \to S \in V$
8		resttop	$⊢ (J \in Top \land S \in V) \to J ↾_{𝑡} S \in Top$
9	7 8	syldan	$⊢ (J \in Top \land S \subseteq X) \to J ↾_{𝑡} S \in Top$
10		ibar	$⊢ J ↾_{𝑡} S \in Top \to (\forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t) \leftrightarrow (J ↾_{𝑡} S \in Top \land \forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t)))$
11	10	bicomd	$⊢ J ↾_{𝑡} S \in Top \to ((J ↾_{𝑡} S \in Top \land \forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t)) \leftrightarrow \forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
12	9 11	syl	$⊢ (J \in Top \land S \subseteq X) \to ((J ↾_{𝑡} S \in Top \land \forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t)) \leftrightarrow \forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
13	3 12	syl5bb	$⊢ (J \in Top \land S \subseteq X) \to (J ↾_{𝑡} S \in Comp \leftrightarrow \forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
14		vex	$⊢ t \in V$
15		eqeq1	$⊢ x = t \to (x = y \cap S \leftrightarrow t = y \cap S)$
16	15	rexbidv	$⊢ x = t \to (\exists y \in c x = y \cap S \leftrightarrow \exists y \in c t = y \cap S)$
17	14 16	elab	$⊢ t \in \{x \| \exists y \in c x = y \cap S\} \leftrightarrow \exists y \in c t = y \cap S$
18		velpw	$⊢ c \in 𝒫 J \leftrightarrow c \subseteq J$
19		ssel2	$⊢ (c \subseteq J \land y \in c) \to y \in J$
20		ineq1	$⊢ d = y \to d \cap S = y \cap S$
21	20	rspceeqv	$⊢ (y \in J \land t = y \cap S) \to \exists d \in J t = d \cap S$
22	21	ex	$⊢ y \in J \to (t = y \cap S \to \exists d \in J t = d \cap S)$
23	19 22	syl	$⊢ (c \subseteq J \land y \in c) \to (t = y \cap S \to \exists d \in J t = d \cap S)$
24	23	ex	$⊢ c \subseteq J \to (y \in c \to (t = y \cap S \to \exists d \in J t = d \cap S))$
25	18 24	sylbi	$⊢ c \in 𝒫 J \to (y \in c \to (t = y \cap S \to \exists d \in J t = d \cap S))$
26	25	adantl	$⊢ ((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \to (y \in c \to (t = y \cap S \to \exists d \in J t = d \cap S))$
27	26	rexlimdv	$⊢ ((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \to (\exists y \in c t = y \cap S \to \exists d \in J t = d \cap S)$
28		simpll	$⊢ ((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \to J \in Top$
29	1	sseq2i	$⊢ S \subseteq X \leftrightarrow S \subseteq ⋃ J$
30		uniexg	$⊢ J \in Top \to ⋃ J \in V$
31		ssexg	$⊢ (S \subseteq ⋃ J \land ⋃ J \in V) \to S \in V$
32	30 31	sylan2	$⊢ (S \subseteq ⋃ J \land J \in Top) \to S \in V$
33	32	ancoms	$⊢ (J \in Top \land S \subseteq ⋃ J) \to S \in V$
34	29 33	sylan2b	$⊢ (J \in Top \land S \subseteq X) \to S \in V$
35	34	adantr	$⊢ ((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \to S \in V$
36		elrest	$⊢ (J \in Top \land S \in V) \to (t \in (J ↾_{𝑡} S) \leftrightarrow \exists d \in J t = d \cap S)$
37	28 35 36	syl2anc	$⊢ ((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \to (t \in (J ↾_{𝑡} S) \leftrightarrow \exists d \in J t = d \cap S)$
38	27 37	sylibrd	$⊢ ((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \to (\exists y \in c t = y \cap S \to t \in (J ↾_{𝑡} S))$
39	17 38	syl5bi	$⊢ ((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \to (t \in \{x \| \exists y \in c x = y \cap S\} \to t \in (J ↾_{𝑡} S))$
40	39	ssrdv	$⊢ ((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \to \{x \| \exists y \in c x = y \cap S\} \subseteq J ↾_{𝑡} S$
41		vex	$⊢ c \in V$
42	41	abrexex	$⊢ \{x \| \exists y \in c x = y \cap S\} \in V$
43	42	elpw	$⊢ \{x \| \exists y \in c x = y \cap S\} \in 𝒫 (J ↾_{𝑡} S) \leftrightarrow \{x \| \exists y \in c x = y \cap S\} \subseteq J ↾_{𝑡} S$
44	40 43	sylibr	$⊢ ((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \to \{x \| \exists y \in c x = y \cap S\} \in 𝒫 (J ↾_{𝑡} S)$
45		unieq	$⊢ s = \{x \| \exists y \in c x = y \cap S\} \to ⋃ s = ⋃ \{x \| \exists y \in c x = y \cap S\}$
46	45	eqeq2d	$⊢ s = \{x \| \exists y \in c x = y \cap S\} \to (⋃ (J ↾_{𝑡} S) = ⋃ s \leftrightarrow ⋃ (J ↾_{𝑡} S) = ⋃ \{x \| \exists y \in c x = y \cap S\})$
47		pweq	$⊢ s = \{x \| \exists y \in c x = y \cap S\} \to 𝒫 s = 𝒫 \{x \| \exists y \in c x = y \cap S\}$
48	47	ineq1d	$⊢ s = \{x \| \exists y \in c x = y \cap S\} \to 𝒫 s \cap Fin = 𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin$
49	48	rexeqdv	$⊢ s = \{x \| \exists y \in c x = y \cap S\} \to (\exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t \leftrightarrow \exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t)$
50	46 49	imbi12d	$⊢ s = \{x \| \exists y \in c x = y \cap S\} \to ((⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t) \leftrightarrow (⋃ (J ↾_{𝑡} S) = ⋃ \{x \| \exists y \in c x = y \cap S\} \to \exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
51	50	rspcva	$⊢ (\{x \| \exists y \in c x = y \cap S\} \in 𝒫 (J ↾_{𝑡} S) \land \forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t)) \to (⋃ (J ↾_{𝑡} S) = ⋃ \{x \| \exists y \in c x = y \cap S\} \to \exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t)$
52	44 51	sylan	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land \forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t)) \to (⋃ (J ↾_{𝑡} S) = ⋃ \{x \| \exists y \in c x = y \cap S\} \to \exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t)$
53	52	ex	$⊢ ((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \to (\forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t) \to (⋃ (J ↾_{𝑡} S) = ⋃ \{x \| \exists y \in c x = y \cap S\} \to \exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
54	1	restuni	$⊢ (J \in Top \land S \subseteq X) \to S = ⋃ (J ↾_{𝑡} S)$
55	54	ad2antrr	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to S = ⋃ (J ↾_{𝑡} S)$
56		vex	$⊢ y \in V$
57	56	inex1	$⊢ y \cap S \in V$
58	57	dfiun2	$⊢ ⋃_{y \in c} (y \cap S) = ⋃ \{x \| \exists y \in c x = y \cap S\}$
59		incom	$⊢ y \cap S = S \cap y$
60	59	a1i	$⊢ ((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land y \in c) \to y \cap S = S \cap y$
61	60	iuneq2dv	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to ⋃_{y \in c} (y \cap S) = ⋃_{y \in c} (S \cap y)$
62	58 61	eqtr3id	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to ⋃ \{x \| \exists y \in c x = y \cap S\} = ⋃_{y \in c} (S \cap y)$
63		iunin2	$⊢ ⋃_{y \in c} (S \cap y) = S \cap ⋃_{y \in c} y$
64		uniiun	$⊢ ⋃ c = ⋃_{y \in c} y$
65	64	eqcomi	$⊢ ⋃_{y \in c} y = ⋃ c$
66	65	a1i	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to ⋃_{y \in c} y = ⋃ c$
67	66	ineq2d	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to S \cap ⋃_{y \in c} y = S \cap ⋃ c$
68		incom	$⊢ S \cap ⋃ c = ⋃ c \cap S$
69		sseqin2	$⊢ S \subseteq ⋃ c \leftrightarrow ⋃ c \cap S = S$
70	69	biimpi	$⊢ S \subseteq ⋃ c \to ⋃ c \cap S = S$
71	68 70	syl5eq	$⊢ S \subseteq ⋃ c \to S \cap ⋃ c = S$
72	71	adantl	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to S \cap ⋃ c = S$
73	67 72	eqtrd	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to S \cap ⋃_{y \in c} y = S$
74	63 73	syl5eq	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to ⋃_{y \in c} (S \cap y) = S$
75	62 74	eqtr2d	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to S = ⋃ \{x \| \exists y \in c x = y \cap S\}$
76	55 75	eqeq12d	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to (S = S \leftrightarrow ⋃ (J ↾_{𝑡} S) = ⋃ \{x \| \exists y \in c x = y \cap S\})$
77	55	eqeq1d	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to (S = ⋃ t \leftrightarrow ⋃ (J ↾_{𝑡} S) = ⋃ t)$
78	77	rexbidv	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to (\exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) S = ⋃ t \leftrightarrow \exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t)$
79	76 78	imbi12d	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to ((S = S \to \exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) S = ⋃ t) \leftrightarrow (⋃ (J ↾_{𝑡} S) = ⋃ \{x \| \exists y \in c x = y \cap S\} \to \exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
80		eqid	$⊢ S = S$
81	80	a1bi	$⊢ \exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) S = ⋃ t \leftrightarrow (S = S \to \exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) S = ⋃ t)$
82		elin	$⊢ t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) \leftrightarrow (t \in 𝒫 \{x \| \exists y \in c x = y \cap S\} \land t \in Fin)$
83		velpw	$⊢ t \in 𝒫 \{x \| \exists y \in c x = y \cap S\} \leftrightarrow t \subseteq \{x \| \exists y \in c x = y \cap S\}$
84		dfss3	$⊢ t \subseteq \{x \| \exists y \in c x = y \cap S\} \leftrightarrow \forall s \in t s \in \{x \| \exists y \in c x = y \cap S\}$
85		vex	$⊢ s \in V$
86		eqeq1	$⊢ x = s \to (x = y \cap S \leftrightarrow s = y \cap S)$
87	86	rexbidv	$⊢ x = s \to (\exists y \in c x = y \cap S \leftrightarrow \exists y \in c s = y \cap S)$
88	85 87	elab	$⊢ s \in \{x \| \exists y \in c x = y \cap S\} \leftrightarrow \exists y \in c s = y \cap S$
89	88	ralbii	$⊢ \forall s \in t s \in \{x \| \exists y \in c x = y \cap S\} \leftrightarrow \forall s \in t \exists y \in c s = y \cap S$
90	83 84 89	3bitri	$⊢ t \in 𝒫 \{x \| \exists y \in c x = y \cap S\} \leftrightarrow \forall s \in t \exists y \in c s = y \cap S$
91	90	anbi1i	$⊢ (t \in 𝒫 \{x \| \exists y \in c x = y \cap S\} \land t \in Fin) \leftrightarrow (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)$
92	82 91	bitri	$⊢ t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) \leftrightarrow (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)$
93		ineq1	$⊢ y = f (s) \to y \cap S = f (s) \cap S$
94	93	eqeq2d	$⊢ y = f (s) \to (s = y \cap S \leftrightarrow s = f (s) \cap S)$
95	94	ac6sfi	$⊢ (t \in Fin \land \forall s \in t \exists y \in c s = y \cap S) \to \exists f (f : t ⟶ c \land \forall s \in t s = f (s) \cap S)$
96	95	ancoms	$⊢ (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin) \to \exists f (f : t ⟶ c \land \forall s \in t s = f (s) \cap S)$
97	96	adantl	$⊢ ((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \to \exists f (f : t ⟶ c \land \forall s \in t s = f (s) \cap S)$
98		frn	$⊢ f : t ⟶ c \to ran f \subseteq c$
99	98	ad2antrl	$⊢ ((((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \land S = ⋃ t) \land (f : t ⟶ c \land \forall s \in t s = f (s) \cap S)) \to ran f \subseteq c$
100		vex	$⊢ f \in V$
101	100	rnex	$⊢ ran f \in V$
102	101	elpw	$⊢ ran f \in 𝒫 c \leftrightarrow ran f \subseteq c$
103	99 102	sylibr	$⊢ ((((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \land S = ⋃ t) \land (f : t ⟶ c \land \forall s \in t s = f (s) \cap S)) \to ran f \in 𝒫 c$
104		simprr	$⊢ ((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \to t \in Fin$
105	104	ad2antrr	$⊢ ((((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \land S = ⋃ t) \land (f : t ⟶ c \land \forall s \in t s = f (s) \cap S)) \to t \in Fin$
106		ffn	$⊢ f : t ⟶ c \to f Fn t$
107		dffn4	$⊢ f Fn t \leftrightarrow f : t \underset{onto}{⟶} ran f$
108	106 107	sylib	$⊢ f : t ⟶ c \to f : t \underset{onto}{⟶} ran f$
109		fodomfi	$⊢ (t \in Fin \land f : t \underset{onto}{⟶} ran f) \to ran f ≼ t$
110	108 109	sylan2	$⊢ (t \in Fin \land f : t ⟶ c) \to ran f ≼ t$
111	110	adantll	$⊢ ((\forall s \in t \exists y \in c s = y \cap S \land t \in Fin) \land f : t ⟶ c) \to ran f ≼ t$
112	111	adantll	$⊢ (((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \land f : t ⟶ c) \to ran f ≼ t$
113	112	ad2ant2r	$⊢ ((((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \land S = ⋃ t) \land (f : t ⟶ c \land \forall s \in t s = f (s) \cap S)) \to ran f ≼ t$
114		domfi	$⊢ (t \in Fin \land ran f ≼ t) \to ran f \in Fin$
115	105 113 114	syl2anc	$⊢ ((((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \land S = ⋃ t) \land (f : t ⟶ c \land \forall s \in t s = f (s) \cap S)) \to ran f \in Fin$
116	103 115	elind	$⊢ ((((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \land S = ⋃ t) \land (f : t ⟶ c \land \forall s \in t s = f (s) \cap S)) \to ran f \in (𝒫 c \cap Fin)$
117		id	$⊢ s = u \to s = u$
118		fveq2	$⊢ s = u \to f (s) = f (u)$
119	118	ineq1d	$⊢ s = u \to f (s) \cap S = f (u) \cap S$
120	117 119	eqeq12d	$⊢ s = u \to (s = f (s) \cap S \leftrightarrow u = f (u) \cap S)$
121	120	rspccv	$⊢ \forall s \in t s = f (s) \cap S \to (u \in t \to u = f (u) \cap S)$
122		pm2.27	$⊢ u \in t \to ((u \in t \to u = f (u) \cap S) \to u = f (u) \cap S)$
123		inss1	$⊢ f (u) \cap S \subseteq f (u)$
124		sseq1	$⊢ u = f (u) \cap S \to (u \subseteq f (u) \leftrightarrow f (u) \cap S \subseteq f (u))$
125	123 124	mpbiri	$⊢ u = f (u) \cap S \to u \subseteq f (u)$
126		ssel	$⊢ u \subseteq f (u) \to (w \in u \to w \in f (u))$
127	126	a1dd	$⊢ u \subseteq f (u) \to (w \in u \to (f : t ⟶ c \to w \in f (u)))$
128	125 127	syl	$⊢ u = f (u) \cap S \to (w \in u \to (f : t ⟶ c \to w \in f (u)))$
129	128	a1i	$⊢ u \in t \to (u = f (u) \cap S \to (w \in u \to (f : t ⟶ c \to w \in f (u))))$
130	129	3imp	$⊢ (u \in t \land u = f (u) \cap S \land w \in u) \to (f : t ⟶ c \to w \in f (u))$
131		fnfvelrn	$⊢ (f Fn t \land u \in t) \to f (u) \in ran f$
132	131	expcom	$⊢ u \in t \to (f Fn t \to f (u) \in ran f)$
133	132	3ad2ant1	$⊢ (u \in t \land u = f (u) \cap S \land w \in u) \to (f Fn t \to f (u) \in ran f)$
134	106 133	syl5	$⊢ (u \in t \land u = f (u) \cap S \land w \in u) \to (f : t ⟶ c \to f (u) \in ran f)$
135	130 134	jcad	$⊢ (u \in t \land u = f (u) \cap S \land w \in u) \to (f : t ⟶ c \to (w \in f (u) \land f (u) \in ran f))$
136	135	3exp	$⊢ u \in t \to (u = f (u) \cap S \to (w \in u \to (f : t ⟶ c \to (w \in f (u) \land f (u) \in ran f))))$
137	122 136	syld	$⊢ u \in t \to ((u \in t \to u = f (u) \cap S) \to (w \in u \to (f : t ⟶ c \to (w \in f (u) \land f (u) \in ran f))))$
138	137	com3r	$⊢ w \in u \to (u \in t \to ((u \in t \to u = f (u) \cap S) \to (f : t ⟶ c \to (w \in f (u) \land f (u) \in ran f))))$
139	138	imp	$⊢ (w \in u \land u \in t) \to ((u \in t \to u = f (u) \cap S) \to (f : t ⟶ c \to (w \in f (u) \land f (u) \in ran f)))$
140	139	com3l	$⊢ (u \in t \to u = f (u) \cap S) \to (f : t ⟶ c \to ((w \in u \land u \in t) \to (w \in f (u) \land f (u) \in ran f)))$
141	140	impcom	$⊢ (f : t ⟶ c \land (u \in t \to u = f (u) \cap S)) \to ((w \in u \land u \in t) \to (w \in f (u) \land f (u) \in ran f))$
142	121 141	sylan2	$⊢ (f : t ⟶ c \land \forall s \in t s = f (s) \cap S) \to ((w \in u \land u \in t) \to (w \in f (u) \land f (u) \in ran f))$
143		fvex	$⊢ f (u) \in V$
144		eleq2	$⊢ v = f (u) \to (w \in v \leftrightarrow w \in f (u))$
145		eleq1	$⊢ v = f (u) \to (v \in ran f \leftrightarrow f (u) \in ran f)$
146	144 145	anbi12d	$⊢ v = f (u) \to ((w \in v \land v \in ran f) \leftrightarrow (w \in f (u) \land f (u) \in ran f))$
147	143 146	spcev	$⊢ (w \in f (u) \land f (u) \in ran f) \to \exists v (w \in v \land v \in ran f)$
148	142 147	syl6	$⊢ (f : t ⟶ c \land \forall s \in t s = f (s) \cap S) \to ((w \in u \land u \in t) \to \exists v (w \in v \land v \in ran f))$
149	148	exlimdv	$⊢ (f : t ⟶ c \land \forall s \in t s = f (s) \cap S) \to (\exists u (w \in u \land u \in t) \to \exists v (w \in v \land v \in ran f))$
150		eluni	$⊢ w \in ⋃ t \leftrightarrow \exists u (w \in u \land u \in t)$
151		eluni	$⊢ w \in ⋃ ran f \leftrightarrow \exists v (w \in v \land v \in ran f)$
152	149 150 151	3imtr4g	$⊢ (f : t ⟶ c \land \forall s \in t s = f (s) \cap S) \to (w \in ⋃ t \to w \in ⋃ ran f)$
153	152	ssrdv	$⊢ (f : t ⟶ c \land \forall s \in t s = f (s) \cap S) \to ⋃ t \subseteq ⋃ ran f$
154	153	adantl	$⊢ ((((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \land S = ⋃ t) \land (f : t ⟶ c \land \forall s \in t s = f (s) \cap S)) \to ⋃ t \subseteq ⋃ ran f$
155		sseq1	$⊢ S = ⋃ t \to (S \subseteq ⋃ ran f \leftrightarrow ⋃ t \subseteq ⋃ ran f)$
156	155	ad2antlr	$⊢ ((((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \land S = ⋃ t) \land (f : t ⟶ c \land \forall s \in t s = f (s) \cap S)) \to (S \subseteq ⋃ ran f \leftrightarrow ⋃ t \subseteq ⋃ ran f)$
157	154 156	mpbird	$⊢ ((((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \land S = ⋃ t) \land (f : t ⟶ c \land \forall s \in t s = f (s) \cap S)) \to S \subseteq ⋃ ran f$
158	116 157	jca	$⊢ ((((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \land S = ⋃ t) \land (f : t ⟶ c \land \forall s \in t s = f (s) \cap S)) \to (ran f \in (𝒫 c \cap Fin) \land S \subseteq ⋃ ran f)$
159	158	ex	$⊢ (((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \land S = ⋃ t) \to ((f : t ⟶ c \land \forall s \in t s = f (s) \cap S) \to (ran f \in (𝒫 c \cap Fin) \land S \subseteq ⋃ ran f))$
160	159	eximdv	$⊢ (((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \land S = ⋃ t) \to (\exists f (f : t ⟶ c \land \forall s \in t s = f (s) \cap S) \to \exists f (ran f \in (𝒫 c \cap Fin) \land S \subseteq ⋃ ran f))$
161	160	ex	$⊢ ((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \to (S = ⋃ t \to (\exists f (f : t ⟶ c \land \forall s \in t s = f (s) \cap S) \to \exists f (ran f \in (𝒫 c \cap Fin) \land S \subseteq ⋃ ran f)))$
162	161	com23	$⊢ ((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \to (\exists f (f : t ⟶ c \land \forall s \in t s = f (s) \cap S) \to (S = ⋃ t \to \exists f (ran f \in (𝒫 c \cap Fin) \land S \subseteq ⋃ ran f)))$
163		unieq	$⊢ d = ran f \to ⋃ d = ⋃ ran f$
164	163	sseq2d	$⊢ d = ran f \to (S \subseteq ⋃ d \leftrightarrow S \subseteq ⋃ ran f)$
165	164	rspcev	$⊢ (ran f \in (𝒫 c \cap Fin) \land S \subseteq ⋃ ran f) \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d$
166	165	exlimiv	$⊢ \exists f (ran f \in (𝒫 c \cap Fin) \land S \subseteq ⋃ ran f) \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d$
167	162 166	syl8	$⊢ ((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \to (\exists f (f : t ⟶ c \land \forall s \in t s = f (s) \cap S) \to (S = ⋃ t \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d))$
168	97 167	mpd	$⊢ ((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land (\forall s \in t \exists y \in c s = y \cap S \land t \in Fin)) \to (S = ⋃ t \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d)$
169	92 168	sylan2b	$⊢ ((((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \land t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin)) \to (S = ⋃ t \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d)$
170	169	rexlimdva	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to (\exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) S = ⋃ t \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d)$
171	81 170	syl5bir	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to ((S = S \to \exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) S = ⋃ t) \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d)$
172	79 171	sylbird	$⊢ (((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \land S \subseteq ⋃ c) \to ((⋃ (J ↾_{𝑡} S) = ⋃ \{x \| \exists y \in c x = y \cap S\} \to \exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t) \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d)$
173	172	ex	$⊢ ((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \to (S \subseteq ⋃ c \to ((⋃ (J ↾_{𝑡} S) = ⋃ \{x \| \exists y \in c x = y \cap S\} \to \exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t) \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d))$
174	173	com23	$⊢ ((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \to ((⋃ (J ↾_{𝑡} S) = ⋃ \{x \| \exists y \in c x = y \cap S\} \to \exists t \in (𝒫 \{x \| \exists y \in c x = y \cap S\} \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t) \to (S \subseteq ⋃ c \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d))$
175	53 174	syld	$⊢ ((J \in Top \land S \subseteq X) \land c \in 𝒫 J) \to (\forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t) \to (S \subseteq ⋃ c \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d))$
176	175	ralrimdva	$⊢ (J \in Top \land S \subseteq X) \to (\forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t) \to \forall c \in 𝒫 J (S \subseteq ⋃ c \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d))$
177	1	cmpsublem	$⊢ (J \in Top \land S \subseteq X) \to (\forall c \in 𝒫 J (S \subseteq ⋃ c \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d) \to \forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t))$
178	176 177	impbid	$⊢ (J \in Top \land S \subseteq X) \to (\forall s \in 𝒫 (J ↾_{𝑡} S) (⋃ (J ↾_{𝑡} S) = ⋃ s \to \exists t \in (𝒫 s \cap Fin) ⋃ (J ↾_{𝑡} S) = ⋃ t) \leftrightarrow \forall c \in 𝒫 J (S \subseteq ⋃ c \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d))$
179	13 178	bitrd	$⊢ (J \in Top \land S \subseteq X) \to (J ↾_{𝑡} S \in Comp \leftrightarrow \forall c \in 𝒫 J (S \subseteq ⋃ c \to \exists d \in (𝒫 c \cap Fin) S \subseteq ⋃ d))$

Metamath Proof Explorer

Theorem cmpsub

Proof