Metamath Proof Explorer

Theorem tgdif0

Description: A generated topology is not affected by the addition or removal of the empty set from the base. (Contributed by Mario Carneiro, 28-Aug-2015)

		Ref	Expression
	Assertion	tgdif0	$⊢ topGen (B ∖ \{\emptyset\}) = topGen (B)$

Proof

Step	Hyp	Ref	Expression
1		indif1	$⊢ (B ∖ \{\emptyset\}) \cap 𝒫 x = (B \cap 𝒫 x) ∖ \{\emptyset\}$
2	1	unieqi	$⊢ ⋃ ((B ∖ \{\emptyset\}) \cap 𝒫 x) = ⋃ ((B \cap 𝒫 x) ∖ \{\emptyset\})$
3		unidif0	$⊢ ⋃ ((B \cap 𝒫 x) ∖ \{\emptyset\}) = ⋃ (B \cap 𝒫 x)$
4	2 3	eqtri	$⊢ ⋃ ((B ∖ \{\emptyset\}) \cap 𝒫 x) = ⋃ (B \cap 𝒫 x)$
5	4	sseq2i	$⊢ x \subseteq ⋃ ((B ∖ \{\emptyset\}) \cap 𝒫 x) \leftrightarrow x \subseteq ⋃ (B \cap 𝒫 x)$
6	5	abbii	$⊢ \{x \| x \subseteq ⋃ ((B ∖ \{\emptyset\}) \cap 𝒫 x)\} = \{x \| x \subseteq ⋃ (B \cap 𝒫 x)\}$
7		difexg	$⊢ B \in V \to B ∖ \{\emptyset\} \in V$
8		tgval	$⊢ B ∖ \{\emptyset\} \in V \to topGen (B ∖ \{\emptyset\}) = \{x \| x \subseteq ⋃ ((B ∖ \{\emptyset\}) \cap 𝒫 x)\}$
9	7 8	syl	$⊢ B \in V \to topGen (B ∖ \{\emptyset\}) = \{x \| x \subseteq ⋃ ((B ∖ \{\emptyset\}) \cap 𝒫 x)\}$
10		tgval	$⊢ B \in V \to topGen (B) = \{x \| x \subseteq ⋃ (B \cap 𝒫 x)\}$
11	6 9 10	3eqtr4a	$⊢ B \in V \to topGen (B ∖ \{\emptyset\}) = topGen (B)$
12		difsnexi	$⊢ B ∖ \{\emptyset\} \in V \to B \in V$
13		fvprc	$⊢ \neg B ∖ \{\emptyset\} \in V \to topGen (B ∖ \{\emptyset\}) = \emptyset$
14	12 13	nsyl5	$⊢ \neg B \in V \to topGen (B ∖ \{\emptyset\}) = \emptyset$
15		fvprc	$⊢ \neg B \in V \to topGen (B) = \emptyset$
16	14 15	eqtr4d	$⊢ \neg B \in V \to topGen (B ∖ \{\emptyset\}) = topGen (B)$
17	11 16	pm2.61i	$⊢ topGen (B ∖ \{\emptyset\}) = topGen (B)$