Metamath Proof Explorer

Theorem pjhfval

Description: The value of the projection map. (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion pjhfval ⊢ H ∈ C ℋ → proj ℎ ⁡ H = x ∈ ℋ ⟼ ι z ∈ H | ∃ y ∈ ⊥ ⁡ H x = z + ℎ y

Proof

Step Hyp Ref Expression
1 id ⊢ h = H → h = H
2 fveq2 ⊢ h = H → ⊥ ⁡ h = ⊥ ⁡ H
3 2 rexeqdv ⊢ h = H → ∃ y ∈ ⊥ ⁡ h x = z + ℎ y ↔ ∃ y ∈ ⊥ ⁡ H x = z + ℎ y
4 1 3 riotaeqbidv ⊢ h = H → ι z ∈ h | ∃ y ∈ ⊥ ⁡ h x = z + ℎ y = ι z ∈ H | ∃ y ∈ ⊥ ⁡ H x = z + ℎ y
5 4 mpteq2dv ⊢ h = H → x ∈ ℋ ⟼ ι z ∈ h | ∃ y ∈ ⊥ ⁡ h x = z + ℎ y = x ∈ ℋ ⟼ ι z ∈ H | ∃ y ∈ ⊥ ⁡ H x = z + ℎ y
6 df-pjh ⊢ proj ℎ = h ∈ C ℋ ⟼ x ∈ ℋ ⟼ ι z ∈ h | ∃ y ∈ ⊥ ⁡ h x = z + ℎ y
7 ax-hilex ⊢ ℋ ∈ V
8 7 mptex ⊢ x ∈ ℋ ⟼ ι z ∈ H | ∃ y ∈ ⊥ ⁡ H x = z + ℎ y ∈ V
9 5 6 8 fvmpt ⊢ H ∈ C ℋ → proj ℎ ⁡ H = x ∈ ℋ ⟼ ι z ∈ H | ∃ y ∈ ⊥ ⁡ H x = z + ℎ y