| Step | Hyp | Ref
| Expression |
| 1 | | hmeoimaf1o.1 |
. 2
⊢ 𝐺 = (𝑥 ∈ 𝐽 ↦ (𝐹 “ 𝑥)) |
| 2 | | hmeoima 23773 |
. 2
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐾) |
| 3 | | hmeocn 23768 |
. . 3
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
| 4 | | cnima 23273 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑦 ∈ 𝐾) → (◡𝐹 “ 𝑦) ∈ 𝐽) |
| 5 | 3, 4 | sylan 580 |
. 2
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑦 ∈ 𝐾) → (◡𝐹 “ 𝑦) ∈ 𝐽) |
| 6 | | eqid 2737 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 7 | | eqid 2737 |
. . . . . . 7
⊢ ∪ 𝐾 =
∪ 𝐾 |
| 8 | 6, 7 | hmeof1o 23772 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹:∪ 𝐽–1-1-onto→∪ 𝐾) |
| 9 | 8 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝐹:∪ 𝐽–1-1-onto→∪ 𝐾) |
| 10 | | f1of1 6847 |
. . . . 5
⊢ (𝐹:∪
𝐽–1-1-onto→∪ 𝐾
→ 𝐹:∪ 𝐽–1-1→∪ 𝐾) |
| 11 | 9, 10 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝐹:∪ 𝐽–1-1→∪ 𝐾) |
| 12 | | elssuni 4937 |
. . . . 5
⊢ (𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽) |
| 13 | 12 | ad2antrl 728 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝑥 ⊆ ∪ 𝐽) |
| 14 | | cnvimass 6100 |
. . . . 5
⊢ (◡𝐹 “ 𝑦) ⊆ dom 𝐹 |
| 15 | | f1dm 6808 |
. . . . . 6
⊢ (𝐹:∪
𝐽–1-1→∪ 𝐾 → dom 𝐹 = ∪ 𝐽) |
| 16 | 11, 15 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → dom 𝐹 = ∪ 𝐽) |
| 17 | 14, 16 | sseqtrid 4026 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (◡𝐹 “ 𝑦) ⊆ ∪ 𝐽) |
| 18 | | f1imaeq 7285 |
. . . 4
⊢ ((𝐹:∪
𝐽–1-1→∪ 𝐾 ∧ (𝑥 ⊆ ∪ 𝐽 ∧ (◡𝐹 “ 𝑦) ⊆ ∪ 𝐽)) → ((𝐹 “ 𝑥) = (𝐹 “ (◡𝐹 “ 𝑦)) ↔ 𝑥 = (◡𝐹 “ 𝑦))) |
| 19 | 11, 13, 17, 18 | syl12anc 837 |
. . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → ((𝐹 “ 𝑥) = (𝐹 “ (◡𝐹 “ 𝑦)) ↔ 𝑥 = (◡𝐹 “ 𝑦))) |
| 20 | | f1ofo 6855 |
. . . . . . 7
⊢ (𝐹:∪
𝐽–1-1-onto→∪ 𝐾
→ 𝐹:∪ 𝐽–onto→∪ 𝐾) |
| 21 | 9, 20 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝐹:∪ 𝐽–onto→∪ 𝐾) |
| 22 | | elssuni 4937 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐾 → 𝑦 ⊆ ∪ 𝐾) |
| 23 | 22 | ad2antll 729 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝑦 ⊆ ∪ 𝐾) |
| 24 | | foimacnv 6865 |
. . . . . 6
⊢ ((𝐹:∪
𝐽–onto→∪ 𝐾 ∧ 𝑦 ⊆ ∪ 𝐾) → (𝐹 “ (◡𝐹 “ 𝑦)) = 𝑦) |
| 25 | 21, 23, 24 | syl2anc 584 |
. . . . 5
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (𝐹 “ (◡𝐹 “ 𝑦)) = 𝑦) |
| 26 | 25 | eqeq2d 2748 |
. . . 4
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → ((𝐹 “ 𝑥) = (𝐹 “ (◡𝐹 “ 𝑦)) ↔ (𝐹 “ 𝑥) = 𝑦)) |
| 27 | | eqcom 2744 |
. . . 4
⊢ ((𝐹 “ 𝑥) = 𝑦 ↔ 𝑦 = (𝐹 “ 𝑥)) |
| 28 | 26, 27 | bitrdi 287 |
. . 3
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → ((𝐹 “ 𝑥) = (𝐹 “ (◡𝐹 “ 𝑦)) ↔ 𝑦 = (𝐹 “ 𝑥))) |
| 29 | 19, 28 | bitr3d 281 |
. 2
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (𝑥 = (◡𝐹 “ 𝑦) ↔ 𝑦 = (𝐹 “ 𝑥))) |
| 30 | 1, 2, 5, 29 | f1o2d 7687 |
1
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐺:𝐽–1-1-onto→𝐾) |