Step | Hyp | Ref
| Expression |
1 | | simplll 794 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → 𝐽 ∈ (TopOn‘𝑋)) |
2 | | simplrl 796 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → 𝐹:𝑋–onto→𝑌) |
3 | | elqtop3 21316 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → ((◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ ((◡𝐺 “ 𝑥) ⊆ 𝑌 ∧ (◡𝐹 “ (◡𝐺 “ 𝑥)) ∈ 𝐽))) |
4 | 1, 2, 3 | syl2anc 691 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → ((◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ ((◡𝐺 “ 𝑥) ⊆ 𝑌 ∧ (◡𝐹 “ (◡𝐺 “ 𝑥)) ∈ 𝐽))) |
5 | | cnvimass 5404 |
. . . . . . . 8
⊢ (◡𝐺 “ 𝑥) ⊆ dom 𝐺 |
6 | | simplrr 797 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → 𝐺:𝑌⟶𝑍) |
7 | | fdm 5964 |
. . . . . . . . 9
⊢ (𝐺:𝑌⟶𝑍 → dom 𝐺 = 𝑌) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → dom 𝐺 = 𝑌) |
9 | 5, 8 | syl5sseq 3616 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → (◡𝐺 “ 𝑥) ⊆ 𝑌) |
10 | 9 | biantrurd 528 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → ((◡𝐹 “ (◡𝐺 “ 𝑥)) ∈ 𝐽 ↔ ((◡𝐺 “ 𝑥) ⊆ 𝑌 ∧ (◡𝐹 “ (◡𝐺 “ 𝑥)) ∈ 𝐽))) |
11 | 4, 10 | bitr4d 270 |
. . . . 5
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → ((◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ (◡𝐹 “ (◡𝐺 “ 𝑥)) ∈ 𝐽)) |
12 | | cnvco 5230 |
. . . . . . . 8
⊢ ◡(𝐺 ∘ 𝐹) = (◡𝐹 ∘ ◡𝐺) |
13 | 12 | imaeq1i 5382 |
. . . . . . 7
⊢ (◡(𝐺 ∘ 𝐹) “ 𝑥) = ((◡𝐹 ∘ ◡𝐺) “ 𝑥) |
14 | | imaco 5557 |
. . . . . . 7
⊢ ((◡𝐹 ∘ ◡𝐺) “ 𝑥) = (◡𝐹 “ (◡𝐺 “ 𝑥)) |
15 | 13, 14 | eqtri 2632 |
. . . . . 6
⊢ (◡(𝐺 ∘ 𝐹) “ 𝑥) = (◡𝐹 “ (◡𝐺 “ 𝑥)) |
16 | 15 | eleq1i 2679 |
. . . . 5
⊢ ((◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽 ↔ (◡𝐹 “ (◡𝐺 “ 𝑥)) ∈ 𝐽) |
17 | 11, 16 | syl6bbr 277 |
. . . 4
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → ((◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ (◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽)) |
18 | 17 | ralbidva 2968 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (∀𝑥 ∈ 𝐾 (◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ ∀𝑥 ∈ 𝐾 (◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽)) |
19 | | simprr 792 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → 𝐺:𝑌⟶𝑍) |
20 | 19 | biantrurd 528 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (∀𝑥 ∈ 𝐾 (◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ (𝐺:𝑌⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹)))) |
21 | | fof 6028 |
. . . . . 6
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
22 | 21 | ad2antrl 760 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → 𝐹:𝑋⟶𝑌) |
23 | | fco 5971 |
. . . . 5
⊢ ((𝐺:𝑌⟶𝑍 ∧ 𝐹:𝑋⟶𝑌) → (𝐺 ∘ 𝐹):𝑋⟶𝑍) |
24 | 19, 22, 23 | syl2anc 691 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (𝐺 ∘ 𝐹):𝑋⟶𝑍) |
25 | 24 | biantrurd 528 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (∀𝑥 ∈ 𝐾 (◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽 ↔ ((𝐺 ∘ 𝐹):𝑋⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽))) |
26 | 18, 20, 25 | 3bitr3d 297 |
. 2
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → ((𝐺:𝑌⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹)) ↔ ((𝐺 ∘ 𝐹):𝑋⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽))) |
27 | | qtoptopon 21317 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
28 | 27 | ad2ant2r 779 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
29 | | simplr 788 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → 𝐾 ∈ (TopOn‘𝑍)) |
30 | | iscn 20849 |
. . 3
⊢ (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘𝑍)) → (𝐺 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ (𝐺:𝑌⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹)))) |
31 | 28, 29, 30 | syl2anc 691 |
. 2
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (𝐺 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ (𝐺:𝑌⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹)))) |
32 | | iscn 20849 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) → ((𝐺 ∘ 𝐹) ∈ (𝐽 Cn 𝐾) ↔ ((𝐺 ∘ 𝐹):𝑋⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽))) |
33 | 32 | adantr 480 |
. 2
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → ((𝐺 ∘ 𝐹) ∈ (𝐽 Cn 𝐾) ↔ ((𝐺 ∘ 𝐹):𝑋⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽))) |
34 | 26, 31, 33 | 3bitr4d 299 |
1
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (𝐺 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ (𝐺 ∘ 𝐹) ∈ (𝐽 Cn 𝐾))) |