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 ⊢ ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑧 ∈ ℎ ∃ 𝑦 ∈ ( ⊥ ‘ ℎ ) 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) ) ∈ V
3 df-pjh ⊢ projℎ = ( ℎ ∈ Cℋ ↦ ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑧 ∈ ℎ ∃ 𝑦 ∈ ( ⊥ ‘ ℎ ) 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) ) )
4 2 3 fnmpti ⊢ projℎ Fn Cℋ