Theorem tgcl 14929

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

Assertion

Ref	Expression
tgcl	|- ( B e. TopBases -> ( topGen ` B ) e. Top )

Proof of Theorem tgcl

Dummy variables x y z u t v w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		uniss 3935	. . . . . . . 8 |- ( u C_ ( topGen ` B ) -> U. u C_ U. ( topGen ` B ) )
2	1	adantl 277	. . . . . . 7 |- ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) -> U. u C_ U. ( topGen ` B ) )
3		unitg 14927	. . . . . . . 8 |- ( B e. TopBases -> U. ( topGen ` B ) = U. B )
4	3	adantr 276	. . . . . . 7 |- ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) -> U. ( topGen ` B ) = U. B )
5	2, 4	sseqtrd 3276	. . . . . 6 |- ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) -> U. u C_ U. B )
6		eluni2 3918	. . . . . . . 8 |- ( x e. U. u <-> E. t e. u x e. t )
7		ssel2 3233	. . . . . . . . . . . 12 |- ( ( u C_ ( topGen ` B ) /\ t e. u ) -> t e. ( topGen ` B ) )
8		eltg2b 14919	. . . . . . . . . . . . . . 15 |- ( B e. TopBases -> ( t e. ( topGen ` B ) <-> A. x e. t E. y e. B ( x e. y /\ y C_ t ) ) )
9		rsp 2589	. . . . . . . . . . . . . . 15 |- ( A. x e. t E. y e. B ( x e. y /\ y C_ t ) -> ( x e. t -> E. y e. B ( x e. y /\ y C_ t ) ) )
10	8, 9	biimtrdi 163	. . . . . . . . . . . . . 14 |- ( B e. TopBases -> ( t e. ( topGen ` B ) -> ( x e. t -> E. y e. B ( x e. y /\ y C_ t ) ) ) )
11	10	imp31 256	. . . . . . . . . . . . 13 |- ( ( ( B e. TopBases /\ t e. ( topGen ` B ) ) /\ x e. t ) -> E. y e. B ( x e. y /\ y C_ t ) )
12	11	an32s 570	. . . . . . . . . . . 12 |- ( ( ( B e. TopBases /\ x e. t ) /\ t e. ( topGen ` B ) ) -> E. y e. B ( x e. y /\ y C_ t ) )
13	7, 12	sylan2 286	. . . . . . . . . . 11 |- ( ( ( B e. TopBases /\ x e. t ) /\ ( u C_ ( topGen ` B ) /\ t e. u ) ) -> E. y e. B ( x e. y /\ y C_ t ) )
14	13	an42s 593	. . . . . . . . . 10 |- ( ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) /\ ( t e. u /\ x e. t ) ) -> E. y e. B ( x e. y /\ y C_ t ) )
15		elssuni 3942	. . . . . . . . . . . . . 14 |- ( t e. u -> t C_ U. u )
16		sstr2 3245	. . . . . . . . . . . . . 14 |- ( y C_ t -> ( t C_ U. u -> y C_ U. u ) )
17	15, 16	syl5com 29	. . . . . . . . . . . . 13 |- ( t e. u -> ( y C_ t -> y C_ U. u ) )
18	17	anim2d 337	. . . . . . . . . . . 12 |- ( t e. u -> ( ( x e. y /\ y C_ t ) -> ( x e. y /\ y C_ U. u ) ) )
19	18	reximdv 2643	. . . . . . . . . . 11 |- ( t e. u -> ( E. y e. B ( x e. y /\ y C_ t ) -> E. y e. B ( x e. y /\ y C_ U. u ) ) )
20	19	ad2antrl 490	. . . . . . . . . 10 |- ( ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) /\ ( t e. u /\ x e. t ) ) -> ( E. y e. B ( x e. y /\ y C_ t ) -> E. y e. B ( x e. y /\ y C_ U. u ) ) )
21	14, 20	mpd 13	. . . . . . . . 9 |- ( ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) /\ ( t e. u /\ x e. t ) ) -> E. y e. B ( x e. y /\ y C_ U. u ) )
22	21	rexlimdvaa 2661	. . . . . . . 8 |- ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) -> ( E. t e. u x e. t -> E. y e. B ( x e. y /\ y C_ U. u ) ) )
23	6, 22	biimtrid 152	. . . . . . 7 |- ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) -> ( x e. U. u -> E. y e. B ( x e. y /\ y C_ U. u ) ) )
24	23	ralrimiv 2614	. . . . . 6 |- ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) -> A. x e. U. u E. y e. B ( x e. y /\ y C_ U. u ) )
25	5, 24	jca 306	. . . . 5 |- ( ( B e. TopBases /\ u C_ ( topGen ` B ) ) -> ( U. u C_ U. B /\ A. x e. U. u E. y e. B ( x e. y /\ y C_ U. u ) ) )
26	25	ex 115	. . . 4 |- ( B e. TopBases -> ( u C_ ( topGen ` B ) -> ( U. u C_ U. B /\ A. x e. U. u E. y e. B ( x e. y /\ y C_ U. u ) ) ) )
27		eltg2 14918	. . . 4 |- ( B e. TopBases -> ( U. u e. ( topGen ` B ) <-> ( U. u C_ U. B /\ A. x e. U. u E. y e. B ( x e. y /\ y C_ U. u ) ) ) )
28	26, 27	sylibrd 169	. . 3 |- ( B e. TopBases -> ( u C_ ( topGen ` B ) -> U. u e. ( topGen ` B ) ) )
29	28	alrimiv 1923	. 2 |- ( B e. TopBases -> A. u ( u C_ ( topGen ` B ) -> U. u e. ( topGen ` B ) ) )
30		inss1 3441	. . . . . . . 8 |- ( u i^i v ) C_ u
31		tg1 14924	. . . . . . . 8 |- ( u e. ( topGen ` B ) -> u C_ U. B )
32	30, 31	sstrid 3249	. . . . . . 7 |- ( u e. ( topGen ` B ) -> ( u i^i v ) C_ U. B )
33	32	ad2antrl 490	. . . . . 6 |- ( ( B e. TopBases /\ ( u e. ( topGen ` B ) /\ v e. ( topGen ` B ) ) ) -> ( u i^i v ) C_ U. B )
34		eltg2 14918	. . . . . . . . . . . . 13 |- ( B e. TopBases -> ( u e. ( topGen ` B ) <-> ( u C_ U. B /\ A. x e. u E. z e. B ( x e. z /\ z C_ u ) ) ) )
35	34	simplbda 384	. . . . . . . . . . . 12 |- ( ( B e. TopBases /\ u e. ( topGen ` B ) ) -> A. x e. u E. z e. B ( x e. z /\ z C_ u ) )
36		rsp 2589	. . . . . . . . . . . 12 |- ( A. x e. u E. z e. B ( x e. z /\ z C_ u ) -> ( x e. u -> E. z e. B ( x e. z /\ z C_ u ) ) )
37	35, 36	syl 14	. . . . . . . . . . 11 |- ( ( B e. TopBases /\ u e. ( topGen ` B ) ) -> ( x e. u -> E. z e. B ( x e. z /\ z C_ u ) ) )
38		eltg2 14918	. . . . . . . . . . . . 13 |- ( B e. TopBases -> ( v e. ( topGen ` B ) <-> ( v C_ U. B /\ A. x e. v E. w e. B ( x e. w /\ w C_ v ) ) ) )
39	38	simplbda 384	. . . . . . . . . . . 12 |- ( ( B e. TopBases /\ v e. ( topGen ` B ) ) -> A. x e. v E. w e. B ( x e. w /\ w C_ v ) )
40		rsp 2589	. . . . . . . . . . . 12 |- ( A. x e. v E. w e. B ( x e. w /\ w C_ v ) -> ( x e. v -> E. w e. B ( x e. w /\ w C_ v ) ) )
41	39, 40	syl 14	. . . . . . . . . . 11 |- ( ( B e. TopBases /\ v e. ( topGen ` B ) ) -> ( x e. v -> E. w e. B ( x e. w /\ w C_ v ) ) )
42	37, 41	im2anan9 602	. . . . . . . . . 10 |- ( ( ( B e. TopBases /\ u e. ( topGen ` B ) ) /\ ( B e. TopBases /\ v e. ( topGen ` B ) ) ) -> ( ( x e. u /\ x e. v ) -> ( E. z e. B ( x e. z /\ z C_ u ) /\ E. w e. B ( x e. w /\ w C_ v ) ) ) )
43		elin 3402	. . . . . . . . . 10 |- ( x e. ( u i^i v ) <-> ( x e. u /\ x e. v ) )
44		reeanv 2713	. . . . . . . . . 10 |- ( E. z e. B E. w e. B ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) <-> ( E. z e. B ( x e. z /\ z C_ u ) /\ E. w e. B ( x e. w /\ w C_ v ) ) )
45	42, 43, 44	3imtr4g 205	. . . . . . . . 9 |- ( ( ( B e. TopBases /\ u e. ( topGen ` B ) ) /\ ( B e. TopBases /\ v e. ( topGen ` B ) ) ) -> ( x e. ( u i^i v ) -> E. z e. B E. w e. B ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) ) )
46	45	anandis 596	. . . . . . . 8 |- ( ( B e. TopBases /\ ( 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 C_ u ) /\ ( x e. w /\ w C_ v ) ) ) )
47		elin 3402	. . . . . . . . . . . . . . . . 17 |- ( x e. ( z i^i w ) <-> ( x e. z /\ x e. w ) )
48	47	biimpri 133	. . . . . . . . . . . . . . . 16 |- ( ( x e. z /\ x e. w ) -> x e. ( z i^i w ) )
49		ss2in 3449	. . . . . . . . . . . . . . . 16 |- ( ( z C_ u /\ w C_ v ) -> ( z i^i w ) C_ ( u i^i v ) )
50	48, 49	anim12i 338	. . . . . . . . . . . . . . 15 |- ( ( ( x e. z /\ x e. w ) /\ ( z C_ u /\ w C_ v ) ) -> ( x e. ( z i^i w ) /\ ( z i^i w ) C_ ( u i^i v ) ) )
51	50	an4s 592	. . . . . . . . . . . . . 14 |- ( ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) -> ( x e. ( z i^i w ) /\ ( z i^i w ) C_ ( u i^i v ) ) )
52		basis2 14913	. . . . . . . . . . . . . . . . 17 |- ( ( ( B e. TopBases /\ z e. B ) /\ ( w e. B /\ x e. ( z i^i w ) ) ) -> E. t e. B ( x e. t /\ t C_ ( z i^i w ) ) )
53	52	adantllr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ( B e. TopBases /\ 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 C_ ( z i^i w ) ) )
54	53	adantrrr 487	. . . . . . . . . . . . . . 15 |- ( ( ( ( B e. TopBases /\ x e. ( u i^i v ) ) /\ z e. B ) /\ ( w e. B /\ ( x e. ( z i^i w ) /\ ( z i^i w ) C_ ( u i^i v ) ) ) ) -> E. t e. B ( x e. t /\ t C_ ( z i^i w ) ) )
55		sstr2 3245	. . . . . . . . . . . . . . . . . . . 20 |- ( t C_ ( z i^i w ) -> ( ( z i^i w ) C_ ( u i^i v ) -> t C_ ( u i^i v ) ) )
56	55	com12 30	. . . . . . . . . . . . . . . . . . 19 |- ( ( z i^i w ) C_ ( u i^i v ) -> ( t C_ ( z i^i w ) -> t C_ ( u i^i v ) ) )
57	56	anim2d 337	. . . . . . . . . . . . . . . . . 18 |- ( ( z i^i w ) C_ ( u i^i v ) -> ( ( x e. t /\ t C_ ( z i^i w ) ) -> ( x e. t /\ t C_ ( u i^i v ) ) ) )
58	57	reximdv 2643	. . . . . . . . . . . . . . . . 17 |- ( ( z i^i w ) C_ ( u i^i v ) -> ( E. t e. B ( x e. t /\ t C_ ( z i^i w ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
59	58	adantl 277	. . . . . . . . . . . . . . . 16 |- ( ( x e. ( z i^i w ) /\ ( z i^i w ) C_ ( u i^i v ) ) -> ( E. t e. B ( x e. t /\ t C_ ( z i^i w ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
60	59	ad2antll 491	. . . . . . . . . . . . . . 15 |- ( ( ( ( B e. TopBases /\ x e. ( u i^i v ) ) /\ z e. B ) /\ ( w e. B /\ ( x e. ( z i^i w ) /\ ( z i^i w ) C_ ( u i^i v ) ) ) ) -> ( E. t e. B ( x e. t /\ t C_ ( z i^i w ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
61	54, 60	mpd 13	. . . . . . . . . . . . . 14 |- ( ( ( ( B e. TopBases /\ x e. ( u i^i v ) ) /\ z e. B ) /\ ( w e. B /\ ( x e. ( z i^i w ) /\ ( z i^i w ) C_ ( u i^i v ) ) ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) )
62	51, 61	sylanr2 405	. . . . . . . . . . . . 13 |- ( ( ( ( B e. TopBases /\ x e. ( u i^i v ) ) /\ z e. B ) /\ ( w e. B /\ ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) )
63	62	rexlimdvaa 2661	. . . . . . . . . . . 12 |- ( ( ( B e. TopBases /\ x e. ( u i^i v ) ) /\ z e. B ) -> ( E. w e. B ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
64	63	rexlimdva 2660	. . . . . . . . . . 11 |- ( ( B e. TopBases /\ x e. ( u i^i v ) ) -> ( E. z e. B E. w e. B ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
65	64	ex 115	. . . . . . . . . 10 |- ( B e. TopBases -> ( x e. ( u i^i v ) -> ( E. z e. B E. w e. B ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) ) )
66	65	a2d 26	. . . . . . . . 9 |- ( B e. TopBases -> ( ( x e. ( u i^i v ) -> E. z e. B E. w e. B ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) ) -> ( x e. ( u i^i v ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) ) )
67	66	imp 124	. . . . . . . 8 |- ( ( B e. TopBases /\ ( x e. ( u i^i v ) -> E. z e. B E. w e. B ( ( x e. z /\ z C_ u ) /\ ( x e. w /\ w C_ v ) ) ) ) -> ( x e. ( u i^i v ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
68	46, 67	syldan 282	. . . . . . 7 |- ( ( B e. TopBases /\ ( u e. ( topGen ` B ) /\ v e. ( topGen ` B ) ) ) -> ( x e. ( u i^i v ) -> E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
69	68	ralrimiv 2614	. . . . . 6 |- ( ( B e. TopBases /\ ( u e. ( topGen ` B ) /\ v e. ( topGen ` B ) ) ) -> A. x e. ( u i^i v ) E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) )
70	33, 69	jca 306	. . . . 5 |- ( ( B e. TopBases /\ ( u e. ( topGen ` B ) /\ v e. ( topGen ` B ) ) ) -> ( ( u i^i v ) C_ U. B /\ A. x e. ( u i^i v ) E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) )
71	70	ex 115	. . . 4 |- ( B e. TopBases -> ( ( u e. ( topGen ` B ) /\ v e. ( topGen ` B ) ) -> ( ( u i^i v ) C_ U. B /\ A. x e. ( u i^i v ) E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) ) )
72		eltg2 14918	. . . 4 |- ( B e. TopBases -> ( ( u i^i v ) e. ( topGen ` B ) <-> ( ( u i^i v ) C_ U. B /\ A. x e. ( u i^i v ) E. t e. B ( x e. t /\ t C_ ( u i^i v ) ) ) ) )
73	71, 72	sylibrd 169	. . 3 |- ( B e. TopBases -> ( ( u e. ( topGen ` B ) /\ v e. ( topGen ` B ) ) -> ( u i^i v ) e. ( topGen ` B ) ) )
74	73	ralrimivv 2623	. 2 |- ( B e. TopBases -> A. u e. ( topGen ` B ) A. v e. ( topGen ` B ) ( u i^i v ) e. ( topGen ` B ) )
75		tgvalex 13476	. . 3 |- ( B e. TopBases -> ( topGen ` B ) e. _V )
76		istopg 14864	. . 3 |- ( ( topGen ` B ) e. _V -> ( ( topGen ` B ) e. Top <-> ( A. u ( u C_ ( topGen ` B ) -> U. u e. ( topGen ` B ) ) /\ A. u e. ( topGen ` B ) A. v e. ( topGen ` B ) ( u i^i v ) e. ( topGen ` B ) ) ) )
77	75, 76	syl 14	. 2 |- ( B e. TopBases -> ( ( topGen ` B ) e. Top <-> ( A. u ( u C_ ( topGen ` B ) -> U. u e. ( topGen ` B ) ) /\ A. u e. ( topGen ` B ) A. v e. ( topGen ` B ) ( u i^i v ) e. ( topGen ` B ) ) ) )
78	29, 74, 77	mpbir2and 953	1 |- ( B e. TopBases -> ( topGen ` B ) e. Top )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1396   = wceq 1398   e. wcel 2203   A.wral 2520   E.wrex 2521   _Vcvv 2813   i^i cin 3210   C_ wss 3211   U.cuni 3914   ` cfv 5352   topGenctg 13467   Topctop 14862   TopBasesctb 14907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-un 4554

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-sbc 3043  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-mpt 4173  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-iota 5312  df-fun 5354  df-fv 5360  df-topgen 13473  df-top 14863  df-bases 14908

This theorem is referenced by:  tgclb  14930  tgtopon  14931  bastop  14940  resttop  15035  txtop  15125  mopnval  15307  retop  15389