Metamath Proof Explorer

Theorem haust1

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

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 hausnei 
 |-  ( ( 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 
 |-  ( ( ( ( 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 
 |-  -. y e. (/)
5 simprr3 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( y e. ( z i^i w ) <-> ( y e. z /\ y e. w ) )
10 9 simplbi2com 
 |-  ( y e. w -> ( y e. z -> y e. ( z i^i w ) ) )
11 8 10 syl 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( E. z e. J ( x e. z /\ -. y e. z ) <-> -. A. z e. J ( x e. z -> y e. z ) )
18 16 17 sylib 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( J e. Haus -> J e. Top )
24 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
25 23 24 sylib 
 |-  ( J e. Haus -> J e. ( TopOn ` U. J ) )
26 ist1-2 
 |-  ( 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 
 |-  ( 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 
 |-  ( J e. Haus -> J e. Fre )