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 ( ( 𝐴 ⊆ 𝒫 ℋ ∧ 𝐵 ⊆ 𝒫 ℋ ) → ( 𝐴 ⊆ 𝐵 → ( ∨ℋ ‘ 𝐴 ) ⊆ ( ∨ℋ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 uniss ⊢ ( 𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵 )
2 sspwuni ⊢ ( 𝐴 ⊆ 𝒫 ℋ ↔ ∪ 𝐴 ⊆ ℋ )
3 sspwuni ⊢ ( 𝐵 ⊆ 𝒫 ℋ ↔ ∪ 𝐵 ⊆ ℋ )
4 occon2 ⊢ ( ( ∪ 𝐴 ⊆ ℋ ∧ ∪ 𝐵 ⊆ ℋ ) → ( ∪ 𝐴 ⊆ ∪ 𝐵 → ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐵 ) ) ) )
5 2 3 4 syl2anb ⊢ ( ( 𝐴 ⊆ 𝒫 ℋ ∧ 𝐵 ⊆ 𝒫 ℋ ) → ( ∪ 𝐴 ⊆ ∪ 𝐵 → ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐵 ) ) ) )
6 1 5 syl5 ⊢ ( ( 𝐴 ⊆ 𝒫 ℋ ∧ 𝐵 ⊆ 𝒫 ℋ ) → ( 𝐴 ⊆ 𝐵 → ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐵 ) ) ) )
7 hsupval ⊢ ( 𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘ 𝐴 ) = ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) )
8 7 adantr ⊢ ( ( 𝐴 ⊆ 𝒫 ℋ ∧ 𝐵 ⊆ 𝒫 ℋ ) → ( ∨ℋ ‘ 𝐴 ) = ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) )
9 hsupval ⊢ ( 𝐵 ⊆ 𝒫 ℋ → ( ∨ℋ ‘ 𝐵 ) = ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐵 ) ) )
10 9 adantl ⊢ ( ( 𝐴 ⊆ 𝒫 ℋ ∧ 𝐵 ⊆ 𝒫 ℋ ) → ( ∨ℋ ‘ 𝐵 ) = ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐵 ) ) )
11 8 10 sseq12d ⊢ ( ( 𝐴 ⊆ 𝒫 ℋ ∧ 𝐵 ⊆ 𝒫 ℋ ) → ( ( ∨ℋ ‘ 𝐴 ) ⊆ ( ∨ℋ ‘ 𝐵 ) ↔ ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐵 ) ) ) )
12 6 11 sylibrd ⊢ ( ( 𝐴 ⊆ 𝒫 ℋ ∧ 𝐵 ⊆ 𝒫 ℋ ) → ( 𝐴 ⊆ 𝐵 → ( ∨ℋ ‘ 𝐴 ) ⊆ ( ∨ℋ ‘ 𝐵 ) ) )