txtube

Description: The "tube lemma". If X is compact and there is an open set U containing the line X X. { A } , then there is a "tube" X X. u for some neighborhood u of A which is entirely contained within U . (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Hypotheses	txtube.x	$⊢ X = ⋃ R$
	txtube.y	$⊢ Y = ⋃ S$
	txtube.r	$⊢ φ \to R \in Comp$
	txtube.s	$⊢ φ \to S \in Top$
	txtube.w	$⊢ φ \to U \in (R \times_{t} S)$
	txtube.u	$⊢ φ \to X \times \{A\} \subseteq U$
	txtube.a	$⊢ φ \to A \in Y$
Assertion	txtube	$⊢ φ \to \exists u \in S (A \in u \land X \times u \subseteq U)$

Proof

Step	Hyp	Ref	Expression
1		txtube.x	$⊢ X = ⋃ R$
2		txtube.y	$⊢ Y = ⋃ S$
3		txtube.r	$⊢ φ \to R \in Comp$
4		txtube.s	$⊢ φ \to S \in Top$
5		txtube.w	$⊢ φ \to U \in (R \times_{t} S)$
6		txtube.u	$⊢ φ \to X \times \{A\} \subseteq U$
7		txtube.a	$⊢ φ \to A \in Y$
8		eleq1	$⊢ y = ⟨x, A⟩ \to (y \in (u \times v) \leftrightarrow ⟨x, A⟩ \in (u \times v))$
9	8	anbi1d	$⊢ y = ⟨x, A⟩ \to ((y \in (u \times v) \land u \times v \subseteq U) \leftrightarrow (⟨x, A⟩ \in (u \times v) \land u \times v \subseteq U))$
10	9	2rexbidv	$⊢ y = ⟨x, A⟩ \to (\exists u \in R \exists v \in S (y \in (u \times v) \land u \times v \subseteq U) \leftrightarrow \exists u \in R \exists v \in S (⟨x, A⟩ \in (u \times v) \land u \times v \subseteq U))$
11		eltx	$⊢ (R \in Comp \land S \in Top) \to (U \in (R \times_{t} S) \leftrightarrow \forall y \in U \exists u \in R \exists v \in S (y \in (u \times v) \land u \times v \subseteq U))$
12	3 4 11	syl2anc	$⊢ φ \to (U \in (R \times_{t} S) \leftrightarrow \forall y \in U \exists u \in R \exists v \in S (y \in (u \times v) \land u \times v \subseteq U))$
13	5 12	mpbid	$⊢ φ \to \forall y \in U \exists u \in R \exists v \in S (y \in (u \times v) \land u \times v \subseteq U)$
14	13	adantr	$⊢ (φ \land x \in X) \to \forall y \in U \exists u \in R \exists v \in S (y \in (u \times v) \land u \times v \subseteq U)$
15	6	adantr	$⊢ (φ \land x \in X) \to X \times \{A\} \subseteq U$
16		id	$⊢ x \in X \to x \in X$
17		snidg	$⊢ A \in Y \to A \in \{A\}$
18	7 17	syl	$⊢ φ \to A \in \{A\}$
19		opelxpi	$⊢ (x \in X \land A \in \{A\}) \to ⟨x, A⟩ \in (X \times \{A\})$
20	16 18 19	syl2anr	$⊢ (φ \land x \in X) \to ⟨x, A⟩ \in (X \times \{A\})$
21	15 20	sseldd	$⊢ (φ \land x \in X) \to ⟨x, A⟩ \in U$
22	10 14 21	rspcdva	$⊢ (φ \land x \in X) \to \exists u \in R \exists v \in S (⟨x, A⟩ \in (u \times v) \land u \times v \subseteq U)$
23		opelxp	$⊢ ⟨x, A⟩ \in (u \times v) \leftrightarrow (x \in u \land A \in v)$
24	23	anbi1i	$⊢ (⟨x, A⟩ \in (u \times v) \land u \times v \subseteq U) \leftrightarrow ((x \in u \land A \in v) \land u \times v \subseteq U)$
25		anass	$⊢ ((x \in u \land A \in v) \land u \times v \subseteq U) \leftrightarrow (x \in u \land (A \in v \land u \times v \subseteq U))$
26	24 25	bitri	$⊢ (⟨x, A⟩ \in (u \times v) \land u \times v \subseteq U) \leftrightarrow (x \in u \land (A \in v \land u \times v \subseteq U))$
27	26	rexbii	$⊢ \exists v \in S (⟨x, A⟩ \in (u \times v) \land u \times v \subseteq U) \leftrightarrow \exists v \in S (x \in u \land (A \in v \land u \times v \subseteq U))$
28		r19.42v	$⊢ \exists v \in S (x \in u \land (A \in v \land u \times v \subseteq U)) \leftrightarrow (x \in u \land \exists v \in S (A \in v \land u \times v \subseteq U))$
29	27 28	bitri	$⊢ \exists v \in S (⟨x, A⟩ \in (u \times v) \land u \times v \subseteq U) \leftrightarrow (x \in u \land \exists v \in S (A \in v \land u \times v \subseteq U))$
30	29	rexbii	$⊢ \exists u \in R \exists v \in S (⟨x, A⟩ \in (u \times v) \land u \times v \subseteq U) \leftrightarrow \exists u \in R (x \in u \land \exists v \in S (A \in v \land u \times v \subseteq U))$
31	22 30	sylib	$⊢ (φ \land x \in X) \to \exists u \in R (x \in u \land \exists v \in S (A \in v \land u \times v \subseteq U))$
32	31	ralrimiva	$⊢ φ \to \forall x \in X \exists u \in R (x \in u \land \exists v \in S (A \in v \land u \times v \subseteq U))$
33		eleq2	$⊢ v = f (u) \to (A \in v \leftrightarrow A \in f (u))$
34		xpeq2	$⊢ v = f (u) \to u \times v = u \times f (u)$
35	34	sseq1d	$⊢ v = f (u) \to (u \times v \subseteq U \leftrightarrow u \times f (u) \subseteq U)$
36	33 35	anbi12d	$⊢ v = f (u) \to ((A \in v \land u \times v \subseteq U) \leftrightarrow (A \in f (u) \land u \times f (u) \subseteq U))$
37	1 36	cmpcovf	$⊢ (R \in Comp \land \forall x \in X \exists u \in R (x \in u \land \exists v \in S (A \in v \land u \times v \subseteq U))) \to \exists t \in (𝒫 R \cap Fin) (X = ⋃ t \land \exists f (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))$
38	3 32 37	syl2anc	$⊢ φ \to \exists t \in (𝒫 R \cap Fin) (X = ⋃ t \land \exists f (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))$
39		rint0	$⊢ ran f = \emptyset \to Y \cap ⋂ ran f = Y$
40	39	adantl	$⊢ (((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \land ran f = \emptyset) \to Y \cap ⋂ ran f = Y$
41	2	topopn	$⊢ S \in Top \to Y \in S$
42	4 41	syl	$⊢ φ \to Y \in S$
43	42	ad3antrrr	$⊢ (((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \land ran f = \emptyset) \to Y \in S$
44	40 43	eqeltrd	$⊢ (((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \land ran f = \emptyset) \to Y \cap ⋂ ran f \in S$
45	4	ad3antrrr	$⊢ (((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \land ran f \neq \emptyset) \to S \in Top$
46		simprrl	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to f : t ⟶ S$
47	46	frnd	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to ran f \subseteq S$
48	47	adantr	$⊢ (((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \land ran f \neq \emptyset) \to ran f \subseteq S$
49		simpr	$⊢ (((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \land ran f \neq \emptyset) \to ran f \neq \emptyset$
50		simplr	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to t \in (𝒫 R \cap Fin)$
51	50	elin2d	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to t \in Fin$
52	46	ffnd	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to f Fn t$
53		dffn4	$⊢ f Fn t \leftrightarrow f : t \underset{onto}{⟶} ran f$
54	52 53	sylib	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to f : t \underset{onto}{⟶} ran f$
55		fofi	$⊢ (t \in Fin \land f : t \underset{onto}{⟶} ran f) \to ran f \in Fin$
56	51 54 55	syl2anc	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to ran f \in Fin$
57	56	adantr	$⊢ (((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \land ran f \neq \emptyset) \to ran f \in Fin$
58		fiinopn	$⊢ S \in Top \to ((ran f \subseteq S \land ran f \neq \emptyset \land ran f \in Fin) \to ⋂ ran f \in S)$
59	58	imp	$⊢ (S \in Top \land (ran f \subseteq S \land ran f \neq \emptyset \land ran f \in Fin)) \to ⋂ ran f \in S$
60	45 48 49 57 59	syl13anc	$⊢ (((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \land ran f \neq \emptyset) \to ⋂ ran f \in S$
61		elssuni	$⊢ ⋂ ran f \in S \to ⋂ ran f \subseteq ⋃ S$
62	60 61	syl	$⊢ (((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \land ran f \neq \emptyset) \to ⋂ ran f \subseteq ⋃ S$
63	62 2	sseqtrrdi	$⊢ (((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \land ran f \neq \emptyset) \to ⋂ ran f \subseteq Y$
64		sseqin2	$⊢ ⋂ ran f \subseteq Y \leftrightarrow Y \cap ⋂ ran f = ⋂ ran f$
65	63 64	sylib	$⊢ (((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \land ran f \neq \emptyset) \to Y \cap ⋂ ran f = ⋂ ran f$
66	65 60	eqeltrd	$⊢ (((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \land ran f \neq \emptyset) \to Y \cap ⋂ ran f \in S$
67	44 66	pm2.61dane	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to Y \cap ⋂ ran f \in S$
68	7	ad2antrr	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to A \in Y$
69		simprrr	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)$
70		simpl	$⊢ (A \in f (u) \land u \times f (u) \subseteq U) \to A \in f (u)$
71	70	ralimi	$⊢ \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U) \to \forall u \in t A \in f (u)$
72	69 71	syl	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to \forall u \in t A \in f (u)$
73		eliin	$⊢ A \in Y \to (A \in ⋂_{u \in t} f (u) \leftrightarrow \forall u \in t A \in f (u))$
74	68 73	syl	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to (A \in ⋂_{u \in t} f (u) \leftrightarrow \forall u \in t A \in f (u))$
75	72 74	mpbird	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to A \in ⋂_{u \in t} f (u)$
76		fniinfv	$⊢ f Fn t \to ⋂_{u \in t} f (u) = ⋂ ran f$
77	52 76	syl	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to ⋂_{u \in t} f (u) = ⋂ ran f$
78	75 77	eleqtrd	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to A \in ⋂ ran f$
79	68 78	elind	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to A \in (Y \cap ⋂ ran f)$
80		simprl	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to X = ⋃ t$
81		uniiun	$⊢ ⋃ t = ⋃_{u \in t} u$
82	80 81	eqtrdi	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to X = ⋃_{u \in t} u$
83	82	xpeq1d	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to X \times (Y \cap ⋂ ran f) = ⋃_{u \in t} u \times (Y \cap ⋂ ran f)$
84		xpiundir	$⊢ ⋃_{u \in t} u \times (Y \cap ⋂ ran f) = ⋃_{u \in t} (u \times (Y \cap ⋂ ran f))$
85	83 84	eqtrdi	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to X \times (Y \cap ⋂ ran f) = ⋃_{u \in t} (u \times (Y \cap ⋂ ran f))$
86		simpr	$⊢ (A \in f (u) \land u \times f (u) \subseteq U) \to u \times f (u) \subseteq U$
87	86	ralimi	$⊢ \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U) \to \forall u \in t u \times f (u) \subseteq U$
88	69 87	syl	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to \forall u \in t u \times f (u) \subseteq U$
89		inss2	$⊢ Y \cap ⋂ ran f \subseteq ⋂ ran f$
90	76	adantr	$⊢ (f Fn t \land u \in t) \to ⋂_{u \in t} f (u) = ⋂ ran f$
91		iinss2	$⊢ u \in t \to ⋂_{u \in t} f (u) \subseteq f (u)$
92	91	adantl	$⊢ (f Fn t \land u \in t) \to ⋂_{u \in t} f (u) \subseteq f (u)$
93	90 92	eqsstrrd	$⊢ (f Fn t \land u \in t) \to ⋂ ran f \subseteq f (u)$
94	89 93	sstrid	$⊢ (f Fn t \land u \in t) \to Y \cap ⋂ ran f \subseteq f (u)$
95		xpss2	$⊢ Y \cap ⋂ ran f \subseteq f (u) \to u \times (Y \cap ⋂ ran f) \subseteq u \times f (u)$
96		sstr2	$⊢ u \times (Y \cap ⋂ ran f) \subseteq u \times f (u) \to (u \times f (u) \subseteq U \to u \times (Y \cap ⋂ ran f) \subseteq U)$
97	94 95 96	3syl	$⊢ (f Fn t \land u \in t) \to (u \times f (u) \subseteq U \to u \times (Y \cap ⋂ ran f) \subseteq U)$
98	97	ralimdva	$⊢ f Fn t \to (\forall u \in t u \times f (u) \subseteq U \to \forall u \in t u \times (Y \cap ⋂ ran f) \subseteq U)$
99	52 88 98	sylc	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to \forall u \in t u \times (Y \cap ⋂ ran f) \subseteq U$
100		iunss	$⊢ ⋃_{u \in t} (u \times (Y \cap ⋂ ran f)) \subseteq U \leftrightarrow \forall u \in t u \times (Y \cap ⋂ ran f) \subseteq U$
101	99 100	sylibr	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to ⋃_{u \in t} (u \times (Y \cap ⋂ ran f)) \subseteq U$
102	85 101	eqsstrd	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to X \times (Y \cap ⋂ ran f) \subseteq U$
103		eleq2	$⊢ u = Y \cap ⋂ ran f \to (A \in u \leftrightarrow A \in (Y \cap ⋂ ran f))$
104		xpeq2	$⊢ u = Y \cap ⋂ ran f \to X \times u = X \times (Y \cap ⋂ ran f)$
105	104	sseq1d	$⊢ u = Y \cap ⋂ ran f \to (X \times u \subseteq U \leftrightarrow X \times (Y \cap ⋂ ran f) \subseteq U)$
106	103 105	anbi12d	$⊢ u = Y \cap ⋂ ran f \to ((A \in u \land X \times u \subseteq U) \leftrightarrow (A \in (Y \cap ⋂ ran f) \land X \times (Y \cap ⋂ ran f) \subseteq U))$
107	106	rspcev	$⊢ (Y \cap ⋂ ran f \in S \land (A \in (Y \cap ⋂ ran f) \land X \times (Y \cap ⋂ ran f) \subseteq U)) \to \exists u \in S (A \in u \land X \times u \subseteq U)$
108	67 79 102 107	syl12anc	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land (X = ⋃ t \land (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)))) \to \exists u \in S (A \in u \land X \times u \subseteq U)$
109	108	expr	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land X = ⋃ t) \to ((f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)) \to \exists u \in S (A \in u \land X \times u \subseteq U))$
110	109	exlimdv	$⊢ ((φ \land t \in (𝒫 R \cap Fin)) \land X = ⋃ t) \to (\exists f (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U)) \to \exists u \in S (A \in u \land X \times u \subseteq U))$
111	110	expimpd	$⊢ (φ \land t \in (𝒫 R \cap Fin)) \to ((X = ⋃ t \land \exists f (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U))) \to \exists u \in S (A \in u \land X \times u \subseteq U))$
112	111	rexlimdva	$⊢ φ \to (\exists t \in (𝒫 R \cap Fin) (X = ⋃ t \land \exists f (f : t ⟶ S \land \forall u \in t (A \in f (u) \land u \times f (u) \subseteq U))) \to \exists u \in S (A \in u \land X \times u \subseteq U))$
113	38 112	mpd	$⊢ φ \to \exists u \in S (A \in u \land X \times u \subseteq U)$

Metamath Proof Explorer

Theorem txtube

Proof