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

Theorem dfac14 22323
 Description: Theorem ptcls 22321 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 6662 . . . . . . . . . 10 (𝑘 = 𝑥 → (𝑓𝑘) = (𝑓𝑥))
21unieqd 4815 . . . . . . . . 9 (𝑘 = 𝑥 (𝑓𝑘) = (𝑓𝑥))
32pweqd 4516 . . . . . . . 8 (𝑘 = 𝑥 → 𝒫 (𝑓𝑘) = 𝒫 (𝑓𝑥))
43cbvixpv 8502 . . . . . . 7 X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) = X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)
54eleq2i 2843 . . . . . 6 (𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) ↔ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥))
6 simplr 768 . . . . . . . . . . 11 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑓:dom 𝑓⟶Top)
76feqmptd 6725 . . . . . . . . . 10 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑓 = (𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘)))
87fveq2d 6666 . . . . . . . . 9 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → (∏t𝑓) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))))
98fveq2d 6666 . . . . . . . 8 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → (cls‘(∏t𝑓)) = (cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘)))))
109fveq1d 6664 . . . . . . 7 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)))
11 eqid 2758 . . . . . . . 8 (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘)))
12 vex 3413 . . . . . . . . . 10 𝑓 ∈ V
1312dmex 7626 . . . . . . . . 9 dom 𝑓 ∈ V
1413a1i 11 . . . . . . . 8 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → dom 𝑓 ∈ V)
156ffvelrnda 6847 . . . . . . . . 9 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑓𝑘) ∈ Top)
16 toptopon2 21623 . . . . . . . . 9 ((𝑓𝑘) ∈ Top ↔ (𝑓𝑘) ∈ (TopOn‘ (𝑓𝑘)))
1715, 16sylib 221 . . . . . . . 8 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑓𝑘) ∈ (TopOn‘ (𝑓𝑘)))
18 simpr 488 . . . . . . . . . . . 12 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥))
1918, 5sylibr 237 . . . . . . . . . . 11 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘))
20 vex 3413 . . . . . . . . . . . . 13 𝑠 ∈ V
2120elixp 8491 . . . . . . . . . . . 12 (𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) ↔ (𝑠 Fn dom 𝑓 ∧ ∀𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ 𝒫 (𝑓𝑘)))
2221simprbi 500 . . . . . . . . . . 11 (𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) → ∀𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ 𝒫 (𝑓𝑘))
2319, 22syl 17 . . . . . . . . . 10 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ∀𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ 𝒫 (𝑓𝑘))
2423r19.21bi 3137 . . . . . . . . 9 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠𝑘) ∈ 𝒫 (𝑓𝑘))
2524elpwid 4508 . . . . . . . 8 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠𝑘) ⊆ (𝑓𝑘))
26 fvex 6675 . . . . . . . . . 10 (𝑠𝑘) ∈ V
2713, 26iunex 7678 . . . . . . . . 9 𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ V
28 simpll 766 . . . . . . . . . 10 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → CHOICE)
29 acacni 9605 . . . . . . . . . 10 ((CHOICE ∧ dom 𝑓 ∈ V) → AC dom 𝑓 = V)
3028, 13, 29sylancl 589 . . . . . . . . 9 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → AC dom 𝑓 = V)
3127, 30eleqtrrid 2859 . . . . . . . 8 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ AC dom 𝑓)
3211, 14, 17, 25, 31ptclsg 22320 . . . . . . 7 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
3310, 32eqtrd 2793 . . . . . 6 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
345, 33sylan2b 596 . . . . 5 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
3534ralrimiva 3113 . . . 4 ((CHOICE𝑓:dom 𝑓⟶Top) → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
3635ex 416 . . 3 (CHOICE → (𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))))
3736alrimiv 1928 . 2 (CHOICE → ∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))))
38 vex 3413 . . . . . . . 8 𝑔 ∈ V
3938dmex 7626 . . . . . . 7 dom 𝑔 ∈ V
4039a1i 11 . . . . . 6 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → dom 𝑔 ∈ V)
41 fvex 6675 . . . . . . 7 (𝑔𝑥) ∈ V
4241a1i 11 . . . . . 6 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔𝑥) ∈ V)
43 simplrr 777 . . . . . . . 8 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ∅ ∉ ran 𝑔)
44 df-nel 3056 . . . . . . . 8 (∅ ∉ ran 𝑔 ↔ ¬ ∅ ∈ ran 𝑔)
4543, 44sylib 221 . . . . . . 7 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ¬ ∅ ∈ ran 𝑔)
46 funforn 6587 . . . . . . . . . . . 12 (Fun 𝑔𝑔:dom 𝑔onto→ran 𝑔)
47 fof 6580 . . . . . . . . . . . 12 (𝑔:dom 𝑔onto→ran 𝑔𝑔:dom 𝑔⟶ran 𝑔)
4846, 47sylbi 220 . . . . . . . . . . 11 (Fun 𝑔𝑔:dom 𝑔⟶ran 𝑔)
4948ad2antrl 727 . . . . . . . . . 10 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔:dom 𝑔⟶ran 𝑔)
5049ffvelrnda 6847 . . . . . . . . 9 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔𝑥) ∈ ran 𝑔)
51 eleq1 2839 . . . . . . . . 9 ((𝑔𝑥) = ∅ → ((𝑔𝑥) ∈ ran 𝑔 ↔ ∅ ∈ ran 𝑔))
5250, 51syl5ibcom 248 . . . . . . . 8 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ((𝑔𝑥) = ∅ → ∅ ∈ ran 𝑔))
5352necon3bd 2965 . . . . . . 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 2758 . . . . . 6 𝒫 (𝑔𝑥) = 𝒫 (𝑔𝑥)
56 eqid 2758 . . . . . 6 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}
57 eqid 2758 . . . . . 6 (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})) = (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
58 fveq1 6661 . . . . . . . . . . 11 (𝑠 = 𝑔 → (𝑠𝑘) = (𝑔𝑘))
5958ixpeq2dv 8500 . . . . . . . . . 10 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔(𝑠𝑘) = X𝑘 ∈ dom 𝑔(𝑔𝑘))
60 fveq2 6662 . . . . . . . . . . 11 (𝑘 = 𝑥 → (𝑔𝑘) = (𝑔𝑥))
6160cbvixpv 8502 . . . . . . . . . 10 X𝑘 ∈ dom 𝑔(𝑔𝑘) = X𝑥 ∈ dom 𝑔(𝑔𝑥)
6259, 61eqtrdi 2809 . . . . . . . . 9 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔(𝑠𝑘) = X𝑥 ∈ dom 𝑔(𝑔𝑥))
6362fveq2d 6666 . . . . . . . 8 (𝑠 = 𝑔 → ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔𝑥)))
6458fveq2d 6666 . . . . . . . . . 10 (𝑠 = 𝑔 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)))
6564ixpeq2dv 8500 . . . . . . . . 9 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)))
6660unieqd 4815 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑥 (𝑔𝑘) = (𝑔𝑥))
6766pweqd 4516 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → 𝒫 (𝑔𝑘) = 𝒫 (𝑔𝑥))
6867sneqd 4537 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → {𝒫 (𝑔𝑘)} = {𝒫 (𝑔𝑥)})
6960, 68uneq12d 4071 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))
7069pweqd 4516 . . . . . . . . . . . . 13 (𝑘 = 𝑥 → 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) = 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))
7167eleq1d 2836 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → (𝒫 (𝑔𝑘) ∈ 𝑦 ↔ 𝒫 (𝑔𝑥) ∈ 𝑦))
7269eqeq2d 2769 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → (𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ↔ 𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})))
7371, 72imbi12d 348 . . . . . . . . . . . . 13 (𝑘 = 𝑥 → ((𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})) ↔ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))))
7470, 73rabeqbidv 3398 . . . . . . . . . . . 12 (𝑘 = 𝑥 → {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} = {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})
7574fveq2d 6666 . . . . . . . . . . 11 (𝑘 = 𝑥 → (cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))}) = (cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
7675, 60fveq12d 6669 . . . . . . . . . 10 (𝑘 = 𝑥 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥)))
7776cbvixpv 8502 . . . . . . . . 9 X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥))
7865, 77eqtrdi 2809 . . . . . . . 8 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥)))
7963, 78eqeq12d 2774 . . . . . . 7 (𝑠 = 𝑔 → (((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔𝑥)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥))))
80 simpl 486 . . . . . . . 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 5303 . . . . . . . . . . . . 13 {𝒫 (𝑔𝑥)} ∈ V
8241, 81unex 7472 . . . . . . . . . . . 12 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∈ V
83 ssun2 4080 . . . . . . . . . . . . 13 {𝒫 (𝑔𝑥)} ⊆ ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})
8441uniex 7470 . . . . . . . . . . . . . . 15 (𝑔𝑥) ∈ V
8584pwex 5252 . . . . . . . . . . . . . 14 𝒫 (𝑔𝑥) ∈ V
8685snid 4561 . . . . . . . . . . . . 13 𝒫 (𝑔𝑥) ∈ {𝒫 (𝑔𝑥)}
8783, 86sselii 3891 . . . . . . . . . . . 12 𝒫 (𝑔𝑥) ∈ ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})
88 epttop 21714 . . . . . . . . . . . 12 ((((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∈ V ∧ 𝒫 (𝑔𝑥) ∈ ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})) → {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ (TopOn‘((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})))
8982, 87, 88mp2an 691 . . . . . . . . . . 11 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ (TopOn‘((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))
9089topontopi 21620 . . . . . . . . . 10 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ Top
9190a1i 11 . . . . . . . . 9 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ Top)
9291fmpttd 6875 . . . . . . . 8 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}):dom 𝑔⟶Top)
9339mptex 6982 . . . . . . . . 9 (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∈ V
94 id 22 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → 𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
95 dmeq 5748 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → dom 𝑓 = dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
9682pwex 5252 . . . . . . . . . . . . . 14 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∈ V
9796rabex 5205 . . . . . . . . . . . . 13 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ V
98 eqid 2758 . . . . . . . . . . . . 13 (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})
9997, 98dmmpti 6479 . . . . . . . . . . . 12 dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) = dom 𝑔
10095, 99eqtrdi 2809 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → dom 𝑓 = dom 𝑔)
10194, 100feq12d 6490 . . . . . . . . . 10 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (𝑓:dom 𝑓⟶Top ↔ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}):dom 𝑔⟶Top))
102100ixpeq1d 8496 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) = X𝑘 ∈ dom 𝑔𝒫 (𝑓𝑘))
103 fveq1 6661 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (𝑓𝑘) = ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘𝑘))
104 fveq2 6662 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑘 → (𝑔𝑥) = (𝑔𝑘))
105104unieqd 4815 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑘 (𝑔𝑥) = (𝑔𝑘))
106105pweqd 4516 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑘 → 𝒫 (𝑔𝑥) = 𝒫 (𝑔𝑘))
107106sneqd 4537 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑘 → {𝒫 (𝑔𝑥)} = {𝒫 (𝑔𝑘)})
108104, 107uneq12d 4071 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
109108pweqd 4516 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) = 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
110106eleq1d 2836 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → (𝒫 (𝑔𝑥) ∈ 𝑦 ↔ 𝒫 (𝑔𝑘) ∈ 𝑦))
111108eqeq2d 2769 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → (𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ↔ 𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})))
112110, 111imbi12d 348 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → ((𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})) ↔ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))))
113109, 112rabeqbidv 3398 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑘 → {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
114 fvex 6675 . . . . . . . . . . . . . . . . . . . . 21 (𝑔𝑘) ∈ V
115 snex 5303 . . . . . . . . . . . . . . . . . . . . 21 {𝒫 (𝑔𝑘)} ∈ V
116114, 115unex 7472 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∈ V
117116pwex 5252 . . . . . . . . . . . . . . . . . . 19 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∈ V
118117rabex 5205 . . . . . . . . . . . . . . . . . 18 {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} ∈ V
119113, 98, 118fvmpt 6763 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ dom 𝑔 → ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘𝑘) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
120103, 119sylan9eq 2813 . . . . . . . . . . . . . . . 16 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓𝑘) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
121120unieqd 4815 . . . . . . . . . . . . . . 15 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓𝑘) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
122 ssun2 4080 . . . . . . . . . . . . . . . . . 18 {𝒫 (𝑔𝑘)} ⊆ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
123114uniex 7470 . . . . . . . . . . . . . . . . . . . 20 (𝑔𝑘) ∈ V
124123pwex 5252 . . . . . . . . . . . . . . . . . . 19 𝒫 (𝑔𝑘) ∈ V
125124snid 4561 . . . . . . . . . . . . . . . . . 18 𝒫 (𝑔𝑘) ∈ {𝒫 (𝑔𝑘)}
126122, 125sselii 3891 . . . . . . . . . . . . . . . . 17 𝒫 (𝑔𝑘) ∈ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
127 epttop 21714 . . . . . . . . . . . . . . . . 17 ((((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∈ V ∧ 𝒫 (𝑔𝑘) ∈ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})) → {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} ∈ (TopOn‘((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})))
128116, 126, 127mp2an 691 . . . . . . . . . . . . . . . 16 {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} ∈ (TopOn‘((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
129128toponunii 21621 . . . . . . . . . . . . . . 15 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))}
130121, 129eqtr4di 2811 . . . . . . . . . . . . . 14 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓𝑘) = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
131130pweqd 4516 . . . . . . . . . . . . 13 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → 𝒫 (𝑓𝑘) = 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
132131ixpeq2dva 8499 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑔𝒫 (𝑓𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
133102, 132eqtrd 2793 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
134 2fveq3 6667 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (cls‘(∏t𝑓)) = (cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))))
135100ixpeq1d 8496 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓(𝑠𝑘) = X𝑘 ∈ dom 𝑔(𝑠𝑘))
136134, 135fveq12d 6669 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)))
137100ixpeq1d 8496 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘(𝑓𝑘))‘(𝑠𝑘)))
138120fveq2d 6666 . . . . . . . . . . . . . . 15 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (cls‘(𝑓𝑘)) = (cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))}))
139138fveq1d 6664 . . . . . . . . . . . . . 14 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ((cls‘(𝑓𝑘))‘(𝑠𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))
140139ixpeq2dva 8499 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑔((cls‘(𝑓𝑘))‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))
141137, 140eqtrd 2793 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))
142136, 141eqeq12d 2774 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘))))
143133, 142raleqbidv 3319 . . . . . . . . . 10 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) ↔ ∀𝑠X 𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘))))
144101, 143imbi12d 348 . . . . . . . . 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 3526 . . . . . . . 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 770 . . . . . . . . 9 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → Fun 𝑔)
148147funfnd 6370 . . . . . . . 8 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔 Fn dom 𝑔)
149 ssun1 4079 . . . . . . . . . 10 (𝑔𝑘) ⊆ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
150114elpw 4501 . . . . . . . . . 10 ((𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ↔ (𝑔𝑘) ⊆ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
151149, 150mpbir 234 . . . . . . . . 9 (𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
152151rgenw 3082 . . . . . . . 8 𝑘 ∈ dom 𝑔(𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
15338elixp 8491 . . . . . . . 8 (𝑔X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ↔ (𝑔 Fn dom 𝑔 ∧ ∀𝑘 ∈ dom 𝑔(𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})))
154148, 152, 153sylanblrc 593 . . . . . . 7 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
15579, 146, 154rspcdva 3545 . . . . . 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 22322 . . . . 5 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅)
157156ex 416 . . . 4 (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) → ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
158157alrimiv 1928 . . 3 (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) → ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
159 dfac9 9601 . . 3 (CHOICE ↔ ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
160158, 159sylibr 237 . 2 (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) → CHOICE)
16137, 160impbii 212 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 209   ∧ wa 399  ∀wal 1536   = wceq 1538   ∈ wcel 2111   ≠ wne 2951   ∉ wnel 3055  ∀wral 3070  {crab 3074  Vcvv 3409   ∪ cun 3858   ⊆ wss 3860  ∅c0 4227  𝒫 cpw 4497  {csn 4525  ∪ cuni 4801  ∪ ciun 4886   ↦ cmpt 5115  dom cdm 5527  ran crn 5528  Fun wfun 6333   Fn wfn 6334  ⟶wf 6335  –onto→wfo 6337  ‘cfv 6339  Xcixp 8484  AC wacn 9405  CHOICEwac 9580  ∏tcpt 16775  Topctop 21598  TopOnctopon 21615  clsccl 21723 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5159  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-iin 4889  df-br 5036  df-opab 5098  df-mpt 5116  df-tr 5142  df-id 5433  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-se 5487  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-isom 6348  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-om 7585  df-1st 7698  df-2nd 7699  df-wrecs 7962  df-recs 8023  df-1o 8117  df-er 8304  df-map 8423  df-ixp 8485  df-en 8533  df-dom 8534  df-fin 8536  df-fi 8913  df-card 9406  df-acn 9409  df-ac 9581  df-topgen 16780  df-pt 16781  df-top 21599  df-topon 21616  df-bases 21651  df-cld 21724  df-ntr 21725  df-cls 21726 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator