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

Theorem ptpjopn 21711
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 5292 . . 3 ((𝑥𝑌 ↦ (𝑥𝐼)) “ 𝑈) = ran ((𝑥𝑌 ↦ (𝑥𝐼)) ↾ 𝑈)
2 elssuni 4627 . . . . . . 7 (𝑈𝐽𝑈 𝐽)
3 ptpjcn.1 . . . . . . 7 𝑌 = 𝐽
42, 3syl6sseqr 3814 . . . . . 6 (𝑈𝐽𝑈𝑌)
54adantl 473 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝑈𝑌)
65resmptd 5631 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ((𝑥𝑌 ↦ (𝑥𝐼)) ↾ 𝑈) = (𝑥𝑈 ↦ (𝑥𝐼)))
76rneqd 5523 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ran ((𝑥𝑌 ↦ (𝑥𝐼)) ↾ 𝑈) = ran (𝑥𝑈 ↦ (𝑥𝐼)))
81, 7syl5eq 2811 . 2 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ((𝑥𝑌 ↦ (𝑥𝐼)) “ 𝑈) = ran (𝑥𝑈 ↦ (𝑥𝐼)))
9 ptpjcn.2 . . . . . . . . . . 11 𝐽 = (∏t𝐹)
10 ffn 6225 . . . . . . . . . . . 12 (𝐹:𝐴⟶Top → 𝐹 Fn 𝐴)
11 eqid 2765 . . . . . . . . . . . . 13 {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} = {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}
1211ptval 21669 . . . . . . . . . . . 12 ((𝐴𝑉𝐹 Fn 𝐴) → (∏t𝐹) = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
1310, 12sylan2 586 . . . . . . . . . . 11 ((𝐴𝑉𝐹:𝐴⟶Top) → (∏t𝐹) = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
149, 13syl5eq 2811 . . . . . . . . . 10 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐽 = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
15143adant3 1162 . . . . . . . . 9 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) → 𝐽 = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
1615eleq2d 2830 . . . . . . . 8 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) → (𝑈𝐽𝑈 ∈ (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))})))
1716biimpa 468 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝑈 ∈ (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
18 tg2 21065 . . . . . . 7 ((𝑈 ∈ (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}) ∧ 𝑠𝑈) → ∃𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} (𝑠𝑤𝑤𝑈))
1917, 18sylan 575 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → ∃𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} (𝑠𝑤𝑤𝑈))
20 vex 3353 . . . . . . . . 9 𝑤 ∈ V
21 eqeq1 2769 . . . . . . . . . . 11 (𝑠 = 𝑤 → (𝑠 = X𝑦𝐴 (𝑔𝑦) ↔ 𝑤 = X𝑦𝐴 (𝑔𝑦)))
2221anbi2d 622 . . . . . . . . . 10 (𝑠 = 𝑤 → (((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦)) ↔ ((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦))))
2322exbidv 2016 . . . . . . . . 9 (𝑠 = 𝑤 → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦)) ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦))))
2420, 23elab 3507 . . . . . . . 8 (𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦)))
25 fveq2 6379 . . . . . . . . . . . . . . 15 (𝑦 = 𝐼 → (𝑔𝑦) = (𝑔𝐼))
26 fveq2 6379 . . . . . . . . . . . . . . 15 (𝑦 = 𝐼 → (𝐹𝑦) = (𝐹𝐼))
2725, 26eleq12d 2838 . . . . . . . . . . . . . 14 (𝑦 = 𝐼 → ((𝑔𝑦) ∈ (𝐹𝑦) ↔ (𝑔𝐼) ∈ (𝐹𝐼)))
28 simplr2 1277 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦))
29 simpl3 1246 . . . . . . . . . . . . . . 15 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝐼𝐴)
3029ad3antrrr 721 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → 𝐼𝐴)
3127, 28, 30rspcdva 3468 . . . . . . . . . . . . 13 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑔𝐼) ∈ (𝐹𝐼))
32 fveq2 6379 . . . . . . . . . . . . . . 15 (𝑦 = 𝐼 → (𝑠𝑦) = (𝑠𝐼))
3332, 25eleq12d 2838 . . . . . . . . . . . . . 14 (𝑦 = 𝐼 → ((𝑠𝑦) ∈ (𝑔𝑦) ↔ (𝑠𝐼) ∈ (𝑔𝐼)))
34 vex 3353 . . . . . . . . . . . . . . . . 17 𝑠 ∈ V
3534elixp 8124 . . . . . . . . . . . . . . . 16 (𝑠X𝑦𝐴 (𝑔𝑦) ↔ (𝑠 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦)))
3635simprbi 490 . . . . . . . . . . . . . . 15 (𝑠X𝑦𝐴 (𝑔𝑦) → ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦))
3736ad2antrl 719 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦))
3833, 37, 30rspcdva 3468 . . . . . . . . . . . . 13 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑠𝐼) ∈ (𝑔𝐼))
39 simplrr 796 . . . . . . . . . . . . . . . . . 18 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)
40 simplrl 795 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ 𝑛 = 𝐼) → 𝑘 ∈ (𝑔𝐼))
41 fveq2 6379 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝐼 → (𝑔𝑛) = (𝑔𝐼))
4241adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ 𝑛 = 𝐼) → (𝑔𝑛) = (𝑔𝐼))
4340, 42eleqtrrd 2847 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ 𝑛 = 𝐼) → 𝑘 ∈ (𝑔𝑛))
44 fveq2 6379 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑛 → (𝑠𝑦) = (𝑠𝑛))
45 fveq2 6379 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑛 → (𝑔𝑦) = (𝑔𝑛))
4644, 45eleq12d 2838 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑛 → ((𝑠𝑦) ∈ (𝑔𝑦) ↔ (𝑠𝑛) ∈ (𝑔𝑛)))
47 simplrl 795 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → 𝑠X𝑦𝐴 (𝑔𝑦))
4847, 36syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦))
49 simprr 789 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → 𝑛𝐴)
5046, 48, 49rspcdva 3468 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → (𝑠𝑛) ∈ (𝑔𝑛))
5150adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ ¬ 𝑛 = 𝐼) → (𝑠𝑛) ∈ (𝑔𝑛))
5243, 51ifclda 4279 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛))
5352anassrs 459 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) ∧ 𝑛𝐴) → if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛))
5453ralrimiva 3113 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ∀𝑛𝐴 if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛))
55 simpll1 1269 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → 𝐴𝑉)
5655ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝐴𝑉)
57 mptelixpg 8154 . . . . . . . . . . . . . . . . . . . . 21 (𝐴𝑉 → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑛𝐴 (𝑔𝑛) ↔ ∀𝑛𝐴 if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛)))
5856, 57syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑛𝐴 (𝑔𝑛) ↔ ∀𝑛𝐴 if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛)))
5954, 58mpbird 248 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑛𝐴 (𝑔𝑛))
60 fveq2 6379 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑦 → (𝑔𝑛) = (𝑔𝑦))
6160cbvixpv 8135 . . . . . . . . . . . . . . . . . . 19 X𝑛𝐴 (𝑔𝑛) = X𝑦𝐴 (𝑔𝑦)
6259, 61syl6eleq 2854 . . . . . . . . . . . . . . . . . 18 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑦𝐴 (𝑔𝑦))
6339, 62sseldd 3764 . . . . . . . . . . . . . . . . 17 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ 𝑈)
6430adantr 472 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝐼𝐴)
65 iftrue 4251 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝐼 → if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) = 𝑘)
66 eqid 2765 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) = (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))
67 vex 3353 . . . . . . . . . . . . . . . . . . . 20 𝑘 ∈ V
6865, 66, 67fvmpt 6475 . . . . . . . . . . . . . . . . . . 19 (𝐼𝐴 → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼) = 𝑘)
6964, 68syl 17 . . . . . . . . . . . . . . . . . 18 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼) = 𝑘)
7069eqcomd 2771 . . . . . . . . . . . . . . . . 17 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝑘 = ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼))
71 fveq1 6378 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) → (𝑥𝐼) = ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼))
7271rspceeqv 3480 . . . . . . . . . . . . . . . . 17 (((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ 𝑈𝑘 = ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼)) → ∃𝑥𝑈 𝑘 = (𝑥𝐼))
7363, 70, 72syl2anc 579 . . . . . . . . . . . . . . . 16 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ∃𝑥𝑈 𝑘 = (𝑥𝐼))
74 eqid 2765 . . . . . . . . . . . . . . . . . 18 (𝑥𝑈 ↦ (𝑥𝐼)) = (𝑥𝑈 ↦ (𝑥𝐼))
7574elrnmpt 5543 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ V → (𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼)) ↔ ∃𝑥𝑈 𝑘 = (𝑥𝐼)))
7667, 75ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼)) ↔ ∃𝑥𝑈 𝑘 = (𝑥𝐼))
7773, 76sylibr 225 . . . . . . . . . . . . . . 15 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼)))
7877ex 401 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑘 ∈ (𝑔𝐼) → 𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))))
7978ssrdv 3769 . . . . . . . . . . . . 13 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))
80 eleq2 2833 . . . . . . . . . . . . . . 15 (𝑧 = (𝑔𝐼) → ((𝑠𝐼) ∈ 𝑧 ↔ (𝑠𝐼) ∈ (𝑔𝐼)))
81 sseq1 3788 . . . . . . . . . . . . . . 15 (𝑧 = (𝑔𝐼) → (𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)) ↔ (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
8280, 81anbi12d 624 . . . . . . . . . . . . . 14 (𝑧 = (𝑔𝐼) → (((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ((𝑠𝐼) ∈ (𝑔𝐼) ∧ (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
8382rspcev 3462 . . . . . . . . . . . . 13 (((𝑔𝐼) ∈ (𝐹𝐼) ∧ ((𝑠𝐼) ∈ (𝑔𝐼) ∧ (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
8431, 38, 79, 83syl12anc 865 . . . . . . . . . . . 12 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
8584ex 401 . . . . . . . . . . 11 (((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) → ((𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
86 eleq2 2833 . . . . . . . . . . . . 13 (𝑤 = X𝑦𝐴 (𝑔𝑦) → (𝑠𝑤𝑠X𝑦𝐴 (𝑔𝑦)))
87 sseq1 3788 . . . . . . . . . . . . 13 (𝑤 = X𝑦𝐴 (𝑔𝑦) → (𝑤𝑈X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈))
8886, 87anbi12d 624 . . . . . . . . . . . 12 (𝑤 = X𝑦𝐴 (𝑔𝑦) → ((𝑠𝑤𝑤𝑈) ↔ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)))
8988imbi1d 332 . . . . . . . . . . 11 (𝑤 = X𝑦𝐴 (𝑔𝑦) → (((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))) ↔ ((𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9085, 89syl5ibrcom 238 . . . . . . . . . 10 (((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) → (𝑤 = X𝑦𝐴 (𝑔𝑦) → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9190expimpd 445 . . . . . . . . 9 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦)) → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9291exlimdv 2028 . . . . . . . 8 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦)) → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9324, 92syl5bi 233 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9493rexlimdv 3177 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (∃𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} (𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
9519, 94mpd 15 . . . . 5 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
9695ralrimiva 3113 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ∀𝑠𝑈𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
97 fvex 6392 . . . . . 6 (𝑠𝐼) ∈ V
9897rgenw 3071 . . . . 5 𝑠𝑈 (𝑠𝐼) ∈ V
99 fveq1 6378 . . . . . . 7 (𝑥 = 𝑠 → (𝑥𝐼) = (𝑠𝐼))
10099cbvmptv 4911 . . . . . 6 (𝑥𝑈 ↦ (𝑥𝐼)) = (𝑠𝑈 ↦ (𝑠𝐼))
101 eleq1 2832 . . . . . . . 8 (𝑦 = (𝑠𝐼) → (𝑦𝑧 ↔ (𝑠𝐼) ∈ 𝑧))
102101anbi1d 623 . . . . . . 7 (𝑦 = (𝑠𝐼) → ((𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
103102rexbidv 3199 . . . . . 6 (𝑦 = (𝑠𝐼) → (∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
104100, 103ralrnmpt 6562 . . . . 5 (∀𝑠𝑈 (𝑠𝐼) ∈ V → (∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ∀𝑠𝑈𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
10598, 104ax-mp 5 . . . 4 (∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ∀𝑠𝑈𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
10696, 105sylibr 225 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
107 simpl2 1244 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝐹:𝐴⟶Top)
108107, 29ffvelrnd 6554 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → (𝐹𝐼) ∈ Top)
109 eltop2 21075 . . . 4 ((𝐹𝐼) ∈ Top → (ran (𝑥𝑈 ↦ (𝑥𝐼)) ∈ (𝐹𝐼) ↔ ∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
110108, 109syl 17 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → (ran (𝑥𝑈 ↦ (𝑥𝐼)) ∈ (𝐹𝐼) ↔ ∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
111106, 110mpbird 248 . 2 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ran (𝑥𝑈 ↦ (𝑥𝐼)) ∈ (𝐹𝐼))
1128, 111eqeltrd 2844 1 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ((𝑥𝑌 ↦ (𝑥𝐼)) “ 𝑈) ∈ (𝐹𝐼))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wex 1874  wcel 2155  {cab 2751  wral 3055  wrex 3056  Vcvv 3350  cdif 3731  wss 3734  ifcif 4245   cuni 4596  cmpt 4890  ran crn 5280  cres 5281  cima 5282   Fn wfn 6065  wf 6066  cfv 6070  Xcixp 8117  Fincfn 8164  topGenctg 16380  tcpt 16381  Topctop 20993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-ixp 8118  df-topgen 16386  df-pt 16387  df-top 20994
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator