Metamath Proof Explorer
Description: Closure of a projection in its subspace. (Contributed by NM, 30-Oct-1999) (New usage is discouraged.)
|
|
Ref |
Expression |
|
Hypotheses |
pjcli.1 |
⊢ 𝐻 ∈ Cℋ |
|
|
pjcli.2 |
⊢ 𝐴 ∈ ℋ |
|
Assertion |
pjclii |
⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
pjcli.1 |
⊢ 𝐻 ∈ Cℋ |
2 |
|
pjcli.2 |
⊢ 𝐴 ∈ ℋ |
3 |
1
|
pjcli |
⊢ ( 𝐴 ∈ ℋ → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 ) |
4 |
2 3
|
ax-mp |
⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 |