This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hsupss

Description: Subset relation for supremum of Hilbert space subsets. (Contributed by NM, 24-Nov-2004) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hsupss ⊢ A ⊆ 𝒫 ℋ ∧ B ⊆ 𝒫 ℋ → A ⊆ B → ⋁ ℋ ⁡ A ⊆ ⋁ ℋ ⁡ B

Proof

Step Hyp Ref Expression
1 uniss ⊢ A ⊆ B → ⋃ A ⊆ ⋃ B
2 sspwuni ⊢ A ⊆ 𝒫 ℋ ↔ ⋃ A ⊆ ℋ
3 sspwuni ⊢ B ⊆ 𝒫 ℋ ↔ ⋃ B ⊆ ℋ
4 occon2 ⊢ ⋃ A ⊆ ℋ ∧ ⋃ B ⊆ ℋ → ⋃ A ⊆ ⋃ B → ⊥ ⁡ ⊥ ⁡ ⋃ A ⊆ ⊥ ⁡ ⊥ ⁡ ⋃ B
5 2 3 4 syl2anb ⊢ A ⊆ 𝒫 ℋ ∧ B ⊆ 𝒫 ℋ → ⋃ A ⊆ ⋃ B → ⊥ ⁡ ⊥ ⁡ ⋃ A ⊆ ⊥ ⁡ ⊥ ⁡ ⋃ B
6 1 5 syl5 ⊢ A ⊆ 𝒫 ℋ ∧ B ⊆ 𝒫 ℋ → A ⊆ B → ⊥ ⁡ ⊥ ⁡ ⋃ A ⊆ ⊥ ⁡ ⊥ ⁡ ⋃ B
7 hsupval ⊢ A ⊆ 𝒫 ℋ → ⋁ ℋ ⁡ A = ⊥ ⁡ ⊥ ⁡ ⋃ A
8 7 adantr ⊢ A ⊆ 𝒫 ℋ ∧ B ⊆ 𝒫 ℋ → ⋁ ℋ ⁡ A = ⊥ ⁡ ⊥ ⁡ ⋃ A
9 hsupval ⊢ B ⊆ 𝒫 ℋ → ⋁ ℋ ⁡ B = ⊥ ⁡ ⊥ ⁡ ⋃ B
10 9 adantl ⊢ A ⊆ 𝒫 ℋ ∧ B ⊆ 𝒫 ℋ → ⋁ ℋ ⁡ B = ⊥ ⁡ ⊥ ⁡ ⋃ B
11 8 10 sseq12d ⊢ A ⊆ 𝒫 ℋ ∧ B ⊆ 𝒫 ℋ → ⋁ ℋ ⁡ A ⊆ ⋁ ℋ ⁡ B ↔ ⊥ ⁡ ⊥ ⁡ ⋃ A ⊆ ⊥ ⁡ ⊥ ⁡ ⋃ B
12 6 11 sylibrd ⊢ A ⊆ 𝒫 ℋ ∧ B ⊆ 𝒫 ℋ → A ⊆ B → ⋁ ℋ ⁡ A ⊆ ⋁ ℋ ⁡ B