fiuncmp

Description: A finite union of compact sets is compact. (Contributed by Mario Carneiro, 19-Mar-2015)

		Ref	Expression
	Hypothesis	fiuncmp.1	$⊢ X = ⋃ J$
	Assertion	fiuncmp	$⊢ (J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to J ↾_{𝑡} ⋃_{x \in A} B \in Comp$

Proof

Step	Hyp	Ref	Expression
1		fiuncmp.1	$⊢ X = ⋃ J$
2		ssid	$⊢ A \subseteq A$
3		simp2	$⊢ (J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to A \in Fin$
4		sseq1	$⊢ t = \emptyset \to (t \subseteq A \leftrightarrow \emptyset \subseteq A)$
5		iuneq1	$⊢ t = \emptyset \to ⋃_{x \in t} B = ⋃_{x \in \emptyset} B$
6		0iun	$⊢ ⋃_{x \in \emptyset} B = \emptyset$
7	5 6	eqtrdi	$⊢ t = \emptyset \to ⋃_{x \in t} B = \emptyset$
8	7	oveq2d	$⊢ t = \emptyset \to J ↾_{𝑡} ⋃_{x \in t} B = J ↾_{𝑡} \emptyset$
9	8	eleq1d	$⊢ t = \emptyset \to (J ↾_{𝑡} ⋃_{x \in t} B \in Comp \leftrightarrow J ↾_{𝑡} \emptyset \in Comp)$
10	4 9	imbi12d	$⊢ t = \emptyset \to ((t \subseteq A \to J ↾_{𝑡} ⋃_{x \in t} B \in Comp) \leftrightarrow (\emptyset \subseteq A \to J ↾_{𝑡} \emptyset \in Comp))$
11	10	imbi2d	$⊢ t = \emptyset \to (((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (t \subseteq A \to J ↾_{𝑡} ⋃_{x \in t} B \in Comp)) \leftrightarrow ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (\emptyset \subseteq A \to J ↾_{𝑡} \emptyset \in Comp)))$
12		sseq1	$⊢ t = y \to (t \subseteq A \leftrightarrow y \subseteq A)$
13		iuneq1	$⊢ t = y \to ⋃_{x \in t} B = ⋃_{x \in y} B$
14	13	oveq2d	$⊢ t = y \to J ↾_{𝑡} ⋃_{x \in t} B = J ↾_{𝑡} ⋃_{x \in y} B$
15	14	eleq1d	$⊢ t = y \to (J ↾_{𝑡} ⋃_{x \in t} B \in Comp \leftrightarrow J ↾_{𝑡} ⋃_{x \in y} B \in Comp)$
16	12 15	imbi12d	$⊢ t = y \to ((t \subseteq A \to J ↾_{𝑡} ⋃_{x \in t} B \in Comp) \leftrightarrow (y \subseteq A \to J ↾_{𝑡} ⋃_{x \in y} B \in Comp))$
17	16	imbi2d	$⊢ t = y \to (((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (t \subseteq A \to J ↾_{𝑡} ⋃_{x \in t} B \in Comp)) \leftrightarrow ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (y \subseteq A \to J ↾_{𝑡} ⋃_{x \in y} B \in Comp)))$
18		sseq1	$⊢ t = y \cup \{z\} \to (t \subseteq A \leftrightarrow y \cup \{z\} \subseteq A)$
19		iuneq1	$⊢ t = y \cup \{z\} \to ⋃_{x \in t} B = ⋃_{x \in y \cup \{z\}} B$
20	19	oveq2d	$⊢ t = y \cup \{z\} \to J ↾_{𝑡} ⋃_{x \in t} B = J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B$
21	20	eleq1d	$⊢ t = y \cup \{z\} \to (J ↾_{𝑡} ⋃_{x \in t} B \in Comp \leftrightarrow J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B \in Comp)$
22	18 21	imbi12d	$⊢ t = y \cup \{z\} \to ((t \subseteq A \to J ↾_{𝑡} ⋃_{x \in t} B \in Comp) \leftrightarrow (y \cup \{z\} \subseteq A \to J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B \in Comp))$
23	22	imbi2d	$⊢ t = y \cup \{z\} \to (((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (t \subseteq A \to J ↾_{𝑡} ⋃_{x \in t} B \in Comp)) \leftrightarrow ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (y \cup \{z\} \subseteq A \to J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B \in Comp)))$
24		sseq1	$⊢ t = A \to (t \subseteq A \leftrightarrow A \subseteq A)$
25		iuneq1	$⊢ t = A \to ⋃_{x \in t} B = ⋃_{x \in A} B$
26	25	oveq2d	$⊢ t = A \to J ↾_{𝑡} ⋃_{x \in t} B = J ↾_{𝑡} ⋃_{x \in A} B$
27	26	eleq1d	$⊢ t = A \to (J ↾_{𝑡} ⋃_{x \in t} B \in Comp \leftrightarrow J ↾_{𝑡} ⋃_{x \in A} B \in Comp)$
28	24 27	imbi12d	$⊢ t = A \to ((t \subseteq A \to J ↾_{𝑡} ⋃_{x \in t} B \in Comp) \leftrightarrow (A \subseteq A \to J ↾_{𝑡} ⋃_{x \in A} B \in Comp))$
29	28	imbi2d	$⊢ t = A \to (((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (t \subseteq A \to J ↾_{𝑡} ⋃_{x \in t} B \in Comp)) \leftrightarrow ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (A \subseteq A \to J ↾_{𝑡} ⋃_{x \in A} B \in Comp)))$
30		rest0	$⊢ J \in Top \to J ↾_{𝑡} \emptyset = \{\emptyset\}$
31		0cmp	$⊢ \{\emptyset\} \in Comp$
32	30 31	eqeltrdi	$⊢ J \in Top \to J ↾_{𝑡} \emptyset \in Comp$
33	32	3ad2ant1	$⊢ (J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to J ↾_{𝑡} \emptyset \in Comp$
34	33	a1d	$⊢ (J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (\emptyset \subseteq A \to J ↾_{𝑡} \emptyset \in Comp)$
35		ssun1	$⊢ y \subseteq y \cup \{z\}$
36		id	$⊢ y \cup \{z\} \subseteq A \to y \cup \{z\} \subseteq A$
37	35 36	sstrid	$⊢ y \cup \{z\} \subseteq A \to y \subseteq A$
38	37	imim1i	$⊢ (y \subseteq A \to J ↾_{𝑡} ⋃_{x \in y} B \in Comp) \to (y \cup \{z\} \subseteq A \to J ↾_{𝑡} ⋃_{x \in y} B \in Comp)$
39		simpl1	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to J \in Top$
40		iunxun	$⊢ ⋃_{x \in y \cup \{z\}} B = ⋃_{x \in y} B \cup ⋃_{x \in \{z\}} B$
41		simprr	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to J ↾_{𝑡} ⋃_{x \in y} B \in Comp$
42		cmptop	$⊢ J ↾_{𝑡} ⋃_{x \in y} B \in Comp \to J ↾_{𝑡} ⋃_{x \in y} B \in Top$
43		restrcl	$⊢ J ↾_{𝑡} ⋃_{x \in y} B \in Top \to (J \in V \land ⋃_{x \in y} B \in V)$
44	43	simprd	$⊢ J ↾_{𝑡} ⋃_{x \in y} B \in Top \to ⋃_{x \in y} B \in V$
45	41 42 44	3syl	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to ⋃_{x \in y} B \in V$
46		nfcv	$⊢ \underline{Ⅎ} t B$
47		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ t / x ⦌ B$
48		csbeq1a	$⊢ x = t \to B = ⦋ t / x ⦌ B$
49	46 47 48	cbviun	$⊢ ⋃_{x \in \{z\}} B = ⋃_{t \in \{z\}} ⦋ t / x ⦌ B$
50		vex	$⊢ z \in V$
51		csbeq1	$⊢ t = z \to ⦋ t / x ⦌ B = ⦋ z / x ⦌ B$
52	50 51	iunxsn	$⊢ ⋃_{t \in \{z\}} ⦋ t / x ⦌ B = ⦋ z / x ⦌ B$
53	49 52	eqtri	$⊢ ⋃_{x \in \{z\}} B = ⦋ z / x ⦌ B$
54	51	oveq2d	$⊢ t = z \to J ↾_{𝑡} ⦋ t / x ⦌ B = J ↾_{𝑡} ⦋ z / x ⦌ B$
55	54	eleq1d	$⊢ t = z \to (J ↾_{𝑡} ⦋ t / x ⦌ B \in Comp \leftrightarrow J ↾_{𝑡} ⦋ z / x ⦌ B \in Comp)$
56		simpl3	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to \forall x \in A J ↾_{𝑡} B \in Comp$
57		nfv	$⊢ Ⅎ t J ↾_{𝑡} B \in Comp$
58		nfcv	$⊢ \underline{Ⅎ} x J$
59		nfcv	$⊢ \underline{Ⅎ} x ↾_{𝑡}$
60	58 59 47	nfov	$⊢ \underline{Ⅎ} x (J ↾_{𝑡} ⦋ t / x ⦌ B)$
61	60	nfel1	$⊢ Ⅎ x J ↾_{𝑡} ⦋ t / x ⦌ B \in Comp$
62	48	oveq2d	$⊢ x = t \to J ↾_{𝑡} B = J ↾_{𝑡} ⦋ t / x ⦌ B$
63	62	eleq1d	$⊢ x = t \to (J ↾_{𝑡} B \in Comp \leftrightarrow J ↾_{𝑡} ⦋ t / x ⦌ B \in Comp)$
64	57 61 63	cbvralw	$⊢ \forall x \in A J ↾_{𝑡} B \in Comp \leftrightarrow \forall t \in A J ↾_{𝑡} ⦋ t / x ⦌ B \in Comp$
65	56 64	sylib	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to \forall t \in A J ↾_{𝑡} ⦋ t / x ⦌ B \in Comp$
66		ssun2	$⊢ \{z\} \subseteq y \cup \{z\}$
67		simprl	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to y \cup \{z\} \subseteq A$
68	66 67	sstrid	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to \{z\} \subseteq A$
69	50	snss	$⊢ z \in A \leftrightarrow \{z\} \subseteq A$
70	68 69	sylibr	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to z \in A$
71	55 65 70	rspcdva	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to J ↾_{𝑡} ⦋ z / x ⦌ B \in Comp$
72		cmptop	$⊢ J ↾_{𝑡} ⦋ z / x ⦌ B \in Comp \to J ↾_{𝑡} ⦋ z / x ⦌ B \in Top$
73		restrcl	$⊢ J ↾_{𝑡} ⦋ z / x ⦌ B \in Top \to (J \in V \land ⦋ z / x ⦌ B \in V)$
74	73	simprd	$⊢ J ↾_{𝑡} ⦋ z / x ⦌ B \in Top \to ⦋ z / x ⦌ B \in V$
75	71 72 74	3syl	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to ⦋ z / x ⦌ B \in V$
76	53 75	eqeltrid	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to ⋃_{x \in \{z\}} B \in V$
77		unexg	$⊢ (⋃_{x \in y} B \in V \land ⋃_{x \in \{z\}} B \in V) \to ⋃_{x \in y} B \cup ⋃_{x \in \{z\}} B \in V$
78	45 76 77	syl2anc	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to ⋃_{x \in y} B \cup ⋃_{x \in \{z\}} B \in V$
79	40 78	eqeltrid	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to ⋃_{x \in y \cup \{z\}} B \in V$
80		resttop	$⊢ (J \in Top \land ⋃_{x \in y \cup \{z\}} B \in V) \to J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B \in Top$
81	39 79 80	syl2anc	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B \in Top$
82		eqid	$⊢ ⋃ J = ⋃ J$
83	82	restin	$⊢ (J \in Top \land ⋃_{x \in y \cup \{z\}} B \in V) \to J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B = J ↾_{𝑡} (⋃_{x \in y \cup \{z\}} B \cap ⋃ J)$
84	39 79 83	syl2anc	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B = J ↾_{𝑡} (⋃_{x \in y \cup \{z\}} B \cap ⋃ J)$
85	84	unieqd	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to ⋃ (J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B) = ⋃ (J ↾_{𝑡} (⋃_{x \in y \cup \{z\}} B \cap ⋃ J))$
86		inss2	$⊢ ⋃_{x \in y \cup \{z\}} B \cap ⋃ J \subseteq ⋃ J$
87	86 1	sseqtrri	$⊢ ⋃_{x \in y \cup \{z\}} B \cap ⋃ J \subseteq X$
88	1	restuni	$⊢ (J \in Top \land ⋃_{x \in y \cup \{z\}} B \cap ⋃ J \subseteq X) \to ⋃_{x \in y \cup \{z\}} B \cap ⋃ J = ⋃ (J ↾_{𝑡} (⋃_{x \in y \cup \{z\}} B \cap ⋃ J))$
89	39 87 88	sylancl	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to ⋃_{x \in y \cup \{z\}} B \cap ⋃ J = ⋃ (J ↾_{𝑡} (⋃_{x \in y \cup \{z\}} B \cap ⋃ J))$
90	85 89	eqtr4d	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to ⋃ (J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B) = ⋃_{x \in y \cup \{z\}} B \cap ⋃ J$
91	53	uneq2i	$⊢ ⋃_{x \in y} B \cup ⋃_{x \in \{z\}} B = ⋃_{x \in y} B \cup ⦋ z / x ⦌ B$
92	40 91	eqtri	$⊢ ⋃_{x \in y \cup \{z\}} B = ⋃_{x \in y} B \cup ⦋ z / x ⦌ B$
93	92	ineq1i	$⊢ ⋃_{x \in y \cup \{z\}} B \cap ⋃ J = (⋃_{x \in y} B \cup ⦋ z / x ⦌ B) \cap ⋃ J$
94		indir	$⊢ (⋃_{x \in y} B \cup ⦋ z / x ⦌ B) \cap ⋃ J = (⋃_{x \in y} B \cap ⋃ J) \cup (⦋ z / x ⦌ B \cap ⋃ J)$
95	93 94	eqtri	$⊢ ⋃_{x \in y \cup \{z\}} B \cap ⋃ J = (⋃_{x \in y} B \cap ⋃ J) \cup (⦋ z / x ⦌ B \cap ⋃ J)$
96	90 95	eqtrdi	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to ⋃ (J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B) = (⋃_{x \in y} B \cap ⋃ J) \cup (⦋ z / x ⦌ B \cap ⋃ J)$
97		inss1	$⊢ ⋃_{x \in y} B \cap ⋃ J \subseteq ⋃_{x \in y} B$
98		ssun1	$⊢ ⋃_{x \in y} B \subseteq ⋃_{x \in y} B \cup ⋃_{x \in \{z\}} B$
99	98 40	sseqtrri	$⊢ ⋃_{x \in y} B \subseteq ⋃_{x \in y \cup \{z\}} B$
100	97 99	sstri	$⊢ ⋃_{x \in y} B \cap ⋃ J \subseteq ⋃_{x \in y \cup \{z\}} B$
101	100	a1i	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to ⋃_{x \in y} B \cap ⋃ J \subseteq ⋃_{x \in y \cup \{z\}} B$
102		restabs	$⊢ (J \in Top \land ⋃_{x \in y} B \cap ⋃ J \subseteq ⋃_{x \in y \cup \{z\}} B \land ⋃_{x \in y \cup \{z\}} B \in V) \to (J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B) ↾_{𝑡} (⋃_{x \in y} B \cap ⋃ J) = J ↾_{𝑡} (⋃_{x \in y} B \cap ⋃ J)$
103	39 101 79 102	syl3anc	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to (J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B) ↾_{𝑡} (⋃_{x \in y} B \cap ⋃ J) = J ↾_{𝑡} (⋃_{x \in y} B \cap ⋃ J)$
104	82	restin	$⊢ (J \in Top \land ⋃_{x \in y} B \in V) \to J ↾_{𝑡} ⋃_{x \in y} B = J ↾_{𝑡} (⋃_{x \in y} B \cap ⋃ J)$
105	39 45 104	syl2anc	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to J ↾_{𝑡} ⋃_{x \in y} B = J ↾_{𝑡} (⋃_{x \in y} B \cap ⋃ J)$
106	103 105	eqtr4d	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to (J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B) ↾_{𝑡} (⋃_{x \in y} B \cap ⋃ J) = J ↾_{𝑡} ⋃_{x \in y} B$
107	106 41	eqeltrd	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to (J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B) ↾_{𝑡} (⋃_{x \in y} B \cap ⋃ J) \in Comp$
108		inss1	$⊢ ⦋ z / x ⦌ B \cap ⋃ J \subseteq ⦋ z / x ⦌ B$
109		ssun2	$⊢ ⋃_{x \in \{z\}} B \subseteq ⋃_{x \in y} B \cup ⋃_{x \in \{z\}} B$
110	109 40	sseqtrri	$⊢ ⋃_{x \in \{z\}} B \subseteq ⋃_{x \in y \cup \{z\}} B$
111	53 110	eqsstrri	$⊢ ⦋ z / x ⦌ B \subseteq ⋃_{x \in y \cup \{z\}} B$
112	108 111	sstri	$⊢ ⦋ z / x ⦌ B \cap ⋃ J \subseteq ⋃_{x \in y \cup \{z\}} B$
113	112	a1i	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to ⦋ z / x ⦌ B \cap ⋃ J \subseteq ⋃_{x \in y \cup \{z\}} B$
114		restabs	$⊢ (J \in Top \land ⦋ z / x ⦌ B \cap ⋃ J \subseteq ⋃_{x \in y \cup \{z\}} B \land ⋃_{x \in y \cup \{z\}} B \in V) \to (J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B) ↾_{𝑡} (⦋ z / x ⦌ B \cap ⋃ J) = J ↾_{𝑡} (⦋ z / x ⦌ B \cap ⋃ J)$
115	39 113 79 114	syl3anc	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to (J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B) ↾_{𝑡} (⦋ z / x ⦌ B \cap ⋃ J) = J ↾_{𝑡} (⦋ z / x ⦌ B \cap ⋃ J)$
116	82	restin	$⊢ (J \in Top \land ⦋ z / x ⦌ B \in V) \to J ↾_{𝑡} ⦋ z / x ⦌ B = J ↾_{𝑡} (⦋ z / x ⦌ B \cap ⋃ J)$
117	39 75 116	syl2anc	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to J ↾_{𝑡} ⦋ z / x ⦌ B = J ↾_{𝑡} (⦋ z / x ⦌ B \cap ⋃ J)$
118	115 117	eqtr4d	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to (J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B) ↾_{𝑡} (⦋ z / x ⦌ B \cap ⋃ J) = J ↾_{𝑡} ⦋ z / x ⦌ B$
119	118 71	eqeltrd	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to (J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B) ↾_{𝑡} (⦋ z / x ⦌ B \cap ⋃ J) \in Comp$
120		eqid	$⊢ ⋃ (J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B) = ⋃ (J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B)$
121	120	uncmp	$⊢ ((J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B \in Top \land ⋃ (J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B) = (⋃_{x \in y} B \cap ⋃ J) \cup (⦋ z / x ⦌ B \cap ⋃ J)) \land ((J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B) ↾_{𝑡} (⋃_{x \in y} B \cap ⋃ J) \in Comp \land (J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B) ↾_{𝑡} (⦋ z / x ⦌ B \cap ⋃ J) \in Comp)) \to J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B \in Comp$
122	81 96 107 119 121	syl22anc	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \land (y \cup \{z\} \subseteq A \land J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B \in Comp$
123	122	exp32	$⊢ (J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (y \cup \{z\} \subseteq A \to (J ↾_{𝑡} ⋃_{x \in y} B \in Comp \to J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B \in Comp))$
124	123	a2d	$⊢ (J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to ((y \cup \{z\} \subseteq A \to J ↾_{𝑡} ⋃_{x \in y} B \in Comp) \to (y \cup \{z\} \subseteq A \to J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B \in Comp))$
125	38 124	syl5	$⊢ (J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to ((y \subseteq A \to J ↾_{𝑡} ⋃_{x \in y} B \in Comp) \to (y \cup \{z\} \subseteq A \to J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B \in Comp))$
126	125	a2i	$⊢ ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (y \subseteq A \to J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (y \cup \{z\} \subseteq A \to J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B \in Comp))$
127	126	a1i	$⊢ y \in Fin \to (((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (y \subseteq A \to J ↾_{𝑡} ⋃_{x \in y} B \in Comp)) \to ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (y \cup \{z\} \subseteq A \to J ↾_{𝑡} ⋃_{x \in y \cup \{z\}} B \in Comp)))$
128	11 17 23 29 34 127	findcard2	$⊢ A \in Fin \to ((J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (A \subseteq A \to J ↾_{𝑡} ⋃_{x \in A} B \in Comp))$
129	3 128	mpcom	$⊢ (J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to (A \subseteq A \to J ↾_{𝑡} ⋃_{x \in A} B \in Comp)$
130	2 129	mpi	$⊢ (J \in Top \land A \in Fin \land \forall x \in A J ↾_{𝑡} B \in Comp) \to J ↾_{𝑡} ⋃_{x \in A} B \in Comp$

Metamath Proof Explorer

Theorem fiuncmp

Proof