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

Theorem dfac14 21910
Description: Theorem ptcls 21908 is an equivalent of the axiom of choice. (Contributed by Mario Carneiro, 3-Sep-2015.)
Assertion
Ref Expression
dfac14 (CHOICE ↔ ∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))))
Distinct variable group:   𝑓,𝑘,𝑠

Proof of Theorem dfac14
Dummy variables 𝑔 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6538 . . . . . . . . . 10 (𝑘 = 𝑥 → (𝑓𝑘) = (𝑓𝑥))
21unieqd 4755 . . . . . . . . 9 (𝑘 = 𝑥 (𝑓𝑘) = (𝑓𝑥))
32pweqd 4458 . . . . . . . 8 (𝑘 = 𝑥 → 𝒫 (𝑓𝑘) = 𝒫 (𝑓𝑥))
43cbvixpv 8328 . . . . . . 7 X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) = X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)
54eleq2i 2874 . . . . . 6 (𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) ↔ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥))
6 simplr 765 . . . . . . . . . . 11 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑓:dom 𝑓⟶Top)
76feqmptd 6601 . . . . . . . . . 10 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑓 = (𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘)))
87fveq2d 6542 . . . . . . . . 9 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → (∏t𝑓) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))))
98fveq2d 6542 . . . . . . . 8 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → (cls‘(∏t𝑓)) = (cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘)))))
109fveq1d 6540 . . . . . . 7 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)))
11 eqid 2795 . . . . . . . 8 (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘)))
12 vex 3440 . . . . . . . . . 10 𝑓 ∈ V
1312dmex 7472 . . . . . . . . 9 dom 𝑓 ∈ V
1413a1i 11 . . . . . . . 8 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → dom 𝑓 ∈ V)
156ffvelrnda 6716 . . . . . . . . 9 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑓𝑘) ∈ Top)
16 toptopon2 21210 . . . . . . . . 9 ((𝑓𝑘) ∈ Top ↔ (𝑓𝑘) ∈ (TopOn‘ (𝑓𝑘)))
1715, 16sylib 219 . . . . . . . 8 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑓𝑘) ∈ (TopOn‘ (𝑓𝑘)))
18 simpr 485 . . . . . . . . . . . 12 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥))
1918, 5sylibr 235 . . . . . . . . . . 11 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘))
20 vex 3440 . . . . . . . . . . . . 13 𝑠 ∈ V
2120elixp 8317 . . . . . . . . . . . 12 (𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) ↔ (𝑠 Fn dom 𝑓 ∧ ∀𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ 𝒫 (𝑓𝑘)))
2221simprbi 497 . . . . . . . . . . 11 (𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) → ∀𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ 𝒫 (𝑓𝑘))
2319, 22syl 17 . . . . . . . . . 10 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ∀𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ 𝒫 (𝑓𝑘))
2423r19.21bi 3175 . . . . . . . . 9 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠𝑘) ∈ 𝒫 (𝑓𝑘))
2524elpwid 4465 . . . . . . . 8 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠𝑘) ⊆ (𝑓𝑘))
26 fvex 6551 . . . . . . . . . 10 (𝑠𝑘) ∈ V
2713, 26iunex 7525 . . . . . . . . 9 𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ V
28 simpll 763 . . . . . . . . . 10 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → CHOICE)
29 acacni 9412 . . . . . . . . . 10 ((CHOICE ∧ dom 𝑓 ∈ V) → AC dom 𝑓 = V)
3028, 13, 29sylancl 586 . . . . . . . . 9 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → AC dom 𝑓 = V)
3127, 30syl5eleqr 2890 . . . . . . . 8 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ AC dom 𝑓)
3211, 14, 17, 25, 31ptclsg 21907 . . . . . . 7 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
3310, 32eqtrd 2831 . . . . . 6 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
345, 33sylan2b 593 . . . . 5 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
3534ralrimiva 3149 . . . 4 ((CHOICE𝑓:dom 𝑓⟶Top) → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
3635ex 413 . . 3 (CHOICE → (𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))))
3736alrimiv 1905 . 2 (CHOICE → ∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))))
38 vex 3440 . . . . . . . 8 𝑔 ∈ V
3938dmex 7472 . . . . . . 7 dom 𝑔 ∈ V
4039a1i 11 . . . . . 6 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → dom 𝑔 ∈ V)
41 fvex 6551 . . . . . . 7 (𝑔𝑥) ∈ V
4241a1i 11 . . . . . 6 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔𝑥) ∈ V)
43 simplrr 774 . . . . . . . 8 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ∅ ∉ ran 𝑔)
44 df-nel 3091 . . . . . . . 8 (∅ ∉ ran 𝑔 ↔ ¬ ∅ ∈ ran 𝑔)
4543, 44sylib 219 . . . . . . 7 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ¬ ∅ ∈ ran 𝑔)
46 funforn 6465 . . . . . . . . . . . 12 (Fun 𝑔𝑔:dom 𝑔onto→ran 𝑔)
47 fof 6458 . . . . . . . . . . . 12 (𝑔:dom 𝑔onto→ran 𝑔𝑔:dom 𝑔⟶ran 𝑔)
4846, 47sylbi 218 . . . . . . . . . . 11 (Fun 𝑔𝑔:dom 𝑔⟶ran 𝑔)
4948ad2antrl 724 . . . . . . . . . 10 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔:dom 𝑔⟶ran 𝑔)
5049ffvelrnda 6716 . . . . . . . . 9 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔𝑥) ∈ ran 𝑔)
51 eleq1 2870 . . . . . . . . 9 ((𝑔𝑥) = ∅ → ((𝑔𝑥) ∈ ran 𝑔 ↔ ∅ ∈ ran 𝑔))
5250, 51syl5ibcom 246 . . . . . . . 8 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ((𝑔𝑥) = ∅ → ∅ ∈ ran 𝑔))
5352necon3bd 2998 . . . . . . 7 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (¬ ∅ ∈ ran 𝑔 → (𝑔𝑥) ≠ ∅))
5445, 53mpd 15 . . . . . 6 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔𝑥) ≠ ∅)
55 eqid 2795 . . . . . 6 𝒫 (𝑔𝑥) = 𝒫 (𝑔𝑥)
56 eqid 2795 . . . . . 6 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}
57 eqid 2795 . . . . . 6 (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})) = (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
58 fveq1 6537 . . . . . . . . . . 11 (𝑠 = 𝑔 → (𝑠𝑘) = (𝑔𝑘))
5958ixpeq2dv 8326 . . . . . . . . . 10 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔(𝑠𝑘) = X𝑘 ∈ dom 𝑔(𝑔𝑘))
60 fveq2 6538 . . . . . . . . . . 11 (𝑘 = 𝑥 → (𝑔𝑘) = (𝑔𝑥))
6160cbvixpv 8328 . . . . . . . . . 10 X𝑘 ∈ dom 𝑔(𝑔𝑘) = X𝑥 ∈ dom 𝑔(𝑔𝑥)
6259, 61syl6eq 2847 . . . . . . . . 9 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔(𝑠𝑘) = X𝑥 ∈ dom 𝑔(𝑔𝑥))
6362fveq2d 6542 . . . . . . . 8 (𝑠 = 𝑔 → ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔𝑥)))
6458fveq2d 6542 . . . . . . . . . 10 (𝑠 = 𝑔 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)))
6564ixpeq2dv 8326 . . . . . . . . 9 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)))
6660unieqd 4755 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑥 (𝑔𝑘) = (𝑔𝑥))
6766pweqd 4458 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → 𝒫 (𝑔𝑘) = 𝒫 (𝑔𝑥))
6867sneqd 4484 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → {𝒫 (𝑔𝑘)} = {𝒫 (𝑔𝑥)})
6960, 68uneq12d 4061 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))
7069pweqd 4458 . . . . . . . . . . . . 13 (𝑘 = 𝑥 → 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) = 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))
7167eleq1d 2867 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → (𝒫 (𝑔𝑘) ∈ 𝑦 ↔ 𝒫 (𝑔𝑥) ∈ 𝑦))
7269eqeq2d 2805 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → (𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ↔ 𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})))
7371, 72imbi12d 346 . . . . . . . . . . . . 13 (𝑘 = 𝑥 → ((𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})) ↔ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))))
7470, 73rabeqbidv 3430 . . . . . . . . . . . 12 (𝑘 = 𝑥 → {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} = {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})
7574fveq2d 6542 . . . . . . . . . . 11 (𝑘 = 𝑥 → (cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))}) = (cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
7675, 60fveq12d 6545 . . . . . . . . . 10 (𝑘 = 𝑥 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥)))
7776cbvixpv 8328 . . . . . . . . 9 X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥))
7865, 77syl6eq 2847 . . . . . . . 8 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥)))
7963, 78eqeq12d 2810 . . . . . . 7 (𝑠 = 𝑔 → (((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔𝑥)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥))))
80 simpl 483 . . . . . . . 8 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → ∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))))
81 snex 5223 . . . . . . . . . . . . 13 {𝒫 (𝑔𝑥)} ∈ V
8241, 81unex 7326 . . . . . . . . . . . 12 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∈ V
83 ssun2 4070 . . . . . . . . . . . . 13 {𝒫 (𝑔𝑥)} ⊆ ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})
8441uniex 7323 . . . . . . . . . . . . . . 15 (𝑔𝑥) ∈ V
8584pwex 5172 . . . . . . . . . . . . . 14 𝒫 (𝑔𝑥) ∈ V
8685snid 4506 . . . . . . . . . . . . 13 𝒫 (𝑔𝑥) ∈ {𝒫 (𝑔𝑥)}
8783, 86sselii 3886 . . . . . . . . . . . 12 𝒫 (𝑔𝑥) ∈ ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})
88 epttop 21301 . . . . . . . . . . . 12 ((((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∈ V ∧ 𝒫 (𝑔𝑥) ∈ ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})) → {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ (TopOn‘((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})))
8982, 87, 88mp2an 688 . . . . . . . . . . 11 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ (TopOn‘((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))
9089topontopi 21207 . . . . . . . . . 10 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ Top
9190a1i 11 . . . . . . . . 9 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ Top)
9291fmpttd 6742 . . . . . . . 8 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}):dom 𝑔⟶Top)
9339mptex 6852 . . . . . . . . 9 (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∈ V
94 id 22 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → 𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
95 dmeq 5658 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → dom 𝑓 = dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
9682pwex 5172 . . . . . . . . . . . . . 14 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∈ V
9796rabex 5126 . . . . . . . . . . . . 13 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ V
98 eqid 2795 . . . . . . . . . . . . 13 (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})
9997, 98dmmpti 6360 . . . . . . . . . . . 12 dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) = dom 𝑔
10095, 99syl6eq 2847 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → dom 𝑓 = dom 𝑔)
10194, 100feq12d 6370 . . . . . . . . . 10 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (𝑓:dom 𝑓⟶Top ↔ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}):dom 𝑔⟶Top))
102100ixpeq1d 8322 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) = X𝑘 ∈ dom 𝑔𝒫 (𝑓𝑘))
103 fveq1 6537 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (𝑓𝑘) = ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘𝑘))
104 fveq2 6538 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑘 → (𝑔𝑥) = (𝑔𝑘))
105104unieqd 4755 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑘 (𝑔𝑥) = (𝑔𝑘))
106105pweqd 4458 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑘 → 𝒫 (𝑔𝑥) = 𝒫 (𝑔𝑘))
107106sneqd 4484 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑘 → {𝒫 (𝑔𝑥)} = {𝒫 (𝑔𝑘)})
108104, 107uneq12d 4061 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
109108pweqd 4458 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) = 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
110106eleq1d 2867 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → (𝒫 (𝑔𝑥) ∈ 𝑦 ↔ 𝒫 (𝑔𝑘) ∈ 𝑦))
111108eqeq2d 2805 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → (𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ↔ 𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})))
112110, 111imbi12d 346 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → ((𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})) ↔ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))))
113109, 112rabeqbidv 3430 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑘 → {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
114 fvex 6551 . . . . . . . . . . . . . . . . . . . . 21 (𝑔𝑘) ∈ V
115 snex 5223 . . . . . . . . . . . . . . . . . . . . 21 {𝒫 (𝑔𝑘)} ∈ V
116114, 115unex 7326 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∈ V
117116pwex 5172 . . . . . . . . . . . . . . . . . . 19 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∈ V
118117rabex 5126 . . . . . . . . . . . . . . . . . 18 {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} ∈ V
119113, 98, 118fvmpt 6635 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ dom 𝑔 → ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘𝑘) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
120103, 119sylan9eq 2851 . . . . . . . . . . . . . . . 16 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓𝑘) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
121120unieqd 4755 . . . . . . . . . . . . . . 15 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓𝑘) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
122 ssun2 4070 . . . . . . . . . . . . . . . . . 18 {𝒫 (𝑔𝑘)} ⊆ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
123114uniex 7323 . . . . . . . . . . . . . . . . . . . 20 (𝑔𝑘) ∈ V
124123pwex 5172 . . . . . . . . . . . . . . . . . . 19 𝒫 (𝑔𝑘) ∈ V
125124snid 4506 . . . . . . . . . . . . . . . . . 18 𝒫 (𝑔𝑘) ∈ {𝒫 (𝑔𝑘)}
126122, 125sselii 3886 . . . . . . . . . . . . . . . . 17 𝒫 (𝑔𝑘) ∈ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
127 epttop 21301 . . . . . . . . . . . . . . . . 17 ((((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∈ V ∧ 𝒫 (𝑔𝑘) ∈ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})) → {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} ∈ (TopOn‘((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})))
128116, 126, 127mp2an 688 . . . . . . . . . . . . . . . 16 {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} ∈ (TopOn‘((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
129128toponunii 21208 . . . . . . . . . . . . . . 15 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))}
130121, 129syl6eqr 2849 . . . . . . . . . . . . . 14 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓𝑘) = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
131130pweqd 4458 . . . . . . . . . . . . 13 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → 𝒫 (𝑓𝑘) = 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
132131ixpeq2dva 8325 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑔𝒫 (𝑓𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
133102, 132eqtrd 2831 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
134 2fveq3 6543 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (cls‘(∏t𝑓)) = (cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))))
135100ixpeq1d 8322 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓(𝑠𝑘) = X𝑘 ∈ dom 𝑔(𝑠𝑘))
136134, 135fveq12d 6545 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)))
137100ixpeq1d 8322 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘(𝑓𝑘))‘(𝑠𝑘)))
138120fveq2d 6542 . . . . . . . . . . . . . . 15 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (cls‘(𝑓𝑘)) = (cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))}))
139138fveq1d 6540 . . . . . . . . . . . . . 14 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ((cls‘(𝑓𝑘))‘(𝑠𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))
140139ixpeq2dva 8325 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑔((cls‘(𝑓𝑘))‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))
141137, 140eqtrd 2831 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))
142136, 141eqeq12d 2810 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘))))
143133, 142raleqbidv 3361 . . . . . . . . . 10 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) ↔ ∀𝑠X 𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘))))
144101, 143imbi12d 346 . . . . . . . . 9 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → ((𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ↔ ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}):dom 𝑔⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))))
14593, 144spcv 3548 . . . . . . . 8 (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) → ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}):dom 𝑔⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘))))
14680, 92, 145sylc 65 . . . . . . 7 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → ∀𝑠X 𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))
147 simprl 767 . . . . . . . . 9 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → Fun 𝑔)
148147funfnd 6256 . . . . . . . 8 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔 Fn dom 𝑔)
149 ssun1 4069 . . . . . . . . . 10 (𝑔𝑘) ⊆ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
150114elpw 4459 . . . . . . . . . 10 ((𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ↔ (𝑔𝑘) ⊆ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
151149, 150mpbir 232 . . . . . . . . 9 (𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
152151rgenw 3117 . . . . . . . 8 𝑘 ∈ dom 𝑔(𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
15338elixp 8317 . . . . . . . 8 (𝑔X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ↔ (𝑔 Fn dom 𝑔 ∧ ∀𝑘 ∈ dom 𝑔(𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})))
154148, 152, 153sylanblrc 590 . . . . . . 7 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
15579, 146, 154rspcdva 3565 . . . . . 6 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔𝑥)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥)))
15640, 42, 54, 55, 56, 57, 155dfac14lem 21909 . . . . 5 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅)
157156ex 413 . . . 4 (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) → ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
158157alrimiv 1905 . . 3 (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) → ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
159 dfac9 9408 . . 3 (CHOICE ↔ ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
160158, 159sylibr 235 . 2 (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) → CHOICE)
16137, 160impbii 210 1 (CHOICE ↔ ∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wal 1520   = wceq 1522  wcel 2081  wne 2984  wnel 3090  wral 3105  {crab 3109  Vcvv 3437  cun 3857  wss 3859  c0 4211  𝒫 cpw 4453  {csn 4472   cuni 4745   ciun 4825  cmpt 5041  dom cdm 5443  ran crn 5444  Fun wfun 6219   Fn wfn 6220  wf 6221  ontowfo 6223  cfv 6225  Xcixp 8310  AC wacn 9213  CHOICEwac 9387  tcpt 16541  Topctop 21185  TopOnctopon 21202  clsccl 21310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-iin 4828  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-se 5403  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-isom 6234  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-oadd 7957  df-er 8139  df-map 8258  df-ixp 8311  df-en 8358  df-dom 8359  df-fin 8361  df-fi 8721  df-card 9214  df-acn 9217  df-ac 9388  df-topgen 16546  df-pt 16547  df-top 21186  df-topon 21203  df-bases 21238  df-cld 21311  df-ntr 21312  df-cls 21313
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator