tgcl - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > tgcl		Unicode version

Theorem tgcl 12272

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

**Assertion**
Ref	Expression
tgcl

Proof of Theorem tgcl Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		uniss 3765	. . . . . . . 8
2	1	adantl 275	. . . . . . 7 $/\$
3		unitg 12270	. . . . . . . 8
4	3	adantr 274	. . . . . . 7 $/\$
5	2, 4	sseqtrd 3140	. . . . . 6 $/\$
6		eluni2 3748	. . . . . . . 8
7		ssel2 3097	. . . . . . . . . . . 12 $/\$
8		eltg2b 12262	. . . . . . . . . . . . . . 15 $/\$
9		rsp 2483	. . . . . . . . . . . . . . 15 $/\$ $/\$
10	8, 9	syl6bi 162	. . . . . . . . . . . . . 14 $/\$
11	10	imp31 254	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
12	11	an32s 558	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
13	7, 12	sylan2 284	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
14	13	an42s 579	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
15		elssuni 3772	. . . . . . . . . . . . . 14
16		sstr2 3109	. . . . . . . . . . . . . 14
17	15, 16	syl5com 29	. . . . . . . . . . . . 13
18	17	anim2d 335	. . . . . . . . . . . 12 $/\$ $/\$
19	18	reximdv 2536	. . . . . . . . . . 11 $/\$ $/\$
20	19	ad2antrl 482	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
21	14, 20	mpd 13	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
22	21	rexlimdvaa 2553	. . . . . . . 8 $/\$ $/\$
23	6, 22	syl5bi 151	. . . . . . 7 $/\$ $/\$
24	23	ralrimiv 2507	. . . . . 6 $/\$ $/\$
25	5, 24	jca 304	. . . . 5 $/\$ $/\$ $/\$
26	25	ex 114	. . . 4 $/\$ $/\$
27		eltg2 12261	. . . 4 $/\$ $/\$
28	26, 27	sylibrd 168	. . 3
29	28	alrimiv 1847	. 2
30		inss1 3301	. . . . . . . 8
31		tg1 12267	. . . . . . . 8
32	30, 31	sstrid 3113	. . . . . . 7
33	32	ad2antrl 482	. . . . . 6 $/\$ $/\$
34		eltg2 12261	. . . . . . . . . . . . 13 $/\$ $/\$
35	34	simplbda 382	. . . . . . . . . . . 12 $/\$ $/\$
36		rsp 2483	. . . . . . . . . . . 12 $/\$ $/\$
37	35, 36	syl 14	. . . . . . . . . . 11 $/\$ $/\$
38		eltg2 12261	. . . . . . . . . . . . 13 $/\$ $/\$
39	38	simplbda 382	. . . . . . . . . . . 12 $/\$ $/\$
40		rsp 2483	. . . . . . . . . . . 12 $/\$ $/\$
41	39, 40	syl 14	. . . . . . . . . . 11 $/\$ $/\$
42	37, 41	im2anan9 588	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43		elin 3264	. . . . . . . . . 10 $/\$
44		reeanv 2603	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	42, 43, 44	3imtr4g 204	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	45	anandis 582	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
47		elin 3264	. . . . . . . . . . . . . . . . 17 $/\$
48	47	biimpri 132	. . . . . . . . . . . . . . . 16 $/\$
49		ss2in 3309	. . . . . . . . . . . . . . . 16 $/\$
50	48, 49	anim12i 336	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
51	50	an4s 578	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
52		basis2 12254	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
53	52	adantllr 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
54	53	adantrrr 479	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		sstr2 3109	. . . . . . . . . . . . . . . . . . . 20
56	55	com12 30	. . . . . . . . . . . . . . . . . . 19
57	56	anim2d 335	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
58	57	reximdv 2536	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
59	58	adantl 275	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
60	59	ad2antll 483	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	54, 60	mpd 13	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	51, 61	sylanr2 403	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63	62	rexlimdvaa 2553	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	63	rexlimdva 2552	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
65	64	ex 114	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
66	65	a2d 26	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
67	66	imp 123	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
68	46, 67	syldan 280	. . . . . . 7 $/\$ $/\$ $/\$
69	68	ralrimiv 2507	. . . . . 6 $/\$ $/\$ $/\$
70	33, 69	jca 304	. . . . 5 $/\$ $/\$ $/\$ $/\$
71	70	ex 114	. . . 4 $/\$ $/\$ $/\$
72		eltg2 12261	. . . 4 $/\$ $/\$
73	71, 72	sylibrd 168	. . 3 $/\$
74	73	ralrimivv 2516	. 2
75		tgvalex 12258	. . 3
76		istopg 12205	. . 3 $/\$
77	75, 76	syl 14	. 2 $/\$
78	29, 74, 77	mpbir2and 929	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104

wal 1330

wceq 1332

wcel 1481

wral 2417

wrex 2418

cvv 2689

cin 3075

wss 3076

cuni 3744

cfv 5131

ctg 12174

ctop 12203

ctb 12248

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-13 1492 ax-14 1493 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 ax-sep 4054 ax-pow 4106 ax-pr 4139 ax-un 4363

This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1335 df-nf 1438 df-sb 1737 df-eu 2003 df-mo 2004 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ral 2422 df-rex 2423 df-v 2691 df-sbc 2914 df-un 3080 df-in 3082 df-ss 3089 df-pw 3517 df-sn 3538 df-pr 3539 df-op 3541 df-uni 3745 df-br 3938 df-opab 3998 df-mpt 3999 df-id 4223 df-xp 4553 df-rel 4554 df-cnv 4555 df-co 4556 df-dm 4557 df-iota 5096 df-fun 5133 df-fv 5139 df-topgen 12180 df-top 12204 df-bases 12249

This theorem is referenced by: tgclb 12273 tgtopon 12274 bastop 12283 resttop 12378 txtop 12468 mopnval 12650 retop 12732

W3C validator