Description: Value of supremum of set of subsets of Hilbert space. For an alternate version of the value, see hsupval2 . (Contributed by NM, 9-Dec-2003) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | hsupval | ⊢ ( 𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘ 𝐴 ) = ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-hilex | ⊢ ℋ ∈ V | |
| 2 | 1 | pwex | ⊢ 𝒫 ℋ ∈ V |
| 3 | 2 | elpw2 | ⊢ ( 𝐴 ∈ 𝒫 𝒫 ℋ ↔ 𝐴 ⊆ 𝒫 ℋ ) |
| 4 | unieq | ⊢ ( 𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴 ) | |
| 5 | 4 | fveq2d | ⊢ ( 𝑥 = 𝐴 → ( ⊥ ‘ ∪ 𝑥 ) = ( ⊥ ‘ ∪ 𝐴 ) ) |
| 6 | 5 | fveq2d | ⊢ ( 𝑥 = 𝐴 → ( ⊥ ‘ ( ⊥ ‘ ∪ 𝑥 ) ) = ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) ) |
| 7 | df-chsup | ⊢ ∨ℋ = ( 𝑥 ∈ 𝒫 𝒫 ℋ ↦ ( ⊥ ‘ ( ⊥ ‘ ∪ 𝑥 ) ) ) | |
| 8 | fvex | ⊢ ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) ∈ V | |
| 9 | 6 7 8 | fvmpt | ⊢ ( 𝐴 ∈ 𝒫 𝒫 ℋ → ( ∨ℋ ‘ 𝐴 ) = ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) ) |
| 10 | 3 9 | sylbir | ⊢ ( 𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘ 𝐴 ) = ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) ) |