Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . . 7
⊢ (𝑓 ∈ (𝐵 ↑𝑚 𝐴) ↦ (𝐺 Σg 𝑓)) = (𝑓 ∈ (𝐵 ↑𝑚 𝐴) ↦ (𝐺 Σg 𝑓)) |
2 | 1 | mptpreima 5628 |
. . . . . 6
⊢ (◡(𝑓 ∈ (𝐵 ↑𝑚 𝐴) ↦ (𝐺 Σg 𝑓)) “ 𝑈) = {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} |
3 | | tmdgsum2.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ CMnd) |
4 | | tmdgsum2.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ TopMnd) |
5 | | tmdgsum2.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ Fin) |
6 | | tmdgsum.j |
. . . . . . . . 9
⊢ 𝐽 = (TopOpen‘𝐺) |
7 | | tmdgsum.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐺) |
8 | 6, 7 | tmdgsum 21899 |
. . . . . . . 8
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝑓 ∈ (𝐵 ↑𝑚 𝐴) ↦ (𝐺 Σg 𝑓)) ∈ ((𝐽 ^ko 𝒫 𝐴) Cn 𝐽)) |
9 | 3, 4, 5, 8 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (𝑓 ∈ (𝐵 ↑𝑚 𝐴) ↦ (𝐺 Σg 𝑓)) ∈ ((𝐽 ^ko 𝒫 𝐴) Cn 𝐽)) |
10 | | tmdgsum2.u |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ 𝐽) |
11 | | cnima 21069 |
. . . . . . 7
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝐴) ↦ (𝐺 Σg 𝑓)) ∈ ((𝐽 ^ko 𝒫 𝐴) Cn 𝐽) ∧ 𝑈 ∈ 𝐽) → (◡(𝑓 ∈ (𝐵 ↑𝑚 𝐴) ↦ (𝐺 Σg 𝑓)) “ 𝑈) ∈ (𝐽 ^ko 𝒫 𝐴)) |
12 | 9, 10, 11 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (◡(𝑓 ∈ (𝐵 ↑𝑚 𝐴) ↦ (𝐺 Σg 𝑓)) “ 𝑈) ∈ (𝐽 ^ko 𝒫 𝐴)) |
13 | 2, 12 | syl5eqelr 2706 |
. . . . 5
⊢ (𝜑 → {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ∈ (𝐽 ^ko 𝒫 𝐴)) |
14 | 6, 7 | tmdtopon 21885 |
. . . . . . . 8
⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝐵)) |
15 | | topontop 20718 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) |
16 | 4, 14, 15 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ Top) |
17 | | xkopt 21458 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin) → (𝐽 ^ko 𝒫
𝐴) =
(∏t‘(𝐴 × {𝐽}))) |
18 | 16, 5, 17 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝐽 ^ko 𝒫 𝐴) =
(∏t‘(𝐴 × {𝐽}))) |
19 | | fnconstg 6093 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝐵) → (𝐴 × {𝐽}) Fn 𝐴) |
20 | 4, 14, 19 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝐴 × {𝐽}) Fn 𝐴) |
21 | | eqid 2622 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} |
22 | 21 | ptval 21373 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ (𝐴 × {𝐽}) Fn 𝐴) → (∏t‘(𝐴 × {𝐽})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) |
23 | 5, 20, 22 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 →
(∏t‘(𝐴 × {𝐽})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) |
24 | 18, 23 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → (𝐽 ^ko 𝒫 𝐴) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) |
25 | 13, 24 | eleqtrd 2703 |
. . . 4
⊢ (𝜑 → {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ∈ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) |
26 | | tmdgsum2.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
27 | | fconst6g 6094 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → (𝐴 × {𝑋}):𝐴⟶𝐵) |
28 | 26, 27 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐴 × {𝑋}):𝐴⟶𝐵) |
29 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝐺)
∈ V |
30 | 7, 29 | eqeltri 2697 |
. . . . . . 7
⊢ 𝐵 ∈ V |
31 | | elmapg 7870 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ Fin) → ((𝐴 × {𝑋}) ∈ (𝐵 ↑𝑚 𝐴) ↔ (𝐴 × {𝑋}):𝐴⟶𝐵)) |
32 | 30, 5, 31 | sylancr 695 |
. . . . . 6
⊢ (𝜑 → ((𝐴 × {𝑋}) ∈ (𝐵 ↑𝑚 𝐴) ↔ (𝐴 × {𝑋}):𝐴⟶𝐵)) |
33 | 28, 32 | mpbird 247 |
. . . . 5
⊢ (𝜑 → (𝐴 × {𝑋}) ∈ (𝐵 ↑𝑚 𝐴)) |
34 | | fconstmpt 5163 |
. . . . . . . 8
⊢ (𝐴 × {𝑋}) = (𝑘 ∈ 𝐴 ↦ 𝑋) |
35 | 34 | oveq2i 6661 |
. . . . . . 7
⊢ (𝐺 Σg
(𝐴 × {𝑋})) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) |
36 | | cmnmnd 18208 |
. . . . . . . . 9
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
37 | 3, 36 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Mnd) |
38 | | tmdgsum2.t |
. . . . . . . . 9
⊢ · =
(.g‘𝐺) |
39 | 7, 38 | gsumconst 18334 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((#‘𝐴) · 𝑋)) |
40 | 37, 5, 26, 39 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((#‘𝐴) · 𝑋)) |
41 | 35, 40 | syl5eq 2668 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝐴 × {𝑋})) = ((#‘𝐴) · 𝑋)) |
42 | | tmdgsum2.3 |
. . . . . 6
⊢ (𝜑 → ((#‘𝐴) · 𝑋) ∈ 𝑈) |
43 | 41, 42 | eqeltrd 2701 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg (𝐴 × {𝑋})) ∈ 𝑈) |
44 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑓 = (𝐴 × {𝑋}) → (𝐺 Σg 𝑓) = (𝐺 Σg (𝐴 × {𝑋}))) |
45 | 44 | eleq1d 2686 |
. . . . . 6
⊢ (𝑓 = (𝐴 × {𝑋}) → ((𝐺 Σg 𝑓) ∈ 𝑈 ↔ (𝐺 Σg (𝐴 × {𝑋})) ∈ 𝑈)) |
46 | 45 | elrab 3363 |
. . . . 5
⊢ ((𝐴 × {𝑋}) ∈ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ ((𝐴 × {𝑋}) ∈ (𝐵 ↑𝑚 𝐴) ∧ (𝐺 Σg (𝐴 × {𝑋})) ∈ 𝑈)) |
47 | 33, 43, 46 | sylanbrc 698 |
. . . 4
⊢ (𝜑 → (𝐴 × {𝑋}) ∈ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) |
48 | | tg2 20769 |
. . . 4
⊢ (({𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ∈ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}) ∧ (𝐴 × {𝑋}) ∈ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑡 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ((𝐴 × {𝑋}) ∈ 𝑡 ∧ 𝑡 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) |
49 | 25, 47, 48 | syl2anc 693 |
. . 3
⊢ (𝜑 → ∃𝑡 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ((𝐴 × {𝑋}) ∈ 𝑡 ∧ 𝑡 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) |
50 | | eleq2 2690 |
. . . . 5
⊢ (𝑡 = 𝑥 → ((𝐴 × {𝑋}) ∈ 𝑡 ↔ (𝐴 × {𝑋}) ∈ 𝑥)) |
51 | | sseq1 3626 |
. . . . 5
⊢ (𝑡 = 𝑥 → (𝑡 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) |
52 | 50, 51 | anbi12d 747 |
. . . 4
⊢ (𝑡 = 𝑥 → (((𝐴 × {𝑋}) ∈ 𝑡 ∧ 𝑡 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) ↔ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))) |
53 | 52 | rexab2 3373 |
. . 3
⊢
(∃𝑡 ∈
{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ((𝐴 × {𝑋}) ∈ 𝑡 ∧ 𝑡 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) ↔ ∃𝑥(∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))) |
54 | 49, 53 | sylib 208 |
. 2
⊢ (𝜑 → ∃𝑥(∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))) |
55 | | toponuni 20719 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) |
56 | 4, 14, 55 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 = ∪ 𝐽) |
57 | 56 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝐵 = ∪ 𝐽) |
58 | 57 | ineq1d 3813 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝐵 ∩ ∩ ran
𝑔) = (∪ 𝐽
∩ ∩ ran 𝑔)) |
59 | 16 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝐽 ∈ Top) |
60 | | simplrl 800 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑔 Fn 𝐴) |
61 | | simplrr 801 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦)) |
62 | | fvconst2g 6467 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝐴) → ((𝐴 × {𝐽})‘𝑦) = 𝐽) |
63 | 62 | eleq2d 2687 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝐴) → ((𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ↔ (𝑔‘𝑦) ∈ 𝐽)) |
64 | 63 | ralbidva 2985 |
. . . . . . . . . . . . . . . 16
⊢ (𝐽 ∈ Top →
(∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽)) |
65 | 59, 64 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽)) |
66 | 61, 65 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽) |
67 | | ffnfv 6388 |
. . . . . . . . . . . . . 14
⊢ (𝑔:𝐴⟶𝐽 ↔ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ 𝐽)) |
68 | 60, 66, 67 | sylanbrc 698 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑔:𝐴⟶𝐽) |
69 | | frn 6053 |
. . . . . . . . . . . . 13
⊢ (𝑔:𝐴⟶𝐽 → ran 𝑔 ⊆ 𝐽) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ran 𝑔 ⊆ 𝐽) |
71 | 5 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝐴 ∈ Fin) |
72 | | dffn4 6121 |
. . . . . . . . . . . . . 14
⊢ (𝑔 Fn 𝐴 ↔ 𝑔:𝐴–onto→ran 𝑔) |
73 | 60, 72 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑔:𝐴–onto→ran 𝑔) |
74 | | fofi 8252 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑔:𝐴–onto→ran 𝑔) → ran 𝑔 ∈ Fin) |
75 | 71, 73, 74 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ran 𝑔 ∈ Fin) |
76 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ ∪ 𝐽 =
∪ 𝐽 |
77 | 76 | rintopn 20714 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ ran 𝑔 ⊆ 𝐽 ∧ ran 𝑔 ∈ Fin) → (∪ 𝐽
∩ ∩ ran 𝑔) ∈ 𝐽) |
78 | 59, 70, 75, 77 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (∪
𝐽 ∩ ∩ ran 𝑔) ∈ 𝐽) |
79 | 58, 78 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝐵 ∩ ∩ ran
𝑔) ∈ 𝐽) |
80 | 26 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑋 ∈ 𝐵) |
81 | | fconstmpt 5163 |
. . . . . . . . . . . . . 14
⊢ (𝐴 × {𝑋}) = (𝑦 ∈ 𝐴 ↦ 𝑋) |
82 | | simprl 794 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦)) |
83 | 81, 82 | syl5eqelr 2706 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝑦 ∈ 𝐴 ↦ 𝑋) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦)) |
84 | | mptelixpg 7945 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Fin → ((𝑦 ∈ 𝐴 ↦ 𝑋) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦))) |
85 | 71, 84 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ((𝑦 ∈ 𝐴 ↦ 𝑋) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦))) |
86 | 83, 85 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦)) |
87 | | eleq2 2690 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑔‘𝑦) → (𝑋 ∈ 𝑧 ↔ 𝑋 ∈ (𝑔‘𝑦))) |
88 | 87 | ralrn 6362 |
. . . . . . . . . . . . 13
⊢ (𝑔 Fn 𝐴 → (∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧 ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦))) |
89 | 60, 88 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧 ↔ ∀𝑦 ∈ 𝐴 𝑋 ∈ (𝑔‘𝑦))) |
90 | 86, 89 | mpbird 247 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧) |
91 | | elrint 4518 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (𝐵 ∩ ∩ ran
𝑔) ↔ (𝑋 ∈ 𝐵 ∧ ∀𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧)) |
92 | 80, 90, 91 | sylanbrc 698 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑋 ∈ (𝐵 ∩ ∩ ran
𝑔)) |
93 | 30 | inex1 4799 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∩ ∩ ran 𝑔) ∈ V |
94 | | ixpconstg 7917 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∩ ∩ ran 𝑔) ∈ V) → X𝑦 ∈
𝐴 (𝐵 ∩ ∩ ran
𝑔) = ((𝐵 ∩ ∩ ran
𝑔)
↑𝑚 𝐴)) |
95 | 71, 93, 94 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → X𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran
𝑔) = ((𝐵 ∩ ∩ ran
𝑔)
↑𝑚 𝐴)) |
96 | | inss2 3834 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∩ ∩ ran 𝑔) ⊆ ∩ ran
𝑔 |
97 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑔‘𝑦) ∈ ran 𝑔) |
98 | | intss1 4492 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔‘𝑦) ∈ ran 𝑔 → ∩ ran
𝑔 ⊆ (𝑔‘𝑦)) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → ∩ ran
𝑔 ⊆ (𝑔‘𝑦)) |
100 | 96, 99 | syl5ss 3614 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐵 ∩ ∩ ran
𝑔) ⊆ (𝑔‘𝑦)) |
101 | 100 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ (𝑔 Fn 𝐴 → ∀𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran
𝑔) ⊆ (𝑔‘𝑦)) |
102 | | ss2ixp 7921 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
𝐴 (𝐵 ∩ ∩ ran
𝑔) ⊆ (𝑔‘𝑦) → X𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran
𝑔) ⊆ X𝑦 ∈
𝐴 (𝑔‘𝑦)) |
103 | 60, 101, 102 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → X𝑦 ∈ 𝐴 (𝐵 ∩ ∩ ran
𝑔) ⊆ X𝑦 ∈
𝐴 (𝑔‘𝑦)) |
104 | 95, 103 | eqsstr3d 3640 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ((𝐵 ∩ ∩ ran
𝑔)
↑𝑚 𝐴) ⊆ X𝑦 ∈ 𝐴 (𝑔‘𝑦)) |
105 | | ssrab 3680 |
. . . . . . . . . . . . 13
⊢ (X𝑦 ∈
𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ (𝐵 ↑𝑚 𝐴) ∧ ∀𝑓 ∈ X
𝑦 ∈ 𝐴 (𝑔‘𝑦)(𝐺 Σg 𝑓) ∈ 𝑈)) |
106 | 105 | simprbi 480 |
. . . . . . . . . . . 12
⊢ (X𝑦 ∈
𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} → ∀𝑓 ∈ X 𝑦 ∈ 𝐴 (𝑔‘𝑦)(𝐺 Σg 𝑓) ∈ 𝑈) |
107 | 106 | ad2antll 765 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑓 ∈ X 𝑦 ∈ 𝐴 (𝑔‘𝑦)(𝐺 Σg 𝑓) ∈ 𝑈) |
108 | | ssralv 3666 |
. . . . . . . . . . 11
⊢ (((𝐵 ∩ ∩ ran 𝑔) ↑𝑚 𝐴) ⊆ X𝑦 ∈
𝐴 (𝑔‘𝑦) → (∀𝑓 ∈ X 𝑦 ∈ 𝐴 (𝑔‘𝑦)(𝐺 Σg 𝑓) ∈ 𝑈 → ∀𝑓 ∈ ((𝐵 ∩ ∩ ran
𝑔)
↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)) |
109 | 104, 107,
108 | sylc 65 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑓 ∈ ((𝐵 ∩ ∩ ran
𝑔)
↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈) |
110 | | eleq2 2690 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝐵 ∩ ∩ ran
𝑔) → (𝑋 ∈ 𝑢 ↔ 𝑋 ∈ (𝐵 ∩ ∩ ran
𝑔))) |
111 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝐵 ∩ ∩ ran
𝑔) → (𝑢 ↑𝑚
𝐴) = ((𝐵 ∩ ∩ ran
𝑔)
↑𝑚 𝐴)) |
112 | 111 | raleqdv 3144 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝐵 ∩ ∩ ran
𝑔) → (∀𝑓 ∈ (𝑢 ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈 ↔ ∀𝑓 ∈ ((𝐵 ∩ ∩ ran
𝑔)
↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)) |
113 | 110, 112 | anbi12d 747 |
. . . . . . . . . . 11
⊢ (𝑢 = (𝐵 ∩ ∩ ran
𝑔) → ((𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈) ↔ (𝑋 ∈ (𝐵 ∩ ∩ ran
𝑔) ∧ ∀𝑓 ∈ ((𝐵 ∩ ∩ ran
𝑔)
↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))) |
114 | 113 | rspcev 3309 |
. . . . . . . . . 10
⊢ (((𝐵 ∩ ∩ ran 𝑔) ∈ 𝐽 ∧ (𝑋 ∈ (𝐵 ∩ ∩ ran
𝑔) ∧ ∀𝑓 ∈ ((𝐵 ∩ ∩ ran
𝑔)
↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)) |
115 | 79, 92, 109, 114 | syl12anc 1324 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)) |
116 | 115 | ex 450 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) → (((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))) |
117 | 116 | 3adantr3 1222 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦))) → (((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))) |
118 | | eleq2 2690 |
. . . . . . . . 9
⊢ (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → ((𝐴 × {𝑋}) ∈ 𝑥 ↔ (𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) |
119 | | sseq1 3626 |
. . . . . . . . 9
⊢ (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (𝑥 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) |
120 | 118, 119 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) ↔ ((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))) |
121 | 120 | imbi1d 331 |
. . . . . . 7
⊢ (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → ((((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)) ↔ (((𝐴 × {𝑋}) ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∧ X𝑦 ∈ 𝐴 (𝑔‘𝑦) ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))) |
122 | 117, 121 | syl5ibrcom 237 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦))) → (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))) |
123 | 122 | expimpd 629 |
. . . . 5
⊢ (𝜑 → (((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) → (((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))) |
124 | 123 | exlimdv 1861 |
. . . 4
⊢ (𝜑 → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) → (((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))) |
125 | 124 | impd 447 |
. . 3
⊢ (𝜑 → ((∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))) |
126 | 125 | exlimdv 1861 |
. 2
⊢ (𝜑 → (∃𝑥(∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥 ∧ 𝑥 ⊆ {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))) |
127 | 54, 126 | mpd 15 |
1
⊢ (𝜑 → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)) |