MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tmdgsum2 Structured version   Visualization version   GIF version

Theorem tmdgsum2 21947
Description: For any neighborhood 𝑈 of 𝑛𝑋, there is a neighborhood 𝑢 of 𝑋 such that any sum of 𝑛 elements in 𝑢 sums to an element of 𝑈. (Contributed by Mario Carneiro, 19-Sep-2015.)
Hypotheses
Ref Expression
tmdgsum.j 𝐽 = (TopOpen‘𝐺)
tmdgsum.b 𝐵 = (Base‘𝐺)
tmdgsum2.t · = (.g𝐺)
tmdgsum2.1 (𝜑𝐺 ∈ CMnd)
tmdgsum2.2 (𝜑𝐺 ∈ TopMnd)
tmdgsum2.a (𝜑𝐴 ∈ Fin)
tmdgsum2.u (𝜑𝑈𝐽)
tmdgsum2.x (𝜑𝑋𝐵)
tmdgsum2.3 (𝜑 → ((#‘𝐴) · 𝑋) ∈ 𝑈)
Assertion
Ref Expression
tmdgsum2 (𝜑 → ∃𝑢𝐽 (𝑋𝑢 ∧ ∀𝑓 ∈ (𝑢𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))
Distinct variable groups:   𝑢,𝑓,𝐴   𝑓,𝐽,𝑢   𝑓,𝑋,𝑢   𝐵,𝑓,𝑢   𝑓,𝐺,𝑢   𝑈,𝑓,𝑢
Allowed substitution hints:   𝜑(𝑢,𝑓)   · (𝑢,𝑓)

Proof of Theorem tmdgsum2
Dummy variables 𝑔 𝑘 𝑡 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2651 . . . . . . 7 (𝑓 ∈ (𝐵𝑚 𝐴) ↦ (𝐺 Σg 𝑓)) = (𝑓 ∈ (𝐵𝑚 𝐴) ↦ (𝐺 Σg 𝑓))
21mptpreima 5666 . . . . . 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‘𝐺)
86, 7tmdgsum 21946 . . . . . . . 8 ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝑓 ∈ (𝐵𝑚 𝐴) ↦ (𝐺 Σg 𝑓)) ∈ ((𝐽 ^ko 𝒫 𝐴) Cn 𝐽))
93, 4, 5, 8syl3anc 1366 . . . . . . 7 (𝜑 → (𝑓 ∈ (𝐵𝑚 𝐴) ↦ (𝐺 Σg 𝑓)) ∈ ((𝐽 ^ko 𝒫 𝐴) Cn 𝐽))
10 tmdgsum2.u . . . . . . 7 (𝜑𝑈𝐽)
11 cnima 21117 . . . . . . 7 (((𝑓 ∈ (𝐵𝑚 𝐴) ↦ (𝐺 Σg 𝑓)) ∈ ((𝐽 ^ko 𝒫 𝐴) Cn 𝐽) ∧ 𝑈𝐽) → ((𝑓 ∈ (𝐵𝑚 𝐴) ↦ (𝐺 Σg 𝑓)) “ 𝑈) ∈ (𝐽 ^ko 𝒫 𝐴))
129, 10, 11syl2anc 694 . . . . . 6 (𝜑 → ((𝑓 ∈ (𝐵𝑚 𝐴) ↦ (𝐺 Σg 𝑓)) “ 𝑈) ∈ (𝐽 ^ko 𝒫 𝐴))
132, 12syl5eqelr 2735 . . . . 5 (𝜑 → {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ∈ (𝐽 ^ko 𝒫 𝐴))
146, 7tmdtopon 21932 . . . . . . . 8 (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝐵))
15 topontop 20766 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
164, 14, 153syl 18 . . . . . . 7 (𝜑𝐽 ∈ Top)
17 xkopt 21506 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin) → (𝐽 ^ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝐽})))
1816, 5, 17syl2anc 694 . . . . . 6 (𝜑 → (𝐽 ^ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝐽})))
19 fnconstg 6131 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝐵) → (𝐴 × {𝐽}) Fn 𝐴)
204, 14, 193syl 18 . . . . . . 7 (𝜑 → (𝐴 × {𝐽}) Fn 𝐴)
21 eqid 2651 . . . . . . . 8 {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}
2221ptval 21421 . . . . . . 7 ((𝐴 ∈ Fin ∧ (𝐴 × {𝐽}) Fn 𝐴) → (∏t‘(𝐴 × {𝐽})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}))
235, 20, 22syl2anc 694 . . . . . 6 (𝜑 → (∏t‘(𝐴 × {𝐽})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}))
2418, 23eqtrd 2685 . . . . 5 (𝜑 → (𝐽 ^ko 𝒫 𝐴) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}))
2513, 24eleqtrd 2732 . . . 4 (𝜑 → {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ∈ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}))
26 tmdgsum2.x . . . . . . 7 (𝜑𝑋𝐵)
27 fconst6g 6132 . . . . . . 7 (𝑋𝐵 → (𝐴 × {𝑋}):𝐴𝐵)
2826, 27syl 17 . . . . . 6 (𝜑 → (𝐴 × {𝑋}):𝐴𝐵)
29 fvex 6239 . . . . . . . 8 (Base‘𝐺) ∈ V
307, 29eqeltri 2726 . . . . . . 7 𝐵 ∈ V
31 elmapg 7912 . . . . . . 7 ((𝐵 ∈ V ∧ 𝐴 ∈ Fin) → ((𝐴 × {𝑋}) ∈ (𝐵𝑚 𝐴) ↔ (𝐴 × {𝑋}):𝐴𝐵))
3230, 5, 31sylancr 696 . . . . . 6 (𝜑 → ((𝐴 × {𝑋}) ∈ (𝐵𝑚 𝐴) ↔ (𝐴 × {𝑋}):𝐴𝐵))
3328, 32mpbird 247 . . . . 5 (𝜑 → (𝐴 × {𝑋}) ∈ (𝐵𝑚 𝐴))
34 fconstmpt 5197 . . . . . . . 8 (𝐴 × {𝑋}) = (𝑘𝐴𝑋)
3534oveq2i 6701 . . . . . . 7 (𝐺 Σg (𝐴 × {𝑋})) = (𝐺 Σg (𝑘𝐴𝑋))
36 cmnmnd 18254 . . . . . . . . 9 (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
373, 36syl 17 . . . . . . . 8 (𝜑𝐺 ∈ Mnd)
38 tmdgsum2.t . . . . . . . . 9 · = (.g𝐺)
397, 38gsumconst 18380 . . . . . . . 8 ((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋𝐵) → (𝐺 Σg (𝑘𝐴𝑋)) = ((#‘𝐴) · 𝑋))
4037, 5, 26, 39syl3anc 1366 . . . . . . 7 (𝜑 → (𝐺 Σg (𝑘𝐴𝑋)) = ((#‘𝐴) · 𝑋))
4135, 40syl5eq 2697 . . . . . 6 (𝜑 → (𝐺 Σg (𝐴 × {𝑋})) = ((#‘𝐴) · 𝑋))
42 tmdgsum2.3 . . . . . 6 (𝜑 → ((#‘𝐴) · 𝑋) ∈ 𝑈)
4341, 42eqeltrd 2730 . . . . 5 (𝜑 → (𝐺 Σg (𝐴 × {𝑋})) ∈ 𝑈)
44 oveq2 6698 . . . . . . 7 (𝑓 = (𝐴 × {𝑋}) → (𝐺 Σg 𝑓) = (𝐺 Σg (𝐴 × {𝑋})))
4544eleq1d 2715 . . . . . 6 (𝑓 = (𝐴 × {𝑋}) → ((𝐺 Σg 𝑓) ∈ 𝑈 ↔ (𝐺 Σg (𝐴 × {𝑋})) ∈ 𝑈))
4645elrab 3396 . . . . 5 ((𝐴 × {𝑋}) ∈ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ ((𝐴 × {𝑋}) ∈ (𝐵𝑚 𝐴) ∧ (𝐺 Σg (𝐴 × {𝑋})) ∈ 𝑈))
4733, 43, 46sylanbrc 699 . . . 4 (𝜑 → (𝐴 × {𝑋}) ∈ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})
48 tg2 20817 . . . 4 (({𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ∈ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}) ∧ (𝐴 × {𝑋}) ∈ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑡 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))} ((𝐴 × {𝑋}) ∈ 𝑡𝑡 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))
4925, 47, 48syl2anc 694 . . 3 (𝜑 → ∃𝑡 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))} ((𝐴 × {𝑋}) ∈ 𝑡𝑡 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))
50 eleq2 2719 . . . . 5 (𝑡 = 𝑥 → ((𝐴 × {𝑋}) ∈ 𝑡 ↔ (𝐴 × {𝑋}) ∈ 𝑥))
51 sseq1 3659 . . . . 5 (𝑡 = 𝑥 → (𝑡 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ 𝑥 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))
5250, 51anbi12d 747 . . . 4 (𝑡 = 𝑥 → (((𝐴 × {𝑋}) ∈ 𝑡𝑡 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) ↔ ((𝐴 × {𝑋}) ∈ 𝑥𝑥 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})))
5352rexab2 3406 . . 3 (∃𝑡 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))} ((𝐴 × {𝑋}) ∈ 𝑡𝑡 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) ↔ ∃𝑥(∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥𝑥 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})))
5449, 53sylib 208 . 2 (𝜑 → ∃𝑥(∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥𝑥 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})))
55 toponuni 20767 . . . . . . . . . . . . . 14 (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = 𝐽)
564, 14, 553syl 18 . . . . . . . . . . . . 13 (𝜑𝐵 = 𝐽)
5756ad2antrr 762 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝐵 = 𝐽)
5857ineq1d 3846 . . . . . . . . . . 11 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝐵 ran 𝑔) = ( 𝐽 ran 𝑔))
5916ad2antrr 762 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝐽 ∈ Top)
60 simplrl 817 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑔 Fn 𝐴)
61 simplrr 818 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))
62 fvconst2g 6508 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝑦𝐴) → ((𝐴 × {𝐽})‘𝑦) = 𝐽)
6362eleq2d 2716 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑦𝐴) → ((𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ↔ (𝑔𝑦) ∈ 𝐽))
6463ralbidva 3014 . . . . . . . . . . . . . . . 16 (𝐽 ∈ Top → (∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ↔ ∀𝑦𝐴 (𝑔𝑦) ∈ 𝐽))
6559, 64syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ↔ ∀𝑦𝐴 (𝑔𝑦) ∈ 𝐽))
6661, 65mpbid 222 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑦𝐴 (𝑔𝑦) ∈ 𝐽)
67 ffnfv 6428 . . . . . . . . . . . . . 14 (𝑔:𝐴𝐽 ↔ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ 𝐽))
6860, 66, 67sylanbrc 699 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑔:𝐴𝐽)
69 frn 6091 . . . . . . . . . . . . 13 (𝑔:𝐴𝐽 → ran 𝑔𝐽)
7068, 69syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ran 𝑔𝐽)
715ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝐴 ∈ Fin)
72 dffn4 6159 . . . . . . . . . . . . . 14 (𝑔 Fn 𝐴𝑔:𝐴onto→ran 𝑔)
7360, 72sylib 208 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑔:𝐴onto→ran 𝑔)
74 fofi 8293 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ 𝑔:𝐴onto→ran 𝑔) → ran 𝑔 ∈ Fin)
7571, 73, 74syl2anc 694 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ran 𝑔 ∈ Fin)
76 eqid 2651 . . . . . . . . . . . . 13 𝐽 = 𝐽
7776rintopn 20762 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ran 𝑔𝐽 ∧ ran 𝑔 ∈ Fin) → ( 𝐽 ran 𝑔) ∈ 𝐽)
7859, 70, 75, 77syl3anc 1366 . . . . . . . . . . 11 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ( 𝐽 ran 𝑔) ∈ 𝐽)
7958, 78eqeltrd 2730 . . . . . . . . . 10 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝐵 ran 𝑔) ∈ 𝐽)
8026ad2antrr 762 . . . . . . . . . . 11 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑋𝐵)
81 fconstmpt 5197 . . . . . . . . . . . . . 14 (𝐴 × {𝑋}) = (𝑦𝐴𝑋)
82 simprl 809 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦))
8381, 82syl5eqelr 2735 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (𝑦𝐴𝑋) ∈ X𝑦𝐴 (𝑔𝑦))
84 mptelixpg 7987 . . . . . . . . . . . . . 14 (𝐴 ∈ Fin → ((𝑦𝐴𝑋) ∈ X𝑦𝐴 (𝑔𝑦) ↔ ∀𝑦𝐴 𝑋 ∈ (𝑔𝑦)))
8571, 84syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ((𝑦𝐴𝑋) ∈ X𝑦𝐴 (𝑔𝑦) ↔ ∀𝑦𝐴 𝑋 ∈ (𝑔𝑦)))
8683, 85mpbid 222 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑦𝐴 𝑋 ∈ (𝑔𝑦))
87 eleq2 2719 . . . . . . . . . . . . . 14 (𝑧 = (𝑔𝑦) → (𝑋𝑧𝑋 ∈ (𝑔𝑦)))
8887ralrn 6402 . . . . . . . . . . . . 13 (𝑔 Fn 𝐴 → (∀𝑧 ∈ ran 𝑔 𝑋𝑧 ↔ ∀𝑦𝐴 𝑋 ∈ (𝑔𝑦)))
8960, 88syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → (∀𝑧 ∈ ran 𝑔 𝑋𝑧 ↔ ∀𝑦𝐴 𝑋 ∈ (𝑔𝑦)))
9086, 89mpbird 247 . . . . . . . . . . 11 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑧 ∈ ran 𝑔 𝑋𝑧)
91 elrint 4550 . . . . . . . . . . 11 (𝑋 ∈ (𝐵 ran 𝑔) ↔ (𝑋𝐵 ∧ ∀𝑧 ∈ ran 𝑔 𝑋𝑧))
9280, 90, 91sylanbrc 699 . . . . . . . . . 10 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → 𝑋 ∈ (𝐵 ran 𝑔))
9330inex1 4832 . . . . . . . . . . . . 13 (𝐵 ran 𝑔) ∈ V
94 ixpconstg 7959 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ (𝐵 ran 𝑔) ∈ V) → X𝑦𝐴 (𝐵 ran 𝑔) = ((𝐵 ran 𝑔) ↑𝑚 𝐴))
9571, 93, 94sylancl 695 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → X𝑦𝐴 (𝐵 ran 𝑔) = ((𝐵 ran 𝑔) ↑𝑚 𝐴))
96 inss2 3867 . . . . . . . . . . . . . . 15 (𝐵 ran 𝑔) ⊆ ran 𝑔
97 fnfvelrn 6396 . . . . . . . . . . . . . . . 16 ((𝑔 Fn 𝐴𝑦𝐴) → (𝑔𝑦) ∈ ran 𝑔)
98 intss1 4524 . . . . . . . . . . . . . . . 16 ((𝑔𝑦) ∈ ran 𝑔 ran 𝑔 ⊆ (𝑔𝑦))
9997, 98syl 17 . . . . . . . . . . . . . . 15 ((𝑔 Fn 𝐴𝑦𝐴) → ran 𝑔 ⊆ (𝑔𝑦))
10096, 99syl5ss 3647 . . . . . . . . . . . . . 14 ((𝑔 Fn 𝐴𝑦𝐴) → (𝐵 ran 𝑔) ⊆ (𝑔𝑦))
101100ralrimiva 2995 . . . . . . . . . . . . 13 (𝑔 Fn 𝐴 → ∀𝑦𝐴 (𝐵 ran 𝑔) ⊆ (𝑔𝑦))
102 ss2ixp 7963 . . . . . . . . . . . . 13 (∀𝑦𝐴 (𝐵 ran 𝑔) ⊆ (𝑔𝑦) → X𝑦𝐴 (𝐵 ran 𝑔) ⊆ X𝑦𝐴 (𝑔𝑦))
10360, 101, 1023syl 18 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → X𝑦𝐴 (𝐵 ran 𝑔) ⊆ X𝑦𝐴 (𝑔𝑦))
10495, 103eqsstr3d 3673 . . . . . . . . . . 11 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ((𝐵 ran 𝑔) ↑𝑚 𝐴) ⊆ X𝑦𝐴 (𝑔𝑦))
105 ssrab 3713 . . . . . . . . . . . . 13 (X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ (X𝑦𝐴 (𝑔𝑦) ⊆ (𝐵𝑚 𝐴) ∧ ∀𝑓X 𝑦𝐴 (𝑔𝑦)(𝐺 Σg 𝑓) ∈ 𝑈))
106105simprbi 479 . . . . . . . . . . . 12 (X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} → ∀𝑓X 𝑦𝐴 (𝑔𝑦)(𝐺 Σg 𝑓) ∈ 𝑈)
107106ad2antll 765 . . . . . . . . . . 11 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑓X 𝑦𝐴 (𝑔𝑦)(𝐺 Σg 𝑓) ∈ 𝑈)
108 ssralv 3699 . . . . . . . . . . 11 (((𝐵 ran 𝑔) ↑𝑚 𝐴) ⊆ X𝑦𝐴 (𝑔𝑦) → (∀𝑓X 𝑦𝐴 (𝑔𝑦)(𝐺 Σg 𝑓) ∈ 𝑈 → ∀𝑓 ∈ ((𝐵 ran 𝑔) ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))
109104, 107, 108sylc 65 . . . . . . . . . 10 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∀𝑓 ∈ ((𝐵 ran 𝑔) ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)
110 eleq2 2719 . . . . . . . . . . . 12 (𝑢 = (𝐵 ran 𝑔) → (𝑋𝑢𝑋 ∈ (𝐵 ran 𝑔)))
111 oveq1 6697 . . . . . . . . . . . . 13 (𝑢 = (𝐵 ran 𝑔) → (𝑢𝑚 𝐴) = ((𝐵 ran 𝑔) ↑𝑚 𝐴))
112111raleqdv 3174 . . . . . . . . . . . 12 (𝑢 = (𝐵 ran 𝑔) → (∀𝑓 ∈ (𝑢𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈 ↔ ∀𝑓 ∈ ((𝐵 ran 𝑔) ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))
113110, 112anbi12d 747 . . . . . . . . . . 11 (𝑢 = (𝐵 ran 𝑔) → ((𝑋𝑢 ∧ ∀𝑓 ∈ (𝑢𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈) ↔ (𝑋 ∈ (𝐵 ran 𝑔) ∧ ∀𝑓 ∈ ((𝐵 ran 𝑔) ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
114113rspcev 3340 . . . . . . . . . 10 (((𝐵 ran 𝑔) ∈ 𝐽 ∧ (𝑋 ∈ (𝐵 ran 𝑔) ∧ ∀𝑓 ∈ ((𝐵 ran 𝑔) ↑𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)) → ∃𝑢𝐽 (𝑋𝑢 ∧ ∀𝑓 ∈ (𝑢𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))
11579, 92, 109, 114syl12anc 1364 . . . . . . . . 9 (((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) ∧ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∃𝑢𝐽 (𝑋𝑢 ∧ ∀𝑓 ∈ (𝑢𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))
116115ex 449 . . . . . . . 8 ((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦))) → (((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢𝐽 (𝑋𝑢 ∧ ∀𝑓 ∈ (𝑢𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
1171163adantr3 1242 . . . . . . 7 ((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦))) → (((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢𝐽 (𝑋𝑢 ∧ ∀𝑓 ∈ (𝑢𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
118 eleq2 2719 . . . . . . . . 9 (𝑥 = X𝑦𝐴 (𝑔𝑦) → ((𝐴 × {𝑋}) ∈ 𝑥 ↔ (𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦)))
119 sseq1 3659 . . . . . . . . 9 (𝑥 = X𝑦𝐴 (𝑔𝑦) → (𝑥 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈} ↔ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}))
120118, 119anbi12d 747 . . . . . . . 8 (𝑥 = X𝑦𝐴 (𝑔𝑦) → (((𝐴 × {𝑋}) ∈ 𝑥𝑥 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) ↔ ((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})))
121120imbi1d 330 . . . . . . 7 (𝑥 = X𝑦𝐴 (𝑔𝑦) → ((((𝐴 × {𝑋}) ∈ 𝑥𝑥 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢𝐽 (𝑋𝑢 ∧ ∀𝑓 ∈ (𝑢𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)) ↔ (((𝐴 × {𝑋}) ∈ X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢𝐽 (𝑋𝑢 ∧ ∀𝑓 ∈ (𝑢𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))))
122117, 121syl5ibrcom 237 . . . . . 6 ((𝜑 ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦))) → (𝑥 = X𝑦𝐴 (𝑔𝑦) → (((𝐴 × {𝑋}) ∈ 𝑥𝑥 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢𝐽 (𝑋𝑢 ∧ ∀𝑓 ∈ (𝑢𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))))
123122expimpd 628 . . . . 5 (𝜑 → (((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦)) → (((𝐴 × {𝑋}) ∈ 𝑥𝑥 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢𝐽 (𝑋𝑢 ∧ ∀𝑓 ∈ (𝑢𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))))
124123exlimdv 1901 . . . 4 (𝜑 → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦)) → (((𝐴 × {𝑋}) ∈ 𝑥𝑥 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈}) → ∃𝑢𝐽 (𝑋𝑢 ∧ ∀𝑓 ∈ (𝑢𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))))
125124impd 446 . . 3 (𝜑 → ((∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥𝑥 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∃𝑢𝐽 (𝑋𝑢 ∧ ∀𝑓 ∈ (𝑢𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
126125exlimdv 1901 . 2 (𝜑 → (∃𝑥(∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝐴 × {𝐽})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝐴 × {𝐽})‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦)) ∧ ((𝐴 × {𝑋}) ∈ 𝑥𝑥 ⊆ {𝑓 ∈ (𝐵𝑚 𝐴) ∣ (𝐺 Σg 𝑓) ∈ 𝑈})) → ∃𝑢𝐽 (𝑋𝑢 ∧ ∀𝑓 ∈ (𝑢𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)))
12754, 126mpd 15 1 (𝜑 → ∃𝑢𝐽 (𝑋𝑢 ∧ ∀𝑓 ∈ (𝑢𝑚 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wex 1744  wcel 2030  {cab 2637  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  cdif 3604  cin 3606  wss 3607  𝒫 cpw 4191  {csn 4210   cuni 4468   cint 4507  cmpt 4762   × cxp 5141  ccnv 5142  ran crn 5144  cima 5146   Fn wfn 5921  wf 5922  ontowfo 5924  cfv 5926  (class class class)co 6690  𝑚 cmap 7899  Xcixp 7950  Fincfn 7997  #chash 13157  Basecbs 15904  TopOpenctopn 16129  topGenctg 16145  tcpt 16146   Σg cgsu 16148  Mndcmnd 17341  .gcmg 17587  CMndccmn 18239  Topctop 20746  TopOnctopon 20763   Cn ccn 21076   ^ko cxko 21412  TopMndctmd 21921
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505  df-seq 12842  df-hash 13158  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-rest 16130  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-mre 16293  df-mrc 16294  df-acs 16296  df-plusf 17288  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cn 21079  df-cnp 21080  df-cmp 21238  df-tx 21413  df-xko 21414  df-tmd 21923
This theorem is referenced by:  tsmsxp  22005
  Copyright terms: Public domain W3C validator