uncmp

Description: The union of two compact sets is compact. (Contributed by Jeff Hankins, 30-Jan-2010)

		Ref	Expression
	Hypothesis	uncmp.1	$⊢ X = ⋃ J$
	Assertion	uncmp	$⊢ ((J \in Top \land X = S \cup T) \land (J ↾_{𝑡} S \in Comp \land J ↾_{𝑡} T \in Comp)) \to J \in Comp$

Proof

Step	Hyp	Ref	Expression
1		uncmp.1	$⊢ X = ⋃ J$
2		simpll	$⊢ ((J \in Top \land X = S \cup T) \land (J ↾_{𝑡} S \in Comp \land J ↾_{𝑡} T \in Comp)) \to J \in Top$
3		simpll	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to J \in Top$
4		ssun1	$⊢ S \subseteq S \cup T$
5		sseq2	$⊢ X = S \cup T \to (S \subseteq X \leftrightarrow S \subseteq S \cup T)$
6	4 5	mpbiri	$⊢ X = S \cup T \to S \subseteq X$
7	6	ad2antlr	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to S \subseteq X$
8	1	cmpsub	$⊢ (J \in Top \land S \subseteq X) \to (J ↾_{𝑡} S \in Comp \leftrightarrow \forall m \in 𝒫 J (S \subseteq ⋃ m \to \exists n \in (𝒫 m \cap Fin) S \subseteq ⋃ n))$
9	3 7 8	syl2anc	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to (J ↾_{𝑡} S \in Comp \leftrightarrow \forall m \in 𝒫 J (S \subseteq ⋃ m \to \exists n \in (𝒫 m \cap Fin) S \subseteq ⋃ n))$
10		simprr	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to X = ⋃ c$
11	7 10	sseqtrd	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to S \subseteq ⋃ c$
12		unieq	$⊢ m = c \to ⋃ m = ⋃ c$
13	12	sseq2d	$⊢ m = c \to (S \subseteq ⋃ m \leftrightarrow S \subseteq ⋃ c)$
14		pweq	$⊢ m = c \to 𝒫 m = 𝒫 c$
15	14	ineq1d	$⊢ m = c \to 𝒫 m \cap Fin = 𝒫 c \cap Fin$
16	15	rexeqdv	$⊢ m = c \to (\exists n \in (𝒫 m \cap Fin) S \subseteq ⋃ n \leftrightarrow \exists n \in (𝒫 c \cap Fin) S \subseteq ⋃ n)$
17	13 16	imbi12d	$⊢ m = c \to ((S \subseteq ⋃ m \to \exists n \in (𝒫 m \cap Fin) S \subseteq ⋃ n) \leftrightarrow (S \subseteq ⋃ c \to \exists n \in (𝒫 c \cap Fin) S \subseteq ⋃ n))$
18	17	rspcv	$⊢ c \in 𝒫 J \to (\forall m \in 𝒫 J (S \subseteq ⋃ m \to \exists n \in (𝒫 m \cap Fin) S \subseteq ⋃ n) \to (S \subseteq ⋃ c \to \exists n \in (𝒫 c \cap Fin) S \subseteq ⋃ n))$
19	18	ad2antrl	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to (\forall m \in 𝒫 J (S \subseteq ⋃ m \to \exists n \in (𝒫 m \cap Fin) S \subseteq ⋃ n) \to (S \subseteq ⋃ c \to \exists n \in (𝒫 c \cap Fin) S \subseteq ⋃ n))$
20	11 19	mpid	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to (\forall m \in 𝒫 J (S \subseteq ⋃ m \to \exists n \in (𝒫 m \cap Fin) S \subseteq ⋃ n) \to \exists n \in (𝒫 c \cap Fin) S \subseteq ⋃ n)$
21	9 20	sylbid	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to (J ↾_{𝑡} S \in Comp \to \exists n \in (𝒫 c \cap Fin) S \subseteq ⋃ n)$
22		ssun2	$⊢ T \subseteq S \cup T$
23		sseq2	$⊢ X = S \cup T \to (T \subseteq X \leftrightarrow T \subseteq S \cup T)$
24	22 23	mpbiri	$⊢ X = S \cup T \to T \subseteq X$
25	24	ad2antlr	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to T \subseteq X$
26	1	cmpsub	$⊢ (J \in Top \land T \subseteq X) \to (J ↾_{𝑡} T \in Comp \leftrightarrow \forall r \in 𝒫 J (T \subseteq ⋃ r \to \exists s \in (𝒫 r \cap Fin) T \subseteq ⋃ s))$
27	3 25 26	syl2anc	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to (J ↾_{𝑡} T \in Comp \leftrightarrow \forall r \in 𝒫 J (T \subseteq ⋃ r \to \exists s \in (𝒫 r \cap Fin) T \subseteq ⋃ s))$
28	25 10	sseqtrd	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to T \subseteq ⋃ c$
29		unieq	$⊢ r = c \to ⋃ r = ⋃ c$
30	29	sseq2d	$⊢ r = c \to (T \subseteq ⋃ r \leftrightarrow T \subseteq ⋃ c)$
31		pweq	$⊢ r = c \to 𝒫 r = 𝒫 c$
32	31	ineq1d	$⊢ r = c \to 𝒫 r \cap Fin = 𝒫 c \cap Fin$
33	32	rexeqdv	$⊢ r = c \to (\exists s \in (𝒫 r \cap Fin) T \subseteq ⋃ s \leftrightarrow \exists s \in (𝒫 c \cap Fin) T \subseteq ⋃ s)$
34	30 33	imbi12d	$⊢ r = c \to ((T \subseteq ⋃ r \to \exists s \in (𝒫 r \cap Fin) T \subseteq ⋃ s) \leftrightarrow (T \subseteq ⋃ c \to \exists s \in (𝒫 c \cap Fin) T \subseteq ⋃ s))$
35	34	rspcv	$⊢ c \in 𝒫 J \to (\forall r \in 𝒫 J (T \subseteq ⋃ r \to \exists s \in (𝒫 r \cap Fin) T \subseteq ⋃ s) \to (T \subseteq ⋃ c \to \exists s \in (𝒫 c \cap Fin) T \subseteq ⋃ s))$
36	35	ad2antrl	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to (\forall r \in 𝒫 J (T \subseteq ⋃ r \to \exists s \in (𝒫 r \cap Fin) T \subseteq ⋃ s) \to (T \subseteq ⋃ c \to \exists s \in (𝒫 c \cap Fin) T \subseteq ⋃ s))$
37	28 36	mpid	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to (\forall r \in 𝒫 J (T \subseteq ⋃ r \to \exists s \in (𝒫 r \cap Fin) T \subseteq ⋃ s) \to \exists s \in (𝒫 c \cap Fin) T \subseteq ⋃ s)$
38	27 37	sylbid	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to (J ↾_{𝑡} T \in Comp \to \exists s \in (𝒫 c \cap Fin) T \subseteq ⋃ s)$
39		reeanv	$⊢ \exists n \in (𝒫 c \cap Fin) \exists s \in (𝒫 c \cap Fin) (S \subseteq ⋃ n \land T \subseteq ⋃ s) \leftrightarrow (\exists n \in (𝒫 c \cap Fin) S \subseteq ⋃ n \land \exists s \in (𝒫 c \cap Fin) T \subseteq ⋃ s)$
40		elinel1	$⊢ n \in (𝒫 c \cap Fin) \to n \in 𝒫 c$
41	40	elpwid	$⊢ n \in (𝒫 c \cap Fin) \to n \subseteq c$
42		elinel1	$⊢ s \in (𝒫 c \cap Fin) \to s \in 𝒫 c$
43	42	elpwid	$⊢ s \in (𝒫 c \cap Fin) \to s \subseteq c$
44	41 43	anim12i	$⊢ (n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \to (n \subseteq c \land s \subseteq c)$
45	44	ad2antrl	$⊢ (((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \land ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \land (S \subseteq ⋃ n \land T \subseteq ⋃ s))) \to (n \subseteq c \land s \subseteq c)$
46		unss	$⊢ (n \subseteq c \land s \subseteq c) \leftrightarrow n \cup s \subseteq c$
47	45 46	sylib	$⊢ (((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \land ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \land (S \subseteq ⋃ n \land T \subseteq ⋃ s))) \to n \cup s \subseteq c$
48		elinel2	$⊢ n \in (𝒫 c \cap Fin) \to n \in Fin$
49		elinel2	$⊢ s \in (𝒫 c \cap Fin) \to s \in Fin$
50		unfi	$⊢ (n \in Fin \land s \in Fin) \to n \cup s \in Fin$
51	48 49 50	syl2an	$⊢ (n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \to n \cup s \in Fin$
52	51	ad2antrl	$⊢ (((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \land ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \land (S \subseteq ⋃ n \land T \subseteq ⋃ s))) \to n \cup s \in Fin$
53	47 52	jca	$⊢ (((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \land ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \land (S \subseteq ⋃ n \land T \subseteq ⋃ s))) \to (n \cup s \subseteq c \land n \cup s \in Fin)$
54		elin	$⊢ n \cup s \in (𝒫 c \cap Fin) \leftrightarrow (n \cup s \in 𝒫 c \land n \cup s \in Fin)$
55		vex	$⊢ c \in V$
56	55	elpw2	$⊢ n \cup s \in 𝒫 c \leftrightarrow n \cup s \subseteq c$
57	56	anbi1i	$⊢ (n \cup s \in 𝒫 c \land n \cup s \in Fin) \leftrightarrow (n \cup s \subseteq c \land n \cup s \in Fin)$
58	54 57	bitr2i	$⊢ (n \cup s \subseteq c \land n \cup s \in Fin) \leftrightarrow n \cup s \in (𝒫 c \cap Fin)$
59	53 58	sylib	$⊢ (((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \land ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \land (S \subseteq ⋃ n \land T \subseteq ⋃ s))) \to n \cup s \in (𝒫 c \cap Fin)$
60		simpllr	$⊢ (((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \land ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \land (S \subseteq ⋃ n \land T \subseteq ⋃ s))) \to X = S \cup T$
61		ssun3	$⊢ S \subseteq ⋃ n \to S \subseteq ⋃ n \cup ⋃ s$
62		ssun4	$⊢ T \subseteq ⋃ s \to T \subseteq ⋃ n \cup ⋃ s$
63	61 62	anim12i	$⊢ (S \subseteq ⋃ n \land T \subseteq ⋃ s) \to (S \subseteq ⋃ n \cup ⋃ s \land T \subseteq ⋃ n \cup ⋃ s)$
64	63	ad2antll	$⊢ (((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \land ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \land (S \subseteq ⋃ n \land T \subseteq ⋃ s))) \to (S \subseteq ⋃ n \cup ⋃ s \land T \subseteq ⋃ n \cup ⋃ s)$
65		unss	$⊢ (S \subseteq ⋃ n \cup ⋃ s \land T \subseteq ⋃ n \cup ⋃ s) \leftrightarrow S \cup T \subseteq ⋃ n \cup ⋃ s$
66	64 65	sylib	$⊢ (((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \land ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \land (S \subseteq ⋃ n \land T \subseteq ⋃ s))) \to S \cup T \subseteq ⋃ n \cup ⋃ s$
67	60 66	eqsstrd	$⊢ (((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \land ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \land (S \subseteq ⋃ n \land T \subseteq ⋃ s))) \to X \subseteq ⋃ n \cup ⋃ s$
68		uniun	$⊢ ⋃ (n \cup s) = ⋃ n \cup ⋃ s$
69	67 68	sseqtrrdi	$⊢ (((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \land ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \land (S \subseteq ⋃ n \land T \subseteq ⋃ s))) \to X \subseteq ⋃ (n \cup s)$
70		elpwi	$⊢ c \in 𝒫 J \to c \subseteq J$
71	70	adantr	$⊢ (c \in 𝒫 J \land X = ⋃ c) \to c \subseteq J$
72	71	ad2antlr	$⊢ (((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \land ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \land (S \subseteq ⋃ n \land T \subseteq ⋃ s))) \to c \subseteq J$
73	47 72	sstrd	$⊢ (((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \land ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \land (S \subseteq ⋃ n \land T \subseteq ⋃ s))) \to n \cup s \subseteq J$
74		uniss	$⊢ n \cup s \subseteq J \to ⋃ (n \cup s) \subseteq ⋃ J$
75	74 1	sseqtrrdi	$⊢ n \cup s \subseteq J \to ⋃ (n \cup s) \subseteq X$
76	73 75	syl	$⊢ (((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \land ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \land (S \subseteq ⋃ n \land T \subseteq ⋃ s))) \to ⋃ (n \cup s) \subseteq X$
77	69 76	eqssd	$⊢ (((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \land ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \land (S \subseteq ⋃ n \land T \subseteq ⋃ s))) \to X = ⋃ (n \cup s)$
78		unieq	$⊢ d = n \cup s \to ⋃ d = ⋃ (n \cup s)$
79	78	rspceeqv	$⊢ (n \cup s \in (𝒫 c \cap Fin) \land X = ⋃ (n \cup s)) \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d$
80	59 77 79	syl2anc	$⊢ (((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \land ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \land (S \subseteq ⋃ n \land T \subseteq ⋃ s))) \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d$
81	80	exp32	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to ((n \in (𝒫 c \cap Fin) \land s \in (𝒫 c \cap Fin)) \to ((S \subseteq ⋃ n \land T \subseteq ⋃ s) \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d))$
82	81	rexlimdvv	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to (\exists n \in (𝒫 c \cap Fin) \exists s \in (𝒫 c \cap Fin) (S \subseteq ⋃ n \land T \subseteq ⋃ s) \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)$
83	39 82	syl5bir	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to ((\exists n \in (𝒫 c \cap Fin) S \subseteq ⋃ n \land \exists s \in (𝒫 c \cap Fin) T \subseteq ⋃ s) \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)$
84	21 38 83	syl2and	$⊢ ((J \in Top \land X = S \cup T) \land (c \in 𝒫 J \land X = ⋃ c)) \to ((J ↾_{𝑡} S \in Comp \land J ↾_{𝑡} T \in Comp) \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)$
85	84	impancom	$⊢ ((J \in Top \land X = S \cup T) \land (J ↾_{𝑡} S \in Comp \land J ↾_{𝑡} T \in Comp)) \to ((c \in 𝒫 J \land X = ⋃ c) \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)$
86	85	expd	$⊢ ((J \in Top \land X = S \cup T) \land (J ↾_{𝑡} S \in Comp \land J ↾_{𝑡} T \in Comp)) \to (c \in 𝒫 J \to (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d))$
87	86	ralrimiv	$⊢ ((J \in Top \land X = S \cup T) \land (J ↾_{𝑡} S \in Comp \land J ↾_{𝑡} T \in Comp)) \to \forall c \in 𝒫 J (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d)$
88	1	iscmp	$⊢ J \in Comp \leftrightarrow (J \in Top \land \forall c \in 𝒫 J (X = ⋃ c \to \exists d \in (𝒫 c \cap Fin) X = ⋃ d))$
89	2 87 88	sylanbrc	$⊢ ((J \in Top \land X = S \cup T) \land (J ↾_{𝑡} S \in Comp \land J ↾_{𝑡} T \in Comp)) \to J \in Comp$

Metamath Proof Explorer

Theorem uncmp

Proof