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	$⊢ H \in C_{ℋ} \to {proj}_{ℎ} (H) = (x \in ℋ ⟼ (ι z \in H \| \exists y \in ⊥ (H) x = z +_{ℎ} y))$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ h = H \to h = H$
2		fveq2	$⊢ h = H \to ⊥ (h) = ⊥ (H)$
3	2	rexeqdv	$⊢ h = H \to (\exists y \in ⊥ (h) x = z +_{ℎ} y \leftrightarrow \exists y \in ⊥ (H) x = z +_{ℎ} y)$
4	1 3	riotaeqbidv	$⊢ h = H \to (ι z \in h \| \exists y \in ⊥ (h) x = z +_{ℎ} y) = (ι z \in H \| \exists y \in ⊥ (H) x = z +_{ℎ} y)$
5	4	mpteq2dv	$⊢ h = H \to (x \in ℋ ⟼ (ι z \in h \| \exists y \in ⊥ (h) x = z +_{ℎ} y)) = (x \in ℋ ⟼ (ι z \in H \| \exists y \in ⊥ (H) x = z +_{ℎ} y))$
6		df-pjh	$⊢ {proj}_{ℎ} = (h \in C_{ℋ} ⟼ (x \in ℋ ⟼ (ι z \in h \| \exists y \in ⊥ (h) x = z +_{ℎ} y)))$
7		ax-hilex	$⊢ ℋ \in V$
8	7	mptex	$⊢ (x \in ℋ ⟼ (ι z \in H \| \exists y \in ⊥ (H) x = z +_{ℎ} y)) \in V$
9	5 6 8	fvmpt	$⊢ H \in C_{ℋ} \to {proj}_{ℎ} (H) = (x \in ℋ ⟼ (ι z \in H \| \exists y \in ⊥ (H) x = z +_{ℎ} y))$