Metamath Proof Explorer

Theorem pjch1

Description: Property of identity projection. Remark in Beran p. 111. (Contributed by NM, 28-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion pjch1 ⊢ A ∈ ℋ → proj ℎ ⁡ ℋ ⁡ A = A

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A ∈ ℋ ↔ if A ∈ ℋ A 0 ℎ ∈ ℋ
2 fveq2 ⊢ A = if A ∈ ℋ A 0 ℎ → proj ℎ ⁡ ℋ ⁡ A = proj ℎ ⁡ ℋ ⁡ if A ∈ ℋ A 0 ℎ
3 id ⊢ A = if A ∈ ℋ A 0 ℎ → A = if A ∈ ℋ A 0 ℎ
4 2 3 eqeq12d ⊢ A = if A ∈ ℋ A 0 ℎ → proj ℎ ⁡ ℋ ⁡ A = A ↔ proj ℎ ⁡ ℋ ⁡ if A ∈ ℋ A 0 ℎ = if A ∈ ℋ A 0 ℎ
5 1 4 bibi12d ⊢ A = if A ∈ ℋ A 0 ℎ → A ∈ ℋ ↔ proj ℎ ⁡ ℋ ⁡ A = A ↔ if A ∈ ℋ A 0 ℎ ∈ ℋ ↔ proj ℎ ⁡ ℋ ⁡ if A ∈ ℋ A 0 ℎ = if A ∈ ℋ A 0 ℎ
6 helch ⊢ ℋ ∈ C ℋ
7 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
8 6 7 pjchi ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ ↔ proj ℎ ⁡ ℋ ⁡ if A ∈ ℋ A 0 ℎ = if A ∈ ℋ A 0 ℎ
9 5 8 dedth ⊢ A ∈ ℋ → A ∈ ℋ ↔ proj ℎ ⁡ ℋ ⁡ A = A
10 9 ibi ⊢ A ∈ ℋ → proj ℎ ⁡ ℋ ⁡ A = A