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

Theorem dfac14 17418
Description: Theorem ptcls 17416 is an equivalent of the axiom of choice. (Contributed by Mario Carneiro, 3-Sep-2015.)
Assertion
Ref Expression
dfac14  |-  (CHOICE  <->  A. f
( f : dom  f
--> Top  ->  A. s  e.  X_  k  e.  dom  f ~P U. ( f `
 k ) ( ( cls `  ( Xt_ `  f ) ) `
 X_ k  e.  dom  f ( s `  k ) )  = 
X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
) ) )
Distinct variable group:    f, k, s

Proof of Theorem dfac14
Dummy variables  g  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5608 . . . . . . . . . 10  |-  ( k  =  x  ->  (
f `  k )  =  ( f `  x ) )
21unieqd 3919 . . . . . . . . 9  |-  ( k  =  x  ->  U. (
f `  k )  =  U. ( f `  x ) )
32pweqd 3706 . . . . . . . 8  |-  ( k  =  x  ->  ~P U. ( f `  k
)  =  ~P U. ( f `  x
) )
43cbvixpv 6922 . . . . . . 7  |-  X_ k  e.  dom  f ~P U. ( f `  k
)  =  X_ x  e.  dom  f ~P U. ( f `  x
)
54eleq2i 2422 . . . . . 6  |-  ( s  e.  X_ k  e.  dom  f ~P U. ( f `
 k )  <->  s  e.  X_ x  e.  dom  f ~P U. ( f `  x ) )
6 simplr 731 . . . . . . . . . . 11  |-  ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  ->  f : dom  f
--> Top )
76feqmptd 5658 . . . . . . . . . 10  |-  ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  ->  f  =  ( k  e.  dom  f  |->  ( f `  k
) ) )
87fveq2d 5612 . . . . . . . . 9  |-  ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  ->  ( Xt_ `  f
)  =  ( Xt_ `  ( k  e.  dom  f  |->  ( f `  k ) ) ) )
98fveq2d 5612 . . . . . . . 8  |-  ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  ->  ( cls `  ( Xt_ `  f ) )  =  ( cls `  ( Xt_ `  ( k  e. 
dom  f  |->  ( f `
 k ) ) ) ) )
109fveq1d 5610 . . . . . . 7  |-  ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  ->  ( ( cls `  ( Xt_ `  f
) ) `  X_ k  e.  dom  f ( s `
 k ) )  =  ( ( cls `  ( Xt_ `  (
k  e.  dom  f  |->  ( f `  k
) ) ) ) `
 X_ k  e.  dom  f ( s `  k ) ) )
11 eqid 2358 . . . . . . . 8  |-  ( Xt_ `  ( k  e.  dom  f  |->  ( f `  k ) ) )  =  ( Xt_ `  (
k  e.  dom  f  |->  ( f `  k
) ) )
12 vex 2867 . . . . . . . . . 10  |-  f  e. 
_V
1312dmex 5023 . . . . . . . . 9  |-  dom  f  e.  _V
1413a1i 10 . . . . . . . 8  |-  ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  ->  dom  f  e.  _V )
15 ffvelrn 5746 . . . . . . . . . 10  |-  ( ( f : dom  f --> Top  /\  k  e.  dom  f )  ->  (
f `  k )  e.  Top )
166, 15sylan 457 . . . . . . . . 9  |-  ( ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  /\  k  e.  dom  f )  ->  (
f `  k )  e.  Top )
17 eqid 2358 . . . . . . . . . 10  |-  U. (
f `  k )  =  U. ( f `  k )
1817toptopon 16777 . . . . . . . . 9  |-  ( ( f `  k )  e.  Top  <->  ( f `  k )  e.  (TopOn `  U. ( f `  k ) ) )
1916, 18sylib 188 . . . . . . . 8  |-  ( ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  /\  k  e.  dom  f )  ->  (
f `  k )  e.  (TopOn `  U. ( f `
 k ) ) )
20 simpr 447 . . . . . . . . . . . 12  |-  ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  ->  s  e.  X_ x  e.  dom  f ~P
U. ( f `  x ) )
2120, 5sylibr 203 . . . . . . . . . . 11  |-  ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  ->  s  e.  X_ k  e.  dom  f ~P
U. ( f `  k ) )
22 vex 2867 . . . . . . . . . . . . 13  |-  s  e. 
_V
2322elixp 6911 . . . . . . . . . . . 12  |-  ( s  e.  X_ k  e.  dom  f ~P U. ( f `
 k )  <->  ( s  Fn  dom  f  /\  A. k  e.  dom  f ( s `  k )  e.  ~P U. (
f `  k )
) )
2423simprbi 450 . . . . . . . . . . 11  |-  ( s  e.  X_ k  e.  dom  f ~P U. ( f `
 k )  ->  A. k  e.  dom  f ( s `  k )  e.  ~P U. ( f `  k
) )
2521, 24syl 15 . . . . . . . . . 10  |-  ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  ->  A. k  e.  dom  f ( s `  k )  e.  ~P U. ( f `  k
) )
2625r19.21bi 2717 . . . . . . . . 9  |-  ( ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  /\  k  e.  dom  f )  ->  (
s `  k )  e.  ~P U. ( f `
 k ) )
27 elpwi 3709 . . . . . . . . 9  |-  ( ( s `  k )  e.  ~P U. (
f `  k )  ->  ( s `  k
)  C_  U. (
f `  k )
)
2826, 27syl 15 . . . . . . . 8  |-  ( ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  /\  k  e.  dom  f )  ->  (
s `  k )  C_ 
U. ( f `  k ) )
29 fvex 5622 . . . . . . . . . 10  |-  ( s `
 k )  e. 
_V
3013, 29iunex 5857 . . . . . . . . 9  |-  U_ k  e.  dom  f ( s `
 k )  e. 
_V
31 simpll 730 . . . . . . . . . 10  |-  ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  -> CHOICE
)
32 acacni 7856 . . . . . . . . . 10  |-  ( (CHOICE  /\  dom  f  e.  _V )  -> AC  dom  f  =  _V )
3331, 13, 32sylancl 643 . . . . . . . . 9  |-  ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  -> AC  dom  f  =  _V )
3430, 33syl5eleqr 2445 . . . . . . . 8  |-  ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  ->  U_ k  e.  dom  f ( s `  k )  e. AC  dom  f
)
3511, 14, 19, 28, 34ptclsg 17415 . . . . . . 7  |-  ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  ->  ( ( cls `  ( Xt_ `  (
k  e.  dom  f  |->  ( f `  k
) ) ) ) `
 X_ k  e.  dom  f ( s `  k ) )  = 
X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
) )
3610, 35eqtrd 2390 . . . . . 6  |-  ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ x  e.  dom  f ~P U. ( f `
 x ) )  ->  ( ( cls `  ( Xt_ `  f
) ) `  X_ k  e.  dom  f ( s `
 k ) )  =  X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
) )
375, 36sylan2b 461 . . . . 5  |-  ( ( (CHOICE 
/\  f : dom  f
--> Top )  /\  s  e.  X_ k  e.  dom  f ~P U. ( f `
 k ) )  ->  ( ( cls `  ( Xt_ `  f
) ) `  X_ k  e.  dom  f ( s `
 k ) )  =  X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
) )
3837ralrimiva 2702 . . . 4  |-  ( (CHOICE  /\  f : dom  f --> Top )  ->  A. s  e.  X_  k  e.  dom  f ~P U. ( f `
 k ) ( ( cls `  ( Xt_ `  f ) ) `
 X_ k  e.  dom  f ( s `  k ) )  = 
X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
) )
3938ex 423 . . 3  |-  (CHOICE  ->  (
f : dom  f --> Top  ->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) ) )
4039alrimiv 1631 . 2  |-  (CHOICE  ->  A. f
( f : dom  f
--> Top  ->  A. s  e.  X_  k  e.  dom  f ~P U. ( f `
 k ) ( ( cls `  ( Xt_ `  f ) ) `
 X_ k  e.  dom  f ( s `  k ) )  = 
X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
) ) )
41 vex 2867 . . . . . . . 8  |-  g  e. 
_V
4241dmex 5023 . . . . . . 7  |-  dom  g  e.  _V
4342a1i 10 . . . . . 6  |-  ( ( A. f ( f : dom  f --> Top 
->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  ->  dom  g  e.  _V )
44 fvex 5622 . . . . . . 7  |-  ( g `
 x )  e. 
_V
4544a1i 10 . . . . . 6  |-  ( ( ( A. f ( f : dom  f --> Top  ->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  /\  x  e.  dom  g )  -> 
( g `  x
)  e.  _V )
46 simplrr 737 . . . . . . . 8  |-  ( ( ( A. f ( f : dom  f --> Top  ->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  /\  x  e.  dom  g )  ->  (/) 
e/  ran  g )
47 df-nel 2524 . . . . . . . 8  |-  ( (/)  e/ 
ran  g  <->  -.  (/)  e.  ran  g )
4846, 47sylib 188 . . . . . . 7  |-  ( ( ( A. f ( f : dom  f --> Top  ->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  /\  x  e.  dom  g )  ->  -.  (/)  e.  ran  g
)
49 funforn 5541 . . . . . . . . . . . 12  |-  ( Fun  g  <->  g : dom  g -onto-> ran  g )
50 fof 5534 . . . . . . . . . . . 12  |-  ( g : dom  g -onto-> ran  g  ->  g : dom  g --> ran  g )
5149, 50sylbi 187 . . . . . . . . . . 11  |-  ( Fun  g  ->  g : dom  g --> ran  g )
5251ad2antrl 708 . . . . . . . . . 10  |-  ( ( A. f ( f : dom  f --> Top 
->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  ->  g : dom  g --> ran  g
)
53 ffvelrn 5746 . . . . . . . . . 10  |-  ( ( g : dom  g --> ran  g  /\  x  e.  dom  g )  -> 
( g `  x
)  e.  ran  g
)
5452, 53sylan 457 . . . . . . . . 9  |-  ( ( ( A. f ( f : dom  f --> Top  ->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  /\  x  e.  dom  g )  -> 
( g `  x
)  e.  ran  g
)
55 eleq1 2418 . . . . . . . . 9  |-  ( ( g `  x )  =  (/)  ->  ( ( g `  x )  e.  ran  g  <->  (/)  e.  ran  g ) )
5654, 55syl5ibcom 211 . . . . . . . 8  |-  ( ( ( A. f ( f : dom  f --> Top  ->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  /\  x  e.  dom  g )  -> 
( ( g `  x )  =  (/)  -> 
(/)  e.  ran  g ) )
5756necon3bd 2558 . . . . . . 7  |-  ( ( ( A. f ( f : dom  f --> Top  ->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  /\  x  e.  dom  g )  -> 
( -.  (/)  e.  ran  g  ->  ( g `  x )  =/=  (/) ) )
5848, 57mpd 14 . . . . . 6  |-  ( ( ( A. f ( f : dom  f --> Top  ->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  /\  x  e.  dom  g )  -> 
( g `  x
)  =/=  (/) )
59 eqid 2358 . . . . . 6  |-  ~P U. ( g `  x
)  =  ~P U. ( g `  x
)
60 eqid 2358 . . . . . 6  |-  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) }  =  {
y  e.  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) }
61 eqid 2358 . . . . . 6  |-  ( Xt_ `  ( x  e.  dom  g  |->  { y  e. 
~P ( ( g `
 x )  u. 
{ ~P U. (
g `  x ) } )  |  ( ~P U. ( g `
 x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) )  =  ( Xt_ `  (
x  e.  dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  |  ( ~P U. ( g `  x
)  e.  y  -> 
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) ) } ) )
62 simprl 732 . . . . . . . . 9  |-  ( ( A. f ( f : dom  f --> Top 
->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  ->  Fun  g )
63 funfn 5365 . . . . . . . . 9  |-  ( Fun  g  <->  g  Fn  dom  g )
6462, 63sylib 188 . . . . . . . 8  |-  ( ( A. f ( f : dom  f --> Top 
->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  ->  g  Fn  dom  g )
65 ssun1 3414 . . . . . . . . . . 11  |-  ( g `
 k )  C_  ( ( g `  k )  u.  { ~P U. ( g `  k ) } )
66 fvex 5622 . . . . . . . . . . . 12  |-  ( g `
 k )  e. 
_V
6766elpw 3707 . . . . . . . . . . 11  |-  ( ( g `  k )  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k
) } )  <->  ( g `  k )  C_  (
( g `  k
)  u.  { ~P U. ( g `  k
) } ) )
6865, 67mpbir 200 . . . . . . . . . 10  |-  ( g `
 k )  e. 
~P ( ( g `
 k )  u. 
{ ~P U. (
g `  k ) } )
6968rgenw 2686 . . . . . . . . 9  |-  A. k  e.  dom  g ( g `
 k )  e. 
~P ( ( g `
 k )  u. 
{ ~P U. (
g `  k ) } )
7069a1i 10 . . . . . . . 8  |-  ( ( A. f ( f : dom  f --> Top 
->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  ->  A. k  e.  dom  g ( g `
 k )  e. 
~P ( ( g `
 k )  u. 
{ ~P U. (
g `  k ) } ) )
7141elixp 6911 . . . . . . . 8  |-  ( g  e.  X_ k  e.  dom  g ~P ( ( g `
 k )  u. 
{ ~P U. (
g `  k ) } )  <->  ( g  Fn  dom  g  /\  A. k  e.  dom  g ( g `  k )  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) ) )
7264, 70, 71sylanbrc 645 . . . . . . 7  |-  ( ( A. f ( f : dom  f --> Top 
->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  ->  g  e.  X_ k  e.  dom  g ~P ( ( g `
 k )  u. 
{ ~P U. (
g `  k ) } ) )
73 simpl 443 . . . . . . . 8  |-  ( ( A. f ( f : dom  f --> Top 
->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  ->  A. f
( f : dom  f
--> Top  ->  A. s  e.  X_  k  e.  dom  f ~P U. ( f `
 k ) ( ( cls `  ( Xt_ `  f ) ) `
 X_ k  e.  dom  f ( s `  k ) )  = 
X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
) ) )
74 snex 4297 . . . . . . . . . . . . 13  |-  { ~P U. ( g `  x
) }  e.  _V
7544, 74unex 4600 . . . . . . . . . . . 12  |-  ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  e. 
_V
76 ssun2 3415 . . . . . . . . . . . . 13  |-  { ~P U. ( g `  x
) }  C_  (
( g `  x
)  u.  { ~P U. ( g `  x
) } )
7744uniex 4598 . . . . . . . . . . . . . . 15  |-  U. (
g `  x )  e.  _V
7877pwex 4274 . . . . . . . . . . . . . 14  |-  ~P U. ( g `  x
)  e.  _V
7978snid 3743 . . . . . . . . . . . . 13  |-  ~P U. ( g `  x
)  e.  { ~P U. ( g `  x
) }
8076, 79sselii 3253 . . . . . . . . . . . 12  |-  ~P U. ( g `  x
)  e.  ( ( g `  x )  u.  { ~P U. ( g `  x
) } )
81 epttop 16852 . . . . . . . . . . . 12  |-  ( ( ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  e.  _V  /\  ~P U. ( g `  x
)  e.  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) )  ->  { y  e. 
~P ( ( g `
 x )  u. 
{ ~P U. (
g `  x ) } )  |  ( ~P U. ( g `
 x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) }  e.  (TopOn `  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) )
8275, 80, 81mp2an 653 . . . . . . . . . . 11  |-  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) }  e.  (TopOn `  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) )
8382topontopi 16775 . . . . . . . . . 10  |-  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) }  e.  Top
8483a1i 10 . . . . . . . . 9  |-  ( ( ( A. f ( f : dom  f --> Top  ->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  /\  x  e.  dom  g )  ->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  |  ( ~P U. ( g `  x
)  e.  y  -> 
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) ) }  e.  Top )
85 eqid 2358 . . . . . . . . 9  |-  ( x  e.  dom  g  |->  { y  e.  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  =  ( x  e.  dom  g  |->  { y  e. 
~P ( ( g `
 x )  u. 
{ ~P U. (
g `  x ) } )  |  ( ~P U. ( g `
 x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )
8684, 85fmptd 5767 . . . . . . . 8  |-  ( ( A. f ( f : dom  f --> Top 
->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  ->  (
x  e.  dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  |  ( ~P U. ( g `  x
)  e.  y  -> 
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) ) } ) : dom  g
--> Top )
8742mptex 5832 . . . . . . . . 9  |-  ( x  e.  dom  g  |->  { y  e.  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  e. 
_V
88 id 19 . . . . . . . . . . 11  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  -> 
f  =  ( x  e.  dom  g  |->  { y  e.  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) )
89 dmeq 4961 . . . . . . . . . . . 12  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  ->  dom  f  =  dom  ( x  e.  dom  g  |->  { y  e. 
~P ( ( g `
 x )  u. 
{ ~P U. (
g `  x ) } )  |  ( ~P U. ( g `
 x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) )
9075pwex 4274 . . . . . . . . . . . . . 14  |-  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  e. 
_V
9190rabex 4246 . . . . . . . . . . . . 13  |-  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) }  e.  _V
9291, 85dmmpti 5455 . . . . . . . . . . . 12  |-  dom  (
x  e.  dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  |  ( ~P U. ( g `  x
)  e.  y  -> 
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) ) } )  =  dom  g
9389, 92syl6eq 2406 . . . . . . . . . . 11  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  ->  dom  f  =  dom  g )
9488, 93feq12d 5463 . . . . . . . . . 10  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  -> 
( f : dom  f
--> Top  <->  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) : dom  g --> Top )
)
95 ixpeq1 6915 . . . . . . . . . . . . 13  |-  ( dom  f  =  dom  g  -> 
X_ k  e.  dom  f ~P U. ( f `
 k )  = 
X_ k  e.  dom  g ~P U. ( f `
 k ) )
9693, 95syl 15 . . . . . . . . . . . 12  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  ->  X_ k  e.  dom  f ~P U. ( f `  k )  =  X_ k  e.  dom  g ~P
U. ( f `  k ) )
97 fveq1 5607 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  -> 
( f `  k
)  =  ( ( x  e.  dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  |  ( ~P U. ( g `  x
)  e.  y  -> 
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) ) } ) `  k
) )
98 fveq2 5608 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  k  ->  (
g `  x )  =  ( g `  k ) )
9998unieqd 3919 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  k  ->  U. (
g `  x )  =  U. ( g `  k ) )
10099pweqd 3706 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  k  ->  ~P U. ( g `  x
)  =  ~P U. ( g `  k
) )
101100sneqd 3729 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  k  ->  { ~P U. ( g `  x
) }  =  { ~P U. ( g `  k ) } )
10298, 101uneq12d 3406 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  k  ->  (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) )
103102pweqd 3706 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  k  ->  ~P ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  =  ~P ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) )
104100eleq1d 2424 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  k  ->  ( ~P U. ( g `  x )  e.  y  <->  ~P U. ( g `  k )  e.  y ) )
105102eqeq2d 2369 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  k  ->  (
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  <->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) )
106104, 105imbi12d 311 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  k  ->  (
( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) )  <->  ( ~P U. ( g `  k
)  e.  y  -> 
y  =  ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) ) ) )
107103, 106rabeqbidv 2859 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  k  ->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) }  =  {
y  e.  ~P (
( g `  k
)  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } )
108 snex 4297 . . . . . . . . . . . . . . . . . . . . . 22  |-  { ~P U. ( g `  k
) }  e.  _V
10966, 108unex 4600 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( g `  k )  u.  { ~P U. ( g `  k
) } )  e. 
_V
110109pwex 4274 . . . . . . . . . . . . . . . . . . . 20  |-  ~P (
( g `  k
)  u.  { ~P U. ( g `  k
) } )  e. 
_V
111110rabex 4246 . . . . . . . . . . . . . . . . . . 19  |-  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) }  e.  _V
112107, 85, 111fvmpt 5685 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  dom  g  -> 
( ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) `  k )  =  {
y  e.  ~P (
( g `  k
)  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } )
11397, 112sylan9eq 2410 . . . . . . . . . . . . . . . . 17  |-  ( ( f  =  ( x  e.  dom  g  |->  { y  e.  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  /\  k  e.  dom  g )  ->  ( f `  k )  =  {
y  e.  ~P (
( g `  k
)  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } )
114113unieqd 3919 . . . . . . . . . . . . . . . 16  |-  ( ( f  =  ( x  e.  dom  g  |->  { y  e.  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  /\  k  e.  dom  g )  ->  U. ( f `  k )  =  U. { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } )  |  ( ~P U. ( g `  k
)  e.  y  -> 
y  =  ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) ) } )
115 ssun2 3415 . . . . . . . . . . . . . . . . . . 19  |-  { ~P U. ( g `  k
) }  C_  (
( g `  k
)  u.  { ~P U. ( g `  k
) } )
11666uniex 4598 . . . . . . . . . . . . . . . . . . . . 21  |-  U. (
g `  k )  e.  _V
117116pwex 4274 . . . . . . . . . . . . . . . . . . . 20  |-  ~P U. ( g `  k
)  e.  _V
118117snid 3743 . . . . . . . . . . . . . . . . . . 19  |-  ~P U. ( g `  k
)  e.  { ~P U. ( g `  k
) }
119115, 118sselii 3253 . . . . . . . . . . . . . . . . . 18  |-  ~P U. ( g `  k
)  e.  ( ( g `  k )  u.  { ~P U. ( g `  k
) } )
120 epttop 16852 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( g `  k )  u.  { ~P U. ( g `  k ) } )  e.  _V  /\  ~P U. ( g `  k
)  e.  ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) )  ->  { y  e. 
~P ( ( g `
 k )  u. 
{ ~P U. (
g `  k ) } )  |  ( ~P U. ( g `
 k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) }  e.  (TopOn `  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) )
121109, 119, 120mp2an 653 . . . . . . . . . . . . . . . . 17  |-  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) }  e.  (TopOn `  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) )
122121toponunii 16776 . . . . . . . . . . . . . . . 16  |-  ( ( g `  k )  u.  { ~P U. ( g `  k
) } )  = 
U. { y  e. 
~P ( ( g `
 k )  u. 
{ ~P U. (
g `  k ) } )  |  ( ~P U. ( g `
 k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) }
123114, 122syl6eqr 2408 . . . . . . . . . . . . . . 15  |-  ( ( f  =  ( x  e.  dom  g  |->  { y  e.  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  /\  k  e.  dom  g )  ->  U. ( f `  k )  =  ( ( g `  k
)  u.  { ~P U. ( g `  k
) } ) )
124123pweqd 3706 . . . . . . . . . . . . . 14  |-  ( ( f  =  ( x  e.  dom  g  |->  { y  e.  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  /\  k  e.  dom  g )  ->  ~P U. (
f `  k )  =  ~P ( ( g `
 k )  u. 
{ ~P U. (
g `  k ) } ) )
125124ralrimiva 2702 . . . . . . . . . . . . 13  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  ->  A. k  e.  dom  g ~P U. ( f `
 k )  =  ~P ( ( g `
 k )  u. 
{ ~P U. (
g `  k ) } ) )
126 ixpeq2 6918 . . . . . . . . . . . . 13  |-  ( A. k  e.  dom  g ~P
U. ( f `  k )  =  ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } )  ->  X_ k  e.  dom  g ~P U. ( f `
 k )  = 
X_ k  e.  dom  g ~P ( ( g `
 k )  u. 
{ ~P U. (
g `  k ) } ) )
127125, 126syl 15 . . . . . . . . . . . 12  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  ->  X_ k  e.  dom  g ~P U. ( f `  k )  =  X_ k  e.  dom  g ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) )
12896, 127eqtrd 2390 . . . . . . . . . . 11  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  ->  X_ k  e.  dom  f ~P U. ( f `  k )  =  X_ k  e.  dom  g ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) )
129 fveq2 5608 . . . . . . . . . . . . . 14  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  -> 
( Xt_ `  f )  =  ( Xt_ `  (
x  e.  dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  |  ( ~P U. ( g `  x
)  e.  y  -> 
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) ) } ) ) )
130129fveq2d 5612 . . . . . . . . . . . . 13  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  -> 
( cls `  ( Xt_ `  f ) )  =  ( cls `  ( Xt_ `  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) ) ) )
131 ixpeq1 6915 . . . . . . . . . . . . . 14  |-  ( dom  f  =  dom  g  -> 
X_ k  e.  dom  f ( s `  k )  =  X_ k  e.  dom  g ( s `  k ) )
13293, 131syl 15 . . . . . . . . . . . . 13  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  ->  X_ k  e.  dom  f
( s `  k
)  =  X_ k  e.  dom  g ( s `
 k ) )
133130, 132fveq12d 5614 . . . . . . . . . . . 12  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  -> 
( ( cls `  ( Xt_ `  f ) ) `
 X_ k  e.  dom  f ( s `  k ) )  =  ( ( cls `  ( Xt_ `  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) ) ) `  X_ k  e.  dom  g ( s `
 k ) ) )
134 ixpeq1 6915 . . . . . . . . . . . . . 14  |-  ( dom  f  =  dom  g  -> 
X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
)  =  X_ k  e.  dom  g ( ( cls `  ( f `
 k ) ) `
 ( s `  k ) ) )
13593, 134syl 15 . . . . . . . . . . . . 13  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  ->  X_ k  e.  dom  f
( ( cls `  (
f `  k )
) `  ( s `  k ) )  = 
X_ k  e.  dom  g ( ( cls `  ( f `  k
) ) `  (
s `  k )
) )
136113fveq2d 5612 . . . . . . . . . . . . . . . 16  |-  ( ( f  =  ( x  e.  dom  g  |->  { y  e.  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  /\  k  e.  dom  g )  ->  ( cls `  (
f `  k )
)  =  ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } )  |  ( ~P U. ( g `  k
)  e.  y  -> 
y  =  ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) ) } ) )
137136fveq1d 5610 . . . . . . . . . . . . . . 15  |-  ( ( f  =  ( x  e.  dom  g  |->  { y  e.  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  /\  k  e.  dom  g )  ->  ( ( cls `  ( f `  k
) ) `  (
s `  k )
)  =  ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( s `  k
) ) )
138137ralrimiva 2702 . . . . . . . . . . . . . 14  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  ->  A. k  e.  dom  g ( ( cls `  ( f `  k
) ) `  (
s `  k )
)  =  ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( s `  k
) ) )
139 ixpeq2 6918 . . . . . . . . . . . . . 14  |-  ( A. k  e.  dom  g ( ( cls `  (
f `  k )
) `  ( s `  k ) )  =  ( ( cls `  {
y  e.  ~P (
( g `  k
)  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( s `  k
) )  ->  X_ k  e.  dom  g ( ( cls `  ( f `
 k ) ) `
 ( s `  k ) )  = 
X_ k  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } )  |  ( ~P U. ( g `  k
)  e.  y  -> 
y  =  ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) ) } ) `  (
s `  k )
) )
140138, 139syl 15 . . . . . . . . . . . . 13  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  ->  X_ k  e.  dom  g
( ( cls `  (
f `  k )
) `  ( s `  k ) )  = 
X_ k  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } )  |  ( ~P U. ( g `  k
)  e.  y  -> 
y  =  ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) ) } ) `  (
s `  k )
) )
141135, 140eqtrd 2390 . . . . . . . . . . . 12  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  ->  X_ k  e.  dom  f
( ( cls `  (
f `  k )
) `  ( s `  k ) )  = 
X_ k  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } )  |  ( ~P U. ( g `  k
)  e.  y  -> 
y  =  ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) ) } ) `  (
s `  k )
) )
142133, 141eqeq12d 2372 . . . . . . . . . . 11  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  -> 
( ( ( cls `  ( Xt_ `  f
) ) `  X_ k  e.  dom  f ( s `
 k ) )  =  X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
)  <->  ( ( cls `  ( Xt_ `  (
x  e.  dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  |  ( ~P U. ( g `  x
)  e.  y  -> 
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) ) } ) ) ) `
 X_ k  e.  dom  g ( s `  k ) )  = 
X_ k  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } )  |  ( ~P U. ( g `  k
)  e.  y  -> 
y  =  ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) ) } ) `  (
s `  k )
) ) )
143128, 142raleqbidv 2824 . . . . . . . . . 10  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  -> 
( A. s  e.  X_  k  e.  dom  f ~P U. ( f `
 k ) ( ( cls `  ( Xt_ `  f ) ) `
 X_ k  e.  dom  f ( s `  k ) )  = 
X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
)  <->  A. s  e.  X_  k  e.  dom  g ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ( ( cls `  ( Xt_ `  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) ) ) `  X_ k  e.  dom  g ( s `
 k ) )  =  X_ k  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } )  |  ( ~P U. ( g `  k
)  e.  y  -> 
y  =  ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) ) } ) `  (
s `  k )
) ) )
14494, 143imbi12d 311 . . . . . . . . 9  |-  ( f  =  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )  -> 
( ( f : dom  f --> Top  ->  A. s  e.  X_  k  e.  dom  f ~P U. ( f `  k
) ( ( cls `  ( Xt_ `  f
) ) `  X_ k  e.  dom  f ( s `
 k ) )  =  X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
) )  <->  ( (
x  e.  dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  |  ( ~P U. ( g `  x
)  e.  y  -> 
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) ) } ) : dom  g
--> Top  ->  A. s  e.  X_  k  e.  dom  g ~P ( ( g `
 k )  u. 
{ ~P U. (
g `  k ) } ) ( ( cls `  ( Xt_ `  ( x  e.  dom  g  |->  { y  e. 
~P ( ( g `
 x )  u. 
{ ~P U. (
g `  x ) } )  |  ( ~P U. ( g `
 x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) ) ) `  X_ k  e.  dom  g ( s `
 k ) )  =  X_ k  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } )  |  ( ~P U. ( g `  k
)  e.  y  -> 
y  =  ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) ) } ) `  (
s `  k )
) ) ) )
14587, 144spcv 2950 . . . . . . . 8  |-  ( A. f ( f : dom  f --> Top  ->  A. s  e.  X_  k  e.  dom  f ~P U. ( f `  k
) ( ( cls `  ( Xt_ `  f
) ) `  X_ k  e.  dom  f ( s `
 k ) )  =  X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
) )  ->  (
( x  e.  dom  g  |->  { y  e. 
~P ( ( g `
 x )  u. 
{ ~P U. (
g `  x ) } )  |  ( ~P U. ( g `
 x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) : dom  g --> Top  ->  A. s  e.  X_  k  e.  dom  g ~P (
( g `  k
)  u.  { ~P U. ( g `  k
) } ) ( ( cls `  ( Xt_ `  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) ) ) `  X_ k  e.  dom  g ( s `
 k ) )  =  X_ k  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } )  |  ( ~P U. ( g `  k
)  e.  y  -> 
y  =  ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) ) } ) `  (
s `  k )
) ) )
14673, 86, 145sylc 56 . . . . . . 7  |-  ( ( A. f ( f : dom  f --> Top 
->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  ->  A. s  e.  X_  k  e.  dom  g ~P ( ( g `
 k )  u. 
{ ~P U. (
g `  k ) } ) ( ( cls `  ( Xt_ `  ( x  e.  dom  g  |->  { y  e. 
~P ( ( g `
 x )  u. 
{ ~P U. (
g `  x ) } )  |  ( ~P U. ( g `
 x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) ) ) `  X_ k  e.  dom  g ( s `
 k ) )  =  X_ k  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } )  |  ( ~P U. ( g `  k
)  e.  y  -> 
y  =  ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) ) } ) `  (
s `  k )
) )
147 fveq1 5607 . . . . . . . . . . . . 13  |-  ( s  =  g  ->  (
s `  k )  =  ( g `  k ) )
148147ralrimivw 2703 . . . . . . . . . . . 12  |-  ( s  =  g  ->  A. k  e.  dom  g ( s `
 k )  =  ( g `  k
) )
149 ixpeq2 6918 . . . . . . . . . . . 12  |-  ( A. k  e.  dom  g ( s `  k )  =  ( g `  k )  ->  X_ k  e.  dom  g ( s `
 k )  = 
X_ k  e.  dom  g ( g `  k ) )
150148, 149syl 15 . . . . . . . . . . 11  |-  ( s  =  g  ->  X_ k  e.  dom  g ( s `
 k )  = 
X_ k  e.  dom  g ( g `  k ) )
151 fveq2 5608 . . . . . . . . . . . 12  |-  ( k  =  x  ->  (
g `  k )  =  ( g `  x ) )
152151cbvixpv 6922 . . . . . . . . . . 11  |-  X_ k  e.  dom  g ( g `
 k )  = 
X_ x  e.  dom  g ( g `  x )
153150, 152syl6eq 2406 . . . . . . . . . 10  |-  ( s  =  g  ->  X_ k  e.  dom  g ( s `
 k )  = 
X_ x  e.  dom  g ( g `  x ) )
154153fveq2d 5612 . . . . . . . . 9  |-  ( s  =  g  ->  (
( cls `  ( Xt_ `  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) ) ) `  X_ k  e.  dom  g ( s `
 k ) )  =  ( ( cls `  ( Xt_ `  (
x  e.  dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  |  ( ~P U. ( g `  x
)  e.  y  -> 
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) ) } ) ) ) `
 X_ x  e.  dom  g ( g `  x ) ) )
155147fveq2d 5612 . . . . . . . . . . . 12  |-  ( s  =  g  ->  (
( cls `  {
y  e.  ~P (
( g `  k
)  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( s `  k
) )  =  ( ( cls `  {
y  e.  ~P (
( g `  k
)  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( g `  k
) ) )
156155ralrimivw 2703 . . . . . . . . . . 11  |-  ( s  =  g  ->  A. k  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( s `  k
) )  =  ( ( cls `  {
y  e.  ~P (
( g `  k
)  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( g `  k
) ) )
157 ixpeq2 6918 . . . . . . . . . . 11  |-  ( A. k  e.  dom  g ( ( cls `  {
y  e.  ~P (
( g `  k
)  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( s `  k
) )  =  ( ( cls `  {
y  e.  ~P (
( g `  k
)  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( g `  k
) )  ->  X_ k  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( s `  k
) )  =  X_ k  e.  dom  g ( ( cls `  {
y  e.  ~P (
( g `  k
)  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( g `  k
) ) )
158156, 157syl 15 . . . . . . . . . 10  |-  ( s  =  g  ->  X_ k  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( s `  k
) )  =  X_ k  e.  dom  g ( ( cls `  {
y  e.  ~P (
( g `  k
)  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( g `  k
) ) )
159151unieqd 3919 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  x  ->  U. (
g `  k )  =  U. ( g `  x ) )
160159pweqd 3706 . . . . . . . . . . . . . . . . 17  |-  ( k  =  x  ->  ~P U. ( g `  k
)  =  ~P U. ( g `  x
) )
161160sneqd 3729 . . . . . . . . . . . . . . . 16  |-  ( k  =  x  ->  { ~P U. ( g `  k
) }  =  { ~P U. ( g `  x ) } )
162151, 161uneq12d 3406 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
( g `  k
)  u.  { ~P U. ( g `  k
) } )  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) )
163162pweqd 3706 . . . . . . . . . . . . . 14  |-  ( k  =  x  ->  ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } )  =  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) )
164160eleq1d 2424 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  ( ~P U. ( g `  k )  e.  y  <->  ~P U. ( g `  x )  e.  y ) )
165162eqeq2d 2369 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
y  =  ( ( g `  k )  u.  { ~P U. ( g `  k
) } )  <->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) )
166164, 165imbi12d 311 . . . . . . . . . . . . . 14  |-  ( k  =  x  ->  (
( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) )  <->  ( ~P U. ( g `  x
)  e.  y  -> 
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) ) ) )
167163, 166rabeqbidv 2859 . . . . . . . . . . . . 13  |-  ( k  =  x  ->  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) }  =  {
y  e.  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } )
168167fveq2d 5612 . . . . . . . . . . . 12  |-  ( k  =  x  ->  ( cls `  { y  e. 
~P ( ( g `
 k )  u. 
{ ~P U. (
g `  k ) } )  |  ( ~P U. ( g `
 k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } )  =  ( cls `  {
y  e.  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) )
169168, 151fveq12d 5614 . . . . . . . . . . 11  |-  ( k  =  x  ->  (
( cls `  {
y  e.  ~P (
( g `  k
)  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( g `  k
) )  =  ( ( cls `  {
y  e.  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) `  ( g `  x
) ) )
170169cbvixpv 6922 . . . . . . . . . 10  |-  X_ k  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( g `  k
) )  =  X_ x  e.  dom  g ( ( cls `  {
y  e.  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) `  ( g `  x
) )
171158, 170syl6eq 2406 . . . . . . . . 9  |-  ( s  =  g  ->  X_ k  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k
) } )  |  ( ~P U. (
g `  k )  e.  y  ->  y  =  ( ( g `  k )  u.  { ~P U. ( g `  k ) } ) ) } ) `  ( s `  k
) )  =  X_ x  e.  dom  g ( ( cls `  {
y  e.  ~P (
( g `  x
)  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) `  ( g `  x
) ) )
172154, 171eqeq12d 2372 . . . . . . . 8  |-  ( s  =  g  ->  (
( ( cls `  ( Xt_ `  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) ) ) `  X_ k  e.  dom  g ( s `
 k ) )  =  X_ k  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } )  |  ( ~P U. ( g `  k
)  e.  y  -> 
y  =  ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) ) } ) `  (
s `  k )
)  <->  ( ( cls `  ( Xt_ `  (
x  e.  dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  |  ( ~P U. ( g `  x
)  e.  y  -> 
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) ) } ) ) ) `
 X_ x  e.  dom  g ( g `  x ) )  = 
X_ x  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  |  ( ~P U. ( g `  x
)  e.  y  -> 
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) ) } ) `  (
g `  x )
) ) )
173172rspcv 2956 . . . . . . 7  |-  ( g  e.  X_ k  e.  dom  g ~P ( ( g `
 k )  u. 
{ ~P U. (
g `  k ) } )  ->  ( A. s  e.  X_  k  e.  dom  g ~P (
( g `  k
)  u.  { ~P U. ( g `  k
) } ) ( ( cls `  ( Xt_ `  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) ) ) `  X_ k  e.  dom  g ( s `
 k ) )  =  X_ k  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  k )  u.  { ~P U. ( g `  k ) } )  |  ( ~P U. ( g `  k
)  e.  y  -> 
y  =  ( ( g `  k )  u.  { ~P U. ( g `  k
) } ) ) } ) `  (
s `  k )
)  ->  ( ( cls `  ( Xt_ `  (
x  e.  dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  |  ( ~P U. ( g `  x
)  e.  y  -> 
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) ) } ) ) ) `
 X_ x  e.  dom  g ( g `  x ) )  = 
X_ x  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  |  ( ~P U. ( g `  x
)  e.  y  -> 
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) ) } ) `  (
g `  x )
) ) )
17472, 146, 173sylc 56 . . . . . 6  |-  ( ( A. f ( f : dom  f --> Top 
->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  ->  (
( cls `  ( Xt_ `  ( x  e. 
dom  g  |->  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x
) } )  |  ( ~P U. (
g `  x )  e.  y  ->  y  =  ( ( g `  x )  u.  { ~P U. ( g `  x ) } ) ) } ) ) ) `  X_ x  e.  dom  g ( g `
 x ) )  =  X_ x  e.  dom  g ( ( cls `  { y  e.  ~P ( ( g `  x )  u.  { ~P U. ( g `  x ) } )  |  ( ~P U. ( g `  x
)  e.  y  -> 
y  =  ( ( g `  x )  u.  { ~P U. ( g `  x
) } ) ) } ) `  (
g `  x )
) )
17543, 45, 58, 59, 60, 61, 174dfac14lem 17417 . . . . 5  |-  ( ( A. f ( f : dom  f --> Top 
->  A. s  e.  X_  k  e.  dom  f ~P
U. ( f `  k ) ( ( cls `  ( Xt_ `  f ) ) `  X_ k  e.  dom  f
( s `  k
) )  =  X_ k  e.  dom  f ( ( cls `  (
f `  k )
) `  ( s `  k ) ) )  /\  ( Fun  g  /\  (/)  e/  ran  g
) )  ->  X_ x  e.  dom  g ( g `
 x )  =/=  (/) )
176175ex 423 . . . 4  |-  ( A. f ( f : dom  f --> Top  ->  A. s  e.  X_  k  e.  dom  f ~P U. ( f `  k
) ( ( cls `  ( Xt_ `  f
) ) `  X_ k  e.  dom  f ( s `
 k ) )  =  X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
) )  ->  (
( Fun  g  /\  (/) 
e/  ran  g )  -> 
X_ x  e.  dom  g ( g `  x )  =/=  (/) ) )
177176alrimiv 1631 . . 3  |-  ( A. f ( f : dom  f --> Top  ->  A. s  e.  X_  k  e.  dom  f ~P U. ( f `  k
) ( ( cls `  ( Xt_ `  f
) ) `  X_ k  e.  dom  f ( s `
 k ) )  =  X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
) )  ->  A. g
( ( Fun  g  /\  (/)  e/  ran  g
)  ->  X_ x  e. 
dom  g ( g `
 x )  =/=  (/) ) )
178 dfac9 7852 . . 3  |-  (CHOICE  <->  A. g
( ( Fun  g  /\  (/)  e/  ran  g
)  ->  X_ x  e. 
dom  g ( g `
 x )  =/=  (/) ) )
179177, 178sylibr 203 . 2  |-  ( A. f ( f : dom  f --> Top  ->  A. s  e.  X_  k  e.  dom  f ~P U. ( f `  k
) ( ( cls `  ( Xt_ `  f
) ) `  X_ k  e.  dom  f ( s `
 k ) )  =  X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
) )  -> CHOICE )
18040, 179impbii 180 1  |-  (CHOICE  <->  A. f
( f : dom  f
--> Top  ->  A. s  e.  X_  k  e.  dom  f ~P U. ( f `
 k ) ( ( cls `  ( Xt_ `  f ) ) `
 X_ k  e.  dom  f ( s `  k ) )  = 
X_ k  e.  dom  f ( ( cls `  ( f `  k
) ) `  (
s `  k )
) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1540    = wceq 1642    e. wcel 1710    =/= wne 2521    e/ wnel 2522   A.wral 2619   {crab 2623   _Vcvv 2864    u. cun 3226    C_ wss 3228   (/)c0 3531   ~Pcpw 3701   {csn 3716   U.cuni 3908   U_ciun 3986    e. cmpt 4158   dom cdm 4771   ran crn 4772   Fun wfun 5331    Fn wfn 5332   -->wf 5333   -onto->wfo 5335   ` cfv 5337   X_cixp 6905  AC wacn 7661  CHOICEwac 7832   Xt_cpt 13442   Topctop 16737  TopOnctopon 16738   clsccl 16861
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4212  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-reu 2626  df-rmo 2627  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3909  df-int 3944  df-iun 3988  df-iin 3989  df-br 4105  df-opab 4159  df-mpt 4160  df-tr 4195  df-eprel 4387  df-id 4391  df-po 4396  df-so 4397  df-fr 4434  df-se 4435  df-we 4436  df-ord 4477  df-on 4478  df-lim 4479  df-suc 4480  df-om 4739  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-isom 5346  df-ov 5948  df-oprab 5949  df-mpt2 5950  df-1st 6209  df-2nd 6210  df-riota 6391  df-recs 6475  df-rdg 6510  df-1o 6566  df-oadd 6570  df-er 6747  df-map 6862  df-ixp 6906  df-en 6952  df-dom 6953  df-fin 6955  df-fi 7255  df-card 7662  df-acn 7665  df-ac 7833  df-topgen 13443  df-pt 13444  df-top 16742  df-bases 16744  df-topon 16745  df-cld 16862  df-ntr 16863  df-cls 16864
  Copyright terms: Public domain W3C validator