Metamath Proof Explorer

Theorem tmdgsum2

Description: For any neighborhood U of n X , there is a neighborhood u of X such that any sum of n elements in u sums to an element of U . (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Hypotheses tmdgsum.j 
|- J = ( TopOpen ` G )
tmdgsum.b 
|- B = ( Base ` G )
tmdgsum2.t 
|- .x. = ( .g ` G )
tmdgsum2.1 
|- ( ph -> G e. CMnd )
tmdgsum2.2 
|- ( ph -> G e. TopMnd )
tmdgsum2.a 
|- ( ph -> A e. Fin )
tmdgsum2.u 
|- ( ph -> U e. J )
tmdgsum2.x 
|- ( ph -> X e. B )
tmdgsum2.3 
|- ( ph -> ( ( # ` A ) .x. X ) e. U )
Assertion tmdgsum2 
|- ( ph -> E. u e. J ( X e. u /\ A. f e. ( u ^m A ) ( G gsum f ) e. U ) )

Proof

Step Hyp Ref Expression
1 tmdgsum.j 
 |-  J = ( TopOpen ` G )
2 tmdgsum.b 
 |-  B = ( Base ` G )
3 tmdgsum2.t 
 |-  .x. = ( .g ` G )
4 tmdgsum2.1 
 |-  ( ph -> G e. CMnd )
5 tmdgsum2.2 
 |-  ( ph -> G e. TopMnd )
6 tmdgsum2.a 
 |-  ( ph -> A e. Fin )
7 tmdgsum2.u 
 |-  ( ph -> U e. J )
8 tmdgsum2.x 
 |-  ( ph -> X e. B )
9 tmdgsum2.3 
 |-  ( ph -> ( ( # ` A ) .x. X ) e. U )
10 eqid 
 |-  ( f e. ( B ^m A ) |-> ( G gsum f ) ) = ( f e. ( B ^m A ) |-> ( G gsum f ) )
11 10 mptpreima 
 |-  ( `' ( f e. ( B ^m A ) |-> ( G gsum f ) ) " U ) = { f e. ( B ^m A ) | ( G gsum f ) e. U }
12 1 2 tmdgsum 
 |-  ( ( G e. CMnd /\ G e. TopMnd /\ A e. Fin ) -> ( f e. ( B ^m A ) |-> ( G gsum f ) ) e. ( ( J ^ko ~P A ) Cn J ) )
13 4 5 6 12 syl3anc 
 |-  ( ph -> ( f e. ( B ^m A ) |-> ( G gsum f ) ) e. ( ( J ^ko ~P A ) Cn J ) )
14 cnima 
 |-  ( ( ( f e. ( B ^m A ) |-> ( G gsum f ) ) e. ( ( J ^ko ~P A ) Cn J ) /\ U e. J ) -> ( `' ( f e. ( B ^m A ) |-> ( G gsum f ) ) " U ) e. ( J ^ko ~P A ) )
15 13 7 14 syl2anc 
 |-  ( ph -> ( `' ( f e. ( B ^m A ) |-> ( G gsum f ) ) " U ) e. ( J ^ko ~P A ) )
16 11 15 eqeltrrid 
 |-  ( ph -> { f e. ( B ^m A ) | ( G gsum f ) e. U } e. ( J ^ko ~P A ) )
17 1 2 tmdtopon 
 |-  ( G e. TopMnd -> J e. ( TopOn ` B ) )
18 topontop 
 |-  ( J e. ( TopOn ` B ) -> J e. Top )
19 5 17 18 3syl 
 |-  ( ph -> J e. Top )
20 xkopt 
 |-  ( ( J e. Top /\ A e. Fin ) -> ( J ^ko ~P A ) = ( Xt_ ` ( A X. { J } ) ) )
21 19 6 20 syl2anc 
 |-  ( ph -> ( J ^ko ~P A ) = ( Xt_ ` ( A X. { J } ) ) )
22 fnconstg 
 |-  ( J e. ( TopOn ` B ) -> ( A X. { J } ) Fn A )
23 5 17 22 3syl 
 |-  ( ph -> ( A X. { J } ) Fn A )
24 eqid 
 |-  { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }
25 24 ptval 
 |-  ( ( A e. Fin /\ ( A X. { J } ) Fn A ) -> ( Xt_ ` ( A X. { J } ) ) = ( topGen ` { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ) )
26 6 23 25 syl2anc 
 |-  ( ph -> ( Xt_ ` ( A X. { J } ) ) = ( topGen ` { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ) )
27 21 26 eqtrd 
 |-  ( ph -> ( J ^ko ~P A ) = ( topGen ` { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ) )
28 16 27 eleqtrd 
 |-  ( ph -> { f e. ( B ^m A ) | ( G gsum f ) e. U } e. ( topGen ` { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ) )
29 oveq2 
 |-  ( f = ( A X. { X } ) -> ( G gsum f ) = ( G gsum ( A X. { X } ) ) )
30 29 eleq1d 
 |-  ( f = ( A X. { X } ) -> ( ( G gsum f ) e. U <-> ( G gsum ( A X. { X } ) ) e. U ) )
31 fconst6g 
 |-  ( X e. B -> ( A X. { X } ) : A --> B )
32 8 31 syl 
 |-  ( ph -> ( A X. { X } ) : A --> B )
33 2 fvexi 
 |-  B e. _V
34 elmapg 
 |-  ( ( B e. _V /\ A e. Fin ) -> ( ( A X. { X } ) e. ( B ^m A ) <-> ( A X. { X } ) : A --> B ) )
35 33 6 34 sylancr 
 |-  ( ph -> ( ( A X. { X } ) e. ( B ^m A ) <-> ( A X. { X } ) : A --> B ) )
36 32 35 mpbird 
 |-  ( ph -> ( A X. { X } ) e. ( B ^m A ) )
37 fconstmpt 
 |-  ( A X. { X } ) = ( k e. A |-> X )
38 37 oveq2i 
 |-  ( G gsum ( A X. { X } ) ) = ( G gsum ( k e. A |-> X ) )
39 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
40 4 39 syl 
 |-  ( ph -> G e. Mnd )
41 2 3 gsumconst 
 |-  ( ( G e. Mnd /\ A e. Fin /\ X e. B ) -> ( G gsum ( k e. A |-> X ) ) = ( ( # ` A ) .x. X ) )
42 40 6 8 41 syl3anc 
 |-  ( ph -> ( G gsum ( k e. A |-> X ) ) = ( ( # ` A ) .x. X ) )
43 38 42 eqtrid 
 |-  ( ph -> ( G gsum ( A X. { X } ) ) = ( ( # ` A ) .x. X ) )
44 43 9 eqeltrd 
 |-  ( ph -> ( G gsum ( A X. { X } ) ) e. U )
45 30 36 44 elrabd 
 |-  ( ph -> ( A X. { X } ) e. { f e. ( B ^m A ) | ( G gsum f ) e. U } )
46 tg2 
 |-  ( ( { f e. ( B ^m A ) | ( G gsum f ) e. U } e. ( topGen ` { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ) /\ ( A X. { X } ) e. { f e. ( B ^m A ) | ( G gsum f ) e. U } ) -> E. t e. { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ( ( A X. { X } ) e. t /\ t C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) )
47 28 45 46 syl2anc 
 |-  ( ph -> E. t e. { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ( ( A X. { X } ) e. t /\ t C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) )
48 eleq2 
 |-  ( t = x -> ( ( A X. { X } ) e. t <-> ( A X. { X } ) e. x ) )
49 sseq1 
 |-  ( t = x -> ( t C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } <-> x C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) )
50 48 49 anbi12d 
 |-  ( t = x -> ( ( ( A X. { X } ) e. t /\ t C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) <-> ( ( A X. { X } ) e. x /\ x C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) )
51 50 rexab2 
 |-  ( E. t e. { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ( ( A X. { X } ) e. t /\ t C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) <-> E. x ( E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) /\ ( ( A X. { X } ) e. x /\ x C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) )
52 47 51 sylib 
 |-  ( ph -> E. x ( E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) /\ ( ( A X. { X } ) e. x /\ x C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) )
53 toponuni 
 |-  ( J e. ( TopOn ` B ) -> B = U. J )
54 5 17 53 3syl 
 |-  ( ph -> B = U. J )
55 54 ad2antrr 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> B = U. J )
56 55 ineq1d 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> ( B i^i |^| ran g ) = ( U. J i^i |^| ran g ) )
57 19 ad2antrr 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> J e. Top )
58 simplrl 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> g Fn A )
59 simplrr 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) )
60 fvconst2g 
 |-  ( ( J e. Top /\ y e. A ) -> ( ( A X. { J } ) ` y ) = J )
61 60 eleq2d 
 |-  ( ( J e. Top /\ y e. A ) -> ( ( g ` y ) e. ( ( A X. { J } ) ` y ) <-> ( g ` y ) e. J ) )
62 61 ralbidva 
 |-  ( J e. Top -> ( A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) <-> A. y e. A ( g ` y ) e. J ) )
63 57 62 syl 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> ( A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) <-> A. y e. A ( g ` y ) e. J ) )
64 59 63 mpbid 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> A. y e. A ( g ` y ) e. J )
65 ffnfv 
 |-  ( g : A --> J <-> ( g Fn A /\ A. y e. A ( g ` y ) e. J ) )
66 58 64 65 sylanbrc 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> g : A --> J )
67 66 frnd 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> ran g C_ J )
68 6 ad2antrr 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> A e. Fin )
69 dffn4 
 |-  ( g Fn A <-> g : A -onto-> ran g )
70 58 69 sylib 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> g : A -onto-> ran g )
71 fofi 
 |-  ( ( A e. Fin /\ g : A -onto-> ran g ) -> ran g e. Fin )
72 68 70 71 syl2anc 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> ran g e. Fin )
73 eqid 
 |-  U. J = U. J
74 73 rintopn 
 |-  ( ( J e. Top /\ ran g C_ J /\ ran g e. Fin ) -> ( U. J i^i |^| ran g ) e. J )
75 57 67 72 74 syl3anc 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> ( U. J i^i |^| ran g ) e. J )
76 56 75 eqeltrd 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> ( B i^i |^| ran g ) e. J )
77 8 ad2antrr 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> X e. B )
78 fconstmpt 
 |-  ( A X. { X } ) = ( y e. A |-> X )
79 simprl 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> ( A X. { X } ) e. X_ y e. A ( g ` y ) )
80 78 79 eqeltrrid 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> ( y e. A |-> X ) e. X_ y e. A ( g ` y ) )
81 mptelixpg 
 |-  ( A e. Fin -> ( ( y e. A |-> X ) e. X_ y e. A ( g ` y ) <-> A. y e. A X e. ( g ` y ) ) )
82 68 81 syl 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> ( ( y e. A |-> X ) e. X_ y e. A ( g ` y ) <-> A. y e. A X e. ( g ` y ) ) )
83 80 82 mpbid 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> A. y e. A X e. ( g ` y ) )
84 eleq2 
 |-  ( z = ( g ` y ) -> ( X e. z <-> X e. ( g ` y ) ) )
85 84 ralrn 
 |-  ( g Fn A -> ( A. z e. ran g X e. z <-> A. y e. A X e. ( g ` y ) ) )
86 58 85 syl 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> ( A. z e. ran g X e. z <-> A. y e. A X e. ( g ` y ) ) )
87 83 86 mpbird 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> A. z e. ran g X e. z )
88 elrint 
 |-  ( X e. ( B i^i |^| ran g ) <-> ( X e. B /\ A. z e. ran g X e. z ) )
89 77 87 88 sylanbrc 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> X e. ( B i^i |^| ran g ) )
90 33 inex1 
 |-  ( B i^i |^| ran g ) e. _V
91 ixpconstg 
 |-  ( ( A e. Fin /\ ( B i^i |^| ran g ) e. _V ) -> X_ y e. A ( B i^i |^| ran g ) = ( ( B i^i |^| ran g ) ^m A ) )
92 68 90 91 sylancl 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> X_ y e. A ( B i^i |^| ran g ) = ( ( B i^i |^| ran g ) ^m A ) )
93 inss2 
 |-  ( B i^i |^| ran g ) C_ |^| ran g
94 fnfvelrn 
 |-  ( ( g Fn A /\ y e. A ) -> ( g ` y ) e. ran g )
95 intss1 
 |-  ( ( g ` y ) e. ran g -> |^| ran g C_ ( g ` y ) )
96 94 95 syl 
 |-  ( ( g Fn A /\ y e. A ) -> |^| ran g C_ ( g ` y ) )
97 93 96 sstrid 
 |-  ( ( g Fn A /\ y e. A ) -> ( B i^i |^| ran g ) C_ ( g ` y ) )
98 97 ralrimiva 
 |-  ( g Fn A -> A. y e. A ( B i^i |^| ran g ) C_ ( g ` y ) )
99 ss2ixp 
 |-  ( A. y e. A ( B i^i |^| ran g ) C_ ( g ` y ) -> X_ y e. A ( B i^i |^| ran g ) C_ X_ y e. A ( g ` y ) )
100 58 98 99 3syl 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> X_ y e. A ( B i^i |^| ran g ) C_ X_ y e. A ( g ` y ) )
101 92 100 eqsstrrd 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> ( ( B i^i |^| ran g ) ^m A ) C_ X_ y e. A ( g ` y ) )
102 ssrab 
 |-  ( X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } <-> ( X_ y e. A ( g ` y ) C_ ( B ^m A ) /\ A. f e. X_ y e. A ( g ` y ) ( G gsum f ) e. U ) )
103 102 simprbi 
 |-  ( X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } -> A. f e. X_ y e. A ( g ` y ) ( G gsum f ) e. U )
104 103 ad2antll 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> A. f e. X_ y e. A ( g ` y ) ( G gsum f ) e. U )
105 ssralv 
 |-  ( ( ( B i^i |^| ran g ) ^m A ) C_ X_ y e. A ( g ` y ) -> ( A. f e. X_ y e. A ( g ` y ) ( G gsum f ) e. U -> A. f e. ( ( B i^i |^| ran g ) ^m A ) ( G gsum f ) e. U ) )
106 101 104 105 sylc 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> A. f e. ( ( B i^i |^| ran g ) ^m A ) ( G gsum f ) e. U )
107 eleq2 
 |-  ( u = ( B i^i |^| ran g ) -> ( X e. u <-> X e. ( B i^i |^| ran g ) ) )
108 oveq1 
 |-  ( u = ( B i^i |^| ran g ) -> ( u ^m A ) = ( ( B i^i |^| ran g ) ^m A ) )
109 108 raleqdv 
 |-  ( u = ( B i^i |^| ran g ) -> ( A. f e. ( u ^m A ) ( G gsum f ) e. U <-> A. f e. ( ( B i^i |^| ran g ) ^m A ) ( G gsum f ) e. U ) )
110 107 109 anbi12d 
 |-  ( u = ( B i^i |^| ran g ) -> ( ( X e. u /\ A. f e. ( u ^m A ) ( G gsum f ) e. U ) <-> ( X e. ( B i^i |^| ran g ) /\ A. f e. ( ( B i^i |^| ran g ) ^m A ) ( G gsum f ) e. U ) ) )
111 110 rspcev 
 |-  ( ( ( B i^i |^| ran g ) e. J /\ ( X e. ( B i^i |^| ran g ) /\ A. f e. ( ( B i^i |^| ran g ) ^m A ) ( G gsum f ) e. U ) ) -> E. u e. J ( X e. u /\ A. f e. ( u ^m A ) ( G gsum f ) e. U ) )
112 76 89 106 111 syl12anc 
 |-  ( ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) /\ ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> E. u e. J ( X e. u /\ A. f e. ( u ^m A ) ( G gsum f ) e. U ) )
113 112 ex 
 |-  ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) ) ) -> ( ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) -> E. u e. J ( X e. u /\ A. f e. ( u ^m A ) ( G gsum f ) e. U ) ) )
114 113 3adantr3 
 |-  ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) ) -> ( ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) -> E. u e. J ( X e. u /\ A. f e. ( u ^m A ) ( G gsum f ) e. U ) ) )
115 eleq2 
 |-  ( x = X_ y e. A ( g ` y ) -> ( ( A X. { X } ) e. x <-> ( A X. { X } ) e. X_ y e. A ( g ` y ) ) )
116 sseq1 
 |-  ( x = X_ y e. A ( g ` y ) -> ( x C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } <-> X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) )
117 115 116 anbi12d 
 |-  ( x = X_ y e. A ( g ` y ) -> ( ( ( A X. { X } ) e. x /\ x C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) <-> ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) )
118 117 imbi1d 
 |-  ( x = X_ y e. A ( g ` y ) -> ( ( ( ( A X. { X } ) e. x /\ x C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) -> E. u e. J ( X e. u /\ A. f e. ( u ^m A ) ( G gsum f ) e. U ) ) <-> ( ( ( A X. { X } ) e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) -> E. u e. J ( X e. u /\ A. f e. ( u ^m A ) ( G gsum f ) e. U ) ) ) )
119 114 118 syl5ibrcom 
 |-  ( ( ph /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) ) -> ( x = X_ y e. A ( g ` y ) -> ( ( ( A X. { X } ) e. x /\ x C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) -> E. u e. J ( X e. u /\ A. f e. ( u ^m A ) ( G gsum f ) e. U ) ) ) )
120 119 expimpd 
 |-  ( ph -> ( ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) -> ( ( ( A X. { X } ) e. x /\ x C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) -> E. u e. J ( X e. u /\ A. f e. ( u ^m A ) ( G gsum f ) e. U ) ) ) )
121 120 exlimdv 
 |-  ( ph -> ( E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) -> ( ( ( A X. { X } ) e. x /\ x C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) -> E. u e. J ( X e. u /\ A. f e. ( u ^m A ) ( G gsum f ) e. U ) ) ) )
122 121 impd 
 |-  ( ph -> ( ( E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) /\ ( ( A X. { X } ) e. x /\ x C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> E. u e. J ( X e. u /\ A. f e. ( u ^m A ) ( G gsum f ) e. U ) ) )
123 122 exlimdv 
 |-  ( ph -> ( E. x ( E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( ( A X. { J } ) ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( ( A X. { J } ) ` y ) ) /\ x = X_ y e. A ( g ` y ) ) /\ ( ( A X. { X } ) e. x /\ x C_ { f e. ( B ^m A ) | ( G gsum f ) e. U } ) ) -> E. u e. J ( X e. u /\ A. f e. ( u ^m A ) ( G gsum f ) e. U ) ) )
124 52 123 mpd 
 |-  ( ph -> E. u e. J ( X e. u /\ A. f e. ( u ^m A ) ( G gsum f ) e. U ) )