Step | Hyp | Ref
| Expression |
1 | | hmeoimaf1o.1 |
. 2
⊢ 𝐺 = (𝑥 ∈ 𝐽 ↦ (𝐹 “ 𝑥)) |
2 | | hmeoima 22662 |
. 2
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐾) |
3 | | hmeocn 22657 |
. . 3
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
4 | | cnima 22162 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑦 ∈ 𝐾) → (◡𝐹 “ 𝑦) ∈ 𝐽) |
5 | 3, 4 | sylan 583 |
. 2
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑦 ∈ 𝐾) → (◡𝐹 “ 𝑦) ∈ 𝐽) |
6 | | eqid 2737 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
7 | | eqid 2737 |
. . . . . . 7
⊢ ∪ 𝐾 =
∪ 𝐾 |
8 | 6, 7 | hmeof1o 22661 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹:∪ 𝐽–1-1-onto→∪ 𝐾) |
9 | 8 | adantr 484 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝐹:∪ 𝐽–1-1-onto→∪ 𝐾) |
10 | | f1of1 6660 |
. . . . 5
⊢ (𝐹:∪
𝐽–1-1-onto→∪ 𝐾
→ 𝐹:∪ 𝐽–1-1→∪ 𝐾) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝐹:∪ 𝐽–1-1→∪ 𝐾) |
12 | | elssuni 4851 |
. . . . 5
⊢ (𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽) |
13 | 12 | ad2antrl 728 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝑥 ⊆ ∪ 𝐽) |
14 | | cnvimass 5949 |
. . . . 5
⊢ (◡𝐹 “ 𝑦) ⊆ dom 𝐹 |
15 | | f1dm 6619 |
. . . . . 6
⊢ (𝐹:∪
𝐽–1-1→∪ 𝐾 → dom 𝐹 = ∪ 𝐽) |
16 | 11, 15 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → dom 𝐹 = ∪ 𝐽) |
17 | 14, 16 | sseqtrid 3953 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (◡𝐹 “ 𝑦) ⊆ ∪ 𝐽) |
18 | | f1imaeq 7077 |
. . . 4
⊢ ((𝐹:∪
𝐽–1-1→∪ 𝐾 ∧ (𝑥 ⊆ ∪ 𝐽 ∧ (◡𝐹 “ 𝑦) ⊆ ∪ 𝐽)) → ((𝐹 “ 𝑥) = (𝐹 “ (◡𝐹 “ 𝑦)) ↔ 𝑥 = (◡𝐹 “ 𝑦))) |
19 | 11, 13, 17, 18 | syl12anc 837 |
. . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → ((𝐹 “ 𝑥) = (𝐹 “ (◡𝐹 “ 𝑦)) ↔ 𝑥 = (◡𝐹 “ 𝑦))) |
20 | | f1ofo 6668 |
. . . . . . 7
⊢ (𝐹:∪
𝐽–1-1-onto→∪ 𝐾
→ 𝐹:∪ 𝐽–onto→∪ 𝐾) |
21 | 9, 20 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝐹:∪ 𝐽–onto→∪ 𝐾) |
22 | | elssuni 4851 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐾 → 𝑦 ⊆ ∪ 𝐾) |
23 | 22 | ad2antll 729 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝑦 ⊆ ∪ 𝐾) |
24 | | foimacnv 6678 |
. . . . . 6
⊢ ((𝐹:∪
𝐽–onto→∪ 𝐾 ∧ 𝑦 ⊆ ∪ 𝐾) → (𝐹 “ (◡𝐹 “ 𝑦)) = 𝑦) |
25 | 21, 23, 24 | syl2anc 587 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (𝐹 “ (◡𝐹 “ 𝑦)) = 𝑦) |
26 | 25 | eqeq2d 2748 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → ((𝐹 “ 𝑥) = (𝐹 “ (◡𝐹 “ 𝑦)) ↔ (𝐹 “ 𝑥) = 𝑦)) |
27 | | eqcom 2744 |
. . . 4
⊢ ((𝐹 “ 𝑥) = 𝑦 ↔ 𝑦 = (𝐹 “ 𝑥)) |
28 | 26, 27 | bitrdi 290 |
. . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → ((𝐹 “ 𝑥) = (𝐹 “ (◡𝐹 “ 𝑦)) ↔ 𝑦 = (𝐹 “ 𝑥))) |
29 | 19, 28 | bitr3d 284 |
. 2
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (𝑥 = (◡𝐹 “ 𝑦) ↔ 𝑦 = (𝐹 “ 𝑥))) |
30 | 1, 2, 5, 29 | f1o2d 7459 |
1
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐺:𝐽–1-1-onto→𝐾) |