Description: The identity function is a homeomorphism. (Contributed by FL, 14-Feb-2007) (Proof shortened by Mario Carneiro, 23-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | idhmeo | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( I ↾ 𝑋 ) ∈ ( 𝐽 Homeo 𝐽 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | idcn | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐽 ) ) | |
| 2 | cnvresid | ⊢ ◡ ( I ↾ 𝑋 ) = ( I ↾ 𝑋 ) | |
| 3 | 2 1 | eqeltrid | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ◡ ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐽 ) ) |
| 4 | ishmeo | ⊢ ( ( I ↾ 𝑋 ) ∈ ( 𝐽 Homeo 𝐽 ) ↔ ( ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐽 ) ∧ ◡ ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐽 ) ) ) | |
| 5 | 1 3 4 | sylanbrc | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( I ↾ 𝑋 ) ∈ ( 𝐽 Homeo 𝐽 ) ) |