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

Theorem ptpjopn 21325
 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 5087 . . 3 ((𝑥𝑌 ↦ (𝑥𝐼)) “ 𝑈) = ran ((𝑥𝑌 ↦ (𝑥𝐼)) ↾ 𝑈)
2 elssuni 4433 . . . . . . 7 (𝑈𝐽𝑈 𝐽)
3 ptpjcn.1 . . . . . . 7 𝑌 = 𝐽
42, 3syl6sseqr 3631 . . . . . 6 (𝑈𝐽𝑈𝑌)
54adantl 482 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝑈𝑌)
65resmptd 5411 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ((𝑥𝑌 ↦ (𝑥𝐼)) ↾ 𝑈) = (𝑥𝑈 ↦ (𝑥𝐼)))
76rneqd 5313 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ran ((𝑥𝑌 ↦ (𝑥𝐼)) ↾ 𝑈) = ran (𝑥𝑈 ↦ (𝑥𝐼)))
81, 7syl5eq 2667 . 2 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ((𝑥𝑌 ↦ (𝑥𝐼)) “ 𝑈) = ran (𝑥𝑈 ↦ (𝑥𝐼)))
9 ptpjcn.2 . . . . . . . . . . 11 𝐽 = (∏t𝐹)
10 ffn 6002 . . . . . . . . . . . 12 (𝐹:𝐴⟶Top → 𝐹 Fn 𝐴)
11 eqid 2621 . . . . . . . . . . . . 13 {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} = {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}
1211ptval 21283 . . . . . . . . . . . 12 ((𝐴𝑉𝐹 Fn 𝐴) → (∏t𝐹) = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
1310, 12sylan2 491 . . . . . . . . . . 11 ((𝐴𝑉𝐹:𝐴⟶Top) → (∏t𝐹) = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
149, 13syl5eq 2667 . . . . . . . . . 10 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐽 = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
15143adant3 1079 . . . . . . . . 9 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) → 𝐽 = (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
1615eleq2d 2684 . . . . . . . 8 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) → (𝑈𝐽𝑈 ∈ (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))})))
1716biimpa 501 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝑈 ∈ (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}))
18 tg2 20680 . . . . . . 7 ((𝑈 ∈ (topGen‘{𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))}) ∧ 𝑠𝑈) → ∃𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} (𝑠𝑤𝑤𝑈))
1917, 18sylan 488 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → ∃𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} (𝑠𝑤𝑤𝑈))
20 vex 3189 . . . . . . . . 9 𝑤 ∈ V
21 eqeq1 2625 . . . . . . . . . . 11 (𝑠 = 𝑤 → (𝑠 = X𝑦𝐴 (𝑔𝑦) ↔ 𝑤 = X𝑦𝐴 (𝑔𝑦)))
2221anbi2d 739 . . . . . . . . . 10 (𝑠 = 𝑤 → (((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦)) ↔ ((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦))))
2322exbidv 1847 . . . . . . . . 9 (𝑠 = 𝑤 → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦)) ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦))))
2420, 23elab 3333 . . . . . . . 8 (𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦)))
25 simpl3 1064 . . . . . . . . . . . . . . 15 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝐼𝐴)
2625ad3antrrr 765 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → 𝐼𝐴)
27 simplr2 1102 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦))
28 fveq2 6148 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐼 → (𝑔𝑦) = (𝑔𝐼))
29 fveq2 6148 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐼 → (𝐹𝑦) = (𝐹𝐼))
3028, 29eleq12d 2692 . . . . . . . . . . . . . . 15 (𝑦 = 𝐼 → ((𝑔𝑦) ∈ (𝐹𝑦) ↔ (𝑔𝐼) ∈ (𝐹𝐼)))
3130rspcv 3291 . . . . . . . . . . . . . 14 (𝐼𝐴 → (∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) → (𝑔𝐼) ∈ (𝐹𝐼)))
3226, 27, 31sylc 65 . . . . . . . . . . . . 13 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑔𝐼) ∈ (𝐹𝐼))
33 vex 3189 . . . . . . . . . . . . . . . . 17 𝑠 ∈ V
3433elixp 7859 . . . . . . . . . . . . . . . 16 (𝑠X𝑦𝐴 (𝑔𝑦) ↔ (𝑠 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦)))
3534simprbi 480 . . . . . . . . . . . . . . 15 (𝑠X𝑦𝐴 (𝑔𝑦) → ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦))
3635ad2antrl 763 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦))
37 fveq2 6148 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐼 → (𝑠𝑦) = (𝑠𝐼))
3837, 28eleq12d 2692 . . . . . . . . . . . . . . 15 (𝑦 = 𝐼 → ((𝑠𝑦) ∈ (𝑔𝑦) ↔ (𝑠𝐼) ∈ (𝑔𝐼)))
3938rspcv 3291 . . . . . . . . . . . . . 14 (𝐼𝐴 → (∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦) → (𝑠𝐼) ∈ (𝑔𝐼)))
4026, 36, 39sylc 65 . . . . . . . . . . . . 13 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑠𝐼) ∈ (𝑔𝐼))
41 simplrr 800 . . . . . . . . . . . . . . . . . 18 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)
42 simplrl 799 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ 𝑛 = 𝐼) → 𝑘 ∈ (𝑔𝐼))
43 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝐼 → (𝑔𝑛) = (𝑔𝐼))
4443adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ 𝑛 = 𝐼) → (𝑔𝑛) = (𝑔𝐼))
4542, 44eleqtrrd 2701 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ 𝑛 = 𝐼) → 𝑘 ∈ (𝑔𝑛))
46 simprr 795 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → 𝑛𝐴)
47 simplrl 799 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → 𝑠X𝑦𝐴 (𝑔𝑦))
4847, 35syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → ∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦))
49 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑛 → (𝑠𝑦) = (𝑠𝑛))
50 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑛 → (𝑔𝑦) = (𝑔𝑛))
5149, 50eleq12d 2692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑛 → ((𝑠𝑦) ∈ (𝑔𝑦) ↔ (𝑠𝑛) ∈ (𝑔𝑛)))
5251rspcv 3291 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛𝐴 → (∀𝑦𝐴 (𝑠𝑦) ∈ (𝑔𝑦) → (𝑠𝑛) ∈ (𝑔𝑛)))
5346, 48, 52sylc 65 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → (𝑠𝑛) ∈ (𝑔𝑛))
5453adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) ∧ ¬ 𝑛 = 𝐼) → (𝑠𝑛) ∈ (𝑔𝑛))
5545, 54ifclda 4092 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ (𝑘 ∈ (𝑔𝐼) ∧ 𝑛𝐴)) → if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛))
5655anassrs 679 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) ∧ 𝑛𝐴) → if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛))
5756ralrimiva 2960 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ∀𝑛𝐴 if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛))
58 simpll1 1098 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → 𝐴𝑉)
5958ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝐴𝑉)
60 mptelixpg 7889 . . . . . . . . . . . . . . . . . . . . 21 (𝐴𝑉 → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑛𝐴 (𝑔𝑛) ↔ ∀𝑛𝐴 if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛)))
6159, 60syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑛𝐴 (𝑔𝑛) ↔ ∀𝑛𝐴 if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) ∈ (𝑔𝑛)))
6257, 61mpbird 247 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑛𝐴 (𝑔𝑛))
63 fveq2 6148 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑦 → (𝑔𝑛) = (𝑔𝑦))
6463cbvixpv 7870 . . . . . . . . . . . . . . . . . . 19 X𝑛𝐴 (𝑔𝑛) = X𝑦𝐴 (𝑔𝑦)
6562, 64syl6eleq 2708 . . . . . . . . . . . . . . . . . 18 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ X𝑦𝐴 (𝑔𝑦))
6641, 65sseldd 3584 . . . . . . . . . . . . . . . . 17 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ 𝑈)
6726adantr 481 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝐼𝐴)
68 iftrue 4064 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝐼 → if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)) = 𝑘)
69 eqid 2621 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) = (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))
70 vex 3189 . . . . . . . . . . . . . . . . . . . 20 𝑘 ∈ V
7168, 69, 70fvmpt 6239 . . . . . . . . . . . . . . . . . . 19 (𝐼𝐴 → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼) = 𝑘)
7267, 71syl 17 . . . . . . . . . . . . . . . . . 18 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼) = 𝑘)
7372eqcomd 2627 . . . . . . . . . . . . . . . . 17 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝑘 = ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼))
74 fveq1 6147 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) → (𝑥𝐼) = ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼))
7574eqeq2d 2631 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) → (𝑘 = (𝑥𝐼) ↔ 𝑘 = ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼)))
7675rspcev 3295 . . . . . . . . . . . . . . . . 17 (((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛))) ∈ 𝑈𝑘 = ((𝑛𝐴 ↦ if(𝑛 = 𝐼, 𝑘, (𝑠𝑛)))‘𝐼)) → ∃𝑥𝑈 𝑘 = (𝑥𝐼))
7766, 73, 76syl2anc 692 . . . . . . . . . . . . . . . 16 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → ∃𝑥𝑈 𝑘 = (𝑥𝐼))
78 eqid 2621 . . . . . . . . . . . . . . . . . 18 (𝑥𝑈 ↦ (𝑥𝐼)) = (𝑥𝑈 ↦ (𝑥𝐼))
7978elrnmpt 5332 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ V → (𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼)) ↔ ∃𝑥𝑈 𝑘 = (𝑥𝐼)))
8070, 79ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼)) ↔ ∃𝑥𝑈 𝑘 = (𝑥𝐼))
8177, 80sylibr 224 . . . . . . . . . . . . . . 15 (((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) ∧ 𝑘 ∈ (𝑔𝐼)) → 𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼)))
8281ex 450 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑘 ∈ (𝑔𝐼) → 𝑘 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))))
8382ssrdv 3589 . . . . . . . . . . . . 13 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))
84 eleq2 2687 . . . . . . . . . . . . . . 15 (𝑧 = (𝑔𝐼) → ((𝑠𝐼) ∈ 𝑧 ↔ (𝑠𝐼) ∈ (𝑔𝐼)))
85 sseq1 3605 . . . . . . . . . . . . . . 15 (𝑧 = (𝑔𝐼) → (𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)) ↔ (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
8684, 85anbi12d 746 . . . . . . . . . . . . . 14 (𝑧 = (𝑔𝐼) → (((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ((𝑠𝐼) ∈ (𝑔𝐼) ∧ (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
8786rspcev 3295 . . . . . . . . . . . . 13 (((𝑔𝐼) ∈ (𝐹𝐼) ∧ ((𝑠𝐼) ∈ (𝑔𝐼) ∧ (𝑔𝐼) ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
8832, 40, 83, 87syl12anc 1321 . . . . . . . . . . . 12 ((((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) ∧ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
8988ex 450 . . . . . . . . . . 11 (((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) → ((𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
90 eleq2 2687 . . . . . . . . . . . . 13 (𝑤 = X𝑦𝐴 (𝑔𝑦) → (𝑠𝑤𝑠X𝑦𝐴 (𝑔𝑦)))
91 sseq1 3605 . . . . . . . . . . . . 13 (𝑤 = X𝑦𝐴 (𝑔𝑦) → (𝑤𝑈X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈))
9290, 91anbi12d 746 . . . . . . . . . . . 12 (𝑤 = X𝑦𝐴 (𝑔𝑦) → ((𝑠𝑤𝑤𝑈) ↔ (𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈)))
9392imbi1d 331 . . . . . . . . . . 11 (𝑤 = X𝑦𝐴 (𝑔𝑦) → (((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))) ↔ ((𝑠X𝑦𝐴 (𝑔𝑦) ∧ X𝑦𝐴 (𝑔𝑦) ⊆ 𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9489, 93syl5ibrcom 237 . . . . . . . . . 10 (((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))) → (𝑤 = X𝑦𝐴 (𝑔𝑦) → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9594expimpd 628 . . . . . . . . 9 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦)) → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9695exlimdv 1858 . . . . . . . 8 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑤 = X𝑦𝐴 (𝑔𝑦)) → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9724, 96syl5bi 232 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} → ((𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))))
9897rexlimdv 3023 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → (∃𝑤 ∈ {𝑠 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑔𝑦))} (𝑠𝑤𝑤𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
9919, 98mpd 15 . . . . 5 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) ∧ 𝑠𝑈) → ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
10099ralrimiva 2960 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ∀𝑠𝑈𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
101 fvex 6158 . . . . . 6 (𝑠𝐼) ∈ V
102101rgenw 2919 . . . . 5 𝑠𝑈 (𝑠𝐼) ∈ V
103 fveq1 6147 . . . . . . 7 (𝑥 = 𝑠 → (𝑥𝐼) = (𝑠𝐼))
104103cbvmptv 4710 . . . . . 6 (𝑥𝑈 ↦ (𝑥𝐼)) = (𝑠𝑈 ↦ (𝑠𝐼))
105 eleq1 2686 . . . . . . . 8 (𝑦 = (𝑠𝐼) → (𝑦𝑧 ↔ (𝑠𝐼) ∈ 𝑧))
106105anbi1d 740 . . . . . . 7 (𝑦 = (𝑠𝐼) → ((𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
107106rexbidv 3045 . . . . . 6 (𝑦 = (𝑠𝐼) → (∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ∃𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
108104, 107ralrnmpt 6324 . . . . 5 (∀𝑠𝑈 (𝑠𝐼) ∈ V → (∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ∀𝑠𝑈𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
109102, 108ax-mp 5 . . . 4 (∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))) ↔ ∀𝑠𝑈𝑧 ∈ (𝐹𝐼)((𝑠𝐼) ∈ 𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
110100, 109sylibr 224 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼))))
111 simpl2 1063 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → 𝐹:𝐴⟶Top)
112111, 25ffvelrnd 6316 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → (𝐹𝐼) ∈ Top)
113 eltop2 20690 . . . 4 ((𝐹𝐼) ∈ Top → (ran (𝑥𝑈 ↦ (𝑥𝐼)) ∈ (𝐹𝐼) ↔ ∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
114112, 113syl 17 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → (ran (𝑥𝑈 ↦ (𝑥𝐼)) ∈ (𝐹𝐼) ↔ ∀𝑦 ∈ ran (𝑥𝑈 ↦ (𝑥𝐼))∃𝑧 ∈ (𝐹𝐼)(𝑦𝑧𝑧 ⊆ ran (𝑥𝑈 ↦ (𝑥𝐼)))))
115110, 114mpbird 247 . 2 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ran (𝑥𝑈 ↦ (𝑥𝐼)) ∈ (𝐹𝐼))
1168, 115eqeltrd 2698 1 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐼𝐴) ∧ 𝑈𝐽) → ((𝑥𝑌 ↦ (𝑥𝐼)) “ 𝑈) ∈ (𝐹𝐼))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480  ∃wex 1701   ∈ wcel 1987  {cab 2607  ∀wral 2907  ∃wrex 2908  Vcvv 3186   ∖ cdif 3552   ⊆ wss 3555  ifcif 4058  ∪ cuni 4402   ↦ cmpt 4673  ran crn 5075   ↾ cres 5076   “ cima 5077   Fn wfn 5842  ⟶wf 5843  ‘cfv 5847  Xcixp 7852  Fincfn 7899  topGenctg 16019  ∏tcpt 16020  Topctop 20617 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ixp 7853  df-topgen 16025  df-pt 16026  df-top 20621 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator