Step |
Hyp |
Ref |
Expression |
1 |
|
ismtyhmeo.1 |
⊢ 𝐽 = ( MetOpen ‘ 𝑀 ) |
2 |
|
ismtyhmeo.2 |
⊢ 𝐾 = ( MetOpen ‘ 𝑁 ) |
3 |
|
simpll |
⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ) |
4 |
|
simplr |
⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) ) → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) |
5 |
|
simpr |
⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) ) → 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) ) |
6 |
1 2 3 4 5
|
ismtyhmeolem |
⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) ) → 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) |
7 |
|
ismtycnv |
⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) → ◡ 𝑓 ∈ ( 𝑁 Ismty 𝑀 ) ) ) |
8 |
7
|
imp |
⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) ) → ◡ 𝑓 ∈ ( 𝑁 Ismty 𝑀 ) ) |
9 |
2 1 4 3 8
|
ismtyhmeolem |
⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) ) → ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) ) |
10 |
|
ishmeo |
⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ↔ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∧ ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) ) ) |
11 |
6 9 10
|
sylanbrc |
⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) ) → 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) |
12 |
11
|
ex |
⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝑓 ∈ ( 𝑀 Ismty 𝑁 ) → 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ) ) |
13 |
12
|
ssrdv |
⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑁 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝑀 Ismty 𝑁 ) ⊆ ( 𝐽 Homeo 𝐾 ) ) |