Metamath Proof Explorer

Theorem pjhval

Description: Value of a projection. (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion pjhval ⊢ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ H ⁡ A = ι x ∈ H | ∃ y ∈ ⊥ ⁡ H A = x + ℎ y

Proof

Step Hyp Ref Expression
1 pjhfval ⊢ H ∈ C ℋ → proj ℎ ⁡ H = z ∈ ℋ ⟼ ι x ∈ H | ∃ y ∈ ⊥ ⁡ H z = x + ℎ y
2 1 fveq1d ⊢ H ∈ C ℋ → proj ℎ ⁡ H ⁡ A = z ∈ ℋ ⟼ ι x ∈ H | ∃ y ∈ ⊥ ⁡ H z = x + ℎ y ⁡ A
3 eqeq1 ⊢ z = A → z = x + ℎ y ↔ A = x + ℎ y
4 3 rexbidv ⊢ z = A → ∃ y ∈ ⊥ ⁡ H z = x + ℎ y ↔ ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
5 4 riotabidv ⊢ z = A → ι x ∈ H | ∃ y ∈ ⊥ ⁡ H z = x + ℎ y = ι x ∈ H | ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
6 eqid ⊢ z ∈ ℋ ⟼ ι x ∈ H | ∃ y ∈ ⊥ ⁡ H z = x + ℎ y = z ∈ ℋ ⟼ ι x ∈ H | ∃ y ∈ ⊥ ⁡ H z = x + ℎ y
7 riotaex ⊢ ι x ∈ H | ∃ y ∈ ⊥ ⁡ H A = x + ℎ y ∈ V
8 5 6 7 fvmpt ⊢ A ∈ ℋ → z ∈ ℋ ⟼ ι x ∈ H | ∃ y ∈ ⊥ ⁡ H z = x + ℎ y ⁡ A = ι x ∈ H | ∃ y ∈ ⊥ ⁡ H A = x + ℎ y
9 2 8 sylan9eq ⊢ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ H ⁡ A = ι x ∈ H | ∃ y ∈ ⊥ ⁡ H A = x + ℎ y