Metamath Proof Explorer
Description: A restricted identity function is a continuous function. (Contributed by FL, 27-Dec-2006) (Proof shortened by Mario Carneiro, 21-Mar-2015)
|
|
Ref |
Expression |
|
Assertion |
idcn |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐽 ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ssid |
⊢ 𝐽 ⊆ 𝐽 |
| 2 |
|
ssidcn |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐽 ) ↔ 𝐽 ⊆ 𝐽 ) ) |
| 3 |
2
|
anidms |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐽 ) ↔ 𝐽 ⊆ 𝐽 ) ) |
| 4 |
1 3
|
mpbiri |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐽 ) ) |