Metamath Proof Explorer

Theorem hsupval

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 ⊢ A ⊆ 𝒫 ℋ → ⋁ ℋ ⁡ A = ⊥ ⁡ ⊥ ⁡ ⋃ A

Proof

Step Hyp Ref Expression
1 ax-hilex ⊢ ℋ ∈ V
2 1 pwex ⊢ 𝒫 ℋ ∈ V
3 2 elpw2 ⊢ A ∈ 𝒫 𝒫 ℋ ↔ A ⊆ 𝒫 ℋ
4 unieq ⊢ x = A → ⋃ x = ⋃ A
5 4 fveq2d ⊢ x = A → ⊥ ⁡ ⋃ x = ⊥ ⁡ ⋃ A
6 5 fveq2d ⊢ x = A → ⊥ ⁡ ⊥ ⁡ ⋃ x = ⊥ ⁡ ⊥ ⁡ ⋃ A
7 df-chsup ⊢ ⋁ ℋ = x ∈ 𝒫 𝒫 ℋ ⟼ ⊥ ⁡ ⊥ ⁡ ⋃ x
8 fvex ⊢ ⊥ ⁡ ⊥ ⁡ ⋃ A ∈ V
9 6 7 8 fvmpt ⊢ A ∈ 𝒫 𝒫 ℋ → ⋁ ℋ ⁡ A = ⊥ ⁡ ⊥ ⁡ ⋃ A
10 3 9 sylbir ⊢ A ⊆ 𝒫 ℋ → ⋁ ℋ ⁡ A = ⊥ ⁡ ⊥ ⁡ ⋃ A