Theorem tgclt 7566

Description: Show that a basis generates a topology. Remark in [Munkres] p. 79.

Assertion

Ref	Expression
tgclt	|- (B e. Bases -> (topGen` B) e. Top)

Proof of Theorem tgclt

Step	Hyp	Ref	Expression
1		uniss 2511	. . . . . . . . 9 |- (u (_ (topGen` B) -> U.u (_ U.(topGen` B))
2	1	adantl 388	. . . . . . . 8 |- ((B e. Bases /\ u (_ (topGen` B)) -> U.u (_ U.(topGen` B))
3		unitgt 7565	. . . . . . . . 9 |- (B e. Bases -> U.(topGen` B) = U.B)
4	3	adantr 389	. . . . . . . 8 |- ((B e. Bases /\ u (_ (topGen` B)) -> U.(topGen` B) = U.B)
5	2, 4	sseqtrd 2087	. . . . . . 7 |- ((B e. Bases /\ u (_ (topGen` B)) -> U.u (_ U.B)
6		eltg2t 7561	. . . . . . . . . . . . . . . . . 18 |- (B e. Bases -> (t e. (topGen` B) <-> (t (_ U.B /\ A.x e. t E.y e. B (x e. y /\ y (_ t))))
7		pm3.27 323	. . . . . . . . . . . . . . . . . 18 |- ((t (_ U.B /\ A.x e. t E.y e. B (x e. y /\ y (_ t)) -> A.x e. t E.y e. B (x e. y /\ y (_ t))
8	6, 7	syl6bi 214	. . . . . . . . . . . . . . . . 17 |- (B e. Bases -> (t e. (topGen` B) -> A.x e. t E.y e. B (x e. y /\ y (_ t)))
9		ra4 1686	. . . . . . . . . . . . . . . . 17 |- (A.x e. t E.y e. B (x e. y /\ y (_ t) -> (x e. t -> E.y e. B (x e. y /\ y (_ t)))
10	8, 9	syl6 22	. . . . . . . . . . . . . . . 16 |- (B e. Bases -> (t e. (topGen` B) -> (x e. t -> E.y e. B (x e. y /\ y (_ t))))
11	10	imp31 362	. . . . . . . . . . . . . . 15 |- (((B e. Bases /\ t e. (topGen` B)) /\ x e. t) -> E.y e. B (x e. y /\ y (_ t))
12	11	an1rs 488	. . . . . . . . . . . . . 14 |- (((B e. Bases /\ x e. t) /\ t e. (topGen` B)) -> E.y e. B (x e. y /\ y (_ t))
13		ssel2 2054	. . . . . . . . . . . . . 14 |- ((u (_ (topGen` B) /\ t e. u) -> t e. (topGen` B))
14	12, 13	sylan2 451	. . . . . . . . . . . . 13 |- (((B e. Bases /\ x e. t) /\ (u (_ (topGen` B) /\ t e. u)) -> E.y e. B (x e. y /\ y (_ t))
15	14	an42s 508	. . . . . . . . . . . 12 |- (((B e. Bases /\ u (_ (topGen` B)) /\ (t e. u /\ x e. t)) -> E.y e. B (x e. y /\ y (_ t))
16		sstr2 2061	. . . . . . . . . . . . . . . 16 |- (y (_ t -> (t (_ U.u -> y (_ U.u))
17		elssuni 2516	. . . . . . . . . . . . . . . 16 |- (t e. u -> t (_ U.u)
18	16, 17	syl5com 52	. . . . . . . . . . . . . . 15 |- (t e. u -> (y (_ t -> y (_ U.u))
19	18	anim2d 559	. . . . . . . . . . . . . 14 |- (t e. u -> ((x e. y /\ y (_ t) -> (x e. y /\ y (_ U.u)))
20	19	r19.22sdv 1730	. . . . . . . . . . . . 13 |- (t e. u -> (E.y e. B (x e. y /\ y (_ t) -> E.y e. B (x e. y /\ y (_ U.u)))
21	20	ad2antrl 406	. . . . . . . . . . . 12 |- (((B e. Bases /\ u (_ (topGen` B)) /\ (t e. u /\ x e. t)) -> (E.y e. B (x e. y /\ y (_ t) -> E.y e. B (x e. y /\ y (_ U.u)))
22	15, 21	mpd 26	. . . . . . . . . . 11 |- (((B e. Bases /\ u (_ (topGen` B)) /\ (t e. u /\ x e. t)) -> E.y e. B (x e. y /\ y (_ U.u))
23	22	exp32 377	. . . . . . . . . 10 |- ((B e. Bases /\ u (_ (topGen` B)) -> (t e. u -> (x e. t -> E.y e. B (x e. y /\ y (_ U.u))))
24	23	r19.23adv 1738	. . . . . . . . 9 |- ((B e. Bases /\ u (_ (topGen` B)) -> (E.t e. u x e. t -> E.y e. B (x e. y /\ y (_ U.u)))
25		eluni2 2497	. . . . . . . . 9 |- (x e. U.u <-> E.t e. u x e. t)
26	24, 25	syl5ib 206	. . . . . . . 8 |- ((B e. Bases /\ u (_ (topGen` B)) -> (x e. U.u -> E.y e. B (x e. y /\ y (_ U.u)))
27	26	r19.21aiv 1705	. . . . . . 7 |- ((B e. Bases /\ u (_ (topGen` B)) -> A.x e. U.uE.y e. B (x e. y /\ y (_ U.u))
28	5, 27	jca 288	. . . . . 6 |- ((B e. Bases /\ u (_ (topGen` B)) -> (U.u (_ U.B /\ A.x e. U.uE.y e. B (x e. y /\ y (_ U.u)))
29	28	ex 373	. . . . 5 |- (B e. Bases -> (u (_ (topGen` B) -> (U.u (_ U.B /\ A.x e. U.uE.y e. B (x e. y /\ y (_ U.u))))
30		eltg2t 7561	. . . . 5 |- (B e. Bases -> (U.u e. (topGen` B) <-> (U.u (_ U.B /\ A.x e. U.uE.y e. B (x e. y /\ y (_ U.u))))
31	29, 30	sylibrd 204	. . . 4 |- (B e. Bases -> (u (_ (topGen` B) -> U.u e. (topGen` B)))
32	31	19.21aiv 1281	. . 3 |- (B e. Bases -> A.u(u (_ (topGen` B) -> U.u e. (topGen` B)))
33		tg1t 7562	. . . . . . . . 9 |- ((B e. Bases /\ u e. (topGen` B)) -> u (_ U.B)
34		ssinss1 2227	. . . . . . . . 9 |- (u (_ U.B -> (u i^i v) (_ U.B)
35	33, 34	syl 10	. . . . . . . 8 |- ((B e. Bases /\ u e. (topGen` B)) -> (u i^i v) (_ U.B)
36	35	adantrr 395	. . . . . . 7 |- ((B e. Bases /\ (u e. (topGen` B) /\ v e. (topGen` B))) -> (u i^i v) (_ U.B)
37		eltg2t 7561	. . . . . . . . . . . . . 14 |- (B e. Bases -> (u e. (topGen` B) <-> (u (_ U.B /\ A.x e. u E.z e. B (x e. z /\ z (_ u))))
38	37	pm3.27bda 421	. . . . . . . . . . . . 13 |- ((B e. Bases /\ u e. (topGen` B)) -> A.x e. u E.z e. B (x e. z /\ z (_ u))
39		ra4 1686	. . . . . . . . . . . . 13 |- (A.x e. u E.z e. B (x e. z /\ z (_ u) -> (x e. u -> E.z e. B (x e. z /\ z (_ u)))
40	38, 39	syl 10	. . . . . . . . . . . 12 |- ((B e. Bases /\ u e. (topGen` B)) -> (x e. u -> E.z e. B (x e. z /\ z (_ u)))
41		eltg2t 7561	. . . . . . . . . . . . . 14 |- (B e. Bases -> (v e. (topGen` B) <-> (v (_ U.B /\ A.x e. v E.w e. B (x e. w /\ w (_ v))))
42	41	pm3.27bda 421	. . . . . . . . . . . . 13 |- ((B e. Bases /\ v e. (topGen` B)) -> A.x e. v E.w e. B (x e. w /\ w (_ v))
43		ra4 1686	. . . . . . . . . . . . 13 |- (A.x e. v E.w e. B (x e. w /\ w (_ v) -> (x e. v -> E.w e. B (x e. w /\ w (_ v)))
44	42, 43	syl 10	. . . . . . . . . . . 12 |- ((B e. Bases /\ v e. (topGen` B)) -> (x e. v -> E.w e. B (x e. w /\ w (_ v)))
45	40, 44	im2anan9 561	. . . . . . . . . . 11 |- (((B e. Bases /\ u e. (topGen` B)) /\ (B e. Bases /\ v e. (topGen` B))) -> ((x e. u /\ x e. v) -> (E.z e. B (x e. z /\ z (_ u) /\ E.w e. B (x e. w /\ w (_ v))))
46		elin 2197	. . . . . . . . . . 11 |- (x e. (u i^i v) <-> (x e. u /\ x e. v))
47		reeanv 1770	. . . . . . . . . . 11 |- (E.z e. B E.w e. B ((x e. z /\ z (_ u) /\ (x e. w /\ w (_ v)) <-> (E.z e. B (x e. z /\ z (_ u) /\ E.w e. B (x e. w /\ w (_ v)))
48	45, 46, 47	3imtr4g 551	. . . . . . . . . 10 |- (((B e. Bases /\ u e. (topGen` B)) /\ (B e. Bases /\ v e. (topGen` B))) -> (x e. (u i^i v) -> E.z e. B E.w e. B ((x e. z /\ z (_ u) /\ (x e. w /\ w (_ v))))
49	48	anandis 511	. . . . . . . . 9 |- ((B e. Bases /\ (u e. (topGen` B) /\ v e. (topGen` B))) -> (x e. (u i^i v) -> E.z e. B E.w e. B ((x e. z /\ z (_ u) /\ (x e. w /\ w (_ v))))
50		basis2t 7557	. . . . . . . . . . . . . . . . . . 19 |- (((B e. Bases /\ z e. B) /\ (w e. B /\ x e. (z i^i w))) -> E.t e. B (x e. t /\ t (_ (z i^i w)))
51	50	adantllr 397	. . . . . . . . . . . . . . . . . 18 |- ((((B e. Bases /\ x e. (u i^i v)) /\ z e. B) /\ (w e. B /\ x e. (z i^i w))) -> E.t e. B (x e. t /\ t (_ (z i^i w)))
52	51	adantrrr 403	. . . . . . . . . . . . . . . . 17 |- ((((B e. Bases /\ x e. (u i^i v)) /\ z e. B) /\ (w e. B /\ (x e. (z i^i w) /\ (z i^i w) (_ (u i^i v)))) -> E.t e. B (x e. t /\ t (_ (z i^i w)))
53		sstr2 2061	. . . . . . . . . . . . . . . . . . . . . 22 |- (t (_ (z i^i w) -> ((z i^i w) (_ (u i^i v) -> t (_ (u i^i v)))
54	53	com12 11	. . . . . . . . . . . . . . . . . . . . 21 |- ((z i^i w) (_ (u i^i v) -> (t (_ (z i^i w) -> t (_ (u i^i v)))
55	54	anim2d 559	. . . . . . . . . . . . . . . . . . . 20 |- ((z i^i w) (_ (u i^i v) -> ((x e. t /\ t (_ (z i^i w)) -> (x e. t /\ t (_ (u i^i v))))
56	55	r19.22sdv 1730	. . . . . . . . . . . . . . . . . . 19 |- ((z i^i w) (_ (u i^i v) -> (E.t e. B (x e. t /\ t (_ (z i^i w)) -> E.t e. B (x e. t /\ t (_