Theorem sshjval3

Description: Value of join for subsets of Hilbert space in terms of supremum: the join is the supremum of its two arguments. Based on the definition of join in Beran p. 3. For later convenience we prove a general version that works for any subset of Hilbert space, not just the elements of the lattice CH . (Contributed by NM, 2-Mar-2004) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	sshjval3	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = ( ∨ℋ ‘ { 𝐴 , 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	⊢ ℋ ∈ V
2	1	elpw2	⊢ ( 𝐴 ∈ 𝒫 ℋ ↔ 𝐴 ⊆ ℋ )
3	1	elpw2	⊢ ( 𝐵 ∈ 𝒫 ℋ ↔ 𝐵 ⊆ ℋ )
4		uniprg	⊢ ( ( 𝐴 ∈ 𝒫 ℋ ∧ 𝐵 ∈ 𝒫 ℋ ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
5	2 3 4	syl2anbr	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
6	5	fveq2d	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( ⊥ ‘ ∪ { 𝐴 , 𝐵 } ) = ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) )
7	6	fveq2d	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( ⊥ ‘ ( ⊥ ‘ ∪ { 𝐴 , 𝐵 } ) ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
8		prssi	⊢ ( ( 𝐴 ∈ 𝒫 ℋ ∧ 𝐵 ∈ 𝒫 ℋ ) → { 𝐴 , 𝐵 } ⊆ 𝒫 ℋ )
9	2 3 8	syl2anbr	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → { 𝐴 , 𝐵 } ⊆ 𝒫 ℋ )
10		hsupval	⊢ ( { 𝐴 , 𝐵 } ⊆ 𝒫 ℋ → ( ∨ℋ ‘ { 𝐴 , 𝐵 } ) = ( ⊥ ‘ ( ⊥ ‘ ∪ { 𝐴 , 𝐵 } ) ) )
11	9 10	syl	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( ∨ℋ ‘ { 𝐴 , 𝐵 } ) = ( ⊥ ‘ ( ⊥ ‘ ∪ { 𝐴 , 𝐵 } ) ) )
12		sshjval	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
13	7 11 12	3eqtr4rd	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = ( ∨ℋ ‘ { 𝐴 , 𝐵 } ) )