Metamath Proof Explorer
Description: The mapping of a projection. (Contributed by NM, 11-Nov-2000)
(New usage is discouraged.)
|
|
Ref |
Expression |
|
Hypothesis |
pjfn.1 |
⊢ 𝐻 ∈ Cℋ |
|
Assertion |
pjfi |
⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pjfn.1 |
⊢ 𝐻 ∈ Cℋ |
| 2 |
1
|
pjfni |
⊢ ( projℎ ‘ 𝐻 ) Fn ℋ |
| 3 |
1
|
pjrni |
⊢ ran ( projℎ ‘ 𝐻 ) = 𝐻 |
| 4 |
1
|
chssii |
⊢ 𝐻 ⊆ ℋ |
| 5 |
3 4
|
eqsstri |
⊢ ran ( projℎ ‘ 𝐻 ) ⊆ ℋ |
| 6 |
|
df-f |
⊢ ( ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ ↔ ( ( projℎ ‘ 𝐻 ) Fn ℋ ∧ ran ( projℎ ‘ 𝐻 ) ⊆ ℋ ) ) |
| 7 |
2 5 6
|
mpbir2an |
⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ |