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

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 ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) = ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑧 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( ℎ = 𝐻 → ℎ = 𝐻 )
2 fveq2 ⊢ ( ℎ = 𝐻 → ( ⊥ ‘ ℎ ) = ( ⊥ ‘ 𝐻 ) )
3 2 rexeqdv ⊢ ( ℎ = 𝐻 → ( ∃ 𝑦 ∈ ( ⊥ ‘ ℎ ) 𝑥 = ( 𝑧 +ℎ 𝑦 ) ↔ ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) )
4 1 3 riotaeqbidv ⊢ ( ℎ = 𝐻 → ( ℩ 𝑧 ∈ ℎ ∃ 𝑦 ∈ ( ⊥ ‘ ℎ ) 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) = ( ℩ 𝑧 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) )
5 4 mpteq2dv ⊢ ( ℎ = 𝐻 → ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑧 ∈ ℎ ∃ 𝑦 ∈ ( ⊥ ‘ ℎ ) 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) ) = ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑧 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) ) )
6 df-pjh ⊢ projℎ = ( ℎ ∈ Cℋ ↦ ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑧 ∈ ℎ ∃ 𝑦 ∈ ( ⊥ ‘ ℎ ) 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) ) )
7 ax-hilex ⊢ ℋ ∈ V
8 7 mptex ⊢ ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑧 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) ) ∈ V
9 5 6 8 fvmpt ⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) = ( 𝑥 ∈ ℋ ↦ ( ℩ 𝑧 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝑥 = ( 𝑧 +ℎ 𝑦 ) ) ) )