tgcl

Description: Show that a basis generates a topology. Remark in Munkres p. 79. (Contributed by NM, 17-Jul-2006)

		Ref	Expression
	Assertion	tgcl	$⊢ B \in TopBases \to topGen (B) \in Top$

Proof

Step	Hyp	Ref	Expression
1		uniss	$⊢ u \subseteq topGen (B) \to ⋃ u \subseteq ⋃ topGen (B)$
2	1	adantl	$⊢ (B \in TopBases \land u \subseteq topGen (B)) \to ⋃ u \subseteq ⋃ topGen (B)$
3		unitg	$⊢ B \in TopBases \to ⋃ topGen (B) = ⋃ B$
4	3	adantr	$⊢ (B \in TopBases \land u \subseteq topGen (B)) \to ⋃ topGen (B) = ⋃ B$
5	2 4	sseqtrd	$⊢ (B \in TopBases \land u \subseteq topGen (B)) \to ⋃ u \subseteq ⋃ B$
6		eluni2	$⊢ x \in ⋃ u \leftrightarrow \exists t \in u x \in t$
7		ssel2	$⊢ (u \subseteq topGen (B) \land t \in u) \to t \in topGen (B)$
8		eltg2b	$⊢ B \in TopBases \to (t \in topGen (B) \leftrightarrow \forall x \in t \exists y \in B (x \in y \land y \subseteq t))$
9		rsp	$⊢ \forall x \in t \exists y \in B (x \in y \land y \subseteq t) \to (x \in t \to \exists y \in B (x \in y \land y \subseteq t))$
10	8 9	biimtrdi	$⊢ B \in TopBases \to (t \in topGen (B) \to (x \in t \to \exists y \in B (x \in y \land y \subseteq t)))$
11	10	imp31	$⊢ ((B \in TopBases \land t \in topGen (B)) \land x \in t) \to \exists y \in B (x \in y \land y \subseteq t)$
12	11	an32s	$⊢ ((B \in TopBases \land x \in t) \land t \in topGen (B)) \to \exists y \in B (x \in y \land y \subseteq t)$
13	7 12	sylan2	$⊢ ((B \in TopBases \land x \in t) \land (u \subseteq topGen (B) \land t \in u)) \to \exists y \in B (x \in y \land y \subseteq t)$
14	13	an42s	$⊢ ((B \in TopBases \land u \subseteq topGen (B)) \land (t \in u \land x \in t)) \to \exists y \in B (x \in y \land y \subseteq t)$
15		elssuni	$⊢ t \in u \to t \subseteq ⋃ u$
16		sstr2	$⊢ y \subseteq t \to (t \subseteq ⋃ u \to y \subseteq ⋃ u)$
17	15 16	syl5com	$⊢ t \in u \to (y \subseteq t \to y \subseteq ⋃ u)$
18	17	anim2d	$⊢ t \in u \to ((x \in y \land y \subseteq t) \to (x \in y \land y \subseteq ⋃ u))$
19	18	reximdv	$⊢ t \in u \to (\exists y \in B (x \in y \land y \subseteq t) \to \exists y \in B (x \in y \land y \subseteq ⋃ u))$
20	19	ad2antrl	$⊢ ((B \in TopBases \land u \subseteq topGen (B)) \land (t \in u \land x \in t)) \to (\exists y \in B (x \in y \land y \subseteq t) \to \exists y \in B (x \in y \land y \subseteq ⋃ u))$
21	14 20	mpd	$⊢ ((B \in TopBases \land u \subseteq topGen (B)) \land (t \in u \land x \in t)) \to \exists y \in B (x \in y \land y \subseteq ⋃ u)$
22	21	rexlimdvaa	$⊢ (B \in TopBases \land u \subseteq topGen (B)) \to (\exists t \in u x \in t \to \exists y \in B (x \in y \land y \subseteq ⋃ u))$
23	6 22	biimtrid	$⊢ (B \in TopBases \land u \subseteq topGen (B)) \to (x \in ⋃ u \to \exists y \in B (x \in y \land y \subseteq ⋃ u))$
24	23	ralrimiv	$⊢ (B \in TopBases \land u \subseteq topGen (B)) \to \forall x \in ⋃ u \exists y \in B (x \in y \land y \subseteq ⋃ u)$
25	5 24	jca	$⊢ (B \in TopBases \land u \subseteq topGen (B)) \to (⋃ u \subseteq ⋃ B \land \forall x \in ⋃ u \exists y \in B (x \in y \land y \subseteq ⋃ u))$
26	25	ex	$⊢ B \in TopBases \to (u \subseteq topGen (B) \to (⋃ u \subseteq ⋃ B \land \forall x \in ⋃ u \exists y \in B (x \in y \land y \subseteq ⋃ u)))$
27		eltg2	$⊢ B \in TopBases \to (⋃ u \in topGen (B) \leftrightarrow (⋃ u \subseteq ⋃ B \land \forall x \in ⋃ u \exists y \in B (x \in y \land y \subseteq ⋃ u)))$
28	26 27	sylibrd	$⊢ B \in TopBases \to (u \subseteq topGen (B) \to ⋃ u \in topGen (B))$
29	28	alrimiv	$⊢ B \in TopBases \to \forall u (u \subseteq topGen (B) \to ⋃ u \in topGen (B))$
30		inss1	$⊢ u \cap v \subseteq u$
31		tg1	$⊢ u \in topGen (B) \to u \subseteq ⋃ B$
32	30 31	sstrid	$⊢ u \in topGen (B) \to u \cap v \subseteq ⋃ B$
33	32	ad2antrl	$⊢ (B \in TopBases \land (u \in topGen (B) \land v \in topGen (B))) \to u \cap v \subseteq ⋃ B$
34		eltg2	$⊢ B \in TopBases \to (u \in topGen (B) \leftrightarrow (u \subseteq ⋃ B \land \forall x \in u \exists z \in B (x \in z \land z \subseteq u)))$
35	34	simplbda	$⊢ (B \in TopBases \land u \in topGen (B)) \to \forall x \in u \exists z \in B (x \in z \land z \subseteq u)$
36		rsp	$⊢ \forall x \in u \exists z \in B (x \in z \land z \subseteq u) \to (x \in u \to \exists z \in B (x \in z \land z \subseteq u))$
37	35 36	syl	$⊢ (B \in TopBases \land u \in topGen (B)) \to (x \in u \to \exists z \in B (x \in z \land z \subseteq u))$
38		eltg2	$⊢ B \in TopBases \to (v \in topGen (B) \leftrightarrow (v \subseteq ⋃ B \land \forall x \in v \exists w \in B (x \in w \land w \subseteq v)))$
39	38	simplbda	$⊢ (B \in TopBases \land v \in topGen (B)) \to \forall x \in v \exists w \in B (x \in w \land w \subseteq v)$
40		rsp	$⊢ \forall x \in v \exists w \in B (x \in w \land w \subseteq v) \to (x \in v \to \exists w \in B (x \in w \land w \subseteq v))$
41	39 40	syl	$⊢ (B \in TopBases \land v \in topGen (B)) \to (x \in v \to \exists w \in B (x \in w \land w \subseteq v))$
42	37 41	im2anan9	$⊢ ((B \in TopBases \land u \in topGen (B)) \land (B \in TopBases \land v \in topGen (B))) \to ((x \in u \land x \in v) \to (\exists z \in B (x \in z \land z \subseteq u) \land \exists w \in B (x \in w \land w \subseteq v)))$
43		elin	$⊢ x \in (u \cap v) \leftrightarrow (x \in u \land x \in v)$
44		reeanv	$⊢ \exists z \in B \exists w \in B ((x \in z \land z \subseteq u) \land (x \in w \land w \subseteq v)) \leftrightarrow (\exists z \in B (x \in z \land z \subseteq u) \land \exists w \in B (x \in w \land w \subseteq v))$
45	42 43 44	3imtr4g	$⊢ ((B \in TopBases \land u \in topGen (B)) \land (B \in TopBases \land v \in topGen (B))) \to (x \in (u \cap v) \to \exists z \in B \exists w \in B ((x \in z \land z \subseteq u) \land (x \in w \land w \subseteq v)))$
46	45	anandis	$⊢ (B \in TopBases \land (u \in topGen (B) \land v \in topGen (B))) \to (x \in (u \cap v) \to \exists z \in B \exists w \in B ((x \in z \land z \subseteq u) \land (x \in w \land w \subseteq v)))$
47		elin	$⊢ x \in (z \cap w) \leftrightarrow (x \in z \land x \in w)$
48	47	biimpri	$⊢ (x \in z \land x \in w) \to x \in (z \cap w)$
49		ss2in	$⊢ (z \subseteq u \land w \subseteq v) \to z \cap w \subseteq u \cap v$
50	48 49	anim12i	$⊢ ((x \in z \land x \in w) \land (z \subseteq u \land w \subseteq v)) \to (x \in (z \cap w) \land z \cap w \subseteq u \cap v)$
51	50	an4s	$⊢ ((x \in z \land z \subseteq u) \land (x \in w \land w \subseteq v)) \to (x \in (z \cap w) \land z \cap w \subseteq u \cap v)$
52		basis2	$⊢ ((B \in TopBases \land z \in B) \land (w \in B \land x \in (z \cap w))) \to \exists t \in B (x \in t \land t \subseteq z \cap w)$
53	52	adantllr	$⊢ (((B \in TopBases \land x \in (u \cap v)) \land z \in B) \land (w \in B \land x \in (z \cap w))) \to \exists t \in B (x \in t \land t \subseteq z \cap w)$
54	53	adantrrr	$⊢ (((B \in TopBases \land x \in (u \cap v)) \land z \in B) \land (w \in B \land (x \in (z \cap w) \land z \cap w \subseteq u \cap v))) \to \exists t \in B (x \in t \land t \subseteq z \cap w)$
55		sstr2	$⊢ t \subseteq z \cap w \to (z \cap w \subseteq u \cap v \to t \subseteq u \cap v)$
56	55	com12	$⊢ z \cap w \subseteq u \cap v \to (t \subseteq z \cap w \to t \subseteq u \cap v)$
57	56	anim2d	$⊢ z \cap w \subseteq u \cap v \to ((x \in t \land t \subseteq z \cap w) \to (x \in t \land t \subseteq u \cap v))$
58	57	reximdv	$⊢ z \cap w \subseteq u \cap v \to (\exists t \in B (x \in t \land t \subseteq z \cap w) \to \exists t \in B (x \in t \land t \subseteq u \cap v))$
59	58	adantl	$⊢ (x \in (z \cap w) \land z \cap w \subseteq u \cap v) \to (\exists t \in B (x \in t \land t \subseteq z \cap w) \to \exists t \in B (x \in t \land t \subseteq u \cap v))$
60	59	ad2antll	$⊢ (((B \in TopBases \land x \in (u \cap v)) \land z \in B) \land (w \in B \land (x \in (z \cap w) \land z \cap w \subseteq u \cap v))) \to (\exists t \in B (x \in t \land t \subseteq z \cap w) \to \exists t \in B (x \in t \land t \subseteq u \cap v))$
61	54 60	mpd	$⊢ (((B \in TopBases \land x \in (u \cap v)) \land z \in B) \land (w \in B \land (x \in (z \cap w) \land z \cap w \subseteq u \cap v))) \to \exists t \in B (x \in t \land t \subseteq u \cap v)$
62	51 61	sylanr2	$⊢ (((B \in TopBases \land x \in (u \cap v)) \land z \in B) \land (w \in B \land ((x \in z \land z \subseteq u) \land (x \in w \land w \subseteq v)))) \to \exists t \in B (x \in t \land t \subseteq u \cap v)$
63	62	rexlimdvaa	$⊢ ((B \in TopBases \land x \in (u \cap v)) \land z \in B) \to (\exists w \in B ((x \in z \land z \subseteq u) \land (x \in w \land w \subseteq v)) \to \exists t \in B (x \in t \land t \subseteq u \cap v))$
64	63	rexlimdva	$⊢ (B \in TopBases \land x \in (u \cap v)) \to (\exists z \in B \exists w \in B ((x \in z \land z \subseteq u) \land (x \in w \land w \subseteq v)) \to \exists t \in B (x \in t \land t \subseteq u \cap v))$
65	64	ex	$⊢ B \in TopBases \to (x \in (u \cap v) \to (\exists z \in B \exists w \in B ((x \in z \land z \subseteq u) \land (x \in w \land w \subseteq v)) \to \exists t \in B (x \in t \land t \subseteq u \cap v)))$
66	65	a2d	$⊢ B \in TopBases \to ((x \in (u \cap v) \to \exists z \in B \exists w \in B ((x \in z \land z \subseteq u) \land (x \in w \land w \subseteq v))) \to (x \in (u \cap v) \to \exists t \in B (x \in t \land t \subseteq u \cap v)))$
67	66	imp	$⊢ (B \in TopBases \land (x \in (u \cap v) \to \exists z \in B \exists w \in B ((x \in z \land z \subseteq u) \land (x \in w \land w \subseteq v)))) \to (x \in (u \cap v) \to \exists t \in B (x \in t \land t \subseteq u \cap v))$
68	46 67	syldan	$⊢ (B \in TopBases \land (u \in topGen (B) \land v \in topGen (B))) \to (x \in (u \cap v) \to \exists t \in B (x \in t \land t \subseteq u \cap v))$
69	68	ralrimiv	$⊢ (B \in TopBases \land (u \in topGen (B) \land v \in topGen (B))) \to \forall x \in (u \cap v) \exists t \in B (x \in t \land t \subseteq u \cap v)$
70	33 69	jca	$⊢ (B \in TopBases \land (u \in topGen (B) \land v \in topGen (B))) \to (u \cap v \subseteq ⋃ B \land \forall x \in (u \cap v) \exists t \in B (x \in t \land t \subseteq u \cap v))$
71	70	ex	$⊢ B \in TopBases \to ((u \in topGen (B) \land v \in topGen (B)) \to (u \cap v \subseteq ⋃ B \land \forall x \in (u \cap v) \exists t \in B (x \in t \land t \subseteq u \cap v)))$
72		eltg2	$⊢ B \in TopBases \to (u \cap v \in topGen (B) \leftrightarrow (u \cap v \subseteq ⋃ B \land \forall x \in (u \cap v) \exists t \in B (x \in t \land t \subseteq u \cap v)))$
73	71 72	sylibrd	$⊢ B \in TopBases \to ((u \in topGen (B) \land v \in topGen (B)) \to u \cap v \in topGen (B))$
74	73	ralrimivv	$⊢ B \in TopBases \to \forall u \in topGen (B) \forall v \in topGen (B) u \cap v \in topGen (B)$
75		fvex	$⊢ topGen (B) \in V$
76		istopg	$⊢ topGen (B) \in V \to (topGen (B) \in Top \leftrightarrow (\forall u (u \subseteq topGen (B) \to ⋃ u \in topGen (B)) \land \forall u \in topGen (B) \forall v \in topGen (B) u \cap v \in topGen (B)))$
77	75 76	ax-mp	$⊢ topGen (B) \in Top \leftrightarrow (\forall u (u \subseteq topGen (B) \to ⋃ u \in topGen (B)) \land \forall u \in topGen (B) \forall v \in topGen (B) u \cap v \in topGen (B))$
78	29 74 77	sylanbrc	$⊢ B \in TopBases \to topGen (B) \in Top$

Metamath Proof Explorer

Theorem tgcl

Proof