txbas - Intuitionistic Logic Explorer

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

Theorem txbas 12427

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 4553	. . . . . . . . . 10
3		xpeq2 4554	. . . . . . . . . 10
4	2, 3	cbvmpov 5851	. . . . . . . . 9
5	4	rnmpo 5881	. . . . . . . 8
6	1, 5	eqtri 2160	. . . . . . 7
7	6	abeq2i 2250	. . . . . 6
8		xpeq1 4553	. . . . . . . . . 10
9		xpeq2 4554	. . . . . . . . . 10
10	8, 9	cbvmpov 5851	. . . . . . . . 9
11	10	rnmpo 5881	. . . . . . . 8
12	1, 11	eqtri 2160	. . . . . . 7
13	12	abeq2i 2250	. . . . . 6
14	7, 13	anbi12i 455	. . . . 5 $/\$ $/\$
15		reeanv 2600	. . . . 5 $/\$ $/\$
16	14, 15	bitr4i 186	. . . 4 $/\$ $/\$
17		reeanv 2600	. . . . . 6 $/\$ $/\$
18		basis2 12215	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
19	18	exp43 369	. . . . . . . . . . . . . . 15 $/\$
20	19	imp42 351	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
21		basis2 12215	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
22	21	exp43 369	. . . . . . . . . . . . . . 15 $/\$
23	22	imp42 351	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
24		reeanv 2600	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25		opelxpi 4571	. . . . . . . . . . . . . . . . . . 19 $/\$
26		xpss12 4646	. . . . . . . . . . . . . . . . . . 19 $/\$
27	25, 26	anim12i 336	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
28	27	an4s 577	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
29	28	reximi 2529	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
30	29	reximi 2529	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
31	24, 30	sylbir 134	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
32	20, 23, 31	syl2an 287	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	32	an4s 577	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	33	ralrimivva 2514	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		eleq1 2202	. . . . . . . . . . . . . 14
36	35	anbi1d 460	. . . . . . . . . . . . 13 $/\$ $/\$
37	36	2rexbidv 2460	. . . . . . . . . . . 12 $/\$ $/\$
38	37	ralxp 4682	. . . . . . . . . . 11 $/\$ $/\$
39	34, 38	sylibr 133	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40	39	an4s 577	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	40	anassrs 397	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		ineq12 3272	. . . . . . . . . 10 $/\$
43		inxp 4673	. . . . . . . . . 10
44	42, 43	syl6eq 2188	. . . . . . . . 9 $/\$
45	44	sseq2d 3127	. . . . . . . . . . . 12 $/\$
46	45	anbi2d 459	. . . . . . . . . . 11 $/\$ $/\$ $/\$
47	46	rexbidv 2438	. . . . . . . . . 10 $/\$ $/\$ $/\$
48	1	rexeqi 2631	. . . . . . . . . . 11 $/\$ $/\$
49		1stexg 6065	. . . . . . . . . . . . . . 15
50	49	elv 2690	. . . . . . . . . . . . . 14
51		2ndexg 6066	. . . . . . . . . . . . . . 15
52	51	elv 2690	. . . . . . . . . . . . . 14
53	50, 52	xpex 4654	. . . . . . . . . . . . 13
54	53	rgenw 2487	. . . . . . . . . . . 12
55		vex 2689	. . . . . . . . . . . . . . . . 17
56		vex 2689	. . . . . . . . . . . . . . . . 17
57	55, 56	op1std 6046	. . . . . . . . . . . . . . . 16
58	55, 56	op2ndd 6047	. . . . . . . . . . . . . . . 16
59	57, 58	xpeq12d 4564	. . . . . . . . . . . . . . 15
60	59	mpompt 5863	. . . . . . . . . . . . . 14
61	60	eqcomi 2143	. . . . . . . . . . . . 13
62		eleq2 2203	. . . . . . . . . . . . . 14
63		sseq1 3120	. . . . . . . . . . . . . 14
64	62, 63	anbi12d 464	. . . . . . . . . . . . 13 $/\$ $/\$
65	61, 64	rexrnmpt 5563	. . . . . . . . . . . 12 $/\$ $/\$
66	54, 65	ax-mp 5	. . . . . . . . . . 11 $/\$ $/\$
67	59	eleq2d 2209	. . . . . . . . . . . . 13
68	59	sseq1d 3126	. . . . . . . . . . . . 13
69	67, 68	anbi12d 464	. . . . . . . . . . . 12 $/\$ $/\$
70	69	rexxp 4683	. . . . . . . . . . 11 $/\$ $/\$
71	48, 66, 70	3bitri 205	. . . . . . . . . 10 $/\$ $/\$
72	47, 71	syl6bb 195	. . . . . . . . 9 $/\$ $/\$ $/\$
73	44, 72	raleqbidv 2638	. . . . . . . 8 $/\$ $/\$ $/\$
74	41, 73	syl5ibrcom 156	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	74	rexlimdvva 2557	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
76	17, 75	syl5bir 152	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
77	76	rexlimdvva 2557	. . . 4 $/\$ $/\$ $/\$
78	16, 77	syl5bi 151	. . 3 $/\$ $/\$ $/\$
79	78	ralrimivv 2513	. 2 $/\$ $/\$
80	1	txbasex 12426	. . 3 $/\$
81		isbasis2g 12212	. . 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 1331

wcel 1480

cab 2125

wral 2416

wrex 2417

cvv 2686

cin 3070

wss 3071

cop 3530

cmpt 3989

cxp 4537

crn 4540

cfv 5123

cmpo 5776

c1st 6036

c2nd 6037

ctb 12209

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 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-pow 4098 ax-pr 4131 ax-un 4355

This theorem depends on definitions: df-bi 116 df-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ral 2421 df-rex 2422 df-rab 2425 df-v 2688 df-sbc 2910 df-csb 3004 df-un 3075 df-in 3077 df-ss 3084 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-iun 3815 df-br 3930 df-opab 3990 df-mpt 3991 df-id 4215 df-xp 4545 df-rel 4546 df-cnv 4547 df-co 4548 df-dm 4549 df-rn 4550 df-res 4551 df-ima 4552 df-iota 5088 df-fun 5125 df-fn 5126 df-f 5127 df-fo 5129 df-fv 5131 df-oprab 5778 df-mpo 5779 df-1st 6038 df-2nd 6039 df-bases 12210

This theorem is referenced by: txtop 12429

W3C validator