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	⊢ 𝑋 = ∪ 𝐽
Assertion	ntruni	⊢ ( ( 𝐽 ∈ Top ∧ 𝑂 ⊆ 𝒫 𝑋 ) → ∪ 𝑜 ∈ 𝑂 ( ( int ‘ 𝐽 ) ‘ 𝑜 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		ntruni.1	⊢ 𝑋 = ∪ 𝐽
2		elssuni	⊢ ( 𝑜 ∈ 𝑂 → 𝑜 ⊆ ∪ 𝑂 )
3		sspwuni	⊢ ( 𝑂 ⊆ 𝒫 𝑋 ↔ ∪ 𝑂 ⊆ 𝑋 )
4	1	ntrss	⊢ ( ( 𝐽 ∈ Top ∧ ∪ 𝑂 ⊆ 𝑋 ∧ 𝑜 ⊆ ∪ 𝑂 ) → ( ( int ‘ 𝐽 ) ‘ 𝑜 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ 𝑂 ) )
5	4	3expia	⊢ ( ( 𝐽 ∈ Top ∧ ∪ 𝑂 ⊆ 𝑋 ) → ( 𝑜 ⊆ ∪ 𝑂 → ( ( int ‘ 𝐽 ) ‘ 𝑜 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ 𝑂 ) ) )
6	3 5	sylan2b	⊢ ( ( 𝐽 ∈ Top ∧ 𝑂 ⊆ 𝒫 𝑋 ) → ( 𝑜 ⊆ ∪ 𝑂 → ( ( int ‘ 𝐽 ) ‘ 𝑜 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ 𝑂 ) ) )
7	2 6	syl5	⊢ ( ( 𝐽 ∈ Top ∧ 𝑂 ⊆ 𝒫 𝑋 ) → ( 𝑜 ∈ 𝑂 → ( ( int ‘ 𝐽 ) ‘ 𝑜 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ 𝑂 ) ) )
8	7	ralrimiv	⊢ ( ( 𝐽 ∈ Top ∧ 𝑂 ⊆ 𝒫 𝑋 ) → ∀ 𝑜 ∈ 𝑂 ( ( int ‘ 𝐽 ) ‘ 𝑜 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ 𝑂 ) )
9		iunss	⊢ ( ∪ 𝑜 ∈ 𝑂 ( ( int ‘ 𝐽 ) ‘ 𝑜 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ 𝑂 ) ↔ ∀ 𝑜 ∈ 𝑂 ( ( int ‘ 𝐽 ) ‘ 𝑜 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ 𝑂 ) )
10	8 9	sylibr	⊢ ( ( 𝐽 ∈ Top ∧ 𝑂 ⊆ 𝒫 𝑋 ) → ∪ 𝑜 ∈ 𝑂 ( ( int ‘ 𝐽 ) ‘ 𝑜 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ∪ 𝑂 ) )