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

Theorem dfac14 21231
 Description: Theorem ptcls 21229 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 6103 . . . . . . . . . 10 (𝑘 = 𝑥 → (𝑓𝑘) = (𝑓𝑥))
21unieqd 4382 . . . . . . . . 9 (𝑘 = 𝑥 (𝑓𝑘) = (𝑓𝑥))
32pweqd 4113 . . . . . . . 8 (𝑘 = 𝑥 → 𝒫 (𝑓𝑘) = 𝒫 (𝑓𝑥))
43cbvixpv 7812 . . . . . . 7 X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) = X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)
54eleq2i 2680 . . . . . 6 (𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) ↔ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥))
6 simplr 788 . . . . . . . . . . 11 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑓:dom 𝑓⟶Top)
76feqmptd 6159 . . . . . . . . . 10 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑓 = (𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘)))
87fveq2d 6107 . . . . . . . . 9 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → (∏t𝑓) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))))
98fveq2d 6107 . . . . . . . 8 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → (cls‘(∏t𝑓)) = (cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘)))))
109fveq1d 6105 . . . . . . 7 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)))
11 eqid 2610 . . . . . . . 8 (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))) = (∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘)))
12 vex 3176 . . . . . . . . . 10 𝑓 ∈ V
1312dmex 6991 . . . . . . . . 9 dom 𝑓 ∈ V
1413a1i 11 . . . . . . . 8 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → dom 𝑓 ∈ V)
156ffvelrnda 6267 . . . . . . . . 9 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑓𝑘) ∈ Top)
16 eqid 2610 . . . . . . . . . 10 (𝑓𝑘) = (𝑓𝑘)
1716toptopon 20548 . . . . . . . . 9 ((𝑓𝑘) ∈ Top ↔ (𝑓𝑘) ∈ (TopOn‘ (𝑓𝑘)))
1815, 17sylib 207 . . . . . . . 8 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑓𝑘) ∈ (TopOn‘ (𝑓𝑘)))
19 simpr 476 . . . . . . . . . . . 12 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥))
2019, 5sylibr 223 . . . . . . . . . . 11 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘))
21 vex 3176 . . . . . . . . . . . . 13 𝑠 ∈ V
2221elixp 7801 . . . . . . . . . . . 12 (𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) ↔ (𝑠 Fn dom 𝑓 ∧ ∀𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ 𝒫 (𝑓𝑘)))
2322simprbi 479 . . . . . . . . . . 11 (𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) → ∀𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ 𝒫 (𝑓𝑘))
2420, 23syl 17 . . . . . . . . . 10 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ∀𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ 𝒫 (𝑓𝑘))
2524r19.21bi 2916 . . . . . . . . 9 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠𝑘) ∈ 𝒫 (𝑓𝑘))
2625elpwid 4118 . . . . . . . 8 ((((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) ∧ 𝑘 ∈ dom 𝑓) → (𝑠𝑘) ⊆ (𝑓𝑘))
27 fvex 6113 . . . . . . . . . 10 (𝑠𝑘) ∈ V
2813, 27iunex 7039 . . . . . . . . 9 𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ V
29 simpll 786 . . . . . . . . . 10 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → CHOICE)
30 acacni 8845 . . . . . . . . . 10 ((CHOICE ∧ dom 𝑓 ∈ V) → AC dom 𝑓 = V)
3129, 13, 30sylancl 693 . . . . . . . . 9 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → AC dom 𝑓 = V)
3228, 31syl5eleqr 2695 . . . . . . . 8 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → 𝑘 ∈ dom 𝑓(𝑠𝑘) ∈ AC dom 𝑓)
3311, 14, 18, 26, 32ptclsg 21228 . . . . . . 7 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ((cls‘(∏t‘(𝑘 ∈ dom 𝑓 ↦ (𝑓𝑘))))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
3410, 33eqtrd 2644 . . . . . 6 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑥 ∈ dom 𝑓𝒫 (𝑓𝑥)) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
355, 34sylan2b 491 . . . . 5 (((CHOICE𝑓:dom 𝑓⟶Top) ∧ 𝑠X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
3635ralrimiva 2949 . . . 4 ((CHOICE𝑓:dom 𝑓⟶Top) → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)))
3736ex 449 . . 3 (CHOICE → (𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))))
3837alrimiv 1842 . 2 (CHOICE → ∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))))
39 vex 3176 . . . . . . . 8 𝑔 ∈ V
4039dmex 6991 . . . . . . 7 dom 𝑔 ∈ V
4140a1i 11 . . . . . 6 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → dom 𝑔 ∈ V)
42 fvex 6113 . . . . . . 7 (𝑔𝑥) ∈ V
4342a1i 11 . . . . . 6 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔𝑥) ∈ V)
44 simplrr 797 . . . . . . . 8 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ∅ ∉ ran 𝑔)
45 df-nel 2783 . . . . . . . 8 (∅ ∉ ran 𝑔 ↔ ¬ ∅ ∈ ran 𝑔)
4644, 45sylib 207 . . . . . . 7 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ¬ ∅ ∈ ran 𝑔)
47 funforn 6035 . . . . . . . . . . . 12 (Fun 𝑔𝑔:dom 𝑔onto→ran 𝑔)
48 fof 6028 . . . . . . . . . . . 12 (𝑔:dom 𝑔onto→ran 𝑔𝑔:dom 𝑔⟶ran 𝑔)
4947, 48sylbi 206 . . . . . . . . . . 11 (Fun 𝑔𝑔:dom 𝑔⟶ran 𝑔)
5049ad2antrl 760 . . . . . . . . . 10 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔:dom 𝑔⟶ran 𝑔)
5150ffvelrnda 6267 . . . . . . . . 9 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → (𝑔𝑥) ∈ ran 𝑔)
52 eleq1 2676 . . . . . . . . 9 ((𝑔𝑥) = ∅ → ((𝑔𝑥) ∈ ran 𝑔 ↔ ∅ ∈ ran 𝑔))
5351, 52syl5ibcom 234 . . . . . . . 8 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → ((𝑔𝑥) = ∅ → ∅ ∈ ran 𝑔))
5453necon3bd 2796 . . . . . . 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 2610 . . . . . 6 𝒫 (𝑔𝑥) = 𝒫 (𝑔𝑥)
57 eqid 2610 . . . . . 6 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}
58 eqid 2610 . . . . . 6 (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})) = (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
59 simprl 790 . . . . . . . . 9 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → Fun 𝑔)
60 funfn 5833 . . . . . . . . 9 (Fun 𝑔𝑔 Fn dom 𝑔)
6159, 60sylib 207 . . . . . . . 8 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔 Fn dom 𝑔)
62 ssun1 3738 . . . . . . . . . . 11 (𝑔𝑘) ⊆ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
63 fvex 6113 . . . . . . . . . . . 12 (𝑔𝑘) ∈ V
6463elpw 4114 . . . . . . . . . . 11 ((𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ↔ (𝑔𝑘) ⊆ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
6562, 64mpbir 220 . . . . . . . . . 10 (𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
6665rgenw 2908 . . . . . . . . 9 𝑘 ∈ dom 𝑔(𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
6766a1i 11 . . . . . . . 8 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → ∀𝑘 ∈ dom 𝑔(𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
6839elixp 7801 . . . . . . . 8 (𝑔X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ↔ (𝑔 Fn dom 𝑔 ∧ ∀𝑘 ∈ dom 𝑔(𝑔𝑘) ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})))
6961, 67, 68sylanbrc 695 . . . . . . 7 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → 𝑔X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
70 simpl 472 . . . . . . . 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‘(𝑓𝑘))‘(𝑠𝑘))))
71 snex 4835 . . . . . . . . . . . . 13 {𝒫 (𝑔𝑥)} ∈ V
7242, 71unex 6854 . . . . . . . . . . . 12 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∈ V
73 ssun2 3739 . . . . . . . . . . . . 13 {𝒫 (𝑔𝑥)} ⊆ ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})
7442uniex 6851 . . . . . . . . . . . . . . 15 (𝑔𝑥) ∈ V
7574pwex 4774 . . . . . . . . . . . . . 14 𝒫 (𝑔𝑥) ∈ V
7675snid 4155 . . . . . . . . . . . . 13 𝒫 (𝑔𝑥) ∈ {𝒫 (𝑔𝑥)}
7773, 76sselii 3565 . . . . . . . . . . . 12 𝒫 (𝑔𝑥) ∈ ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})
78 epttop 20623 . . . . . . . . . . . 12 ((((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∈ V ∧ 𝒫 (𝑔𝑥) ∈ ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})) → {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ (TopOn‘((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})))
7972, 77, 78mp2an 704 . . . . . . . . . . 11 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ (TopOn‘((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))
8079topontopi 20546 . . . . . . . . . 10 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ Top
8180a1i 11 . . . . . . . . 9 (((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) ∧ 𝑥 ∈ dom 𝑔) → {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ Top)
82 eqid 2610 . . . . . . . . 9 (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})
8381, 82fmptd 6292 . . . . . . . 8 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}):dom 𝑔⟶Top)
8440mptex 6390 . . . . . . . . 9 (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∈ V
85 id 22 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → 𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
86 dmeq 5246 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → dom 𝑓 = dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
8772pwex 4774 . . . . . . . . . . . . . 14 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∈ V
8887rabex 4740 . . . . . . . . . . . . 13 {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} ∈ V
8988, 82dmmpti 5936 . . . . . . . . . . . 12 dom (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) = dom 𝑔
9086, 89syl6eq 2660 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → dom 𝑓 = dom 𝑔)
9185, 90feq12d 5946 . . . . . . . . . 10 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (𝑓:dom 𝑓⟶Top ↔ (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}):dom 𝑔⟶Top))
9290ixpeq1d 7806 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) = X𝑘 ∈ dom 𝑔𝒫 (𝑓𝑘))
93 fveq1 6102 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (𝑓𝑘) = ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘𝑘))
94 fveq2 6103 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑘 → (𝑔𝑥) = (𝑔𝑘))
9594unieqd 4382 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑘 (𝑔𝑥) = (𝑔𝑘))
9695pweqd 4113 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑘 → 𝒫 (𝑔𝑥) = 𝒫 (𝑔𝑘))
9796sneqd 4137 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑘 → {𝒫 (𝑔𝑥)} = {𝒫 (𝑔𝑘)})
9894, 97uneq12d 3730 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
9998pweqd 4113 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) = 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
10096eleq1d 2672 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → (𝒫 (𝑔𝑥) ∈ 𝑦 ↔ 𝒫 (𝑔𝑘) ∈ 𝑦))
10198eqeq2d 2620 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑘 → (𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ↔ 𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})))
102100, 101imbi12d 333 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑘 → ((𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})) ↔ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))))
10399, 102rabeqbidv 3168 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑘 → {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))} = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
104 snex 4835 . . . . . . . . . . . . . . . . . . . . 21 {𝒫 (𝑔𝑘)} ∈ V
10563, 104unex 6854 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∈ V
106105pwex 4774 . . . . . . . . . . . . . . . . . . 19 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∈ V
107106rabex 4740 . . . . . . . . . . . . . . . . . 18 {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} ∈ V
108103, 82, 107fvmpt 6191 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ dom 𝑔 → ((𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘𝑘) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
10993, 108sylan9eq 2664 . . . . . . . . . . . . . . . 16 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓𝑘) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
110109unieqd 4382 . . . . . . . . . . . . . . 15 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓𝑘) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})
111 ssun2 3739 . . . . . . . . . . . . . . . . . 18 {𝒫 (𝑔𝑘)} ⊆ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
11263uniex 6851 . . . . . . . . . . . . . . . . . . . 20 (𝑔𝑘) ∈ V
113112pwex 4774 . . . . . . . . . . . . . . . . . . 19 𝒫 (𝑔𝑘) ∈ V
114113snid 4155 . . . . . . . . . . . . . . . . . 18 𝒫 (𝑔𝑘) ∈ {𝒫 (𝑔𝑘)}
115111, 114sselii 3565 . . . . . . . . . . . . . . . . 17 𝒫 (𝑔𝑘) ∈ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})
116 epttop 20623 . . . . . . . . . . . . . . . . 17 ((((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∈ V ∧ 𝒫 (𝑔𝑘) ∈ ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})) → {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} ∈ (TopOn‘((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})))
117105, 115, 116mp2an 704 . . . . . . . . . . . . . . . 16 {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} ∈ (TopOn‘((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
118117toponunii 20547 . . . . . . . . . . . . . . 15 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) = {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))}
119110, 118syl6eqr 2662 . . . . . . . . . . . . . 14 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (𝑓𝑘) = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
120119pweqd 4113 . . . . . . . . . . . . 13 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → 𝒫 (𝑓𝑘) = 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
121120ixpeq2dva 7809 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑔𝒫 (𝑓𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
12292, 121eqtrd 2644 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘) = X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))
123 fveq2 6103 . . . . . . . . . . . . . 14 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (∏t𝑓) = (∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))
124123fveq2d 6107 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (cls‘(∏t𝑓)) = (cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))))
12590ixpeq1d 7806 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓(𝑠𝑘) = X𝑘 ∈ dom 𝑔(𝑠𝑘))
126124, 125fveq12d 6109 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → ((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)))
12790ixpeq1d 7806 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘(𝑓𝑘))‘(𝑠𝑘)))
128109fveq2d 6107 . . . . . . . . . . . . . . 15 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → (cls‘(𝑓𝑘)) = (cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))}))
129128fveq1d 6105 . . . . . . . . . . . . . 14 ((𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) ∧ 𝑘 ∈ dom 𝑔) → ((cls‘(𝑓𝑘))‘(𝑠𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))
130129ixpeq2dva 7809 . . . . . . . . . . . . 13 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑔((cls‘(𝑓𝑘))‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))
131127, 130eqtrd 2644 . . . . . . . . . . . 12 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))
132126, 131eqeq12d 2625 . . . . . . . . . . 11 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘))))
133122, 132raleqbidv 3129 . . . . . . . . . 10 (𝑓 = (𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}) → (∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘)) ↔ ∀𝑠X 𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘))))
13491, 133imbi12d 333 . . . . . . . . 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‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))))
13584, 134spcv 3272 . . . . . . . 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‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘))))
13670, 83, 135sylc 63 . . . . . . 7 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → ∀𝑠X 𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)))
137 fveq1 6102 . . . . . . . . . . . 12 (𝑠 = 𝑔 → (𝑠𝑘) = (𝑔𝑘))
138137ixpeq2dv 7810 . . . . . . . . . . 11 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔(𝑠𝑘) = X𝑘 ∈ dom 𝑔(𝑔𝑘))
139 fveq2 6103 . . . . . . . . . . . 12 (𝑘 = 𝑥 → (𝑔𝑘) = (𝑔𝑥))
140139cbvixpv 7812 . . . . . . . . . . 11 X𝑘 ∈ dom 𝑔(𝑔𝑘) = X𝑥 ∈ dom 𝑔(𝑔𝑥)
141138, 140syl6eq 2660 . . . . . . . . . 10 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔(𝑠𝑘) = X𝑥 ∈ dom 𝑔(𝑔𝑥))
142141fveq2d 6107 . . . . . . . . 9 (𝑠 = 𝑔 → ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔𝑥)))
143137fveq2d 6107 . . . . . . . . . . 11 (𝑠 = 𝑔 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)))
144143ixpeq2dv 7810 . . . . . . . . . 10 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)))
145139unieqd 4382 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑥 (𝑔𝑘) = (𝑔𝑥))
146145pweqd 4113 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑥 → 𝒫 (𝑔𝑘) = 𝒫 (𝑔𝑥))
147146sneqd 4137 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → {𝒫 (𝑔𝑘)} = {𝒫 (𝑔𝑥)})
148139, 147uneq12d 3730 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))
149148pweqd 4113 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) = 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))
150146eleq1d 2672 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (𝒫 (𝑔𝑘) ∈ 𝑦 ↔ 𝒫 (𝑔𝑥) ∈ 𝑦))
151148eqeq2d 2620 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ↔ 𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)})))
152150, 151imbi12d 333 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → ((𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})) ↔ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))))
153149, 152rabeqbidv 3168 . . . . . . . . . . . . 13 (𝑘 = 𝑥 → {𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))} = {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})
154153fveq2d 6107 . . . . . . . . . . . 12 (𝑘 = 𝑥 → (cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))}) = (cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))}))
155154, 139fveq12d 6109 . . . . . . . . . . 11 (𝑘 = 𝑥 → ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)) = ((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥)))
156155cbvixpv 7812 . . . . . . . . . 10 X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑔𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥))
157144, 156syl6eq 2660 . . . . . . . . 9 (𝑠 = 𝑔X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥)))
158142, 157eqeq12d 2625 . . . . . . . 8 (𝑠 = 𝑔 → (((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) ↔ ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔𝑥)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥))))
159158rspcv 3278 . . . . . . 7 (𝑔X𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) → (∀𝑠X 𝑘 ∈ dom 𝑔𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)})((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑘 ∈ dom 𝑔(𝑠𝑘)) = X𝑘 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}) ∣ (𝒫 (𝑔𝑘) ∈ 𝑦𝑦 = ((𝑔𝑘) ∪ {𝒫 (𝑔𝑘)}))})‘(𝑠𝑘)) → ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔𝑥)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥))))
16069, 136, 159sylc 63 . . . . . 6 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → ((cls‘(∏t‘(𝑥 ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})))‘X𝑥 ∈ dom 𝑔(𝑔𝑥)) = X𝑥 ∈ dom 𝑔((cls‘{𝑦 ∈ 𝒫 ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}) ∣ (𝒫 (𝑔𝑥) ∈ 𝑦𝑦 = ((𝑔𝑥) ∪ {𝒫 (𝑔𝑥)}))})‘(𝑔𝑥)))
16141, 43, 55, 56, 57, 58, 160dfac14lem 21230 . . . . 5 ((∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) ∧ (Fun 𝑔 ∧ ∅ ∉ ran 𝑔)) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅)
162161ex 449 . . . 4 (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) → ((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
163162alrimiv 1842 . . 3 (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) → ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
164 dfac9 8841 . . 3 (CHOICE ↔ ∀𝑔((Fun 𝑔 ∧ ∅ ∉ ran 𝑔) → X𝑥 ∈ dom 𝑔(𝑔𝑥) ≠ ∅))
165163, 164sylibr 223 . 2 (∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠X 𝑘 ∈ dom 𝑓𝒫 (𝑓𝑘)((cls‘(∏t𝑓))‘X𝑘 ∈ dom 𝑓(𝑠𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓𝑘))‘(𝑠𝑘))) → CHOICE)
16638, 165impbii 198 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 195   ∧ wa 383  ∀wal 1473   = wceq 1475   ∈ wcel 1977   ≠ wne 2780   ∉ wnel 2781  ∀wral 2896  {crab 2900  Vcvv 3173   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372  ∪ ciun 4455   ↦ cmpt 4643  dom cdm 5038  ran crn 5039  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  ‘cfv 5804  Xcixp 7794  AC wacn 8647  CHOICEwac 8821  ∏tcpt 15922  Topctop 20517  TopOnctopon 20518  clsccl 20632 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-fin 7845  df-fi 8200  df-card 8648  df-acn 8651  df-ac 8822  df-topgen 15927  df-pt 15928  df-top 20521  df-bases 20522  df-topon 20523  df-cld 20633  df-ntr 20634  df-cls 20635 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator