txbas - Intuitionistic Logic Explorer

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

Theorem txbas 12269

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 4513	. . . . . . . . . 10
3		xpeq2 4514	. . . . . . . . . 10
4	2, 3	cbvmpov 5805	. . . . . . . . 9
5	4	rnmpo 5835	. . . . . . . 8
6	1, 5	eqtri 2135	. . . . . . 7
7	6	abeq2i 2225	. . . . . 6
8		xpeq1 4513	. . . . . . . . . 10
9		xpeq2 4514	. . . . . . . . . 10
10	8, 9	cbvmpov 5805	. . . . . . . . 9
11	10	rnmpo 5835	. . . . . . . 8
12	1, 11	eqtri 2135	. . . . . . 7
13	12	abeq2i 2225	. . . . . 6
14	7, 13	anbi12i 453	. . . . 5 $/\$ $/\$
15		reeanv 2574	. . . . 5 $/\$ $/\$
16	14, 15	bitr4i 186	. . . 4 $/\$ $/\$
17		reeanv 2574	. . . . . 6 $/\$ $/\$
18		basis2 12058	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
19	18	exp43 367	. . . . . . . . . . . . . . 15 $/\$
20	19	imp42 349	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
21		basis2 12058	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
22	21	exp43 367	. . . . . . . . . . . . . . 15 $/\$
23	22	imp42 349	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
24		reeanv 2574	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25		opelxpi 4531	. . . . . . . . . . . . . . . . . . 19 $/\$
26		xpss12 4606	. . . . . . . . . . . . . . . . . . 19 $/\$
27	25, 26	anim12i 334	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
28	27	an4s 560	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
29	28	reximi 2503	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
30	29	reximi 2503	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
31	24, 30	sylbir 134	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
32	20, 23, 31	syl2an 285	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	32	an4s 560	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	33	ralrimivva 2488	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		eleq1 2177	. . . . . . . . . . . . . 14
36	35	anbi1d 458	. . . . . . . . . . . . 13 $/\$ $/\$
37	36	2rexbidv 2434	. . . . . . . . . . . 12 $/\$ $/\$
38	37	ralxp 4642	. . . . . . . . . . 11 $/\$ $/\$
39	34, 38	sylibr 133	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40	39	an4s 560	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	40	anassrs 395	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		ineq12 3238	. . . . . . . . . 10 $/\$
43		inxp 4633	. . . . . . . . . 10
44	42, 43	syl6eq 2163	. . . . . . . . 9 $/\$
45	44	sseq2d 3093	. . . . . . . . . . . 12 $/\$
46	45	anbi2d 457	. . . . . . . . . . 11 $/\$ $/\$ $/\$
47	46	rexbidv 2412	. . . . . . . . . 10 $/\$ $/\$ $/\$
48	1	rexeqi 2605	. . . . . . . . . . 11 $/\$ $/\$
49		1stexg 6019	. . . . . . . . . . . . . . 15
50	49	elv 2661	. . . . . . . . . . . . . 14
51		2ndexg 6020	. . . . . . . . . . . . . . 15
52	51	elv 2661	. . . . . . . . . . . . . 14
53	50, 52	xpex 4614	. . . . . . . . . . . . 13
54	53	rgenw 2461	. . . . . . . . . . . 12
55		vex 2660	. . . . . . . . . . . . . . . . 17
56		vex 2660	. . . . . . . . . . . . . . . . 17
57	55, 56	op1std 6000	. . . . . . . . . . . . . . . 16
58	55, 56	op2ndd 6001	. . . . . . . . . . . . . . . 16
59	57, 58	xpeq12d 4524	. . . . . . . . . . . . . . 15
60	59	mpompt 5817	. . . . . . . . . . . . . 14
61	60	eqcomi 2119	. . . . . . . . . . . . 13
62		eleq2 2178	. . . . . . . . . . . . . 14
63		sseq1 3086	. . . . . . . . . . . . . 14
64	62, 63	anbi12d 462	. . . . . . . . . . . . 13 $/\$ $/\$
65	61, 64	rexrnmpt 5517	. . . . . . . . . . . 12 $/\$ $/\$
66	54, 65	ax-mp 7	. . . . . . . . . . 11 $/\$ $/\$
67	59	eleq2d 2184	. . . . . . . . . . . . 13
68	59	sseq1d 3092	. . . . . . . . . . . . 13
69	67, 68	anbi12d 462	. . . . . . . . . . . 12 $/\$ $/\$
70	69	rexxp 4643	. . . . . . . . . . 11 $/\$ $/\$
71	48, 66, 70	3bitri 205	. . . . . . . . . 10 $/\$ $/\$
72	47, 71	syl6bb 195	. . . . . . . . 9 $/\$ $/\$ $/\$
73	44, 72	raleqbidv 2612	. . . . . . . 8 $/\$ $/\$ $/\$
74	41, 73	syl5ibrcom 156	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	74	rexlimdvva 2531	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
76	17, 75	syl5bir 152	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
77	76	rexlimdvva 2531	. . . 4 $/\$ $/\$ $/\$
78	16, 77	syl5bi 151	. . 3 $/\$ $/\$ $/\$
79	78	ralrimivv 2487	. 2 $/\$ $/\$
80	1	txbasex 12268	. . 3 $/\$
81		isbasis2g 12055	. . 3 $/\$
82	80, 81	syl 14	. 2 $/\$ $/\$
83	79, 82	mpbird 166	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104

wceq 1314

wcel 1463

cab 2101

wral 2390

wrex 2391

cvv 2657

cin 3036

wss 3037

cop 3496

cmpt 3949

cxp 4497

crn 4500

cfv 5081

cmpo 5730

c1st 5990

c2nd 5991

ctb 12052

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-13 1474 ax-14 1475 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-sep 4006 ax-pow 4058 ax-pr 4091 ax-un 4315

This theorem depends on definitions: df-bi 116 df-3an 947 df-tru 1317 df-nf 1420 df-sb 1719 df-eu 1978 df-mo 1979 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-ral 2395 df-rex 2396 df-rab 2399 df-v 2659 df-sbc 2879 df-csb 2972 df-un 3041 df-in 3043 df-ss 3050 df-pw 3478 df-sn 3499 df-pr 3500 df-op 3502 df-uni 3703 df-iun 3781 df-br 3896 df-opab 3950 df-mpt 3951 df-id 4175 df-xp 4505 df-rel 4506 df-cnv 4507 df-co 4508 df-dm 4509 df-rn 4510 df-res 4511 df-ima 4512 df-iota 5046 df-fun 5083 df-fn 5084 df-f 5085 df-fo 5087 df-fv 5089 df-oprab 5732 df-mpo 5733 df-1st 5992 df-2nd 5993 df-bases 12053

This theorem is referenced by: txtop 12271

W3C validator