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 ∈ Top ∧ O ⊆ 𝒫 X → ⋃ o ∈ O int ⁡ J ⁡ o ⊆ int ⁡ J ⁡ ⋃ O

Proof

Step Hyp Ref Expression
1 ntruni.1 ⊢ X = ⋃ J
2 elssuni ⊢ o ∈ O → o ⊆ ⋃ O
3 sspwuni ⊢ O ⊆ 𝒫 X ↔ ⋃ O ⊆ X
4 1 ntrss ⊢ J ∈ Top ∧ ⋃ O ⊆ X ∧ o ⊆ ⋃ O → int ⁡ J ⁡ o ⊆ int ⁡ J ⁡ ⋃ O
5 4 3expia ⊢ J ∈ Top ∧ ⋃ O ⊆ X → o ⊆ ⋃ O → int ⁡ J ⁡ o ⊆ int ⁡ J ⁡ ⋃ O
6 3 5 sylan2b ⊢ J ∈ Top ∧ O ⊆ 𝒫 X → o ⊆ ⋃ O → int ⁡ J ⁡ o ⊆ int ⁡ J ⁡ ⋃ O
7 2 6 syl5 ⊢ J ∈ Top ∧ O ⊆ 𝒫 X → o ∈ O → int ⁡ J ⁡ o ⊆ int ⁡ J ⁡ ⋃ O
8 7 ralrimiv ⊢ J ∈ Top ∧ O ⊆ 𝒫 X → ∀ o ∈ O int ⁡ J ⁡ o ⊆ int ⁡ J ⁡ ⋃ O
9 iunss ⊢ ⋃ o ∈ O int ⁡ J ⁡ o ⊆ int ⁡ J ⁡ ⋃ O ↔ ∀ o ∈ O int ⁡ J ⁡ o ⊆ int ⁡ J ⁡ ⋃ O
10 8 9 sylibr ⊢ J ∈ Top ∧ O ⊆ 𝒫 X → ⋃ o ∈ O int ⁡ J ⁡ o ⊆ int ⁡ J ⁡ ⋃ O