Step | Hyp | Ref
| Expression |
1 | | simplll 798 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → 𝐽 ∈ (TopOn‘𝑋)) |
2 | | simplrl 800 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → 𝐹:𝑋–onto→𝑌) |
3 | | elqtop3 21506 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → ((◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ ((◡𝐺 “ 𝑥) ⊆ 𝑌 ∧ (◡𝐹 “ (◡𝐺 “ 𝑥)) ∈ 𝐽))) |
4 | 1, 2, 3 | syl2anc 693 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → ((◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ ((◡𝐺 “ 𝑥) ⊆ 𝑌 ∧ (◡𝐹 “ (◡𝐺 “ 𝑥)) ∈ 𝐽))) |
5 | | cnvimass 5485 |
. . . . . . . 8
⊢ (◡𝐺 “ 𝑥) ⊆ dom 𝐺 |
6 | | simplrr 801 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → 𝐺:𝑌⟶𝑍) |
7 | | fdm 6051 |
. . . . . . . . 9
⊢ (𝐺:𝑌⟶𝑍 → dom 𝐺 = 𝑌) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → dom 𝐺 = 𝑌) |
9 | 5, 8 | syl5sseq 3653 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → (◡𝐺 “ 𝑥) ⊆ 𝑌) |
10 | 9 | biantrurd 529 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → ((◡𝐹 “ (◡𝐺 “ 𝑥)) ∈ 𝐽 ↔ ((◡𝐺 “ 𝑥) ⊆ 𝑌 ∧ (◡𝐹 “ (◡𝐺 “ 𝑥)) ∈ 𝐽))) |
11 | 4, 10 | bitr4d 271 |
. . . . 5
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → ((◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ (◡𝐹 “ (◡𝐺 “ 𝑥)) ∈ 𝐽)) |
12 | | cnvco 5308 |
. . . . . . . 8
⊢ ◡(𝐺 ∘ 𝐹) = (◡𝐹 ∘ ◡𝐺) |
13 | 12 | imaeq1i 5463 |
. . . . . . 7
⊢ (◡(𝐺 ∘ 𝐹) “ 𝑥) = ((◡𝐹 ∘ ◡𝐺) “ 𝑥) |
14 | | imaco 5640 |
. . . . . . 7
⊢ ((◡𝐹 ∘ ◡𝐺) “ 𝑥) = (◡𝐹 “ (◡𝐺 “ 𝑥)) |
15 | 13, 14 | eqtri 2644 |
. . . . . 6
⊢ (◡(𝐺 ∘ 𝐹) “ 𝑥) = (◡𝐹 “ (◡𝐺 “ 𝑥)) |
16 | 15 | eleq1i 2692 |
. . . . 5
⊢ ((◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽 ↔ (◡𝐹 “ (◡𝐺 “ 𝑥)) ∈ 𝐽) |
17 | 11, 16 | syl6bbr 278 |
. . . 4
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) ∧ 𝑥 ∈ 𝐾) → ((◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ (◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽)) |
18 | 17 | ralbidva 2985 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (∀𝑥 ∈ 𝐾 (◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ ∀𝑥 ∈ 𝐾 (◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽)) |
19 | | simprr 796 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → 𝐺:𝑌⟶𝑍) |
20 | 19 | biantrurd 529 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (∀𝑥 ∈ 𝐾 (◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹) ↔ (𝐺:𝑌⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹)))) |
21 | | fof 6115 |
. . . . . 6
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
22 | 21 | ad2antrl 764 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → 𝐹:𝑋⟶𝑌) |
23 | | fco 6058 |
. . . . 5
⊢ ((𝐺:𝑌⟶𝑍 ∧ 𝐹:𝑋⟶𝑌) → (𝐺 ∘ 𝐹):𝑋⟶𝑍) |
24 | 19, 22, 23 | syl2anc 693 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (𝐺 ∘ 𝐹):𝑋⟶𝑍) |
25 | 24 | biantrurd 529 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (∀𝑥 ∈ 𝐾 (◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽 ↔ ((𝐺 ∘ 𝐹):𝑋⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽))) |
26 | 18, 20, 25 | 3bitr3d 298 |
. 2
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → ((𝐺:𝑌⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹)) ↔ ((𝐺 ∘ 𝐹):𝑋⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽))) |
27 | | qtoptopon 21507 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
28 | 27 | ad2ant2r 783 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
29 | | simplr 792 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → 𝐾 ∈ (TopOn‘𝑍)) |
30 | | iscn 21039 |
. . 3
⊢ (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘𝑍)) → (𝐺 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ (𝐺:𝑌⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹)))) |
31 | 28, 29, 30 | syl2anc 693 |
. 2
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (𝐺 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ (𝐺:𝑌⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡𝐺 “ 𝑥) ∈ (𝐽 qTop 𝐹)))) |
32 | | iscn 21039 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) → ((𝐺 ∘ 𝐹) ∈ (𝐽 Cn 𝐾) ↔ ((𝐺 ∘ 𝐹):𝑋⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽))) |
33 | 32 | adantr 481 |
. 2
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → ((𝐺 ∘ 𝐹) ∈ (𝐽 Cn 𝐾) ↔ ((𝐺 ∘ 𝐹):𝑋⟶𝑍 ∧ ∀𝑥 ∈ 𝐾 (◡(𝐺 ∘ 𝐹) “ 𝑥) ∈ 𝐽))) |
34 | 26, 31, 33 | 3bitr4d 300 |
1
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (𝐺 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ (𝐺 ∘ 𝐹) ∈ (𝐽 Cn 𝐾))) |