txhaus - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > txhaus		Structured version Visualization version Unicode version

Theorem txhaus 21450

Description: The topological product of two Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 23-Mar-2015.)

**Assertion**
Ref	Expression
txhaus	$/\$

Proof of Theorem txhaus Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		haustop 21135	. . 3
2		haustop 21135	. . 3
3		txtop 21372	. . 3 $/\$
4	1, 2, 3	syl2an 494	. 2 $/\$
5		eqid 2622	. . . . . . . 8
6		eqid 2622	. . . . . . . 8
7	5, 6	txuni 21395	. . . . . . 7 $/\$
8	1, 2, 7	syl2an 494	. . . . . 6 $/\$
9	8	eleq2d 2687	. . . . 5 $/\$
10	8	eleq2d 2687	. . . . 5 $/\$
11	9, 10	anbi12d 747	. . . 4 $/\$ $/\$ $/\$
12		neorian 2888	. . . . . . 7 $\/$ $/\$
13		xpopth 7207	. . . . . . . . 9 $/\$ $/\$
14	13	adantl 482	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
15	14	necon3bbid 2831	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
16	12, 15	syl5bb 272	. . . . . 6 $/\$ $/\$ $/\$ $\/$
17		simplll 798	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
18		xp1st 7198	. . . . . . . . . . . 12
19	18	ad2antrl 764	. . . . . . . . . . 11 $/\$ $/\$ $/\$
20	19	adantr 481	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
21		xp1st 7198	. . . . . . . . . . . 12
22	21	ad2antll 765	. . . . . . . . . . 11 $/\$ $/\$ $/\$
23	22	adantr 481	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
24		simpr 477	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
25	5	hausnei 21132	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
26	17, 20, 23, 24, 25	syl13anc 1328	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27	1	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
28	27	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	2	ad4antlr 769	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30		simprll 802	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
31	6	topopn 20711	. . . . . . . . . . . . . 14
32	29, 31	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33		txopn 21405	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
34	28, 29, 30, 32, 33	syl22anc 1327	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		simprlr 803	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36		txopn 21405	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
37	28, 29, 35, 32, 36	syl22anc 1327	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38		1st2nd2 7205	. . . . . . . . . . . . . . 15
39	38	ad2antrl 764	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
40	39	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		simprr1 1109	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		xp2nd 7199	. . . . . . . . . . . . . . . 16
43	42	ad2antrl 764	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
44	43	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	41, 44	jca 554	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46		elxp6 7200	. . . . . . . . . . . . 13 $/\$ $/\$
47	40, 45, 46	sylanbrc 698	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48		1st2nd2 7205	. . . . . . . . . . . . . . 15
49	48	ad2antll 765	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
50	49	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51		simprr2 1110	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52		xp2nd 7199	. . . . . . . . . . . . . . . 16
53	52	ad2antll 765	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
54	53	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	51, 54	jca 554	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		elxp6 7200	. . . . . . . . . . . . 13 $/\$ $/\$
57	50, 55, 56	sylanbrc 698	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58		simprr3 1111	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	58	xpeq1d 5138	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		xpindir 5256	. . . . . . . . . . . . 13
61		0xp 5199	. . . . . . . . . . . . 13
62	59, 60, 61	3eqtr3g 2679	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		eleq2 2690	. . . . . . . . . . . . . 14
64		ineq1 3807	. . . . . . . . . . . . . . 15
65	64	eqeq1d 2624	. . . . . . . . . . . . . 14
66	63, 65	3anbi13d 1401	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67		eleq2 2690	. . . . . . . . . . . . . 14
68		ineq2 3808	. . . . . . . . . . . . . . 15
69	68	eqeq1d 2624	. . . . . . . . . . . . . 14
70	67, 69	3anbi23d 1402	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
71	66, 70	rspc2ev 3324	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72	34, 37, 47, 57, 62, 71	syl113anc 1338	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73	72	expr 643	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	73	rexlimdvva 3038	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75	26, 74	mpd 15	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
76		simpllr 799	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
77	43	adantr 481	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
78	53	adantr 481	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
79		simpr 477	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
80	6	hausnei 21132	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
81	76, 77, 78, 79, 80	syl13anc 1328	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
82	27	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83	2	ad4antlr 769	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84	5	topopn 20711	. . . . . . . . . . . . . 14
85	82, 84	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		simprll 802	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87		txopn 21405	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
88	82, 83, 85, 86, 87	syl22anc 1327	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89		simprlr 803	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		txopn 21405	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
91	82, 83, 85, 89, 90	syl22anc 1327	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92	39	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93	19	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94		simprr1 1109	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95	93, 94	jca 554	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		elxp6 7200	. . . . . . . . . . . . 13 $/\$ $/\$
97	92, 95, 96	sylanbrc 698	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	49	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99	22	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100		simprr2 1110	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	99, 100	jca 554	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		elxp6 7200	. . . . . . . . . . . . 13 $/\$ $/\$
103	98, 101, 102	sylanbrc 698	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104		simprr3 1111	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
105	104	xpeq2d 5139	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106		xpindi 5255	. . . . . . . . . . . . 13
107		xp0 5552	. . . . . . . . . . . . 13
108	105, 106, 107	3eqtr3g 2679	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109		eleq2 2690	. . . . . . . . . . . . . 14
110		ineq1 3807	. . . . . . . . . . . . . . 15
111	110	eqeq1d 2624	. . . . . . . . . . . . . 14
112	109, 111	3anbi13d 1401	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
113		eleq2 2690	. . . . . . . . . . . . . 14
114		ineq2 3808	. . . . . . . . . . . . . . 15
115	114	eqeq1d 2624	. . . . . . . . . . . . . 14
116	113, 115	3anbi23d 1402	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
117	112, 116	rspc2ev 3324	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118	88, 91, 97, 103, 108, 117	syl113anc 1338	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
119	118	expr 643	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
120	119	rexlimdvva 3038	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	81, 120	mpd 15	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	75, 121	jaodan 826	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
123	122	ex 450	. . . . . 6 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
124	16, 123	sylbird 250	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
125	124	ex 450	. . . 4 $/\$ $/\$ $/\$ $/\$
126	11, 125	sylbird 250	. . 3 $/\$ $/\$ $/\$ $/\$
127	126	ralrimivv 2970	. 2 $/\$ $/\$ $/\$
128		eqid 2622	. . 3
129	128	ishaus 21126	. 2 $/\$ $/\$ $/\$
130	4, 127, 129	sylanbrc 698	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

cin 3573

c0 3915

cop 4183

cuni 4436

cxp 5112

cfv 5888 (class class class)co 6650

c1st 7166

c2nd 7167

ctop 20698

cha 21112

ctx 21363

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-fv 5896 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-1st 7168 df-2nd 7169 df-topgen 16104 df-top 20699 df-topon 20716 df-bases 20750 df-haus 21119 df-tx 21365

This theorem is referenced by: (None)

W3C validator