Metamath Proof Explorer

Theorem ntruni

Description: A union of interiors is a subset of the interior of the union. The reverse inclusion may not hold. (Contributed by Jeff Hankins, 31-Aug-2009)

		Ref	Expression
	Hypothesis	ntruni.1	$⊢ X = ⋃ J$
	Assertion	ntruni	$⊢ (J \in Top \land O \subseteq 𝒫 X) \to ⋃_{o \in O} int (J) (o) \subseteq int (J) (⋃ O)$

Proof

Step	Hyp	Ref	Expression
1		ntruni.1	$⊢ X = ⋃ J$
2		elssuni	$⊢ o \in O \to o \subseteq ⋃ O$
3		sspwuni	$⊢ O \subseteq 𝒫 X \leftrightarrow ⋃ O \subseteq X$
4	1	ntrss	$⊢ (J \in Top \land ⋃ O \subseteq X \land o \subseteq ⋃ O) \to int (J) (o) \subseteq int (J) (⋃ O)$
5	4	3expia	$⊢ (J \in Top \land ⋃ O \subseteq X) \to (o \subseteq ⋃ O \to int (J) (o) \subseteq int (J) (⋃ O))$
6	3 5	sylan2b	$⊢ (J \in Top \land O \subseteq 𝒫 X) \to (o \subseteq ⋃ O \to int (J) (o) \subseteq int (J) (⋃ O))$
7	2 6	syl5	$⊢ (J \in Top \land O \subseteq 𝒫 X) \to (o \in O \to int (J) (o) \subseteq int (J) (⋃ O))$
8	7	ralrimiv	$⊢ (J \in Top \land O \subseteq 𝒫 X) \to \forall o \in O int (J) (o) \subseteq int (J) (⋃ O)$
9		iunss	$⊢ ⋃_{o \in O} int (J) (o) \subseteq int (J) (⋃ O) \leftrightarrow \forall o \in O int (J) (o) \subseteq int (J) (⋃ O)$
10	8 9	sylibr	$⊢ (J \in Top \land O \subseteq 𝒫 X) \to ⋃_{o \in O} int (J) (o) \subseteq int (J) (⋃ O)$