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