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