Metamath Proof Explorer

Theorem uniopn

Description: The union of a subset of a topology (that is, the union of any family of open sets of a topology) is an open set. (Contributed by Stefan Allan, 27-Feb-2006)

		Ref	Expression
	Assertion	uniopn	$⊢ (J \in Top \land A \subseteq J) \to ⋃ A \in J$

Proof

Step	Hyp	Ref	Expression
1		istopg	$⊢ J \in Top \to (J \in Top \leftrightarrow (\forall x (x \subseteq J \to ⋃ x \in J) \land \forall x \in J \forall y \in J x \cap y \in J))$
2	1	ibi	$⊢ J \in Top \to (\forall x (x \subseteq J \to ⋃ x \in J) \land \forall x \in J \forall y \in J x \cap y \in J)$
3	2	simpld	$⊢ J \in Top \to \forall x (x \subseteq J \to ⋃ x \in J)$
4		elpw2g	$⊢ J \in Top \to (A \in 𝒫 J \leftrightarrow A \subseteq J)$
5	4	biimpar	$⊢ (J \in Top \land A \subseteq J) \to A \in 𝒫 J$
6		sseq1	$⊢ x = A \to (x \subseteq J \leftrightarrow A \subseteq J)$
7		unieq	$⊢ x = A \to ⋃ x = ⋃ A$
8	7	eleq1d	$⊢ x = A \to (⋃ x \in J \leftrightarrow ⋃ A \in J)$
9	6 8	imbi12d	$⊢ x = A \to ((x \subseteq J \to ⋃ x \in J) \leftrightarrow (A \subseteq J \to ⋃ A \in J))$
10	9	spcgv	$⊢ A \in 𝒫 J \to (\forall x (x \subseteq J \to ⋃ x \in J) \to (A \subseteq J \to ⋃ A \in J))$
11	5 10	syl	$⊢ (J \in Top \land A \subseteq J) \to (\forall x (x \subseteq J \to ⋃ x \in J) \to (A \subseteq J \to ⋃ A \in J))$
12	11	com23	$⊢ (J \in Top \land A \subseteq J) \to (A \subseteq J \to (\forall x (x \subseteq J \to ⋃ x \in J) \to ⋃ A \in J))$
13	12	ex	$⊢ J \in Top \to (A \subseteq J \to (A \subseteq J \to (\forall x (x \subseteq J \to ⋃ x \in J) \to ⋃ A \in J)))$
14	13	pm2.43d	$⊢ J \in Top \to (A \subseteq J \to (\forall x (x \subseteq J \to ⋃ x \in J) \to ⋃ A \in J))$
15	3 14	mpid	$⊢ J \in Top \to (A \subseteq J \to ⋃ A \in J)$
16	15	imp	$⊢ (J \in Top \land A \subseteq J) \to ⋃ A \in J$