| Step | Hyp | Ref
| Expression |
| 1 | | lmcnp.4 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝑃)) |
| 2 | | eqid 2737 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 3 | | eqid 2737 |
. . . . . . 7
⊢ ∪ 𝐾 =
∪ 𝐾 |
| 4 | 2, 3 | cnpf 23255 |
. . . . . 6
⊢ (𝐺 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐺:∪ 𝐽⟶∪ 𝐾) |
| 5 | 1, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐺:∪ 𝐽⟶∪ 𝐾) |
| 6 | | lmcnp.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) |
| 7 | | cnptop1 23250 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐽 ∈ Top) |
| 8 | 1, 7 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ Top) |
| 9 | | toptopon2 22924 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
| 10 | 8, 9 | sylib 218 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
| 11 | | nnuz 12921 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
| 12 | | 1zzd 12648 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℤ) |
| 13 | 10, 11, 12 | lmbr2 23267 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (∪ 𝐽 ↑pm ℂ)
∧ 𝑃 ∈ ∪ 𝐽
∧ ∀𝑣 ∈
𝐽 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣))))) |
| 14 | 6, 13 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∈ (∪ 𝐽 ↑pm ℂ)
∧ 𝑃 ∈ ∪ 𝐽
∧ ∀𝑣 ∈
𝐽 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣)))) |
| 15 | 14 | simp1d 1143 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (∪ 𝐽 ↑pm
ℂ)) |
| 16 | 8 | uniexd 7762 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝐽
∈ V) |
| 17 | | cnex 11236 |
. . . . . . . 8
⊢ ℂ
∈ V |
| 18 | | elpm2g 8884 |
. . . . . . . 8
⊢ ((∪ 𝐽
∈ V ∧ ℂ ∈ V) → (𝐹 ∈ (∪ 𝐽 ↑pm ℂ)
↔ (𝐹:dom 𝐹⟶∪ 𝐽
∧ dom 𝐹 ⊆
ℂ))) |
| 19 | 16, 17, 18 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∈ (∪ 𝐽 ↑pm ℂ)
↔ (𝐹:dom 𝐹⟶∪ 𝐽
∧ dom 𝐹 ⊆
ℂ))) |
| 20 | 15, 19 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝐹:dom 𝐹⟶∪ 𝐽 ∧ dom 𝐹 ⊆ ℂ)) |
| 21 | 20 | simpld 494 |
. . . . 5
⊢ (𝜑 → 𝐹:dom 𝐹⟶∪ 𝐽) |
| 22 | | fco 6760 |
. . . . 5
⊢ ((𝐺:∪
𝐽⟶∪ 𝐾
∧ 𝐹:dom 𝐹⟶∪ 𝐽)
→ (𝐺 ∘ 𝐹):dom 𝐹⟶∪ 𝐾) |
| 23 | 5, 21, 22 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐺 ∘ 𝐹):dom 𝐹⟶∪ 𝐾) |
| 24 | 23 | ffdmd 6766 |
. . 3
⊢ (𝜑 → (𝐺 ∘ 𝐹):dom (𝐺 ∘ 𝐹)⟶∪ 𝐾) |
| 25 | 23 | fdmd 6746 |
. . . 4
⊢ (𝜑 → dom (𝐺 ∘ 𝐹) = dom 𝐹) |
| 26 | 20 | simprd 495 |
. . . 4
⊢ (𝜑 → dom 𝐹 ⊆ ℂ) |
| 27 | 25, 26 | eqsstrd 4018 |
. . 3
⊢ (𝜑 → dom (𝐺 ∘ 𝐹) ⊆ ℂ) |
| 28 | | cnptop2 23251 |
. . . . . 6
⊢ (𝐺 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐾 ∈ Top) |
| 29 | 1, 28 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ Top) |
| 30 | 29 | uniexd 7762 |
. . . 4
⊢ (𝜑 → ∪ 𝐾
∈ V) |
| 31 | | elpm2g 8884 |
. . . 4
⊢ ((∪ 𝐾
∈ V ∧ ℂ ∈ V) → ((𝐺 ∘ 𝐹) ∈ (∪ 𝐾 ↑pm ℂ)
↔ ((𝐺 ∘ 𝐹):dom (𝐺 ∘ 𝐹)⟶∪ 𝐾 ∧ dom (𝐺 ∘ 𝐹) ⊆ ℂ))) |
| 32 | 30, 17, 31 | sylancl 586 |
. . 3
⊢ (𝜑 → ((𝐺 ∘ 𝐹) ∈ (∪ 𝐾 ↑pm ℂ)
↔ ((𝐺 ∘ 𝐹):dom (𝐺 ∘ 𝐹)⟶∪ 𝐾 ∧ dom (𝐺 ∘ 𝐹) ⊆ ℂ))) |
| 33 | 24, 27, 32 | mpbir2and 713 |
. 2
⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ (∪ 𝐾 ↑pm
ℂ)) |
| 34 | 14 | simp2d 1144 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ∪ 𝐽) |
| 35 | 5, 34 | ffvelcdmd 7105 |
. 2
⊢ (𝜑 → (𝐺‘𝑃) ∈ ∪ 𝐾) |
| 36 | 14 | simp3d 1145 |
. . . . . 6
⊢ (𝜑 → ∀𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣))) |
| 37 | 36 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) → ∀𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣))) |
| 38 | | cnpimaex 23264 |
. . . . . . 7
⊢ ((𝐺 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢) → ∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) |
| 39 | 38 | 3expb 1121 |
. . . . . 6
⊢ ((𝐺 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) → ∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) |
| 40 | 1, 39 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) → ∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) |
| 41 | | r19.29 3114 |
. . . . . . 7
⊢
((∀𝑣 ∈
𝐽 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣)) ∧ ∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) → ∃𝑣 ∈ 𝐽 ((𝑃 ∈ 𝑣 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣)) ∧ (𝑃 ∈ 𝑣 ∧ (𝐺 “ 𝑣) ⊆ 𝑢))) |
| 42 | | pm3.45 622 |
. . . . . . . . 9
⊢ ((𝑃 ∈ 𝑣 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣)) → ((𝑃 ∈ 𝑣 ∧ (𝐺 “ 𝑣) ⊆ 𝑢) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣) ∧ (𝐺 “ 𝑣) ⊆ 𝑢))) |
| 43 | 42 | imp 406 |
. . . . . . . 8
⊢ (((𝑃 ∈ 𝑣 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣)) ∧ (𝑃 ∈ 𝑣 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣) ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) |
| 44 | 43 | reximi 3084 |
. . . . . . 7
⊢
(∃𝑣 ∈
𝐽 ((𝑃 ∈ 𝑣 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣)) ∧ (𝑃 ∈ 𝑣 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) → ∃𝑣 ∈ 𝐽 (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣) ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) |
| 45 | 41, 44 | syl 17 |
. . . . . 6
⊢
((∀𝑣 ∈
𝐽 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣)) ∧ ∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) → ∃𝑣 ∈ 𝐽 (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣) ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) |
| 46 | 5 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) ∧ 𝑘 ∈ dom 𝐹) → 𝐺:∪ 𝐽⟶∪ 𝐾) |
| 47 | 46 | ffnd 6737 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) ∧ 𝑘 ∈ dom 𝐹) → 𝐺 Fn ∪ 𝐽) |
| 48 | | simplrl 777 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) ∧ 𝑘 ∈ dom 𝐹) → 𝑣 ∈ 𝐽) |
| 49 | | elssuni 4937 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ 𝐽 → 𝑣 ⊆ ∪ 𝐽) |
| 50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) ∧ 𝑘 ∈ dom 𝐹) → 𝑣 ⊆ ∪ 𝐽) |
| 51 | | fnfvima 7253 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 Fn ∪
𝐽 ∧ 𝑣 ⊆ ∪ 𝐽 ∧ (𝐹‘𝑘) ∈ 𝑣) → (𝐺‘(𝐹‘𝑘)) ∈ (𝐺 “ 𝑣)) |
| 52 | 51 | 3expia 1122 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 Fn ∪
𝐽 ∧ 𝑣 ⊆ ∪ 𝐽) → ((𝐹‘𝑘) ∈ 𝑣 → (𝐺‘(𝐹‘𝑘)) ∈ (𝐺 “ 𝑣))) |
| 53 | 47, 50, 52 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) ∧ 𝑘 ∈ dom 𝐹) → ((𝐹‘𝑘) ∈ 𝑣 → (𝐺‘(𝐹‘𝑘)) ∈ (𝐺 “ 𝑣))) |
| 54 | 21 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) → 𝐹:dom 𝐹⟶∪ 𝐽) |
| 55 | | fvco3 7008 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:dom 𝐹⟶∪ 𝐽 ∧ 𝑘 ∈ dom 𝐹) → ((𝐺 ∘ 𝐹)‘𝑘) = (𝐺‘(𝐹‘𝑘))) |
| 56 | 54, 55 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) ∧ 𝑘 ∈ dom 𝐹) → ((𝐺 ∘ 𝐹)‘𝑘) = (𝐺‘(𝐹‘𝑘))) |
| 57 | 56 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) ∧ 𝑘 ∈ dom 𝐹) → (((𝐺 ∘ 𝐹)‘𝑘) ∈ (𝐺 “ 𝑣) ↔ (𝐺‘(𝐹‘𝑘)) ∈ (𝐺 “ 𝑣))) |
| 58 | 53, 57 | sylibrd 259 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) ∧ 𝑘 ∈ dom 𝐹) → ((𝐹‘𝑘) ∈ 𝑣 → ((𝐺 ∘ 𝐹)‘𝑘) ∈ (𝐺 “ 𝑣))) |
| 59 | | simplrr 778 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) ∧ 𝑘 ∈ dom 𝐹) → (𝐺 “ 𝑣) ⊆ 𝑢) |
| 60 | 59 | sseld 3982 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) ∧ 𝑘 ∈ dom 𝐹) → (((𝐺 ∘ 𝐹)‘𝑘) ∈ (𝐺 “ 𝑣) → ((𝐺 ∘ 𝐹)‘𝑘) ∈ 𝑢)) |
| 61 | 58, 60 | syld 47 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) ∧ 𝑘 ∈ dom 𝐹) → ((𝐹‘𝑘) ∈ 𝑣 → ((𝐺 ∘ 𝐹)‘𝑘) ∈ 𝑢)) |
| 62 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) ∧ 𝑘 ∈ dom 𝐹) → 𝑘 ∈ dom 𝐹) |
| 63 | 25 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) ∧ 𝑘 ∈ dom 𝐹) → dom (𝐺 ∘ 𝐹) = dom 𝐹) |
| 64 | 62, 63 | eleqtrrd 2844 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) ∧ 𝑘 ∈ dom 𝐹) → 𝑘 ∈ dom (𝐺 ∘ 𝐹)) |
| 65 | 61, 64 | jctild 525 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) ∧ 𝑘 ∈ dom 𝐹) → ((𝐹‘𝑘) ∈ 𝑣 → (𝑘 ∈ dom (𝐺 ∘ 𝐹) ∧ ((𝐺 ∘ 𝐹)‘𝑘) ∈ 𝑢))) |
| 66 | 65 | expimpd 453 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) → ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣) → (𝑘 ∈ dom (𝐺 ∘ 𝐹) ∧ ((𝐺 ∘ 𝐹)‘𝑘) ∈ 𝑢))) |
| 67 | 66 | ralimdv 3169 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐺 ∘ 𝐹) ∧ ((𝐺 ∘ 𝐹)‘𝑘) ∈ 𝑢))) |
| 68 | 67 | reximdv 3170 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ (𝑣 ∈ 𝐽 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐺 ∘ 𝐹) ∧ ((𝐺 ∘ 𝐹)‘𝑘) ∈ 𝑢))) |
| 69 | 68 | expr 456 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ 𝑣 ∈ 𝐽) → ((𝐺 “ 𝑣) ⊆ 𝑢 → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐺 ∘ 𝐹) ∧ ((𝐺 ∘ 𝐹)‘𝑘) ∈ 𝑢)))) |
| 70 | 69 | impcomd 411 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) ∧ 𝑣 ∈ 𝐽) → ((∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣) ∧ (𝐺 “ 𝑣) ⊆ 𝑢) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐺 ∘ 𝐹) ∧ ((𝐺 ∘ 𝐹)‘𝑘) ∈ 𝑢))) |
| 71 | 70 | rexlimdva 3155 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) → (∃𝑣 ∈ 𝐽 (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣) ∧ (𝐺 “ 𝑣) ⊆ 𝑢) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐺 ∘ 𝐹) ∧ ((𝐺 ∘ 𝐹)‘𝑘) ∈ 𝑢))) |
| 72 | 45, 71 | syl5 34 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) → ((∀𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑣)) ∧ ∃𝑣 ∈ 𝐽 (𝑃 ∈ 𝑣 ∧ (𝐺 “ 𝑣) ⊆ 𝑢)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐺 ∘ 𝐹) ∧ ((𝐺 ∘ 𝐹)‘𝑘) ∈ 𝑢))) |
| 73 | 37, 40, 72 | mp2and 699 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐾 ∧ (𝐺‘𝑃) ∈ 𝑢)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐺 ∘ 𝐹) ∧ ((𝐺 ∘ 𝐹)‘𝑘) ∈ 𝑢)) |
| 74 | 73 | expr 456 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → ((𝐺‘𝑃) ∈ 𝑢 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐺 ∘ 𝐹) ∧ ((𝐺 ∘ 𝐹)‘𝑘) ∈ 𝑢))) |
| 75 | 74 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑢 ∈ 𝐾 ((𝐺‘𝑃) ∈ 𝑢 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐺 ∘ 𝐹) ∧ ((𝐺 ∘ 𝐹)‘𝑘) ∈ 𝑢))) |
| 76 | | toptopon2 22924 |
. . . 4
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
| 77 | 29, 76 | sylib 218 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
| 78 | 77, 11, 12 | lmbr2 23267 |
. 2
⊢ (𝜑 → ((𝐺 ∘ 𝐹)(⇝𝑡‘𝐾)(𝐺‘𝑃) ↔ ((𝐺 ∘ 𝐹) ∈ (∪ 𝐾 ↑pm ℂ)
∧ (𝐺‘𝑃) ∈ ∪ 𝐾
∧ ∀𝑢 ∈
𝐾 ((𝐺‘𝑃) ∈ 𝑢 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐺 ∘ 𝐹) ∧ ((𝐺 ∘ 𝐹)‘𝑘) ∈ 𝑢))))) |
| 79 | 33, 35, 75, 78 | mpbir3and 1343 |
1
⊢ (𝜑 → (𝐺 ∘ 𝐹)(⇝𝑡‘𝐾)(𝐺‘𝑃)) |