MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfac14 Structured version   Visualization version   GIF version
Theorem dfac14 23342
Description: Theorem ptcls 23340 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 6891 . . . . . . . . . 10 (π‘˜ = π‘₯ β†’ (π‘“β€˜π‘˜) = (π‘“β€˜π‘₯))
21unieqd 4922 . . . . . . . . 9 (π‘˜ = π‘₯ β†’ βˆͺ (π‘“β€˜π‘˜) = βˆͺ (π‘“β€˜π‘₯))
32pweqd 4619 . . . . . . . 8 (π‘˜ = π‘₯ β†’ 𝒫 βˆͺ (π‘“β€˜π‘˜) = 𝒫 βˆͺ (π‘“β€˜π‘₯))
43cbvixpv 8911 . . . . . . 7 Xπ‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜) = Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)
54eleq2i 2825 . . . . . 6 (𝑠 ∈ Xπ‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜) ↔ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯))
6 simplr 767 . . . . . . . . . . 11 (((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) β†’ 𝑓:dom π‘“βŸΆTop)
76feqmptd 6960 . . . . . . . . . 10 (((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) β†’ 𝑓 = (π‘˜ ∈ dom 𝑓 ↦ (π‘“β€˜π‘˜)))
87fveq2d 6895 . . . . . . . . 9 (((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) β†’ (∏tβ€˜π‘“) = (∏tβ€˜(π‘˜ ∈ dom 𝑓 ↦ (π‘“β€˜π‘˜))))
98fveq2d 6895 . . . . . . . 8 (((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) β†’ (clsβ€˜(∏tβ€˜π‘“)) = (clsβ€˜(∏tβ€˜(π‘˜ ∈ dom 𝑓 ↦ (π‘“β€˜π‘˜)))))
109fveq1d 6893 . . . . . . 7 (((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) β†’ ((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = ((clsβ€˜(∏tβ€˜(π‘˜ ∈ dom 𝑓 ↦ (π‘“β€˜π‘˜))))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)))
11 eqid 2732 . . . . . . . 8 (∏tβ€˜(π‘˜ ∈ dom 𝑓 ↦ (π‘“β€˜π‘˜))) = (∏tβ€˜(π‘˜ ∈ dom 𝑓 ↦ (π‘“β€˜π‘˜)))
12 vex 3478 . . . . . . . . . 10 𝑓 ∈ V
1312dmex 7904 . . . . . . . . 9 dom 𝑓 ∈ V
1413a1i 11 . . . . . . . 8 (((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) β†’ dom 𝑓 ∈ V)
156ffvelcdmda 7086 . . . . . . . . 9 ((((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) ∧ π‘˜ ∈ dom 𝑓) β†’ (π‘“β€˜π‘˜) ∈ Top)
16 toptopon2 22640 . . . . . . . . 9 ((π‘“β€˜π‘˜) ∈ Top ↔ (π‘“β€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (π‘“β€˜π‘˜)))
1715, 16sylib 217 . . . . . . . 8 ((((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) ∧ π‘˜ ∈ dom 𝑓) β†’ (π‘“β€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (π‘“β€˜π‘˜)))
18 simpr 485 . . . . . . . . . . . 12 (((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) β†’ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯))
1918, 5sylibr 233 . . . . . . . . . . 11 (((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) β†’ 𝑠 ∈ Xπ‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜))
20 vex 3478 . . . . . . . . . . . . 13 𝑠 ∈ V
2120elixp 8900 . . . . . . . . . . . 12 (𝑠 ∈ Xπ‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜) ↔ (𝑠 Fn dom 𝑓 ∧ βˆ€π‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜) ∈ 𝒫 βˆͺ (π‘“β€˜π‘˜)))
2221simprbi 497 . . . . . . . . . . 11 (𝑠 ∈ Xπ‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜) β†’ βˆ€π‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜) ∈ 𝒫 βˆͺ (π‘“β€˜π‘˜))
2319, 22syl 17 . . . . . . . . . 10 (((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) β†’ βˆ€π‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜) ∈ 𝒫 βˆͺ (π‘“β€˜π‘˜))
2423r19.21bi 3248 . . . . . . . . 9 ((((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) ∧ π‘˜ ∈ dom 𝑓) β†’ (π‘ β€˜π‘˜) ∈ 𝒫 βˆͺ (π‘“β€˜π‘˜))
2524elpwid 4611 . . . . . . . 8 ((((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) ∧ π‘˜ ∈ dom 𝑓) β†’ (π‘ β€˜π‘˜) βŠ† βˆͺ (π‘“β€˜π‘˜))
26 fvex 6904 . . . . . . . . . 10 (π‘ β€˜π‘˜) ∈ V
2713, 26iunex 7957 . . . . . . . . 9 βˆͺ π‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜) ∈ V
28 simpll 765 . . . . . . . . . 10 (((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) β†’ CHOICE)
29 acacni 10137 . . . . . . . . . 10 ((CHOICE ∧ dom 𝑓 ∈ V) β†’ AC dom 𝑓 = V)
3028, 13, 29sylancl 586 . . . . . . . . 9 (((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) β†’ AC dom 𝑓 = V)
3127, 30eleqtrrid 2840 . . . . . . . 8 (((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) β†’ βˆͺ π‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜) ∈ AC dom 𝑓)
3211, 14, 17, 25, 31ptclsg 23339 . . . . . . 7 (((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) β†’ ((clsβ€˜(∏tβ€˜(π‘˜ ∈ dom 𝑓 ↦ (π‘“β€˜π‘˜))))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜)))
3310, 32eqtrd 2772 . . . . . 6 (((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘₯ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘₯)) β†’ ((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜)))
345, 33sylan2b 594 . . . . 5 (((CHOICE ∧ 𝑓:dom π‘“βŸΆTop) ∧ 𝑠 ∈ Xπ‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)) β†’ ((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜)))
3534ralrimiva 3146 . . . 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 1930 . 2 (CHOICE β†’ βˆ€π‘“(𝑓:dom π‘“βŸΆTop β†’ βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜))))
38 vex 3478 . . . . . . . 8 𝑔 ∈ V
3938dmex 7904 . . . . . . 7 dom 𝑔 ∈ V
4039a1i 11 . . . . . 6 ((βˆ€π‘“(𝑓:dom π‘“βŸΆTop β†’ βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜))) ∧ (Fun 𝑔 ∧ βˆ… βˆ‰ ran 𝑔)) β†’ dom 𝑔 ∈ V)
41 fvex 6904 . . . . . . 7 (π‘”β€˜π‘₯) ∈ V
4241a1i 11 . . . . . 6 (((βˆ€π‘“(𝑓:dom π‘“βŸΆTop β†’ βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜))) ∧ (Fun 𝑔 ∧ βˆ… βˆ‰ ran 𝑔)) ∧ π‘₯ ∈ dom 𝑔) β†’ (π‘”β€˜π‘₯) ∈ V)
43 simplrr 776 . . . . . . . 8 (((βˆ€π‘“(𝑓:dom π‘“βŸΆTop β†’ βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜))) ∧ (Fun 𝑔 ∧ βˆ… βˆ‰ ran 𝑔)) ∧ π‘₯ ∈ dom 𝑔) β†’ βˆ… βˆ‰ ran 𝑔)
44 df-nel 3047 . . . . . . . 8 (βˆ… βˆ‰ ran 𝑔 ↔ Β¬ βˆ… ∈ ran 𝑔)
4543, 44sylib 217 . . . . . . 7 (((βˆ€π‘“(𝑓:dom π‘“βŸΆTop β†’ βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜))) ∧ (Fun 𝑔 ∧ βˆ… βˆ‰ ran 𝑔)) ∧ π‘₯ ∈ dom 𝑔) β†’ Β¬ βˆ… ∈ ran 𝑔)
46 funforn 6812 . . . . . . . . . . . 12 (Fun 𝑔 ↔ 𝑔:dom 𝑔–ontoβ†’ran 𝑔)
47 fof 6805 . . . . . . . . . . . 12 (𝑔:dom 𝑔–ontoβ†’ran 𝑔 β†’ 𝑔:dom π‘”βŸΆran 𝑔)
4846, 47sylbi 216 . . . . . . . . . . 11 (Fun 𝑔 β†’ 𝑔:dom π‘”βŸΆran 𝑔)
4948ad2antrl 726 . . . . . . . . . 10 ((βˆ€π‘“(𝑓:dom π‘“βŸΆTop β†’ βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜))) ∧ (Fun 𝑔 ∧ βˆ… βˆ‰ ran 𝑔)) β†’ 𝑔:dom π‘”βŸΆran 𝑔)
5049ffvelcdmda 7086 . . . . . . . . 9 (((βˆ€π‘“(𝑓:dom π‘“βŸΆTop β†’ βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜))) ∧ (Fun 𝑔 ∧ βˆ… βˆ‰ ran 𝑔)) ∧ π‘₯ ∈ dom 𝑔) β†’ (π‘”β€˜π‘₯) ∈ ran 𝑔)
51 eleq1 2821 . . . . . . . . 9 ((π‘”β€˜π‘₯) = βˆ… β†’ ((π‘”β€˜π‘₯) ∈ ran 𝑔 ↔ βˆ… ∈ ran 𝑔))
5250, 51syl5ibcom 244 . . . . . . . 8 (((βˆ€π‘“(𝑓:dom π‘“βŸΆTop β†’ βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜))) ∧ (Fun 𝑔 ∧ βˆ… βˆ‰ ran 𝑔)) ∧ π‘₯ ∈ dom 𝑔) β†’ ((π‘”β€˜π‘₯) = βˆ… β†’ βˆ… ∈ ran 𝑔))
5352necon3bd 2954 . . . . . . 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 2732 . . . . . 6 𝒫 βˆͺ (π‘”β€˜π‘₯) = 𝒫 βˆͺ (π‘”β€˜π‘₯)
56 eqid 2732 . . . . . 6 {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))} = {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}
57 eqid 2732 . . . . . 6 (∏tβ€˜(π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))})) = (∏tβ€˜(π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}))
58 fveq1 6890 . . . . . . . . . . 11 (𝑠 = 𝑔 β†’ (π‘ β€˜π‘˜) = (π‘”β€˜π‘˜))
5958ixpeq2dv 8909 . . . . . . . . . 10 (𝑠 = 𝑔 β†’ Xπ‘˜ ∈ dom 𝑔(π‘ β€˜π‘˜) = Xπ‘˜ ∈ dom 𝑔(π‘”β€˜π‘˜))
60 fveq2 6891 . . . . . . . . . . 11 (π‘˜ = π‘₯ β†’ (π‘”β€˜π‘˜) = (π‘”β€˜π‘₯))
6160cbvixpv 8911 . . . . . . . . . 10 Xπ‘˜ ∈ dom 𝑔(π‘”β€˜π‘˜) = Xπ‘₯ ∈ dom 𝑔(π‘”β€˜π‘₯)
6259, 61eqtrdi 2788 . . . . . . . . 9 (𝑠 = 𝑔 β†’ Xπ‘˜ ∈ dom 𝑔(π‘ β€˜π‘˜) = Xπ‘₯ ∈ dom 𝑔(π‘”β€˜π‘₯))
6362fveq2d 6895 . . . . . . . 8 (𝑠 = 𝑔 β†’ ((clsβ€˜(∏tβ€˜(π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))})))β€˜Xπ‘˜ ∈ dom 𝑔(π‘ β€˜π‘˜)) = ((clsβ€˜(∏tβ€˜(π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))})))β€˜Xπ‘₯ ∈ dom 𝑔(π‘”β€˜π‘₯)))
6458fveq2d 6895 . . . . . . . . . 10 (𝑠 = 𝑔 β†’ ((clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})β€˜(π‘ β€˜π‘˜)) = ((clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})β€˜(π‘”β€˜π‘˜)))
6564ixpeq2dv 8909 . . . . . . . . 9 (𝑠 = 𝑔 β†’ Xπ‘˜ ∈ dom 𝑔((clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})β€˜(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑔((clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})β€˜(π‘”β€˜π‘˜)))
6660unieqd 4922 . . . . . . . . . . . . . . . . 17 (π‘˜ = π‘₯ β†’ βˆͺ (π‘”β€˜π‘˜) = βˆͺ (π‘”β€˜π‘₯))
6766pweqd 4619 . . . . . . . . . . . . . . . 16 (π‘˜ = π‘₯ β†’ 𝒫 βˆͺ (π‘”β€˜π‘˜) = 𝒫 βˆͺ (π‘”β€˜π‘₯))
6867sneqd 4640 . . . . . . . . . . . . . . 15 (π‘˜ = π‘₯ β†’ {𝒫 βˆͺ (π‘”β€˜π‘˜)} = {𝒫 βˆͺ (π‘”β€˜π‘₯)})
6960, 68uneq12d 4164 . . . . . . . . . . . . . 14 (π‘˜ = π‘₯ β†’ ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))
7069pweqd 4619 . . . . . . . . . . . . 13 (π‘˜ = π‘₯ β†’ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) = 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))
7167eleq1d 2818 . . . . . . . . . . . . . 14 (π‘˜ = π‘₯ β†’ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 ↔ 𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦))
7269eqeq2d 2743 . . . . . . . . . . . . . 14 (π‘˜ = π‘₯ β†’ (𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ↔ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)})))
7371, 72imbi12d 344 . . . . . . . . . . . . 13 (π‘˜ = π‘₯ β†’ ((𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)})) ↔ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))))
7470, 73rabeqbidv 3449 . . . . . . . . . . . 12 (π‘˜ = π‘₯ β†’ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))} = {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))})
7574fveq2d 6895 . . . . . . . . . . 11 (π‘˜ = π‘₯ β†’ (clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))}) = (clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}))
7675, 60fveq12d 6898 . . . . . . . . . 10 (π‘˜ = π‘₯ β†’ ((clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})β€˜(π‘”β€˜π‘˜)) = ((clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))})β€˜(π‘”β€˜π‘₯)))
7776cbvixpv 8911 . . . . . . . . 9 Xπ‘˜ ∈ dom 𝑔((clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})β€˜(π‘”β€˜π‘˜)) = Xπ‘₯ ∈ dom 𝑔((clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))})β€˜(π‘”β€˜π‘₯))
7865, 77eqtrdi 2788 . . . . . . . 8 (𝑠 = 𝑔 β†’ Xπ‘˜ ∈ dom 𝑔((clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})β€˜(π‘ β€˜π‘˜)) = Xπ‘₯ ∈ dom 𝑔((clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))})β€˜(π‘”β€˜π‘₯)))
7963, 78eqeq12d 2748 . . . . . . 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 5431 . . . . . . . . . . . . 13 {𝒫 βˆͺ (π‘”β€˜π‘₯)} ∈ V
8241, 81unex 7735 . . . . . . . . . . . 12 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∈ V
83 ssun2 4173 . . . . . . . . . . . . 13 {𝒫 βˆͺ (π‘”β€˜π‘₯)} βŠ† ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)})
8441uniex 7733 . . . . . . . . . . . . . . 15 βˆͺ (π‘”β€˜π‘₯) ∈ V
8584pwex 5378 . . . . . . . . . . . . . 14 𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ V
8685snid 4664 . . . . . . . . . . . . 13 𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ {𝒫 βˆͺ (π‘”β€˜π‘₯)}
8783, 86sselii 3979 . . . . . . . . . . . 12 𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)})
88 epttop 22732 . . . . . . . . . . . 12 ((((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∈ V ∧ 𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)})) β†’ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))} ∈ (TopOnβ€˜((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)})))
8982, 87, 88mp2an 690 . . . . . . . . . . 11 {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))} ∈ (TopOnβ€˜((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))
9089topontopi 22637 . . . . . . . . . 10 {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))} ∈ Top
9190a1i 11 . . . . . . . . 9 (((βˆ€π‘“(𝑓:dom π‘“βŸΆTop β†’ βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜))) ∧ (Fun 𝑔 ∧ βˆ… βˆ‰ ran 𝑔)) ∧ π‘₯ ∈ dom 𝑔) β†’ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))} ∈ Top)
9291fmpttd 7116 . . . . . . . 8 ((βˆ€π‘“(𝑓:dom π‘“βŸΆTop β†’ βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜))) ∧ (Fun 𝑔 ∧ βˆ… βˆ‰ ran 𝑔)) β†’ (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}):dom π‘”βŸΆTop)
9339mptex 7227 . . . . . . . . 9 (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) ∈ V
94 id 22 . . . . . . . . . . 11 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ 𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}))
95 dmeq 5903 . . . . . . . . . . . 12 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ dom 𝑓 = dom (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}))
9682pwex 5378 . . . . . . . . . . . . . 14 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∈ V
9796rabex 5332 . . . . . . . . . . . . 13 {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))} ∈ V
98 eqid 2732 . . . . . . . . . . . . 13 (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))})
9997, 98dmmpti 6694 . . . . . . . . . . . 12 dom (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) = dom 𝑔
10095, 99eqtrdi 2788 . . . . . . . . . . 11 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ dom 𝑓 = dom 𝑔)
10194, 100feq12d 6705 . . . . . . . . . 10 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ (𝑓:dom π‘“βŸΆTop ↔ (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}):dom π‘”βŸΆTop))
102100ixpeq1d 8905 . . . . . . . . . . . 12 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ Xπ‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜) = Xπ‘˜ ∈ dom 𝑔𝒫 βˆͺ (π‘“β€˜π‘˜))
103 fveq1 6890 . . . . . . . . . . . . . . . . 17 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ (π‘“β€˜π‘˜) = ((π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))})β€˜π‘˜))
104 fveq2 6891 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = π‘˜ β†’ (π‘”β€˜π‘₯) = (π‘”β€˜π‘˜))
105104unieqd 4922 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = π‘˜ β†’ βˆͺ (π‘”β€˜π‘₯) = βˆͺ (π‘”β€˜π‘˜))
106105pweqd 4619 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = π‘˜ β†’ 𝒫 βˆͺ (π‘”β€˜π‘₯) = 𝒫 βˆͺ (π‘”β€˜π‘˜))
107106sneqd 4640 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = π‘˜ β†’ {𝒫 βˆͺ (π‘”β€˜π‘₯)} = {𝒫 βˆͺ (π‘”β€˜π‘˜)})
108104, 107uneq12d 4164 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = π‘˜ β†’ ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))
109108pweqd 4619 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = π‘˜ β†’ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) = 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))
110106eleq1d 2818 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = π‘˜ β†’ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 ↔ 𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦))
111108eqeq2d 2743 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = π‘˜ β†’ (𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ↔ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)})))
112110, 111imbi12d 344 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = π‘˜ β†’ ((𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)})) ↔ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))))
113109, 112rabeqbidv 3449 . . . . . . . . . . . . . . . . . 18 (π‘₯ = π‘˜ β†’ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))} = {𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})
114 fvex 6904 . . . . . . . . . . . . . . . . . . . . 21 (π‘”β€˜π‘˜) ∈ V
115 snex 5431 . . . . . . . . . . . . . . . . . . . . 21 {𝒫 βˆͺ (π‘”β€˜π‘˜)} ∈ V
116114, 115unex 7735 . . . . . . . . . . . . . . . . . . . 20 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∈ V
117116pwex 5378 . . . . . . . . . . . . . . . . . . 19 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∈ V
118117rabex 5332 . . . . . . . . . . . . . . . . . 18 {𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))} ∈ V
119113, 98, 118fvmpt 6998 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ dom 𝑔 β†’ ((π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))})β€˜π‘˜) = {𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})
120103, 119sylan9eq 2792 . . . . . . . . . . . . . . . 16 ((𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) ∧ π‘˜ ∈ dom 𝑔) β†’ (π‘“β€˜π‘˜) = {𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})
121120unieqd 4922 . . . . . . . . . . . . . . 15 ((𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) ∧ π‘˜ ∈ dom 𝑔) β†’ βˆͺ (π‘“β€˜π‘˜) = βˆͺ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})
122 ssun2 4173 . . . . . . . . . . . . . . . . . 18 {𝒫 βˆͺ (π‘”β€˜π‘˜)} βŠ† ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)})
123114uniex 7733 . . . . . . . . . . . . . . . . . . . 20 βˆͺ (π‘”β€˜π‘˜) ∈ V
124123pwex 5378 . . . . . . . . . . . . . . . . . . 19 𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ V
125124snid 4664 . . . . . . . . . . . . . . . . . 18 𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ {𝒫 βˆͺ (π‘”β€˜π‘˜)}
126122, 125sselii 3979 . . . . . . . . . . . . . . . . 17 𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)})
127 epttop 22732 . . . . . . . . . . . . . . . . 17 ((((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∈ V ∧ 𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)})) β†’ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))} ∈ (TopOnβ€˜((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)})))
128116, 126, 127mp2an 690 . . . . . . . . . . . . . . . 16 {𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))} ∈ (TopOnβ€˜((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))
129128toponunii 22638 . . . . . . . . . . . . . . 15 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) = βˆͺ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))}
130121, 129eqtr4di 2790 . . . . . . . . . . . . . 14 ((𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) ∧ π‘˜ ∈ dom 𝑔) β†’ βˆͺ (π‘“β€˜π‘˜) = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))
131130pweqd 4619 . . . . . . . . . . . . 13 ((𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) ∧ π‘˜ ∈ dom 𝑔) β†’ 𝒫 βˆͺ (π‘“β€˜π‘˜) = 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))
132131ixpeq2dva 8908 . . . . . . . . . . . 12 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ Xπ‘˜ ∈ dom 𝑔𝒫 βˆͺ (π‘“β€˜π‘˜) = Xπ‘˜ ∈ dom 𝑔𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))
133102, 132eqtrd 2772 . . . . . . . . . . 11 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ Xπ‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜) = Xπ‘˜ ∈ dom 𝑔𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))
134 2fveq3 6896 . . . . . . . . . . . . 13 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ (clsβ€˜(∏tβ€˜π‘“)) = (clsβ€˜(∏tβ€˜(π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}))))
135100ixpeq1d 8905 . . . . . . . . . . . . 13 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜) = Xπ‘˜ ∈ dom 𝑔(π‘ β€˜π‘˜))
136134, 135fveq12d 6898 . . . . . . . . . . . 12 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ ((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = ((clsβ€˜(∏tβ€˜(π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))})))β€˜Xπ‘˜ ∈ dom 𝑔(π‘ β€˜π‘˜)))
137100ixpeq1d 8905 . . . . . . . . . . . . 13 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑔((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜)))
138120fveq2d 6895 . . . . . . . . . . . . . . 15 ((𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) ∧ π‘˜ ∈ dom 𝑔) β†’ (clsβ€˜(π‘“β€˜π‘˜)) = (clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))}))
139138fveq1d 6893 . . . . . . . . . . . . . 14 ((𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) ∧ π‘˜ ∈ dom 𝑔) β†’ ((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜)) = ((clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})β€˜(π‘ β€˜π‘˜)))
140139ixpeq2dva 8908 . . . . . . . . . . . . 13 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ Xπ‘˜ ∈ dom 𝑔((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑔((clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})β€˜(π‘ β€˜π‘˜)))
141137, 140eqtrd 2772 . . . . . . . . . . . 12 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑔((clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})β€˜(π‘ β€˜π‘˜)))
142136, 141eqeq12d 2748 . . . . . . . . . . 11 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ (((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜)) ↔ ((clsβ€˜(∏tβ€˜(π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))})))β€˜Xπ‘˜ ∈ dom 𝑔(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑔((clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})β€˜(π‘ β€˜π‘˜))))
143133, 142raleqbidv 3342 . . . . . . . . . 10 (𝑓 = (π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))}) β†’ (βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜)) ↔ βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑔𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)})((clsβ€˜(∏tβ€˜(π‘₯ ∈ dom 𝑔 ↦ {𝑦 ∈ 𝒫 ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘₯) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘₯) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘₯)}))})))β€˜Xπ‘˜ ∈ dom 𝑔(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑔((clsβ€˜{𝑦 ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ∣ (𝒫 βˆͺ (π‘”β€˜π‘˜) ∈ 𝑦 β†’ 𝑦 = ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))})β€˜(π‘ β€˜π‘˜))))
144101, 143imbi12d 344 . . . . . . . . 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 3595 . . . . . . . 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 769 . . . . . . . . 9 ((βˆ€π‘“(𝑓:dom π‘“βŸΆTop β†’ βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜))) ∧ (Fun 𝑔 ∧ βˆ… βˆ‰ ran 𝑔)) β†’ Fun 𝑔)
148147funfnd 6579 . . . . . . . 8 ((βˆ€π‘“(𝑓:dom π‘“βŸΆTop β†’ βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜))) ∧ (Fun 𝑔 ∧ βˆ… βˆ‰ ran 𝑔)) β†’ 𝑔 Fn dom 𝑔)
149 ssun1 4172 . . . . . . . . . 10 (π‘”β€˜π‘˜) βŠ† ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)})
150114elpw 4606 . . . . . . . . . 10 ((π‘”β€˜π‘˜) ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}) ↔ (π‘”β€˜π‘˜) βŠ† ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)}))
151149, 150mpbir 230 . . . . . . . . 9 (π‘”β€˜π‘˜) ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)})
152151rgenw 3065 . . . . . . . 8 βˆ€π‘˜ ∈ dom 𝑔(π‘”β€˜π‘˜) ∈ 𝒫 ((π‘”β€˜π‘˜) βˆͺ {𝒫 βˆͺ (π‘”β€˜π‘˜)})
15338elixp 8900 . . . . . . . 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 3613 . . . . . 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 23341 . . . . 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 1930 . . 3 (βˆ€π‘“(𝑓:dom π‘“βŸΆTop β†’ βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜))) β†’ βˆ€π‘”((Fun 𝑔 ∧ βˆ… βˆ‰ ran 𝑔) β†’ Xπ‘₯ ∈ dom 𝑔(π‘”β€˜π‘₯) β‰  βˆ…))
159 dfac9 10133 . . 3 (CHOICE ↔ βˆ€π‘”((Fun 𝑔 ∧ βˆ… βˆ‰ ran 𝑔) β†’ Xπ‘₯ ∈ dom 𝑔(π‘”β€˜π‘₯) β‰  βˆ…))
160158, 159sylibr 233 . 2 (βˆ€π‘“(𝑓:dom π‘“βŸΆTop β†’ βˆ€π‘  ∈ X π‘˜ ∈ dom 𝑓𝒫 βˆͺ (π‘“β€˜π‘˜)((clsβ€˜(∏tβ€˜π‘“))β€˜Xπ‘˜ ∈ dom 𝑓(π‘ β€˜π‘˜)) = Xπ‘˜ ∈ dom 𝑓((clsβ€˜(π‘“β€˜π‘˜))β€˜(π‘ β€˜π‘˜))) β†’ CHOICE)
16137, 160impbii 208 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 205   ∧ wa 396  βˆ€wal 1539   = wceq 1541   ∈ wcel 2106   β‰  wne 2940   βˆ‰ wnel 3046  βˆ€wral 3061  {crab 3432  Vcvv 3474   βˆͺ cun 3946   βŠ† wss 3948  βˆ…c0 4322  π’« cpw 4602  {csn 4628  βˆͺ cuni 4908  βˆͺ ciun 4997   ↦ cmpt 5231  dom cdm 5676  ran crn 5677  Fun wfun 6537   Fn wfn 6538  βŸΆwf 6539  β€“ontoβ†’wfo 6541  β€˜cfv 6543  Xcixp 8893  AC wacn 9935  CHOICEwac 10112  βˆtcpt 17388  Topctop 22615  TopOnctopon 22632  clsccl 22742
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-1o 8468  df-er 8705  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-fin 8945  df-fi 9408  df-card 9936  df-acn 9939  df-ac 10113  df-topgen 17393  df-pt 17394  df-top 22616  df-topon 22633  df-bases 22669  df-cld 22743  df-ntr 22744  df-cls 22745
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator