Metamath Proof Explorer


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 ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 𝐵 ) = ( ‘ { 𝐴 , 𝐵 } ) )