Metamath Proof Explorer

Theorem dfac14

Description: Theorem ptcls is an equivalent of the axiom of choice. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( k = x -> ( f ` k ) = ( f ` x ) )
2 1 unieqd 
 |-  ( k = x -> U. ( f ` k ) = U. ( f ` x ) )
3 2 pweqd 
 |-  ( k = x -> ~P U. ( f ` k ) = ~P U. ( f ` x ) )
4 3 cbvixpv 
 |-  X_ k e. dom f ~P U. ( f ` k ) = X_ x e. dom f ~P U. ( f ` x )
5 4 eleq2i 
 |-  ( s e. X_ k e. dom f ~P U. ( f ` k ) <-> s e. X_ x e. dom f ~P U. ( f ` x ) )
6 simplr 
 |-  ( ( ( CHOICE /\ f : dom f --> Top ) /\ s e. X_ x e. dom f ~P U. ( f ` x ) ) -> f : dom f --> Top )
7 6 feqmptd 
 |-  ( ( ( CHOICE /\ f : dom f --> Top ) /\ s e. X_ x e. dom f ~P U. ( f ` x ) ) -> f = ( k e. dom f |-> ( f ` k ) ) )
8 7 fveq2d 
 |-  ( ( ( 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 ) ) ) )
9 8 fveq2d 
 |-  ( ( ( 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 ) ) ) ) )
10 9 fveq1d 
 |-  ( ( ( 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 
 |-  ( Xt_ ` ( k e. dom f |-> ( f ` k ) ) ) = ( Xt_ ` ( k e. dom f |-> ( f ` k ) ) )
12 vex 
 |-  f e. _V
13 12 dmex 
 |-  dom f e. _V
14 13 a1i 
 |-  ( ( ( CHOICE /\ f : dom f --> Top ) /\ s e. X_ x e. dom f ~P U. ( f ` x ) ) -> dom f e. _V )
15 6 ffvelcdmda 
 |-  ( ( ( ( CHOICE /\ f : dom f --> Top ) /\ s e. X_ x e. dom f ~P U. ( f ` x ) ) /\ k e. dom f ) -> ( f ` k ) e. Top )
16 toptopon2 
 |-  ( ( f ` k ) e. Top <-> ( f ` k ) e. ( TopOn ` U. ( f ` k ) ) )
17 15 16 sylib 
 |-  ( ( ( ( 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 ) ) )
18 5 bilanri 
 |-  ( ( ( 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 ) )
19 vex 
 |-  s e. _V
20 19 elixp 
 |-  ( 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 ) ) )
21 20 simprbi 
 |-  ( s e. X_ k e. dom f ~P U. ( f ` k ) -> A. k e. dom f ( s ` k ) e. ~P U. ( f ` k ) )
22 18 21 syl 
 |-  ( ( ( 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 ) )
23 22 r19.21bi 
 |-  ( ( ( ( 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 ) )
24 23 elpwid 
 |-  ( ( ( ( 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 ) )
25 fvex 
 |-  ( s ` k ) e. _V
26 13 25 iunex 
 |-  U_ k e. dom f ( s ` k ) e. _V
27 simpll 
 |-  ( ( ( CHOICE /\ f : dom f --> Top ) /\ s e. X_ x e. dom f ~P U. ( f ` x ) ) -> CHOICE )
28 acacni 
 |-  ( ( CHOICE /\ dom f e. _V ) -> AC_ dom f = _V )
29 27 13 28 sylancl 
 |-  ( ( ( CHOICE /\ f : dom f --> Top ) /\ s e. X_ x e. dom f ~P U. ( f ` x ) ) -> AC_ dom f = _V )
30 26 29 eleqtrrid 
 |-  ( ( ( 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 )
31 11 14 17 24 30 ptclsg 
 |-  ( ( ( 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 ) ) )
32 10 31 eqtrd 
 |-  ( ( ( 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 ) ) )
33 5 32 sylan2b 
 |-  ( ( ( 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 ) ) )
34 33 ralrimiva 
 |-  ( ( 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 ) ) )
35 34 ex 
 |-  ( 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 ) ) ) )
36 35 alrimiv 
 |-  ( 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 ) ) ) )
37 vex 
 |-  g e. _V
38 37 dmex 
 |-  dom g e. _V
39 38 a1i 
 |-  ( ( 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 )
40 fvex 
 |-  ( g ` x ) e. _V
41 40 a1i 
 |-  ( ( ( 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 )
42 simplrr 
 |-  ( ( ( 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 )
43 df-nel 
 |-  ( (/) e/ ran g <-> -. (/) e. ran g )
44 42 43 sylib 
 |-  ( ( ( 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 )
45 funforn 
 |-  ( Fun g <-> g : dom g -onto-> ran g )
46 fof 
 |-  ( g : dom g -onto-> ran g -> g : dom g --> ran g )
47 45 46 sylbi 
 |-  ( Fun g -> g : dom g --> ran g )
48 47 ad2antrl 
 |-  ( ( 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 )
49 48 ffvelcdmda 
 |-  ( ( ( 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 )
50 eleq1 
 |-  ( ( g ` x ) = (/) -> ( ( g ` x ) e. ran g <-> (/) e. ran g ) )
51 49 50 syl5ibcom 
 |-  ( ( ( 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 ) )
52 51 necon3bd 
 |-  ( ( ( 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 ) =/= (/) ) )
53 44 52 mpd 
 |-  ( ( ( 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 ) =/= (/) )
54 eqid 
 |-  ~P U. ( g ` x ) = ~P U. ( g ` x )
55 eqid 
 |-  { 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 ) } ) ) }
56 eqid 
 |-  ( 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 ) } ) ) } ) )
57 fveq1 
 |-  ( s = g -> ( s ` k ) = ( g ` k ) )
58 57 ixpeq2dv 
 |-  ( s = g -> X_ k e. dom g ( s ` k ) = X_ k e. dom g ( g ` k ) )
59 fveq2 
 |-  ( k = x -> ( g ` k ) = ( g ` x ) )
60 59 cbvixpv 
 |-  X_ k e. dom g ( g ` k ) = X_ x e. dom g ( g ` x )
61 58 60 eqtrdi 
 |-  ( s = g -> X_ k e. dom g ( s ` k ) = X_ x e. dom g ( g ` x ) )
62 61 fveq2d 
 |-  ( 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 ) ) )
63 57 fveq2d 
 |-  ( 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 ) ) )
64 63 ixpeq2dv 
 |-  ( 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 ) ) )
65 59 unieqd 
 |-  ( k = x -> U. ( g ` k ) = U. ( g ` x ) )
66 65 pweqd 
 |-  ( k = x -> ~P U. ( g ` k ) = ~P U. ( g ` x ) )
67 66 sneqd 
 |-  ( k = x -> { ~P U. ( g ` k ) } = { ~P U. ( g ` x ) } )
68 59 67 uneq12d 
 |-  ( k = x -> ( ( g ` k ) u. { ~P U. ( g ` k ) } ) = ( ( g ` x ) u. { ~P U. ( g ` x ) } ) )
69 68 pweqd 
 |-  ( k = x -> ~P ( ( g ` k ) u. { ~P U. ( g ` k ) } ) = ~P ( ( g ` x ) u. { ~P U. ( g ` x ) } ) )
70 66 eleq1d 
 |-  ( k = x -> ( ~P U. ( g ` k ) e. y <-> ~P U. ( g ` x ) e. y ) )
71 68 eqeq2d 
 |-  ( k = x -> ( y = ( ( g ` k ) u. { ~P U. ( g ` k ) } ) <-> y = ( ( g ` x ) u. { ~P U. ( g ` x ) } ) ) )
72 70 71 imbi12d 
 |-  ( 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 ) } ) ) ) )
73 69 72 rabeqbidv 
 |-  ( 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 ) } ) ) } )
74 73 fveq2d 
 |-  ( 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 ) } ) ) } ) )
75 74 59 fveq12d 
 |-  ( 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 ) ) )
76 75 cbvixpv 
 |-  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 ) )
77 64 76 eqtrdi 
 |-  ( 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 ) ) )
78 62 77 eqeq12d 
 |-  ( 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 ) ) ) )
79 simpl 
 |-  ( ( 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 ) ) ) )
80 snex 
 |-  { ~P U. ( g ` x ) } e. _V
81 40 80 unex 
 |-  ( ( g ` x ) u. { ~P U. ( g ` x ) } ) e. _V
82 ssun2 
 |-  { ~P U. ( g ` x ) } C_ ( ( g ` x ) u. { ~P U. ( g ` x ) } )
83 40 uniex 
 |-  U. ( g ` x ) e. _V
84 83 pwex 
 |-  ~P U. ( g ` x ) e. _V
85 84 snid 
 |-  ~P U. ( g ` x ) e. { ~P U. ( g ` x ) }
86 82 85 sselii 
 |-  ~P U. ( g ` x ) e. ( ( g ` x ) u. { ~P U. ( g ` x ) } )
87 epttop 
 |-  ( ( ( ( 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 ) } ) ) )
88 81 86 87 mp2an 
 |-  { 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 ) } ) )
89 88 topontopi 
 |-  { 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
90 89 a1i 
 |-  ( ( ( 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 )
91 90 fmpttd 
 |-  ( ( 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 )
92 38 mptex 
 |-  ( 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
93 id 
 |-  ( 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 ) } ) ) } ) )
94 dmeq 
 |-  ( 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 ) } ) ) } ) )
95 81 pwex 
 |-  ~P ( ( g ` x ) u. { ~P U. ( g ` x ) } ) e. _V
96 95 rabex 
 |-  { 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
97 eqid 
 |-  ( 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 ) } ) ) } )
98 96 97 dmmpti 
 |-  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
99 94 98 eqtrdi 
 |-  ( 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 )
100 93 99 feq12d 
 |-  ( 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 ) )
101 99 ixpeq1d 
 |-  ( 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 ) )
102 fveq1 
 |-  ( 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 ) )
103 fveq2 
 |-  ( x = k -> ( g ` x ) = ( g ` k ) )
104 103 unieqd 
 |-  ( x = k -> U. ( g ` x ) = U. ( g ` k ) )
105 104 pweqd 
 |-  ( x = k -> ~P U. ( g ` x ) = ~P U. ( g ` k ) )
106 105 sneqd 
 |-  ( x = k -> { ~P U. ( g ` x ) } = { ~P U. ( g ` k ) } )
107 103 106 uneq12d 
 |-  ( x = k -> ( ( g ` x ) u. { ~P U. ( g ` x ) } ) = ( ( g ` k ) u. { ~P U. ( g ` k ) } ) )
108 107 pweqd 
 |-  ( x = k -> ~P ( ( g ` x ) u. { ~P U. ( g ` x ) } ) = ~P ( ( g ` k ) u. { ~P U. ( g ` k ) } ) )
109 105 eleq1d 
 |-  ( x = k -> ( ~P U. ( g ` x ) e. y <-> ~P U. ( g ` k ) e. y ) )
110 107 eqeq2d 
 |-  ( x = k -> ( y = ( ( g ` x ) u. { ~P U. ( g ` x ) } ) <-> y = ( ( g ` k ) u. { ~P U. ( g ` k ) } ) ) )
111 109 110 imbi12d 
 |-  ( 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 ) } ) ) ) )
112 108 111 rabeqbidv 
 |-  ( 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 ) } ) ) } )
113 fvex 
 |-  ( g ` k ) e. _V
114 snex 
 |-  { ~P U. ( g ` k ) } e. _V
115 113 114 unex 
 |-  ( ( g ` k ) u. { ~P U. ( g ` k ) } ) e. _V
116 115 pwex 
 |-  ~P ( ( g ` k ) u. { ~P U. ( g ` k ) } ) e. _V
117 116 rabex 
 |-  { 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
118 112 97 117 fvmpt 
 |-  ( 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 ) } ) ) } )
119 102 118 sylan9eq 
 |-  ( ( 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 ) } ) ) } )
120 119 unieqd 
 |-  ( ( 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 ) } ) ) } )
121 ssun2 
 |-  { ~P U. ( g ` k ) } C_ ( ( g ` k ) u. { ~P U. ( g ` k ) } )
122 113 uniex 
 |-  U. ( g ` k ) e. _V
123 122 pwex 
 |-  ~P U. ( g ` k ) e. _V
124 123 snid 
 |-  ~P U. ( g ` k ) e. { ~P U. ( g ` k ) }
125 121 124 sselii 
 |-  ~P U. ( g ` k ) e. ( ( g ` k ) u. { ~P U. ( g ` k ) } )
126 epttop 
 |-  ( ( ( ( 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 ) } ) ) )
127 115 125 126 mp2an 
 |-  { 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 ) } ) )
128 127 toponunii 
 |-  ( ( 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 ) } ) ) }
129 120 128 eqtr4di 
 |-  ( ( 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 ) } ) )
130 129 pweqd 
 |-  ( ( 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 ) } ) )
131 130 ixpeq2dva 
 |-  ( 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 ) } ) )
132 101 131 eqtrd 
 |-  ( 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 ) } ) )
133 2fveq3 
 |-  ( 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 ) } ) ) } ) ) ) )
134 99 ixpeq1d 
 |-  ( 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 ) )
135 133 134 fveq12d 
 |-  ( 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 ) ) )
136 99 ixpeq1d 
 |-  ( 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 ) ) )
137 119 fveq2d 
 |-  ( ( 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 ) } ) ) } ) )
138 137 fveq1d 
 |-  ( ( 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 ) ) )
139 138 ixpeq2dva 
 |-  ( 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 ) ) )
140 136 139 eqtrd 
 |-  ( 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 ) ) )
141 135 140 eqeq12d 
 |-  ( 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 ) ) ) )
142 132 141 raleqbidv 
 |-  ( 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 ) ) ) )
143 100 142 imbi12d 
 |-  ( 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 ) ) ) ) )
144 92 143 spcv 
 |-  ( 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 ) ) ) )
145 79 91 144 sylc 
 |-  ( ( 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 ) ) )
146 simprl 
 |-  ( ( 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 )
147 146 funfnd 
 |-  ( ( 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 )
148 ssun1 
 |-  ( g ` k ) C_ ( ( g ` k ) u. { ~P U. ( g ` k ) } )
149 113 elpw 
 |-  ( ( g ` k ) e. ~P ( ( g ` k ) u. { ~P U. ( g ` k ) } ) <-> ( g ` k ) C_ ( ( g ` k ) u. { ~P U. ( g ` k ) } ) )
150 148 149 mpbir 
 |-  ( g ` k ) e. ~P ( ( g ` k ) u. { ~P U. ( g ` k ) } )
151 150 rgenw 
 |-  A. k e. dom g ( g ` k ) e. ~P ( ( g ` k ) u. { ~P U. ( g ` k ) } )
152 37 elixp 
 |-  ( 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 ) } ) ) )
153 147 151 152 sylanblrc 
 |-  ( ( 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 ) } ) )
154 78 145 153 rspcdva 
 |-  ( ( 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 ) ) )
155 39 41 53 54 55 56 154 dfac14lem 
 |-  ( ( 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 ) =/= (/) )
156 155 ex 
 |-  ( 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 ) =/= (/) ) )
157 156 alrimiv 
 |-  ( 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 ) =/= (/) ) )
158 dfac9 
 |-  ( CHOICE <-> A. g ( ( Fun g /\ (/) e/ ran g ) -> X_ x e. dom g ( g ` x ) =/= (/) ) )
159 157 158 sylibr 
 |-  ( 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 )
160 36 159 impbii 
 |-  ( 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 ) ) ) )