txbas - Intuitionistic Logic Explorer

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

Theorem txbas 13052

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 4625	. . . . . . . . . 10
3		xpeq2 4626	. . . . . . . . . 10
4	2, 3	cbvmpov 5933	. . . . . . . . 9
5	4	rnmpo 5963	. . . . . . . 8
6	1, 5	eqtri 2191	. . . . . . 7
7	6	abeq2i 2281	. . . . . 6
8		xpeq1 4625	. . . . . . . . . 10
9		xpeq2 4626	. . . . . . . . . 10
10	8, 9	cbvmpov 5933	. . . . . . . . 9
11	10	rnmpo 5963	. . . . . . . 8
12	1, 11	eqtri 2191	. . . . . . 7
13	12	abeq2i 2281	. . . . . 6
14	7, 13	anbi12i 457	. . . . 5 $/\$ $/\$
15		reeanv 2639	. . . . 5 $/\$ $/\$
16	14, 15	bitr4i 186	. . . 4 $/\$ $/\$
17		reeanv 2639	. . . . . 6 $/\$ $/\$
18		basis2 12840	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
19	18	exp43 370	. . . . . . . . . . . . . . 15 $/\$
20	19	imp42 352	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
21		basis2 12840	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
22	21	exp43 370	. . . . . . . . . . . . . . 15 $/\$
23	22	imp42 352	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
24		reeanv 2639	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25		opelxpi 4643	. . . . . . . . . . . . . . . . . . 19 $/\$
26		xpss12 4718	. . . . . . . . . . . . . . . . . . 19 $/\$
27	25, 26	anim12i 336	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
28	27	an4s 583	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
29	28	reximi 2567	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
30	29	reximi 2567	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
31	24, 30	sylbir 134	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
32	20, 23, 31	syl2an 287	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	32	an4s 583	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	33	ralrimivva 2552	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		eleq1 2233	. . . . . . . . . . . . . 14
36	35	anbi1d 462	. . . . . . . . . . . . 13 $/\$ $/\$
37	36	2rexbidv 2495	. . . . . . . . . . . 12 $/\$ $/\$
38	37	ralxp 4754	. . . . . . . . . . 11 $/\$ $/\$
39	34, 38	sylibr 133	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40	39	an4s 583	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	40	anassrs 398	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		ineq12 3323	. . . . . . . . . 10 $/\$
43		inxp 4745	. . . . . . . . . 10
44	42, 43	eqtrdi 2219	. . . . . . . . 9 $/\$
45	44	sseq2d 3177	. . . . . . . . . . . 12 $/\$
46	45	anbi2d 461	. . . . . . . . . . 11 $/\$ $/\$ $/\$
47	46	rexbidv 2471	. . . . . . . . . 10 $/\$ $/\$ $/\$
48	1	rexeqi 2670	. . . . . . . . . . 11 $/\$ $/\$
49		1stexg 6146	. . . . . . . . . . . . . . 15
50	49	elv 2734	. . . . . . . . . . . . . 14
51		2ndexg 6147	. . . . . . . . . . . . . . 15
52	51	elv 2734	. . . . . . . . . . . . . 14
53	50, 52	xpex 4726	. . . . . . . . . . . . 13
54	53	rgenw 2525	. . . . . . . . . . . 12
55		vex 2733	. . . . . . . . . . . . . . . . 17
56		vex 2733	. . . . . . . . . . . . . . . . 17
57	55, 56	op1std 6127	. . . . . . . . . . . . . . . 16
58	55, 56	op2ndd 6128	. . . . . . . . . . . . . . . 16
59	57, 58	xpeq12d 4636	. . . . . . . . . . . . . . 15
60	59	mpompt 5945	. . . . . . . . . . . . . 14
61	60	eqcomi 2174	. . . . . . . . . . . . 13
62		eleq2 2234	. . . . . . . . . . . . . 14
63		sseq1 3170	. . . . . . . . . . . . . 14
64	62, 63	anbi12d 470	. . . . . . . . . . . . 13 $/\$ $/\$
65	61, 64	rexrnmpt 5639	. . . . . . . . . . . 12 $/\$ $/\$
66	54, 65	ax-mp 5	. . . . . . . . . . 11 $/\$ $/\$
67	59	eleq2d 2240	. . . . . . . . . . . . 13
68	59	sseq1d 3176	. . . . . . . . . . . . 13
69	67, 68	anbi12d 470	. . . . . . . . . . . 12 $/\$ $/\$
70	69	rexxp 4755	. . . . . . . . . . 11 $/\$ $/\$
71	48, 66, 70	3bitri 205	. . . . . . . . . 10 $/\$ $/\$
72	47, 71	bitrdi 195	. . . . . . . . 9 $/\$ $/\$ $/\$
73	44, 72	raleqbidv 2677	. . . . . . . 8 $/\$ $/\$ $/\$
74	41, 73	syl5ibrcom 156	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	74	rexlimdvva 2595	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
76	17, 75	syl5bir 152	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
77	76	rexlimdvva 2595	. . . 4 $/\$ $/\$ $/\$
78	16, 77	syl5bi 151	. . 3 $/\$ $/\$ $/\$
79	78	ralrimivv 2551	. 2 $/\$ $/\$
80	1	txbasex 13051	. . 3 $/\$
81		isbasis2g 12837	. . 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 1348

wcel 2141

cab 2156

wral 2448

wrex 2449

cvv 2730

cin 3120

wss 3121

cop 3586

cmpt 4050

cxp 4609

crn 4612

cfv 5198

cmpo 5855

c1st 6117

c2nd 6118

ctb 12834

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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-sep 4107 ax-pow 4160 ax-pr 4194 ax-un 4418

This theorem depends on definitions: df-bi 116 df-3an 975 df-tru 1351 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-rex 2454 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-un 3125 df-in 3127 df-ss 3134 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-iun 3875 df-br 3990 df-opab 4051 df-mpt 4052 df-id 4278 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-fo 5204 df-fv 5206 df-oprab 5857 df-mpo 5858 df-1st 6119 df-2nd 6120 df-bases 12835

This theorem is referenced by: txtop 13054

W3C validator