Metamath Proof Explorer

Theorem resthaus

Description: A subspace of a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015) (Proof shortened by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Assertion	resthaus	\|- ( ( J e. Haus /\ A e. V ) -> ( J \|`t A ) e. Haus )

Proof

Step	Hyp	Ref	Expression
1		haustop	\|- ( J e. Haus -> J e. Top )
2		cnhaus	\|- ( ( J e. Haus /\ ( _I \|` ( A i^i U. J ) ) : ( A i^i U. J ) -1-1-> ( A i^i U. J ) /\ ( _I \|` ( A i^i U. J ) ) e. ( ( J \|`t A ) Cn J ) ) -> ( J \|`t A ) e. Haus )
3	1 2	resthauslem	\|- ( ( J e. Haus /\ A e. V ) -> ( J \|`t A ) e. Haus )

Step

Hyp

Ref

Expression

haustop

 |-  ( J e. Haus -> J e. Top )

cnhaus

 |-  ( ( J e. Haus /\ ( _I |` ( A i^i U. J ) ) : ( A i^i U. J ) -1-1-> ( A i^i U. J ) /\ ( _I |` ( A i^i U. J ) ) e. ( ( J |`t A ) Cn J ) ) -> ( J |`t A ) e. Haus )

1 2

resthauslem

 |-  ( ( J e. Haus /\ A e. V ) -> ( J |`t A ) e. Haus )