Metamath Proof Explorer

Theorem rest0

Description: The subspace topology induced by the topology J on the empty set. (Contributed by FL, 22-Dec-2008) (Revised by Mario Carneiro, 1-May-2015)

		Ref	Expression
	Assertion	rest0	$⊢ J \in Top \to J ↾_{𝑡} \emptyset = \{\emptyset\}$

Proof

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		restval	$⊢ (J \in Top \land \emptyset \in V) \to J ↾_{𝑡} \emptyset = ran (x \in J ⟼ x \cap \emptyset)$
3	1 2	mpan2	$⊢ J \in Top \to J ↾_{𝑡} \emptyset = ran (x \in J ⟼ x \cap \emptyset)$
4		in0	$⊢ x \cap \emptyset = \emptyset$
5	1	elsn2	$⊢ x \cap \emptyset \in \{\emptyset\} \leftrightarrow x \cap \emptyset = \emptyset$
6	4 5	mpbir	$⊢ x \cap \emptyset \in \{\emptyset\}$
7	6	a1i	$⊢ (J \in Top \land x \in J) \to x \cap \emptyset \in \{\emptyset\}$
8	7	fmpttd	$⊢ J \in Top \to (x \in J ⟼ x \cap \emptyset) : J ⟶ \{\emptyset\}$
9	8	frnd	$⊢ J \in Top \to ran (x \in J ⟼ x \cap \emptyset) \subseteq \{\emptyset\}$
10	3 9	eqsstrd	$⊢ J \in Top \to J ↾_{𝑡} \emptyset \subseteq \{\emptyset\}$
11		resttop	$⊢ (J \in Top \land \emptyset \in V) \to J ↾_{𝑡} \emptyset \in Top$
12	1 11	mpan2	$⊢ J \in Top \to J ↾_{𝑡} \emptyset \in Top$
13		0opn	$⊢ J ↾_{𝑡} \emptyset \in Top \to \emptyset \in (J ↾_{𝑡} \emptyset)$
14	12 13	syl	$⊢ J \in Top \to \emptyset \in (J ↾_{𝑡} \emptyset)$
15	14	snssd	$⊢ J \in Top \to \{\emptyset\} \subseteq J ↾_{𝑡} \emptyset$
16	10 15	eqssd	$⊢ J \in Top \to J ↾_{𝑡} \emptyset = \{\emptyset\}$