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 ffvelrnda 
 |-  ( ( ( ( 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 simpr 
 |-  ( ( ( 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 ) )
19 18 5 sylibr 
 |-  ( ( ( 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 ) )
20 vex 
 |-  s e. _V
21 20 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 ) ) )
22 21 simprbi 
 |-  ( s e. X_ k e. dom f ~P U. ( f ` k ) -> A. k e. dom f ( s ` k ) e. ~P U. ( f ` k ) )
23 19 22 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 ) )
24 23 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 ) )
25 24 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 ) )
26 fvex 
 |-  ( s ` k ) e. _V
27 13 26 iunex 
 |-  U_ k e. dom f ( s ` k ) e. _V
28 simpll 
 |-  ( ( ( CHOICE /\ f : dom f --> Top ) /\ s e. X_ x e. dom f ~P U. ( f ` x ) ) -> CHOICE )
29 acacni 
 |-  ( ( CHOICE /\ dom f e. _V ) -> AC_ dom f = _V )
30 28 13 29 sylancl 
 |-  ( ( ( CHOICE /\ f : dom f --> Top ) /\ s e. X_ x e. dom f ~P U. ( f ` x ) ) -> AC_ dom f = _V )
31 27 30 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 )
32 11 14 17 25 31 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 ) ) )
33 10 32 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 ) ) )
34 5 33 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 ) ) )
35 34 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 ) ) )
36 35 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 ) ) ) )
37 36 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 ) ) ) )
38 vex 
 |-  g e. _V
39 38 dmex 
 |-  dom g e. _V
40 39 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 )
41 fvex 
 |-  ( g ` x ) e. _V
42 41 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 )
43 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 )
44 df-nel 
 |-  ( (/) e/ ran g <-> -. (/) e. ran g )
45 43 44 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 )
46 funforn 
 |-  ( Fun g <-> g : dom g -onto-> ran g )
47 fof 
 |-  ( g : dom g -onto-> ran g -> g : dom g --> ran g )
48 46 47 sylbi 
 |-  ( Fun g -> g : dom g --> ran g )
49 48 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 )
50 49 ffvelrnda 
 |-  ( ( ( 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 )
51 eleq1 
 |-  ( ( g ` x ) = (/) -> ( ( g ` x ) e. ran g <-> (/) e. ran g ) )
52 50 51 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 ) )
53 52 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 ) =/= (/) ) )
54 45 53 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 ) =/= (/) )
55 eqid 
 |-  ~P U. ( g ` x ) = ~P U. ( g ` x )
56 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 ) } ) ) }
57 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 ) } ) ) } ) )
58 fveq1 
 |-  ( s = g -> ( s ` k ) = ( g ` k ) )
59 58 ixpeq2dv 
 |-  ( s = g -> X_ k e. dom g ( s ` k ) = X_ k e. dom g ( g ` k ) )
60 fveq2 
 |-  ( k = x -> ( g ` k ) = ( g ` x ) )
61 60 cbvixpv 
 |-  X_ k e. dom g ( g ` k ) = X_ x e. dom g ( g ` x )
62 59 61 eqtrdi 
 |-  ( s = g -> X_ k e. dom g ( s ` k ) = X_ x e. dom g ( g ` x ) )
63 62 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 ) ) )
64 58 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 ) ) )
65 64 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 ) ) )
66 60 unieqd 
 |-  ( k = x -> U. ( g ` k ) = U. ( g ` x ) )
67 66 pweqd 
 |-  ( k = x -> ~P U. ( g ` k ) = ~P U. ( g ` x ) )
68 67 sneqd 
 |-  ( k = x -> { ~P U. ( g ` k ) } = { ~P U. ( g ` x ) } )
69 60 68 uneq12d 
 |-  ( k = x -> ( ( g ` k ) u. { ~P U. ( g ` k ) } ) = ( ( g ` x ) u. { ~P U. ( g ` x ) } ) )
70 69 pweqd 
 |-  ( k = x -> ~P ( ( g ` k ) u. { ~P U. ( g ` k ) } ) = ~P ( ( g ` x ) u. { ~P U. ( g ` x ) } ) )
71 67 eleq1d 
 |-  ( k = x -> ( ~P U. ( g ` k ) e. y <-> ~P U. ( g ` x ) e. y ) )
72 69 eqeq2d 
 |-  ( k = x -> ( y = ( ( g ` k ) u. { ~P U. ( g ` k ) } ) <-> y = ( ( g ` x ) u. { ~P U. ( g ` x ) } ) ) )
73 71 72 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 ) } ) ) ) )
74 70 73 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 ) } ) ) } )
75 74 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 ) } ) ) } ) )
76 75 60 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 ) ) )
77 76 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 ) )
78 65 77 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 ) ) )
79 63 78 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 ) ) ) )
80 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 ) ) ) )
81 snex 
 |-  { ~P U. ( g ` x ) } e. _V
82 41 81 unex 
 |-  ( ( g ` x ) u. { ~P U. ( g ` x ) } ) e. _V
83 ssun2 
 |-  { ~P U. ( g ` x ) } C_ ( ( g ` x ) u. { ~P U. ( g ` x ) } )
84 41 uniex 
 |-  U. ( g ` x ) e. _V
85 84 pwex 
 |-  ~P U. ( g ` x ) e. _V
86 85 snid 
 |-  ~P U. ( g ` x ) e. { ~P U. ( g ` x ) }
87 83 86 sselii 
 |-  ~P U. ( g ` x ) e. ( ( g ` x ) u. { ~P U. ( g ` x ) } )
88 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 ) } ) ) )
89 82 87 88 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 ) } ) )
90 89 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
91 90 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 )
92 91 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 )
93 39 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
94 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 ) } ) ) } ) )
95 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 ) } ) ) } ) )
96 82 pwex 
 |-  ~P ( ( g ` x ) u. { ~P U. ( g ` x ) } ) e. _V
97 96 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
98 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 ) } ) ) } )
99 97 98 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
100 95 99 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 )
101 94 100 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 ) )
102 100 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 ) )
103 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 ) )
104 fveq2 
 |-  ( x = k -> ( g ` x ) = ( g ` k ) )
105 104 unieqd 
 |-  ( x = k -> U. ( g ` x ) = U. ( g ` k ) )
106 105 pweqd 
 |-  ( x = k -> ~P U. ( g ` x ) = ~P U. ( g ` k ) )
107 106 sneqd 
 |-  ( x = k -> { ~P U. ( g ` x ) } = { ~P U. ( g ` k ) } )
108 104 107 uneq12d 
 |-  ( x = k -> ( ( g ` x ) u. { ~P U. ( g ` x ) } ) = ( ( g ` k ) u. { ~P U. ( g ` k ) } ) )
109 108 pweqd 
 |-  ( x = k -> ~P ( ( g ` x ) u. { ~P U. ( g ` x ) } ) = ~P ( ( g ` k ) u. { ~P U. ( g ` k ) } ) )
110 106 eleq1d 
 |-  ( x = k -> ( ~P U. ( g ` x ) e. y <-> ~P U. ( g ` k ) e. y ) )
111 108 eqeq2d 
 |-  ( x = k -> ( y = ( ( g ` x ) u. { ~P U. ( g ` x ) } ) <-> y = ( ( g ` k ) u. { ~P U. ( g ` k ) } ) ) )
112 110 111 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 ) } ) ) ) )
113 109 112 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 ) } ) ) } )
114 fvex 
 |-  ( g ` k ) e. _V
115 snex 
 |-  { ~P U. ( g ` k ) } e. _V
116 114 115 unex 
 |-  ( ( g ` k ) u. { ~P U. ( g ` k ) } ) e. _V
117 116 pwex 
 |-  ~P ( ( g ` k ) u. { ~P U. ( g ` k ) } ) e. _V
118 117 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
119 113 98 118 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 ) } ) ) } )
120 103 119 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 ) } ) ) } )
121 120 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 ) } ) ) } )
122 ssun2 
 |-  { ~P U. ( g ` k ) } C_ ( ( g ` k ) u. { ~P U. ( g ` k ) } )
123 114 uniex 
 |-  U. ( g ` k ) e. _V
124 123 pwex 
 |-  ~P U. ( g ` k ) e. _V
125 124 snid 
 |-  ~P U. ( g ` k ) e. { ~P U. ( g ` k ) }
126 122 125 sselii 
 |-  ~P U. ( g ` k ) e. ( ( g ` k ) u. { ~P U. ( g ` k ) } )
127 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 ) } ) ) )
128 116 126 127 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 ) } ) )
129 128 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 ) } ) ) }
130 121 129 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 ) } ) )
131 130 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 ) } ) )
132 131 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 ) } ) )
133 102 132 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 ) } ) )
134 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 ) } ) ) } ) ) ) )
135 100 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 ) )
136 134 135 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 ) ) )
137 100 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 ) ) )
138 120 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 ) } ) ) } ) )
139 138 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 ) ) )
140 139 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 ) ) )
141 137 140 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 ) ) )
142 136 141 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 ) ) ) )
143 133 142 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 ) ) ) )
144 101 143 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 ) ) ) ) )
145 93 144 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 ) ) ) )
146 80 92 145 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 ) ) )
147 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 )
148 147 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 )
149 ssun1 
 |-  ( g ` k ) C_ ( ( g ` k ) u. { ~P U. ( g ` k ) } )
150 114 elpw 
 |-  ( ( g ` k ) e. ~P ( ( g ` k ) u. { ~P U. ( g ` k ) } ) <-> ( g ` k ) C_ ( ( g ` k ) u. { ~P U. ( g ` k ) } ) )
151 149 150 mpbir 
 |-  ( g ` k ) e. ~P ( ( g ` k ) u. { ~P U. ( g ` k ) } )
152 151 rgenw 
 |-  A. k e. dom g ( g ` k ) e. ~P ( ( g ` k ) u. { ~P U. ( g ` k ) } )
153 38 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 ) } ) ) )
154 148 152 153 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 ) } ) )
155 79 146 154 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 ) ) )
156 40 42 54 55 56 57 155 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 ) =/= (/) )
157 156 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 ) =/= (/) ) )
158 157 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 ) =/= (/) ) )
159 dfac9 
 |-  ( CHOICE <-> A. g ( ( Fun g /\ (/) e/ ran g ) -> X_ x e. dom g ( g ` x ) =/= (/) ) )
160 158 159 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 )
161 37 160 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 ) ) ) )