Metamath Proof Explorer

Theorem neiuni

Description: The union of the neighborhoods of a set equals the topology's underlying set. (Contributed by FL, 18-Sep-2007) (Revised by Mario Carneiro, 9-Apr-2015)

		Ref	Expression
	Hypothesis	tpnei.1	$⊢ X = ⋃ J$
	Assertion	neiuni	$⊢ (J \in Top \land S \subseteq X) \to X = ⋃ nei (J) (S)$

Proof

Step	Hyp	Ref	Expression
1		tpnei.1	$⊢ X = ⋃ J$
2	1	tpnei	$⊢ J \in Top \to (S \subseteq X \leftrightarrow X \in nei (J) (S))$
3	2	biimpa	$⊢ (J \in Top \land S \subseteq X) \to X \in nei (J) (S)$
4		elssuni	$⊢ X \in nei (J) (S) \to X \subseteq ⋃ nei (J) (S)$
5	3 4	syl	$⊢ (J \in Top \land S \subseteq X) \to X \subseteq ⋃ nei (J) (S)$
6	1	neii1	$⊢ (J \in Top \land x \in nei (J) (S)) \to x \subseteq X$
7	6	ex	$⊢ J \in Top \to (x \in nei (J) (S) \to x \subseteq X)$
8	7	adantr	$⊢ (J \in Top \land S \subseteq X) \to (x \in nei (J) (S) \to x \subseteq X)$
9	8	ralrimiv	$⊢ (J \in Top \land S \subseteq X) \to \forall x \in nei (J) (S) x \subseteq X$
10		unissb	$⊢ ⋃ nei (J) (S) \subseteq X \leftrightarrow \forall x \in nei (J) (S) x \subseteq X$
11	9 10	sylibr	$⊢ (J \in Top \land S \subseteq X) \to ⋃ nei (J) (S) \subseteq X$
12	5 11	eqssd	$⊢ (J \in Top \land S \subseteq X) \to X = ⋃ nei (J) (S)$