txbas - Intuitionistic Logic Explorer

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

Theorem txbas 15249

Description: The set of Cartesian products of elements from two topological bases is a basis. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 31-Aug-2015.)

**Hypothesis**
Ref	Expression
txval.1

**Assertion**
Ref	Expression
txbas	$/\$

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem txbas Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		txval.1	. . . . . . . 8
2		xpeq1 4768	. . . . . . . . . 10
3		xpeq2 4769	. . . . . . . . . 10
4	2, 3	cbvmpov 6141	. . . . . . . . 9
5	4	rnmpo 6172	. . . . . . . 8
6	1, 5	eqtri 2255	. . . . . . 7
7	6	abeq2i 2345	. . . . . 6
8		xpeq1 4768	. . . . . . . . . 10
9		xpeq2 4769	. . . . . . . . . 10
10	8, 9	cbvmpov 6141	. . . . . . . . 9
11	10	rnmpo 6172	. . . . . . . 8
12	1, 11	eqtri 2255	. . . . . . 7
13	12	abeq2i 2345	. . . . . 6
14	7, 13	anbi12i 460	. . . . 5 $/\$ $/\$
15		reeanv 2715	. . . . 5 $/\$ $/\$
16	14, 15	bitr4i 187	. . . 4 $/\$ $/\$
17		reeanv 2715	. . . . . 6 $/\$ $/\$
18		basis2 15039	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
19	18	exp43 372	. . . . . . . . . . . . . . 15 $/\$
20	19	imp42 354	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
21		basis2 15039	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
22	21	exp43 372	. . . . . . . . . . . . . . 15 $/\$
23	22	imp42 354	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
24		reeanv 2715	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25		opelxpi 4786	. . . . . . . . . . . . . . . . . . 19 $/\$
26		xpss12 4862	. . . . . . . . . . . . . . . . . . 19 $/\$
27	25, 26	anim12i 338	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
28	27	an4s 592	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
29	28	reximi 2641	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
30	29	reximi 2641	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
31	24, 30	sylbir 135	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
32	20, 23, 31	syl2an 289	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	32	an4s 592	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	33	ralrimivva 2626	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		eleq1 2297	. . . . . . . . . . . . . 14
36	35	anbi1d 465	. . . . . . . . . . . . 13 $/\$ $/\$
37	36	2rexbidv 2569	. . . . . . . . . . . 12 $/\$ $/\$
38	37	ralxp 4903	. . . . . . . . . . 11 $/\$ $/\$
39	34, 38	sylibr 134	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40	39	an4s 592	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	40	anassrs 400	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		ineq12 3421	. . . . . . . . . 10 $/\$
43		inxp 4894	. . . . . . . . . 10
44	42, 43	eqtrdi 2283	. . . . . . . . 9 $/\$
45	44	sseq2d 3272	. . . . . . . . . . . 12 $/\$
46	45	anbi2d 464	. . . . . . . . . . 11 $/\$ $/\$ $/\$
47	46	rexbidv 2545	. . . . . . . . . 10 $/\$ $/\$ $/\$
48	1	rexeqi 2748	. . . . . . . . . . 11 $/\$ $/\$
49		1stexg 6374	. . . . . . . . . . . . . . 15
50	49	elv 2819	. . . . . . . . . . . . . 14
51		2ndexg 6375	. . . . . . . . . . . . . . 15
52	51	elv 2819	. . . . . . . . . . . . . 14
53	50, 52	xpex 4871	. . . . . . . . . . . . 13
54	53	rgenw 2599	. . . . . . . . . . . 12
55		vex 2818	. . . . . . . . . . . . . . . . 17
56		vex 2818	. . . . . . . . . . . . . . . . 17
57	55, 56	op1std 6355	. . . . . . . . . . . . . . . 16
58	55, 56	op2ndd 6356	. . . . . . . . . . . . . . . 16
59	57, 58	xpeq12d 4779	. . . . . . . . . . . . . . 15
60	59	mpompt 6153	. . . . . . . . . . . . . 14
61	60	eqcomi 2238	. . . . . . . . . . . . 13
62		eleq2 2298	. . . . . . . . . . . . . 14
63		sseq1 3265	. . . . . . . . . . . . . 14
64	62, 63	anbi12d 473	. . . . . . . . . . . . 13 $/\$ $/\$
65	61, 64	rexrnmpt 5825	. . . . . . . . . . . 12 $/\$ $/\$
66	54, 65	ax-mp 5	. . . . . . . . . . 11 $/\$ $/\$
67	59	eleq2d 2304	. . . . . . . . . . . . 13
68	59	sseq1d 3271	. . . . . . . . . . . . 13
69	67, 68	anbi12d 473	. . . . . . . . . . . 12 $/\$ $/\$
70	69	rexxp 4904	. . . . . . . . . . 11 $/\$ $/\$
71	48, 66, 70	3bitri 206	. . . . . . . . . 10 $/\$ $/\$
72	47, 71	bitrdi 196	. . . . . . . . 9 $/\$ $/\$ $/\$
73	44, 72	raleqbidv 2759	. . . . . . . 8 $/\$ $/\$ $/\$
74	41, 73	syl5ibrcom 157	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	74	rexlimdvva 2670	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
76	17, 75	biimtrrid 153	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
77	76	rexlimdvva 2670	. . . 4 $/\$ $/\$ $/\$
78	16, 77	biimtrid 152	. . 3 $/\$ $/\$ $/\$
79	78	ralrimivv 2625	. 2 $/\$ $/\$
80	1	txbasex 15248	. . 3 $/\$
81		isbasis2g 15036	. . 3 $/\$
82	80, 81	syl 14	. 2 $/\$ $/\$
83	79, 82	mpbird 167	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105

wceq 1398

wcel 2205

cab 2220

wral 2522

wrex 2523

cvv 2815

cin 3213

wss 3214

cop 3697

cmpt 4176

cxp 4752

crn 4755

cfv 5357

cmpo 6060

c1st 6345

c2nd 6346

ctb 15033

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 2207 ax-14 2208 ax-ext 2216 ax-sep 4233 ax-pow 4292 ax-pr 4327 ax-un 4559

This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ral 2527 df-rex 2528 df-rab 2531 df-v 2817 df-sbc 3046 df-csb 3142 df-un 3218 df-in 3220 df-ss 3227 df-pw 3676 df-sn 3700 df-pr 3701 df-op 3703 df-uni 3920 df-iun 3998 df-br 4115 df-opab 4177 df-mpt 4178 df-id 4419 df-xp 4760 df-rel 4761 df-cnv 4762 df-co 4763 df-dm 4764 df-rn 4765 df-res 4766 df-ima 4767 df-iota 5317 df-fun 5359 df-fn 5360 df-f 5361 df-fo 5363 df-fv 5365 df-oprab 6062 df-mpo 6063 df-1st 6347 df-2nd 6348 df-bases 15034

This theorem is referenced by: txtop 15251

W3C validator