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

Metamath Proof Explorer

Theorem pjfni

Description: Functionality of a projection. (Contributed by NM, 30-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis pjfn.1 ⊢ H ∈ C ℋ
Assertion pjfni ⊢ proj ℎ ⁡ H Fn ℋ

Proof

Step Hyp Ref Expression
1 pjfn.1 ⊢ H ∈ C ℋ
2 riotaex ⊢ ι y ∈ H | ∃ z ∈ ⊥ ⁡ H x = y + ℎ z ∈ V
3 pjhfval ⊢ H ∈ C ℋ → proj ℎ ⁡ H = x ∈ ℋ ⟼ ι y ∈ H | ∃ z ∈ ⊥ ⁡ H x = y + ℎ z
4 1 3 ax-mp ⊢ proj ℎ ⁡ H = x ∈ ℋ ⟼ ι y ∈ H | ∃ z ∈ ⊥ ⁡ H x = y + ℎ z
5 2 4 fnmpti ⊢ proj ℎ ⁡ H Fn ℋ