Metamath Proof Explorer

Theorem iirevcn

Description: The reversion function is a continuous map of the unit interval. (Contributed by Mario Carneiro, 6-Jun-2014)

Ref Expression
Assertion iirevcn ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 1 − 𝑥 ) ) ∈ ( II Cn II )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
2 dfii2 ⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
3 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
4 3 a1i ⊢ ( ⊤ → ( 0 [,] 1 ) ⊆ ℝ )
5 iirev ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → ( 1 − 𝑥 ) ∈ ( 0 [,] 1 ) )
6 5 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 1 − 𝑥 ) ∈ ( 0 [,] 1 ) )
7 1 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
8 7 a1i ⊢ ( ⊤ → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
9 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
10 8 8 9 cnmptc ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 1 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
11 8 cnmptid ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
12 1 subcn ⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
13 12 a1i ⊢ ( ⊤ → − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
14 8 10 11 13 cnmpt12f ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( 1 − 𝑥 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
15 1 2 2 4 4 6 14 cnmptre ⊢ ( ⊤ → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 1 − 𝑥 ) ) ∈ ( II Cn II ) )
16 15 mptru ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 1 − 𝑥 ) ) ∈ ( II Cn II )