Step | Hyp | Ref
| Expression |
1 | | cnptop1 22609 |
. . . 4
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐽 ∈ Top) |
2 | 1 | adantr 482 |
. . 3
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) → 𝐽 ∈ Top) |
3 | | cnptop2 22610 |
. . . 4
⊢ (𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃)) → 𝐿 ∈ Top) |
4 | 3 | adantl 483 |
. . 3
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) → 𝐿 ∈ Top) |
5 | | eqid 2733 |
. . . . 5
⊢ ∪ 𝐽 =
∪ 𝐽 |
6 | 5 | cnprcl 22612 |
. . . 4
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝑃 ∈ ∪ 𝐽) |
7 | 6 | adantr 482 |
. . 3
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) → 𝑃 ∈ ∪ 𝐽) |
8 | 2, 4, 7 | 3jca 1129 |
. 2
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) → (𝐽 ∈ Top ∧ 𝐿 ∈ Top ∧ 𝑃 ∈ ∪ 𝐽)) |
9 | | eqid 2733 |
. . . . . 6
⊢ ∪ 𝐾 =
∪ 𝐾 |
10 | | eqid 2733 |
. . . . . 6
⊢ ∪ 𝐿 =
∪ 𝐿 |
11 | 9, 10 | cnpf 22614 |
. . . . 5
⊢ (𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃)) → 𝐺:∪ 𝐾⟶∪ 𝐿) |
12 | 11 | adantl 483 |
. . . 4
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) → 𝐺:∪ 𝐾⟶∪ 𝐿) |
13 | 5, 9 | cnpf 22614 |
. . . . 5
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
14 | 13 | adantr 482 |
. . . 4
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
15 | | fco 6693 |
. . . 4
⊢ ((𝐺:∪
𝐾⟶∪ 𝐿
∧ 𝐹:∪ 𝐽⟶∪ 𝐾) → (𝐺 ∘ 𝐹):∪ 𝐽⟶∪ 𝐿) |
16 | 12, 14, 15 | syl2anc 585 |
. . 3
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) → (𝐺 ∘ 𝐹):∪ 𝐽⟶∪ 𝐿) |
17 | | simplr 768 |
. . . . . . 7
⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) → 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) |
18 | | simprl 770 |
. . . . . . 7
⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) → 𝑧 ∈ 𝐿) |
19 | | fvco3 6941 |
. . . . . . . . . 10
⊢ ((𝐹:∪
𝐽⟶∪ 𝐾
∧ 𝑃 ∈ ∪ 𝐽)
→ ((𝐺 ∘ 𝐹)‘𝑃) = (𝐺‘(𝐹‘𝑃))) |
20 | 14, 7, 19 | syl2anc 585 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) → ((𝐺 ∘ 𝐹)‘𝑃) = (𝐺‘(𝐹‘𝑃))) |
21 | 20 | adantr 482 |
. . . . . . . 8
⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) → ((𝐺 ∘ 𝐹)‘𝑃) = (𝐺‘(𝐹‘𝑃))) |
22 | | simprr 772 |
. . . . . . . 8
⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) → ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧) |
23 | 21, 22 | eqeltrrd 2835 |
. . . . . . 7
⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) → (𝐺‘(𝐹‘𝑃)) ∈ 𝑧) |
24 | | cnpimaex 22623 |
. . . . . . 7
⊢ ((𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃)) ∧ 𝑧 ∈ 𝐿 ∧ (𝐺‘(𝐹‘𝑃)) ∈ 𝑧) → ∃𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 ∧ (𝐺 “ 𝑦) ⊆ 𝑧)) |
25 | 17, 18, 23, 24 | syl3anc 1372 |
. . . . . 6
⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) → ∃𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 ∧ (𝐺 “ 𝑦) ⊆ 𝑧)) |
26 | | simplll 774 |
. . . . . . . 8
⊢ ((((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((𝐹‘𝑃) ∈ 𝑦 ∧ (𝐺 “ 𝑦) ⊆ 𝑧))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) |
27 | | simprl 770 |
. . . . . . . 8
⊢ ((((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((𝐹‘𝑃) ∈ 𝑦 ∧ (𝐺 “ 𝑦) ⊆ 𝑧))) → 𝑦 ∈ 𝐾) |
28 | | simprrl 780 |
. . . . . . . 8
⊢ ((((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((𝐹‘𝑃) ∈ 𝑦 ∧ (𝐺 “ 𝑦) ⊆ 𝑧))) → (𝐹‘𝑃) ∈ 𝑦) |
29 | | cnpimaex 22623 |
. . . . . . . 8
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝑦 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝑦) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) |
30 | 26, 27, 28, 29 | syl3anc 1372 |
. . . . . . 7
⊢ ((((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((𝐹‘𝑃) ∈ 𝑦 ∧ (𝐺 “ 𝑦) ⊆ 𝑧))) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)) |
31 | | imaco 6204 |
. . . . . . . . . . 11
⊢ ((𝐺 ∘ 𝐹) “ 𝑥) = (𝐺 “ (𝐹 “ 𝑥)) |
32 | | imass2 6055 |
. . . . . . . . . . 11
⊢ ((𝐹 “ 𝑥) ⊆ 𝑦 → (𝐺 “ (𝐹 “ 𝑥)) ⊆ (𝐺 “ 𝑦)) |
33 | 31, 32 | eqsstrid 3993 |
. . . . . . . . . 10
⊢ ((𝐹 “ 𝑥) ⊆ 𝑦 → ((𝐺 ∘ 𝐹) “ 𝑥) ⊆ (𝐺 “ 𝑦)) |
34 | | simprrr 781 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((𝐹‘𝑃) ∈ 𝑦 ∧ (𝐺 “ 𝑦) ⊆ 𝑧))) → (𝐺 “ 𝑦) ⊆ 𝑧) |
35 | | sstr2 3952 |
. . . . . . . . . 10
⊢ (((𝐺 ∘ 𝐹) “ 𝑥) ⊆ (𝐺 “ 𝑦) → ((𝐺 “ 𝑦) ⊆ 𝑧 → ((𝐺 ∘ 𝐹) “ 𝑥) ⊆ 𝑧)) |
36 | 33, 34, 35 | syl2imc 41 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((𝐹‘𝑃) ∈ 𝑦 ∧ (𝐺 “ 𝑦) ⊆ 𝑧))) → ((𝐹 “ 𝑥) ⊆ 𝑦 → ((𝐺 ∘ 𝐹) “ 𝑥) ⊆ 𝑧)) |
37 | 36 | anim2d 613 |
. . . . . . . 8
⊢ ((((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((𝐹‘𝑃) ∈ 𝑦 ∧ (𝐺 “ 𝑦) ⊆ 𝑧))) → ((𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦) → (𝑃 ∈ 𝑥 ∧ ((𝐺 ∘ 𝐹) “ 𝑥) ⊆ 𝑧))) |
38 | 37 | reximdv 3164 |
. . . . . . 7
⊢ ((((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((𝐹‘𝑃) ∈ 𝑦 ∧ (𝐺 “ 𝑦) ⊆ 𝑧))) → (∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ ((𝐺 ∘ 𝐹) “ 𝑥) ⊆ 𝑧))) |
39 | 30, 38 | mpd 15 |
. . . . . 6
⊢ ((((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) ∧ (𝑦 ∈ 𝐾 ∧ ((𝐹‘𝑃) ∈ 𝑦 ∧ (𝐺 “ 𝑦) ⊆ 𝑧))) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ ((𝐺 ∘ 𝐹) “ 𝑥) ⊆ 𝑧)) |
40 | 25, 39 | rexlimddv 3155 |
. . . . 5
⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ (𝑧 ∈ 𝐿 ∧ ((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧)) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ ((𝐺 ∘ 𝐹) “ 𝑥) ⊆ 𝑧)) |
41 | 40 | expr 458 |
. . . 4
⊢ (((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) ∧ 𝑧 ∈ 𝐿) → (((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ ((𝐺 ∘ 𝐹) “ 𝑥) ⊆ 𝑧))) |
42 | 41 | ralrimiva 3140 |
. . 3
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) → ∀𝑧 ∈ 𝐿 (((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ ((𝐺 ∘ 𝐹) “ 𝑥) ⊆ 𝑧))) |
43 | 16, 42 | jca 513 |
. 2
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) → ((𝐺 ∘ 𝐹):∪ 𝐽⟶∪ 𝐿
∧ ∀𝑧 ∈
𝐿 (((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ ((𝐺 ∘ 𝐹) “ 𝑥) ⊆ 𝑧)))) |
44 | 5, 10 | iscnp2 22606 |
. 2
⊢ ((𝐺 ∘ 𝐹) ∈ ((𝐽 CnP 𝐿)‘𝑃) ↔ ((𝐽 ∈ Top ∧ 𝐿 ∈ Top ∧ 𝑃 ∈ ∪ 𝐽) ∧ ((𝐺 ∘ 𝐹):∪ 𝐽⟶∪ 𝐿
∧ ∀𝑧 ∈
𝐿 (((𝐺 ∘ 𝐹)‘𝑃) ∈ 𝑧 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ ((𝐺 ∘ 𝐹) “ 𝑥) ⊆ 𝑧))))) |
45 | 8, 43, 44 | sylanbrc 584 |
1
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) → (𝐺 ∘ 𝐹) ∈ ((𝐽 CnP 𝐿)‘𝑃)) |