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 ⊢ 𝐻 ∈ Cℋ
Assertion pjfni ( projℎ ‘ 𝐻 ) Fn ℋ

Proof

Step Hyp Ref Expression
1 pjfn.1 ⊢ 𝐻 ∈ Cℋ
2 riotaex ⊢ ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑧 ∈ ( ⊥ ‘ 𝐻 ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) ∈ V
3 pjhfval ⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) = ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑧 ∈ ( ⊥ ‘ 𝐻 ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) ) )
4 1 3 ax-mp ⊢ ( projℎ ‘ 𝐻 ) = ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑧 ∈ ( ⊥ ‘ 𝐻 ) 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) )
5 2 4 fnmpti ⊢ ( projℎ ‘ 𝐻 ) Fn ℋ