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

Theorem dfac14 21340
 Description: Theorem ptcls 21338 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 6153 . . . . . . . . . 10 (𝑘 = 𝑥 → (𝑓𝑘) = (𝑓𝑥))
21unieqd 4417 . . . . . . . . 9 (𝑘 = 𝑥 (𝑓𝑘) = (𝑓𝑥))
32pweqd 4140 . . . . . . . 8 (𝑘 = 𝑥 → 𝒫 (𝑓𝑘) = 𝒫 (𝑓𝑥))
43cbvixpv 7877 . . . . . . 7 X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) = X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)
54eleq2i 2690 . . . . . 6 (𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) ↔ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥))
6 simplr 791 . . . . . . . . . . 11 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑓:dom 𝑓⟶Top)
76feqmptd 6211 . . . . . . . . . 10 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑓 = (𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘)))
87fveq2d 6157 . . . . . . . . 9 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → (∏t𝑓) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))))
98fveq2d 6157 . . . . . . . 8 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → (cls‘(∏t𝑓)) = (cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘)))))
109fveq1d 6155 . . . . . . 7 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)))
11 eqid 2621 . . . . . . . 8 (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘)))
12 vex 3192 . . . . . . . . . 10 𝑓 ∈ V
1312dmex 7053 . . . . . . . . 9 dom 𝑓 ∈ V
1413a1i 11 . . . . . . . 8 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → dom 𝑓 ∈ V)
156ffvelrnda 6320 . . . . . . . . 9 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑓𝑘) ∈ Top)
16 eqid 2621 . . . . . . . . . 10 (𝑓𝑘) = (𝑓𝑘)
1716toptopon 20653 . . . . . . . . 9 ((𝑓𝑘) ∈ Top ↔ (𝑓𝑘) ∈ (TopOn‘ (𝑓𝑘)))
1815, 17sylib 208 . . . . . . . 8 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑓𝑘) ∈ (TopOn‘ (𝑓𝑘)))
19 simpr 477 . . . . . . . . . . . 12 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥))
2019, 5sylibr 224 . . . . . . . . . . 11 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘))
21 vex 3192 . . . . . . . . . . . . 13 𝑠 ∈ V
2221elixp 7866 . . . . . . . . . . . 12 (𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) ↔ (𝑠 Fn dom 𝑓 ∧ ∀𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ 𝒫 (𝑓𝑘)))
2322simprbi 480 . . . . . . . . . . 11 (𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) → ∀𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ 𝒫 (𝑓𝑘))
2420, 23syl 17 . . . . . . . . . 10 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ∀𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ 𝒫 (𝑓𝑘))
2524r19.21bi 2927 . . . . . . . . 9 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠𝑘) ∈ 𝒫 (𝑓𝑘))
2625elpwid 4146 . . . . . . . 8 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠𝑘) ⊆ (𝑓𝑘))
27 fvex 6163 . . . . . . . . . 10 (𝑠𝑘) ∈ V
2813, 27iunex 7100 . . . . . . . . 9 𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ V
29 simpll 789 . . . . . . . . . 10 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → CHOICE)
30 acacni 8913 . . . . . . . . . 10 ((CHOICE ∧ dom 𝑓 ∈ V) → AC dom 𝑓 = V)
3129, 13, 30sylancl 693 . . . . . . . . 9 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → AC dom 𝑓 = V)
3228, 31syl5eleqr 2705 . . . . . . . 8 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ AC dom 𝑓)
3311, 14, 18, 26, 32ptclsg 21337 . . . . . . 7 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
3410, 33eqtrd 2655 . . . . . 6 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
355, 34sylan2b 492 . . . . 5 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
3635ralrimiva 2961 . . . 4 ((CHOICE𝑓:dom 𝑓⟶Top) → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
3736ex 450 . . 3 (CHOICE → (𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))))
3837alrimiv 1852 . 2 (CHOICE → ∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))))
39 vex 3192 . . . . . . . 8 𝑔 ∈ V
4039dmex 7053 . . . . . . 7 dom 𝑔 ∈ V
4140a1i 11 . . . . . 6 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → dom 𝑔 ∈ V)
42 fvex 6163 . . . . . . 7 (𝑔𝑥) ∈ V
4342a1i 11 . . . . . 6 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔𝑥) ∈ V)
44 simplrr 800 . . . . . . . 8 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ∅ ∉ ran 𝑔)
45 df-nel 2894 . . . . . . . 8 (∅ ∉ ran 𝑔 ↔ ¬ ∅ ∈ ran 𝑔)
4644, 45sylib 208 . . . . . . 7 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ¬ ∅ ∈ ran 𝑔)
47 funforn 6084 . . . . . . . . . . . 12 (Fun 𝑔𝑔:dom 𝑔onto→ran 𝑔)
48 fof 6077 . . . . . . . . . . . 12 (𝑔:dom 𝑔onto→ran 𝑔𝑔:dom 𝑔⟶ran 𝑔)
4947, 48sylbi 207 . . . . . . . . . . 11 (Fun 𝑔𝑔:dom 𝑔⟶ran 𝑔)
5049ad2antrl 763 . . . . . . . . . 10 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔:dom 𝑔⟶ran 𝑔)
5150ffvelrnda 6320 . . . . . . . . 9 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔𝑥) ∈ ran 𝑔)
52 eleq1 2686 . . . . . . . . 9 ((𝑔𝑥) = ∅ → ((𝑔𝑥) ∈ ran 𝑔 ↔ ∅ ∈ ran 𝑔))
5351, 52syl5ibcom 235 . . . . . . . 8 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ((𝑔𝑥) = ∅ → ∅ ∈ ran 𝑔))
5453necon3bd 2804 . . . . . . 7 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (¬ ∅ ∈ ran 𝑔 → (𝑔𝑥) ≠ ∅))
5546, 54mpd 15 . . . . . 6 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔𝑥) ≠ ∅)
56 eqid 2621 . . . . . 6 𝒫 (𝑔𝑥) = 𝒫 (𝑔𝑥)
57 eqid 2621 . . . . . 6 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}
58 eqid 2621 . . . . . 6 (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})) = (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
59 simprl 793 . . . . . . . . 9 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → Fun 𝑔)
60 funfn 5882 . . . . . . . . 9 (Fun 𝑔𝑔 Fn dom 𝑔)
6159, 60sylib 208 . . . . . . . 8 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔 Fn dom 𝑔)
62 ssun1 3759 . . . . . . . . . 10 (𝑔𝑘) ⊆ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
63 fvex 6163 . . . . . . . . . . 11 (𝑔𝑘) ∈ V
6463elpw 4141 . . . . . . . . . 10 ((𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ↔ (𝑔𝑘) ⊆ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
6562, 64mpbir 221 . . . . . . . . 9 (𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
6665rgenw 2919 . . . . . . . 8 𝑘 ∈ dom 𝑔(𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
6739elixp 7866 . . . . . . . 8 (𝑔X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ↔ (𝑔 Fn dom 𝑔 ∧ ∀𝑘 ∈ dom 𝑔(𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})))
6861, 66, 67sylanblrc 696 . . . . . . 7 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
69 simpl 473 . . . . . . . 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‘(𝑓𝑘))‘(𝑠𝑘))))
70 snex 4874 . . . . . . . . . . . . 13 {𝒫 (𝑔𝑥)} ∈ V
7142, 70unex 6916 . . . . . . . . . . . 12 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∈ V
72 ssun2 3760 . . . . . . . . . . . . 13 {𝒫 (𝑔𝑥)} ⊆ ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})
7342uniex 6913 . . . . . . . . . . . . . . 15 (𝑔𝑥) ∈ V
7473pwex 4813 . . . . . . . . . . . . . 14 𝒫 (𝑔𝑥) ∈ V
7574snid 4184 . . . . . . . . . . . . 13 𝒫 (𝑔𝑥) ∈ {𝒫 (𝑔𝑥)}
7672, 75sselii 3584 . . . . . . . . . . . 12 𝒫 (𝑔𝑥) ∈ ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})
77 epttop 20732 . . . . . . . . . . . 12 ((((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∈ V ∧ 𝒫 (𝑔𝑥) ∈ ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})) → {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ (TopOn‘((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})))
7871, 76, 77mp2an 707 . . . . . . . . . . 11 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ (TopOn‘((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))
7978topontopi 20651 . . . . . . . . . 10 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ Top
8079a1i 11 . . . . . . . . 9 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ Top)
81 eqid 2621 . . . . . . . . 9 (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})
8280, 81fmptd 6346 . . . . . . . 8 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}):dom 𝑔⟶Top)
8340mptex 6446 . . . . . . . . 9 (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∈ V
84 id 22 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → 𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
85 dmeq 5289 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → dom 𝑓 = dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
8671pwex 4813 . . . . . . . . . . . . . 14 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∈ V
8786rabex 4778 . . . . . . . . . . . . 13 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ V
8887, 81dmmpti 5985 . . . . . . . . . . . 12 dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) = dom 𝑔
8985, 88syl6eq 2671 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → dom 𝑓 = dom 𝑔)
9084, 89feq12d 5995 . . . . . . . . . 10 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (𝑓:dom 𝑓⟶Top ↔ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}):dom 𝑔⟶Top))
9189ixpeq1d 7871 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) = X𝑘 ∈ dom 𝑔𝒫 (𝑓𝑘))
92 fveq1 6152 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (𝑓𝑘) = ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘𝑘))
93 fveq2 6153 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑘 → (𝑔𝑥) = (𝑔𝑘))
9493unieqd 4417 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑘 (𝑔𝑥) = (𝑔𝑘))
9594pweqd 4140 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑘 → 𝒫 (𝑔𝑥) = 𝒫 (𝑔𝑘))
9695sneqd 4165 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑘 → {𝒫 (𝑔𝑥)} = {𝒫 (𝑔𝑘)})
9793, 96uneq12d 3751 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
9897pweqd 4140 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) = 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
9995eleq1d 2683 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → (𝒫 (𝑔𝑥) ∈ 𝑦 ↔ 𝒫 (𝑔𝑘) ∈ 𝑦))
10097eqeq2d 2631 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → (𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ↔ 𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})))
10199, 100imbi12d 334 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → ((𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})) ↔ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))))
10298, 101rabeqbidv 3184 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑘 → {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
103 snex 4874 . . . . . . . . . . . . . . . . . . . . 21 {𝒫 (𝑔𝑘)} ∈ V
10463, 103unex 6916 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∈ V
105104pwex 4813 . . . . . . . . . . . . . . . . . . 19 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∈ V
106105rabex 4778 . . . . . . . . . . . . . . . . . 18 {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} ∈ V
107102, 81, 106fvmpt 6244 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ dom 𝑔 → ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘𝑘) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
10892, 107sylan9eq 2675 . . . . . . . . . . . . . . . 16 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓𝑘) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
109108unieqd 4417 . . . . . . . . . . . . . . 15 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓𝑘) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
110 ssun2 3760 . . . . . . . . . . . . . . . . . 18 {𝒫 (𝑔𝑘)} ⊆ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
11163uniex 6913 . . . . . . . . . . . . . . . . . . . 20 (𝑔𝑘) ∈ V
112111pwex 4813 . . . . . . . . . . . . . . . . . . 19 𝒫 (𝑔𝑘) ∈ V
113112snid 4184 . . . . . . . . . . . . . . . . . 18 𝒫 (𝑔𝑘) ∈ {𝒫 (𝑔𝑘)}
114110, 113sselii 3584 . . . . . . . . . . . . . . . . 17 𝒫 (𝑔𝑘) ∈ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
115 epttop 20732 . . . . . . . . . . . . . . . . 17 ((((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∈ V ∧ 𝒫 (𝑔𝑘) ∈ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})) → {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} ∈ (TopOn‘((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})))
116104, 114, 115mp2an 707 . . . . . . . . . . . . . . . 16 {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} ∈ (TopOn‘((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
117116toponunii 20652 . . . . . . . . . . . . . . 15 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))}
118109, 117syl6eqr 2673 . . . . . . . . . . . . . 14 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓𝑘) = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
119118pweqd 4140 . . . . . . . . . . . . 13 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → 𝒫 (𝑓𝑘) = 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
120119ixpeq2dva 7874 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑔𝒫 (𝑓𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
12191, 120eqtrd 2655 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
122 fveq2 6153 . . . . . . . . . . . . . 14 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (∏t𝑓) = (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))
123122fveq2d 6157 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (cls‘(∏t𝑓)) = (cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))))
12489ixpeq1d 7871 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓(𝑠𝑘) = X𝑘 ∈ dom 𝑔(𝑠𝑘))
125123, 124fveq12d 6159 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)))
12689ixpeq1d 7871 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘(𝑓𝑘))‘(𝑠𝑘)))
127108fveq2d 6157 . . . . . . . . . . . . . . 15 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (cls‘(𝑓𝑘)) = (cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))}))
128127fveq1d 6155 . . . . . . . . . . . . . 14 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ((cls‘(𝑓𝑘))‘(𝑠𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))
129128ixpeq2dva 7874 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑔((cls‘(𝑓𝑘))‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))
130126, 129eqtrd 2655 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))
131125, 130eqeq12d 2636 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘))))
132121, 131raleqbidv 3144 . . . . . . . . . 10 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) ↔ ∀𝑠X 𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘))))
13390, 132imbi12d 334 . . . . . . . . 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‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))))
13483, 133spcv 3288 . . . . . . . 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‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘))))
13569, 82, 134sylc 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‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))
136 fveq1 6152 . . . . . . . . . . . 12 (𝑠 = 𝑔 → (𝑠𝑘) = (𝑔𝑘))
137136ixpeq2dv 7875 . . . . . . . . . . 11 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔(𝑠𝑘) = X𝑘 ∈ dom 𝑔(𝑔𝑘))
138 fveq2 6153 . . . . . . . . . . . 12 (𝑘 = 𝑥 → (𝑔𝑘) = (𝑔𝑥))
139138cbvixpv 7877 . . . . . . . . . . 11 X𝑘 ∈ dom 𝑔(𝑔𝑘) = X𝑥 ∈ dom 𝑔(𝑔𝑥)
140137, 139syl6eq 2671 . . . . . . . . . 10 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔(𝑠𝑘) = X𝑥 ∈ dom 𝑔(𝑔𝑥))
141140fveq2d 6157 . . . . . . . . 9 (𝑠 = 𝑔 → ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔𝑥)))
142136fveq2d 6157 . . . . . . . . . . 11 (𝑠 = 𝑔 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)))
143142ixpeq2dv 7875 . . . . . . . . . 10 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)))
144138unieqd 4417 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑥 (𝑔𝑘) = (𝑔𝑥))
145144pweqd 4140 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑥 → 𝒫 (𝑔𝑘) = 𝒫 (𝑔𝑥))
146145sneqd 4165 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → {𝒫 (𝑔𝑘)} = {𝒫 (𝑔𝑥)})
147138, 146uneq12d 3751 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))
148147pweqd 4140 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) = 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))
149145eleq1d 2683 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (𝒫 (𝑔𝑘) ∈ 𝑦 ↔ 𝒫 (𝑔𝑥) ∈ 𝑦))
150147eqeq2d 2631 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ↔ 𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})))
151149, 150imbi12d 334 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → ((𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})) ↔ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))))
152148, 151rabeqbidv 3184 . . . . . . . . . . . . 13 (𝑘 = 𝑥 → {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} = {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})
153152fveq2d 6157 . . . . . . . . . . . 12 (𝑘 = 𝑥 → (cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))}) = (cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
154153, 138fveq12d 6159 . . . . . . . . . . 11 (𝑘 = 𝑥 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥)))
155154cbvixpv 7877 . . . . . . . . . 10 X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥))
156143, 155syl6eq 2671 . . . . . . . . 9 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥)))
157141, 156eqeq12d 2636 . . . . . . . 8 (𝑠 = 𝑔 → (((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔𝑥)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥))))
158157rspcv 3294 . . . . . . 7 (𝑔X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) → (∀𝑠X 𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) → ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔𝑥)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥))))
15968, 135, 158sylc 65 . . . . . 6 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔𝑥)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥)))
16041, 43, 55, 56, 57, 58, 159dfac14lem 21339 . . . . 5 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅)
161160ex 450 . . . 4 (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) → ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
162161alrimiv 1852 . . 3 (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) → ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
163 dfac9 8909 . . 3 (CHOICE ↔ ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
164162, 163sylibr 224 . 2 (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) → CHOICE)
16538, 164impbii 199 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 196   ∧ wa 384  ∀wal 1478   = wceq 1480   ∈ wcel 1987   ≠ wne 2790   ∉ wnel 2893  ∀wral 2907  {crab 2911  Vcvv 3189   ∪ cun 3557   ⊆ wss 3559  ∅c0 3896  𝒫 cpw 4135  {csn 4153  ∪ cuni 4407  ∪ ciun 4490   ↦ cmpt 4678  dom cdm 5079  ran crn 5080  Fun wfun 5846   Fn wfn 5847  ⟶wf 5848  –onto→wfo 5850  ‘cfv 5852  Xcixp 7859  AC wacn 8715  CHOICEwac 8889  ∏tcpt 16027  Topctop 20626  TopOnctopon 20643  clsccl 20741 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 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  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-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-map 7811  df-ixp 7860  df-en 7907  df-dom 7908  df-fin 7910  df-fi 8268  df-card 8716  df-acn 8719  df-ac 8890  df-topgen 16032  df-pt 16033  df-top 20627  df-topon 20644  df-bases 20670  df-cld 20742  df-ntr 20743  df-cls 20744 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator