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

Theorem ptpjopn 23560
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 5691 . . 3 ((𝑥𝑌 ↦ (𝑥𝐼)) “ 𝑈) = ran ((𝑥𝑌 ↦ (𝑥𝐼)) ↾ 𝑈)
2 elssuni 4941 . . . . . . 7 (𝑈𝐽𝑈 𝐽)
3 ptpjcn.1 . . . . . . 7 𝑌 = 𝐽
42, 3sseqtrrdi 4028 . . . . . 6 (𝑈𝐽𝑈𝑌)
54adantl 480 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝑈𝑌)
65resmptd 6045 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ((𝑥𝑌 ↦ (𝑥𝐼)) ↾ 𝑈) = (𝑥𝑈 ↦ (𝑥𝐼)))
76rneqd 5940 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ran ((𝑥𝑌 ↦ (𝑥𝐼)) ↾ 𝑈) = ran (𝑥𝑈 ↦ (𝑥𝐼)))
81, 7eqtrid 2777 . 2 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ((𝑥𝑌 ↦ (𝑥𝐼)) “ 𝑈) = ran (𝑥𝑈 ↦ (𝑥𝐼)))
9 ptpjcn.2 . . . . . . . . . . 11 𝐽 = (∏t𝐹)
10 ffn 6723 . . . . . . . . . . . 12 (𝐹:𝐴⟶Top → 𝐹 Fn 𝐴)
11 eqid 2725 . . . . . . . . . . . . 13 {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} = {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}
1211ptval 23518 . . . . . . . . . . . 12 ((𝐴𝑉𝐹 Fn 𝐴) → (∏t𝐹) = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
1310, 12sylan2 591 . . . . . . . . . . 11 ((𝐴𝑉𝐹:𝐴⟶Top) → (∏t𝐹) = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
149, 13eqtrid 2777 . . . . . . . . . 10 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐽 = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
15143adant3 1129 . . . . . . . . 9 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) → 𝐽 = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
1615eleq2d 2811 . . . . . . . 8 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) → (𝑈𝐽𝑈 ∈ (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))})))
1716biimpa 475 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝑈 ∈ (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
18 tg2 22912 . . . . . . 7 ((𝑈 ∈ (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}) ∧ 𝑠𝑈) → ∃𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} (𝑠𝑤𝑤𝑈))
1917, 18sylan 578 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → ∃𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} (𝑠𝑤𝑤𝑈))
20 vex 3465 . . . . . . . . 9 𝑤 ∈ V
21 eqeq1 2729 . . . . . . . . . . 11 (𝑠 = 𝑤 → (𝑠 = X𝑦𝐴 (𝑔𝑦) ↔ 𝑤 = X𝑦𝐴 (𝑔𝑦)))
2221anbi2d 628 . . . . . . . . . 10 (𝑠 = 𝑤 → (((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦)) ↔ ((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦))))
2322exbidv 1916 . . . . . . . . 9 (𝑠 = 𝑤 → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦)) ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦))))
2420, 23elab 3664 . . . . . . . 8 (𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦)))
25 fveq2 6896 . . . . . . . . . . . . . . 15 (𝑦 = 𝐼 → (𝑔𝑦) = (𝑔𝐼))
26 fveq2 6896 . . . . . . . . . . . . . . 15 (𝑦 = 𝐼 → (𝐹𝑦) = (𝐹𝐼))
2725, 26eleq12d 2819 . . . . . . . . . . . . . 14 (𝑦 = 𝐼 → ((𝑔𝑦) ∈ (𝐹𝑦) ↔ (𝑔𝐼) ∈ (𝐹𝐼)))
28 simplr2 1213 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦))
29 simpl3 1190 . . . . . . . . . . . . . . 15 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝐼𝐴)
3029ad3antrrr 728 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → 𝐼𝐴)
3127, 28, 30rspcdva 3607 . . . . . . . . . . . . 13 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑔𝐼) ∈ (𝐹𝐼))
32 fveq2 6896 . . . . . . . . . . . . . . 15 (𝑦 = 𝐼 → (𝑠𝑦) = (𝑠𝐼))
3332, 25eleq12d 2819 . . . . . . . . . . . . . 14 (𝑦 = 𝐼 → ((𝑠𝑦) ∈ (𝑔𝑦) ↔ (𝑠𝐼) ∈ (𝑔𝐼)))
34 vex 3465 . . . . . . . . . . . . . . . . 17 𝑠 ∈ V
3534elixp 8923 . . . . . . . . . . . . . . . 16 (𝑠X𝑦𝐴 (𝑔𝑦) ↔ (𝑠 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦)))
3635simprbi 495 . . . . . . . . . . . . . . 15 (𝑠X𝑦𝐴 (𝑔𝑦) → ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦))
3736ad2antrl 726 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦))
3833, 37, 30rspcdva 3607 . . . . . . . . . . . . 13 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑠𝐼) ∈ (𝑔𝐼))
39 simplrr 776 . . . . . . . . . . . . . . . . . 18 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)
40 simplrl 775 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ 𝑛 = 𝐼) → 𝑘 ∈ (𝑔𝐼))
41 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝐼 → (𝑔𝑛) = (𝑔𝐼))
4241adantl 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ 𝑛 = 𝐼) → (𝑔𝑛) = (𝑔𝐼))
4340, 42eleqtrrd 2828 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ 𝑛 = 𝐼) → 𝑘 ∈ (𝑔𝑛))
44 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑛 → (𝑠𝑦) = (𝑠𝑛))
45 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑛 → (𝑔𝑦) = (𝑔𝑛))
4644, 45eleq12d 2819 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑛 → ((𝑠𝑦) ∈ (𝑔𝑦) ↔ (𝑠𝑛) ∈ (𝑔𝑛)))
47 simplrl 775 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → 𝑠X𝑦𝐴 (𝑔𝑦))
4847, 36syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦))
49 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → 𝑛𝐴)
5046, 48, 49rspcdva 3607 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → (𝑠𝑛) ∈ (𝑔𝑛))
5150adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ ¬ 𝑛 = 𝐼) → (𝑠𝑛) ∈ (𝑔𝑛))
5243, 51ifclda 4565 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛))
5352anassrs 466 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) ∧ 𝑛𝐴) → if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛))
5453ralrimiva 3135 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ∀𝑛𝐴 if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛))
55 simpll1 1209 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → 𝐴𝑉)
5655ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝐴𝑉)
57 mptelixpg 8954 . . . . . . . . . . . . . . . . . . . . 21 (𝐴𝑉 → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑛𝐴 (𝑔𝑛) ↔ ∀𝑛𝐴 if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛)))
5856, 57syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑛𝐴 (𝑔𝑛) ↔ ∀𝑛𝐴 if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛)))
5954, 58mpbird 256 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑛𝐴 (𝑔𝑛))
60 fveq2 6896 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑦 → (𝑔𝑛) = (𝑔𝑦))
6160cbvixpv 8934 . . . . . . . . . . . . . . . . . . 19 X𝑛𝐴 (𝑔𝑛) = X𝑦𝐴 (𝑔𝑦)
6259, 61eleqtrdi 2835 . . . . . . . . . . . . . . . . . 18 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑦𝐴 (𝑔𝑦))
6339, 62sseldd 3977 . . . . . . . . . . . . . . . . 17 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ 𝑈)
6430adantr 479 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝐼𝐴)
65 iftrue 4536 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝐼 → if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) = 𝑘)
66 eqid 2725 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) = (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))
67 vex 3465 . . . . . . . . . . . . . . . . . . . 20 𝑘 ∈ V
6865, 66, 67fvmpt 7004 . . . . . . . . . . . . . . . . . . 19 (𝐼𝐴 → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼) = 𝑘)
6964, 68syl 17 . . . . . . . . . . . . . . . . . 18 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼) = 𝑘)
7069eqcomd 2731 . . . . . . . . . . . . . . . . 17 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝑘 = ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼))
71 fveq1 6895 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) → (𝑥𝐼) = ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼))
7271rspceeqv 3628 . . . . . . . . . . . . . . . . 17 (((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ 𝑈𝑘 = ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼)) → ∃𝑥𝑈 𝑘 = (𝑥𝐼))
7363, 70, 72syl2anc 582 . . . . . . . . . . . . . . . 16 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ∃𝑥𝑈 𝑘 = (𝑥𝐼))
74 eqid 2725 . . . . . . . . . . . . . . . . . 18 (𝑥𝑈 ↦ (𝑥𝐼)) = (𝑥𝑈 ↦ (𝑥𝐼))
7574elrnmpt 5958 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ V → (𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼)) ↔ ∃𝑥𝑈 𝑘 = (𝑥𝐼)))
7675elv 3467 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼)) ↔ ∃𝑥𝑈 𝑘 = (𝑥𝐼))
7773, 76sylibr 233 . . . . . . . . . . . . . . 15 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼)))
7877ex 411 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑘 ∈ (𝑔𝐼) → 𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))))
7978ssrdv 3982 . . . . . . . . . . . . 13 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))
80 eleq2 2814 . . . . . . . . . . . . . . 15 (𝑧 = (𝑔𝐼) → ((𝑠𝐼) ∈ 𝑧 ↔ (𝑠𝐼) ∈ (𝑔𝐼)))
81 sseq1 4002 . . . . . . . . . . . . . . 15 (𝑧 = (𝑔𝐼) → (𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)) ↔ (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
8280, 81anbi12d 630 . . . . . . . . . . . . . 14 (𝑧 = (𝑔𝐼) → (((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ((𝑠𝐼) ∈ (𝑔𝐼) ∧ (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
8382rspcev 3606 . . . . . . . . . . . . 13 (((𝑔𝐼) ∈ (𝐹𝐼) ∧ ((𝑠𝐼) ∈ (𝑔𝐼) ∧ (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
8431, 38, 79, 83syl12anc 835 . . . . . . . . . . . 12 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
8584ex 411 . . . . . . . . . . 11 (((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) → ((𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
86 eleq2 2814 . . . . . . . . . . . . 13 (𝑤 = X𝑦𝐴 (𝑔𝑦) → (𝑠𝑤𝑠X𝑦𝐴 (𝑔𝑦)))
87 sseq1 4002 . . . . . . . . . . . . 13 (𝑤 = X𝑦𝐴 (𝑔𝑦) → (𝑤𝑈X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈))
8886, 87anbi12d 630 . . . . . . . . . . . 12 (𝑤 = X𝑦𝐴 (𝑔𝑦) → ((𝑠𝑤𝑤𝑈) ↔ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)))
8988imbi1d 340 . . . . . . . . . . 11 (𝑤 = X𝑦𝐴 (𝑔𝑦) → (((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))) ↔ ((𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9085, 89syl5ibrcom 246 . . . . . . . . . 10 (((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) → (𝑤 = X𝑦𝐴 (𝑔𝑦) → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9190expimpd 452 . . . . . . . . 9 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦)) → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9291exlimdv 1928 . . . . . . . 8 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦)) → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9324, 92biimtrid 241 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9493rexlimdv 3142 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (∃𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} (𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
9519, 94mpd 15 . . . . 5 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
9695ralrimiva 3135 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ∀𝑠𝑈𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
97 fvex 6909 . . . . . 6 (𝑠𝐼) ∈ V
9897rgenw 3054 . . . . 5 𝑠𝑈 (𝑠𝐼) ∈ V
99 fveq1 6895 . . . . . . 7 (𝑥 = 𝑠 → (𝑥𝐼) = (𝑠𝐼))
10099cbvmptv 5262 . . . . . 6 (𝑥𝑈 ↦ (𝑥𝐼)) = (𝑠𝑈 ↦ (𝑠𝐼))
101 eleq1 2813 . . . . . . . 8 (𝑦 = (𝑠𝐼) → (𝑦𝑧 ↔ (𝑠𝐼) ∈ 𝑧))
102101anbi1d 629 . . . . . . 7 (𝑦 = (𝑠𝐼) → ((𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
103102rexbidv 3168 . . . . . 6 (𝑦 = (𝑠𝐼) → (∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
104100, 103ralrnmptw 7103 . . . . 5 (∀𝑠𝑈 (𝑠𝐼) ∈ V → (∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ∀𝑠𝑈𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
10598, 104ax-mp 5 . . . 4 (∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ∀𝑠𝑈𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
10696, 105sylibr 233 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
107 simpl2 1189 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝐹:𝐴⟶Top)
108107, 29ffvelcdmd 7094 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → (𝐹𝐼) ∈ Top)
109 eltop2 22922 . . . 4 ((𝐹𝐼) ∈ Top → (ran (𝑥𝑈 ↦ (𝑥𝐼)) ∈ (𝐹𝐼) ↔ ∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
110108, 109syl 17 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → (ran (𝑥𝑈 ↦ (𝑥𝐼)) ∈ (𝐹𝐼) ↔ ∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
111106, 110mpbird 256 . 2 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ran (𝑥𝑈 ↦ (𝑥𝐼)) ∈ (𝐹𝐼))
1128, 111eqeltrd 2825 1 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ((𝑥𝑌 ↦ (𝑥𝐼)) “ 𝑈) ∈ (𝐹𝐼))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wex 1773  wcel 2098  {cab 2702  wral 3050  wrex 3059  Vcvv 3461  cdif 3941  wss 3944  ifcif 4530   cuni 4909  cmpt 5232  ran crn 5679  cres 5680  cima 5681   Fn wfn 6544  wf 6545  cfv 6549  Xcixp 8916  Fincfn 8964  topGenctg 17422  tcpt 17423  Topctop 22839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ixp 8917  df-topgen 17428  df-pt 17429  df-top 22840
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator