Theorem haust1 18925

Description: A Hausdorff space is a T₁ space. (Contributed by FL, 11-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Aug-2015.)

Assertion

Ref	Expression
haust1	|- ( J e. Haus -> J e. Fre )

Proof of Theorem haust1

Dummy variables x y z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2437	. . . . . . . . 9 |- U. J = U. J
2	1	hausnei 18901	. . . . . . . 8 |- ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J /\ x =/= y ) ) -> E. z e. J E. w e. J ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) )
3		simprr1 1036	. . . . . . . . . . 11 |- ( ( ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J /\ x =/= y ) ) /\ z e. J ) /\ ( w e. J /\ ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) ) -> x e. z )
4		noel 3634	. . . . . . . . . . . . 13 |- -. y e. (/)
5		simprr3 1038	. . . . . . . . . . . . . 14 |- ( ( ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J /\ x =/= y ) ) /\ z e. J ) /\ ( w e. J /\ ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) ) -> ( z i^i w ) = (/) )
6	5	eleq2d 2504	. . . . . . . . . . . . 13 |- ( ( ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J /\ x =/= y ) ) /\ z e. J ) /\ ( w e. J /\ ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) ) -> ( y e. ( z i^i w ) <-> y e. (/) ) )
7	4, 6	mtbiri 303	. . . . . . . . . . . 12 |- ( ( ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J /\ x =/= y ) ) /\ z e. J ) /\ ( w e. J /\ ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) ) -> -. y e. ( z i^i w ) )
8		simprr2 1037	. . . . . . . . . . . . 13 |- ( ( ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J /\ x =/= y ) ) /\ z e. J ) /\ ( w e. J /\ ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) ) -> y e. w )
9		elin 3532	. . . . . . . . . . . . . 14 |- ( y e. ( z i^i w ) <-> ( y e. z /\ y e. w ) )
10	9	simplbi2com 627	. . . . . . . . . . . . 13 |- ( y e. w -> ( y e. z -> y e. ( z i^i w ) ) )
11	8, 10	syl 16	. . . . . . . . . . . 12 |- ( ( ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J /\ x =/= y ) ) /\ z e. J ) /\ ( w e. J /\ ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) ) -> ( y e. z -> y e. ( z i^i w ) ) )
12	7, 11	mtod 177	. . . . . . . . . . 11 |- ( ( ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J /\ x =/= y ) ) /\ z e. J ) /\ ( w e. J /\ ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) ) -> -. y e. z )
13	3, 12	jca 532	. . . . . . . . . 10 |- ( ( ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J /\ x =/= y ) ) /\ z e. J ) /\ ( w e. J /\ ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) ) ) -> ( x e. z /\ -. y e. z ) )
14	13	rexlimdvaa 2836	. . . . . . . . 9 |- ( ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J /\ x =/= y ) ) /\ z e. J ) -> ( E. w e. J ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) -> ( x e. z /\ -. y e. z ) ) )
15	14	reximdva 2822	. . . . . . . 8 |- ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J /\ x =/= y ) ) -> ( E. z e. J E. w e. J ( x e. z /\ y e. w /\ ( z i^i w ) = (/) ) -> E. z e. J ( x e. z /\ -. y e. z ) ) )
16	2, 15	mpd 15	. . . . . . 7 |- ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J /\ x =/= y ) ) -> E. z e. J ( x e. z /\ -. y e. z ) )
17		rexanali 2755	. . . . . . 7 |- ( E. z e. J ( x e. z /\ -. y e. z ) <-> -. A. z e. J ( x e. z -> y e. z ) )
18	16, 17	sylib 196	. . . . . 6 |- ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J /\ x =/= y ) ) -> -. A. z e. J ( x e. z -> y e. z ) )
19	18	3exp2 1205	. . . . 5 |- ( J e. Haus -> ( x e. U. J -> ( y e. U. J -> ( x =/= y -> -. A. z e. J ( x e. z -> y e. z ) ) ) ) )
20	19	imp32 433	. . . 4 |- ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J ) ) -> ( x =/= y -> -. A. z e. J ( x e. z -> y e. z ) ) )
21	20	necon4ad 2666	. . 3 |- ( ( J e. Haus /\ ( x e. U. J /\ y e. U. J ) ) -> ( A. z e. J ( x e. z -> y e. z ) -> x = y ) )
22	21	ralrimivva 2802	. 2 |- ( J e. Haus -> A. x e. U. J A. y e. U. J ( A. z e. J ( x e. z -> y e. z ) -> x = y ) )
23		haustop 18904	. . . 4 |- ( J e. Haus -> J e. Top )
24	1	toptopon 18507	. . . 4 |- ( J e. Top <-> J e. (TopOn ` U. J ) )
25	23, 24	sylib 196	. . 3 |- ( J e. Haus -> J e. (TopOn ` U. J ) )
26		ist1-2 18920	. . 3 |- ( J e. (TopOn ` U. J ) -> ( J e. Fre <-> A. x e. U. J A. y e. U. J ( A. z e. J ( x e. z -> y e. z ) -> x = y ) ) )
27	25, 26	syl 16	. 2 |- ( J e. Haus -> ( J e. Fre <-> A. x e. U. J A. y e. U. J ( A. z e. J ( x e. z -> y e. z ) -> x = y ) ) )
28	22, 27	mpbird 232	1 |- ( J e. Haus -> J e. Fre )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   = wceq 1369   e. wcel 1756   =/= wne 2600   A.wral 2709   E.wrex 2710   i^i cin 3320   (/)c0 3630   U.cuni 4084   ` cfv 5411   Topctop 18467  TopOnctopon 18468   Frect1 18880   Hauscha 18881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-opab 4344  df-mpt 4345  df-id 4628  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-iota 5374  df-fun 5413  df-fv 5419  df-topgen 14374  df-top 18472  df-topon 18475  df-cld 18592  df-t1 18887  df-haus 18888

This theorem is referenced by:  sncld  18944  ishaus3  19365  reghaus  19367  nrmhaus  19368  tgpt1  19657  metreg  20408  ipasslem8  24182  onint1  28243  oninhaus  28244