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

Theorem ptpjopn 21637
Description: The projection map is an open map. (Contributed by Mario Carneiro, 2-Sep-2015.)
Hypotheses
Ref Expression
ptpjcn.1 𝑌 = 𝐽
ptpjcn.2 𝐽 = (∏t𝐹)
Assertion
Ref Expression
ptpjopn (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ((𝑥𝑌 ↦ (𝑥𝐼)) “ 𝑈) ∈ (𝐹𝐼))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝐼   𝑥,𝑉   𝑥,𝑌   𝑥,𝑈
Allowed substitution hint:   𝐽(𝑥)

Proof of Theorem ptpjopn
Dummy variables 𝑔 𝑘 𝑛 𝑠 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ima 5279 . . 3 ((𝑥𝑌 ↦ (𝑥𝐼)) “ 𝑈) = ran ((𝑥𝑌 ↦ (𝑥𝐼)) ↾ 𝑈)
2 elssuni 4619 . . . . . . 7 (𝑈𝐽𝑈 𝐽)
3 ptpjcn.1 . . . . . . 7 𝑌 = 𝐽
42, 3syl6sseqr 3793 . . . . . 6 (𝑈𝐽𝑈𝑌)
54adantl 473 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝑈𝑌)
65resmptd 5610 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ((𝑥𝑌 ↦ (𝑥𝐼)) ↾ 𝑈) = (𝑥𝑈 ↦ (𝑥𝐼)))
76rneqd 5508 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ran ((𝑥𝑌 ↦ (𝑥𝐼)) ↾ 𝑈) = ran (𝑥𝑈 ↦ (𝑥𝐼)))
81, 7syl5eq 2806 . 2 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ((𝑥𝑌 ↦ (𝑥𝐼)) “ 𝑈) = ran (𝑥𝑈 ↦ (𝑥𝐼)))
9 ptpjcn.2 . . . . . . . . . . 11 𝐽 = (∏t𝐹)
10 ffn 6206 . . . . . . . . . . . 12 (𝐹:𝐴⟶Top → 𝐹 Fn 𝐴)
11 eqid 2760 . . . . . . . . . . . . 13 {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} = {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}
1211ptval 21595 . . . . . . . . . . . 12 ((𝐴𝑉𝐹 Fn 𝐴) → (∏t𝐹) = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
1310, 12sylan2 492 . . . . . . . . . . 11 ((𝐴𝑉𝐹:𝐴⟶Top) → (∏t𝐹) = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
149, 13syl5eq 2806 . . . . . . . . . 10 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐽 = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
15143adant3 1127 . . . . . . . . 9 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) → 𝐽 = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
1615eleq2d 2825 . . . . . . . 8 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) → (𝑈𝐽𝑈 ∈ (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))})))
1716biimpa 502 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝑈 ∈ (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
18 tg2 20991 . . . . . . 7 ((𝑈 ∈ (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}) ∧ 𝑠𝑈) → ∃𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} (𝑠𝑤𝑤𝑈))
1917, 18sylan 489 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → ∃𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} (𝑠𝑤𝑤𝑈))
20 vex 3343 . . . . . . . . 9 𝑤 ∈ V
21 eqeq1 2764 . . . . . . . . . . 11 (𝑠 = 𝑤 → (𝑠 = X𝑦𝐴 (𝑔𝑦) ↔ 𝑤 = X𝑦𝐴 (𝑔𝑦)))
2221anbi2d 742 . . . . . . . . . 10 (𝑠 = 𝑤 → (((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦)) ↔ ((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦))))
2322exbidv 1999 . . . . . . . . 9 (𝑠 = 𝑤 → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦)) ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦))))
2420, 23elab 3490 . . . . . . . 8 (𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦)))
25 fveq2 6353 . . . . . . . . . . . . . . 15 (𝑦 = 𝐼 → (𝑔𝑦) = (𝑔𝐼))
26 fveq2 6353 . . . . . . . . . . . . . . 15 (𝑦 = 𝐼 → (𝐹𝑦) = (𝐹𝐼))
2725, 26eleq12d 2833 . . . . . . . . . . . . . 14 (𝑦 = 𝐼 → ((𝑔𝑦) ∈ (𝐹𝑦) ↔ (𝑔𝐼) ∈ (𝐹𝐼)))
28 simplr2 1263 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦))
29 simpl3 1232 . . . . . . . . . . . . . . 15 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝐼𝐴)
3029ad3antrrr 768 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → 𝐼𝐴)
3127, 28, 30rspcdva 3455 . . . . . . . . . . . . 13 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑔𝐼) ∈ (𝐹𝐼))
32 fveq2 6353 . . . . . . . . . . . . . . 15 (𝑦 = 𝐼 → (𝑠𝑦) = (𝑠𝐼))
3332, 25eleq12d 2833 . . . . . . . . . . . . . 14 (𝑦 = 𝐼 → ((𝑠𝑦) ∈ (𝑔𝑦) ↔ (𝑠𝐼) ∈ (𝑔𝐼)))
34 vex 3343 . . . . . . . . . . . . . . . . 17 𝑠 ∈ V
3534elixp 8083 . . . . . . . . . . . . . . . 16 (𝑠X𝑦𝐴 (𝑔𝑦) ↔ (𝑠 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦)))
3635simprbi 483 . . . . . . . . . . . . . . 15 (𝑠X𝑦𝐴 (𝑔𝑦) → ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦))
3736ad2antrl 766 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦))
3833, 37, 30rspcdva 3455 . . . . . . . . . . . . 13 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑠𝐼) ∈ (𝑔𝐼))
39 simplrr 820 . . . . . . . . . . . . . . . . . 18 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)
40 simplrl 819 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ 𝑛 = 𝐼) → 𝑘 ∈ (𝑔𝐼))
41 fveq2 6353 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝐼 → (𝑔𝑛) = (𝑔𝐼))
4241adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ 𝑛 = 𝐼) → (𝑔𝑛) = (𝑔𝐼))
4340, 42eleqtrrd 2842 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ 𝑛 = 𝐼) → 𝑘 ∈ (𝑔𝑛))
44 fveq2 6353 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑛 → (𝑠𝑦) = (𝑠𝑛))
45 fveq2 6353 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑛 → (𝑔𝑦) = (𝑔𝑛))
4644, 45eleq12d 2833 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑛 → ((𝑠𝑦) ∈ (𝑔𝑦) ↔ (𝑠𝑛) ∈ (𝑔𝑛)))
47 simplrl 819 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → 𝑠X𝑦𝐴 (𝑔𝑦))
4847, 36syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦))
49 simprr 813 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → 𝑛𝐴)
5046, 48, 49rspcdva 3455 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → (𝑠𝑛) ∈ (𝑔𝑛))
5150adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ ¬ 𝑛 = 𝐼) → (𝑠𝑛) ∈ (𝑔𝑛))
5243, 51ifclda 4264 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛))
5352anassrs 683 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) ∧ 𝑛𝐴) → if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛))
5453ralrimiva 3104 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ∀𝑛𝐴 if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛))
55 simpll1 1255 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → 𝐴𝑉)
5655ad3antrrr 768 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝐴𝑉)
57 mptelixpg 8113 . . . . . . . . . . . . . . . . . . . . 21 (𝐴𝑉 → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑛𝐴 (𝑔𝑛) ↔ ∀𝑛𝐴 if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛)))
5856, 57syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑛𝐴 (𝑔𝑛) ↔ ∀𝑛𝐴 if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛)))
5954, 58mpbird 247 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑛𝐴 (𝑔𝑛))
60 fveq2 6353 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑦 → (𝑔𝑛) = (𝑔𝑦))
6160cbvixpv 8094 . . . . . . . . . . . . . . . . . . 19 X𝑛𝐴 (𝑔𝑛) = X𝑦𝐴 (𝑔𝑦)
6259, 61syl6eleq 2849 . . . . . . . . . . . . . . . . . 18 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑦𝐴 (𝑔𝑦))
6339, 62sseldd 3745 . . . . . . . . . . . . . . . . 17 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ 𝑈)
6430adantr 472 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝐼𝐴)
65 iftrue 4236 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝐼 → if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) = 𝑘)
66 eqid 2760 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) = (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))
67 vex 3343 . . . . . . . . . . . . . . . . . . . 20 𝑘 ∈ V
6865, 66, 67fvmpt 6445 . . . . . . . . . . . . . . . . . . 19 (𝐼𝐴 → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼) = 𝑘)
6964, 68syl 17 . . . . . . . . . . . . . . . . . 18 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼) = 𝑘)
7069eqcomd 2766 . . . . . . . . . . . . . . . . 17 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝑘 = ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼))
71 fveq1 6352 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) → (𝑥𝐼) = ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼))
7271eqeq2d 2770 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) → (𝑘 = (𝑥𝐼) ↔ 𝑘 = ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼)))
7372rspcev 3449 . . . . . . . . . . . . . . . . 17 (((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ 𝑈𝑘 = ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼)) → ∃𝑥𝑈 𝑘 = (𝑥𝐼))
7463, 70, 73syl2anc 696 . . . . . . . . . . . . . . . 16 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ∃𝑥𝑈 𝑘 = (𝑥𝐼))
75 eqid 2760 . . . . . . . . . . . . . . . . . 18 (𝑥𝑈 ↦ (𝑥𝐼)) = (𝑥𝑈 ↦ (𝑥𝐼))
7675elrnmpt 5527 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ V → (𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼)) ↔ ∃𝑥𝑈 𝑘 = (𝑥𝐼)))
7767, 76ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼)) ↔ ∃𝑥𝑈 𝑘 = (𝑥𝐼))
7874, 77sylibr 224 . . . . . . . . . . . . . . 15 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼)))
7978ex 449 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑘 ∈ (𝑔𝐼) → 𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))))
8079ssrdv 3750 . . . . . . . . . . . . 13 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))
81 eleq2 2828 . . . . . . . . . . . . . . 15 (𝑧 = (𝑔𝐼) → ((𝑠𝐼) ∈ 𝑧 ↔ (𝑠𝐼) ∈ (𝑔𝐼)))
82 sseq1 3767 . . . . . . . . . . . . . . 15 (𝑧 = (𝑔𝐼) → (𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)) ↔ (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
8381, 82anbi12d 749 . . . . . . . . . . . . . 14 (𝑧 = (𝑔𝐼) → (((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ((𝑠𝐼) ∈ (𝑔𝐼) ∧ (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
8483rspcev 3449 . . . . . . . . . . . . 13 (((𝑔𝐼) ∈ (𝐹𝐼) ∧ ((𝑠𝐼) ∈ (𝑔𝐼) ∧ (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
8531, 38, 80, 84syl12anc 1475 . . . . . . . . . . . 12 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
8685ex 449 . . . . . . . . . . 11 (((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) → ((𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
87 eleq2 2828 . . . . . . . . . . . . 13 (𝑤 = X𝑦𝐴 (𝑔𝑦) → (𝑠𝑤𝑠X𝑦𝐴 (𝑔𝑦)))
88 sseq1 3767 . . . . . . . . . . . . 13 (𝑤 = X𝑦𝐴 (𝑔𝑦) → (𝑤𝑈X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈))
8987, 88anbi12d 749 . . . . . . . . . . . 12 (𝑤 = X𝑦𝐴 (𝑔𝑦) → ((𝑠𝑤𝑤𝑈) ↔ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)))
9089imbi1d 330 . . . . . . . . . . 11 (𝑤 = X𝑦𝐴 (𝑔𝑦) → (((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))) ↔ ((𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9186, 90syl5ibrcom 237 . . . . . . . . . 10 (((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) → (𝑤 = X𝑦𝐴 (𝑔𝑦) → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9291expimpd 630 . . . . . . . . 9 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦)) → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9392exlimdv 2010 . . . . . . . 8 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦)) → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9424, 93syl5bi 232 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9594rexlimdv 3168 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (∃𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} (𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
9619, 95mpd 15 . . . . 5 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
9796ralrimiva 3104 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ∀𝑠𝑈𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
98 fvex 6363 . . . . . 6 (𝑠𝐼) ∈ V
9998rgenw 3062 . . . . 5 𝑠𝑈 (𝑠𝐼) ∈ V
100 fveq1 6352 . . . . . . 7 (𝑥 = 𝑠 → (𝑥𝐼) = (𝑠𝐼))
101100cbvmptv 4902 . . . . . 6 (𝑥𝑈 ↦ (𝑥𝐼)) = (𝑠𝑈 ↦ (𝑠𝐼))
102 eleq1 2827 . . . . . . . 8 (𝑦 = (𝑠𝐼) → (𝑦𝑧 ↔ (𝑠𝐼) ∈ 𝑧))
103102anbi1d 743 . . . . . . 7 (𝑦 = (𝑠𝐼) → ((𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
104103rexbidv 3190 . . . . . 6 (𝑦 = (𝑠𝐼) → (∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
105101, 104ralrnmpt 6532 . . . . 5 (∀𝑠𝑈 (𝑠𝐼) ∈ V → (∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ∀𝑠𝑈𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
10699, 105ax-mp 5 . . . 4 (∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ∀𝑠𝑈𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
10797, 106sylibr 224 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
108 simpl2 1230 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝐹:𝐴⟶Top)
109108, 29ffvelrnd 6524 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → (𝐹𝐼) ∈ Top)
110 eltop2 21001 . . . 4 ((𝐹𝐼) ∈ Top → (ran (𝑥𝑈 ↦ (𝑥𝐼)) ∈ (𝐹𝐼) ↔ ∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
111109, 110syl 17 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → (ran (𝑥𝑈 ↦ (𝑥𝐼)) ∈ (𝐹𝐼) ↔ ∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
112107, 111mpbird 247 . 2 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ran (𝑥𝑈 ↦ (𝑥𝐼)) ∈ (𝐹𝐼))
1138, 112eqeltrd 2839 1 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ((𝑥𝑌 ↦ (𝑥𝐼)) “ 𝑈) ∈ (𝐹𝐼))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wex 1853  wcel 2139  {cab 2746  wral 3050  wrex 3051  Vcvv 3340  cdif 3712  wss 3715  ifcif 4230   cuni 4588  cmpt 4881  ran crn 5267  cres 5268  cima 5269   Fn wfn 6044  wf 6045  cfv 6049  Xcixp 8076  Fincfn 8123  topGenctg 16320  tcpt 16321  Topctop 20920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ixp 8077  df-topgen 16326  df-pt 16327  df-top 20921
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator