This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjmfn

Description: Functionality of the projection function. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pjmfn ⊢ proj ℎ Fn C ℋ

Proof

Step Hyp Ref Expression
1 ax-hilex ⊢ ℋ ∈ V
2 1 mptex ⊢ x ∈ ℋ ⟼ ι z ∈ h | ∃ y ∈ ⊥ ⁡ h x = z + ℎ y ∈ V
3 df-pjh ⊢ proj ℎ = h ∈ C ℋ ⟼ x ∈ ℋ ⟼ ι z ∈ h | ∃ y ∈ ⊥ ⁡ h x = z + ℎ y
4 2 3 fnmpti ⊢ proj ℎ Fn C ℋ