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

Theorem alexsubALTlem3 17743
Description: Lemma for alexsubALT 17745. If a point is covered by a collection taken from the base with no finite subcover, a set from the subbase can be added that covers the point so that the resulting collection has no finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.)
Hypothesis
Ref Expression
alexsubALT.1  |-  X  = 
U. J
Assertion
Ref Expression
alexsubALTlem3  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  ( a  C_  u  /\  A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b ) ) )  /\  w  e.  u
)  /\  ( (
t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) ) )  ->  E. s  e.  t  A. n  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  -.  X  =  U. n )
Distinct variable groups:    a, b,
c, d, n, s, t, u, w, x, y, J    X, a,
b, c, d, n, s, t, u, w, x, y

Proof of Theorem alexsubALTlem3
Dummy variables  f  m  v  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfrex2 2556 . . . . . . . . . . 11  |-  ( E. n  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin ) X  = 
U. n  <->  -.  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n )
21ralbii 2567 . . . . . . . . . 10  |-  ( A. s  e.  t  E. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin ) X  =  U. n 
<-> 
A. s  e.  t  -.  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n )
3 ralnex 2553 . . . . . . . . . 10  |-  ( A. s  e.  t  -.  A. n  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  -.  X  =  U. n  <->  -.  E. s  e.  t  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n )
42, 3bitr2i 241 . . . . . . . . 9  |-  ( -. 
E. s  e.  t 
A. n  e.  ( ~P ( u  u. 
{ s } )  i^i  Fin )  -.  X  =  U. n  <->  A. s  e.  t  E. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin ) X  =  U. n )
5 elin 3358 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( ~P (
u  u.  { s } )  i^i  Fin ) 
<->  ( n  e.  ~P ( u  u.  { s } )  /\  n  e.  Fin ) )
6 elpwi 3633 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ~P ( u  u.  { s } )  ->  n  C_  (
u  u.  { s } ) )
76adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( n  e.  ~P (
u  u.  { s } )  /\  n  e.  Fin )  ->  n  C_  ( u  u.  {
s } ) )
8 uncom 3319 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  u.  { s } )  =  ( { s }  u.  u
)
97, 8syl6sseq 3224 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  ~P (
u  u.  { s } )  /\  n  e.  Fin )  ->  n  C_  ( { s }  u.  u ) )
10 ssundif 3537 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n 
C_  ( { s }  u.  u )  <-> 
( n  \  {
s } )  C_  u )
119, 10sylib 188 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  ~P (
u  u.  { s } )  /\  n  e.  Fin )  ->  (
n  \  { s } )  C_  u
)
12 diffi 7089 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  Fin  ->  (
n  \  { s } )  e.  Fin )
1312adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  ~P (
u  u.  { s } )  /\  n  e.  Fin )  ->  (
n  \  { s } )  e.  Fin )
1411, 13jca 518 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  e.  ~P (
u  u.  { s } )  /\  n  e.  Fin )  ->  (
( n  \  {
s } )  C_  u  /\  ( n  \  { s } )  e.  Fin ) )
155, 14sylbi 187 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( ~P (
u  u.  { s } )  i^i  Fin )  ->  ( ( n 
\  { s } )  C_  u  /\  ( n  \  { s } )  e.  Fin ) )
1615adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  /\  X  =  U. n )  -> 
( ( n  \  { s } ) 
C_  u  /\  (
n  \  { s } )  e.  Fin ) )
1716ad2antll 709 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  ( ( n 
\  { s } )  C_  u  /\  ( n  \  { s } )  e.  Fin ) )
18 elin 3358 . . . . . . . . . . . . . . . . 17  |-  ( ( n  \  { s } )  e.  ( ~P u  i^i  Fin ) 
<->  ( ( n  \  { s } )  e.  ~P u  /\  ( n  \  { s } )  e.  Fin ) )
19 vex 2791 . . . . . . . . . . . . . . . . . . 19  |-  u  e. 
_V
2019elpw2 4175 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  \  { s } )  e.  ~P u 
<->  ( n  \  {
s } )  C_  u )
2120anbi1i 676 . . . . . . . . . . . . . . . . 17  |-  ( ( ( n  \  {
s } )  e. 
~P u  /\  (
n  \  { s } )  e.  Fin ) 
<->  ( ( n  \  { s } ) 
C_  u  /\  (
n  \  { s } )  e.  Fin ) )
2218, 21bitr2i 241 . . . . . . . . . . . . . . . 16  |-  ( ( ( n  \  {
s } )  C_  u  /\  ( n  \  { s } )  e.  Fin )  <->  ( n  \  { s } )  e.  ( ~P u  i^i  Fin ) )
2317, 22sylib 188 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  ( n  \  { s } )  e.  ( ~P u  i^i  Fin ) )
24 simprrr 741 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  X  =  U. n )
25 eldif 3162 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( n  \  { s } )  <-> 
( x  e.  n  /\  -.  x  e.  {
s } ) )
2625simplbi2 608 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  n  ->  ( -.  x  e.  { s }  ->  x  e.  ( n  \  { s } ) ) )
27 elun 3316 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  ( ( n 
\  { s } )  u.  { s } )  <->  ( x  e.  ( n  \  {
s } )  \/  x  e.  { s } ) )
28 orcom 376 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  { s }  \/  x  e.  ( n  \  {
s } ) )  <-> 
( x  e.  ( n  \  { s } )  \/  x  e.  { s } ) )
2927, 28bitr4i 243 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ( n 
\  { s } )  u.  { s } )  <->  ( x  e.  { s }  \/  x  e.  ( n  \  { s } ) ) )
30 df-or 359 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  { s }  \/  x  e.  ( n  \  {
s } ) )  <-> 
( -.  x  e. 
{ s }  ->  x  e.  ( n  \  { s } ) ) )
3129, 30bitr2i 241 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( -.  x  e.  {
s }  ->  x  e.  ( n  \  {
s } ) )  <-> 
x  e.  ( ( n  \  { s } )  u.  {
s } ) )
3226, 31sylib 188 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  n  ->  x  e.  ( ( n  \  { s } )  u.  { s } ) )
3332ssriv 3184 . . . . . . . . . . . . . . . . . . 19  |-  n  C_  ( ( n  \  { s } )  u.  { s } )
34 uniss 3848 . . . . . . . . . . . . . . . . . . 19  |-  ( n 
C_  ( ( n 
\  { s } )  u.  { s } )  ->  U. n  C_ 
U. ( ( n 
\  { s } )  u.  { s } ) )
3533, 34mp1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  U. n  C_  U. (
( n  \  {
s } )  u. 
{ s } ) )
36 uniun 3846 . . . . . . . . . . . . . . . . . . 19  |-  U. (
( n  \  {
s } )  u. 
{ s } )  =  ( U. (
n  \  { s } )  u.  U. { s } )
37 vex 2791 . . . . . . . . . . . . . . . . . . . . 21  |-  s  e. 
_V
3837unisn 3843 . . . . . . . . . . . . . . . . . . . 20  |-  U. {
s }  =  s
3938uneq2i 3326 . . . . . . . . . . . . . . . . . . 19  |-  ( U. ( n  \  { s } )  u.  U. { s } )  =  ( U. (
n  \  { s } )  u.  s
)
4036, 39eqtri 2303 . . . . . . . . . . . . . . . . . 18  |-  U. (
( n  \  {
s } )  u. 
{ s } )  =  ( U. (
n  \  { s } )  u.  s
)
4135, 40syl6sseq 3224 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  U. n  C_  ( U. ( n  \  {
s } )  u.  s ) )
4224, 41eqsstrd 3212 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  X  C_  ( U. ( n  \  {
s } )  u.  s ) )
43 difss 3303 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n 
\  { s } )  C_  n
44 uniss 3848 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  \  { s } )  C_  n  ->  U. ( n  \  { s } ) 
C_  U. n )
4543, 44ax-mp 8 . . . . . . . . . . . . . . . . . . . 20  |-  U. (
n  \  { s } )  C_  U. n
46 sseq2 3200 . . . . . . . . . . . . . . . . . . . 20  |-  ( X  =  U. n  -> 
( U. ( n 
\  { s } )  C_  X  <->  U. (
n  \  { s } )  C_  U. n
) )
4745, 46mpbiri 224 . . . . . . . . . . . . . . . . . . 19  |-  ( X  =  U. n  ->  U. ( n  \  {
s } )  C_  X )
4847adantl 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  /\  X  =  U. n )  ->  U. ( n  \  {
s } )  C_  X )
4948ad2antll 709 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  U. ( n  \  { s } ) 
C_  X )
50 inss1 3389 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ~P x  i^i  Fin )  C_ 
~P x
5150sseli 3176 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  e.  ( ~P x  i^i  Fin )  ->  t  e.  ~P x )
52 elpwi 3633 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  e.  ~P x  -> 
t  C_  x )
5351, 52syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  e.  ( ~P x  i^i  Fin )  ->  t  C_  x )
5453ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( t  e.  ( ~P x  i^i 
Fin )  /\  w  =  |^| t )  /\  ( y  e.  w  /\  -.  y  e.  U. ( x  i^i  u
) ) )  /\  w  e.  u )  ->  t  C_  x )
5554ad2antlr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  t  C_  x
)
56 simprl 732 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  s  e.  t )
5755, 56sseldd 3181 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  s  e.  x
)
58 elssuni 3855 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  x  ->  s  C_ 
U. x )
5957, 58syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  s  C_  U. x
)
60 fibas 16715 . . . . . . . . . . . . . . . . . . . . 21  |-  ( fi
`  x )  e.  TopBases
61 unitg 16705 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( fi `  x )  e.  TopBases  ->  U. ( topGen `  ( fi `  x ) )  =  U. ( fi
`  x ) )
6260, 61mp1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  U. ( topGen `  ( fi `  x ) )  =  U. ( fi
`  x ) )
63 unieq 3836 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( J  =  ( topGen `  ( fi `  x ) )  ->  U. J  =  U. ( topGen `  ( fi `  x ) ) )
64633ad2ant1 976 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( J  =  ( topGen `  ( fi `  x
) )  /\  A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  /\  a  e.  ~P ( fi `  x ) )  ->  U. J  =  U. ( topGen `  ( fi `  x ) ) )
6564ad3antrrr 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  U. J  =  U. ( topGen `  ( fi `  x ) ) )
66 vex 2791 . . . . . . . . . . . . . . . . . . . . 21  |-  x  e. 
_V
67 fiuni 7181 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  _V  ->  U. x  =  U. ( fi `  x ) )
6866, 67mp1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  U. x  =  U. ( fi `  x ) )
6962, 65, 683eqtr4rd 2326 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  U. x  =  U. J )
70 alexsubALT.1 . . . . . . . . . . . . . . . . . . 19  |-  X  = 
U. J
7169, 70syl6eqr 2333 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  U. x  =  X )
7259, 71sseqtrd 3214 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  s  C_  X
)
7349, 72unssd 3351 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  ( U. (
n  \  { s } )  u.  s
)  C_  X )
7442, 73eqssd 3196 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  X  =  ( U. ( n  \  { s } )  u.  s ) )
75 unieq 3836 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  ( n  \  { s } )  ->  U. m  =  U. ( n  \  { s } ) )
7675uneq1d 3328 . . . . . . . . . . . . . . . . 17  |-  ( m  =  ( n  \  { s } )  ->  ( U. m  u.  s )  =  ( U. ( n  \  { s } )  u.  s ) )
7776eqeq2d 2294 . . . . . . . . . . . . . . . 16  |-  ( m  =  ( n  \  { s } )  ->  ( X  =  ( U. m  u.  s )  <->  X  =  ( U. ( n  \  { s } )  u.  s ) ) )
7877rspcev 2884 . . . . . . . . . . . . . . 15  |-  ( ( ( n  \  {
s } )  e.  ( ~P u  i^i 
Fin )  /\  X  =  ( U. (
n  \  { s } )  u.  s
) )  ->  E. m  e.  ( ~P u  i^i 
Fin ) X  =  ( U. m  u.  s ) )
7923, 74, 78syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( s  e.  t  /\  ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n ) ) )  ->  E. m  e.  ( ~P u  i^i  Fin ) X  =  ( U. m  u.  s
) )
8079expr 598 . . . . . . . . . . . . 13  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  s  e.  t )  ->  ( ( n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  /\  X  =  U. n )  ->  E. m  e.  ( ~P u  i^i 
Fin ) X  =  ( U. m  u.  s ) ) )
8180exp3a 425 . . . . . . . . . . . 12  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  s  e.  t )  ->  ( n  e.  ( ~P ( u  u. 
{ s } )  i^i  Fin )  -> 
( X  =  U. n  ->  E. m  e.  ( ~P u  i^i  Fin ) X  =  ( U. m  u.  s
) ) ) )
8281rexlimdv 2666 . . . . . . . . . . 11  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  s  e.  t )  ->  ( E. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin ) X  =  U. n  ->  E. m  e.  ( ~P u  i^i  Fin ) X  =  ( U. m  u.  s
) ) )
8382ralimdva 2621 . . . . . . . . . 10  |-  ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  /\  a  e.  ~P ( fi `  x ) )  /\  ( u  e.  ~P ( fi `  x )  /\  a  C_  u
) )  /\  (
( ( t  e.  ( ~P x  i^i 
Fin )  /\  w  =  |^| t )  /\  ( y  e.  w  /\  -.  y  e.  U. ( x  i^i  u
) ) )  /\  w  e.  u )
)  ->  ( A. s  e.  t  E. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin ) X  =  U. n  ->  A. s  e.  t  E. m  e.  ( ~P u  i^i  Fin ) X  =  ( U. m  u.  s
) ) )
84 inss2 3390 . . . . . . . . . . . . . . 15  |-  ( ~P x  i^i  Fin )  C_ 
Fin
8584sseli 3176 . . . . . . . . . . . . . 14  |-  ( t  e.  ( ~P x  i^i  Fin )  ->  t  e.  Fin )
8685adantr 451 . . . . . . . . . . . . 13  |-  ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  ->  t  e.  Fin )
87 unieq 3836 . . . . . . . . . . . . . . . . 17  |-  ( m  =  ( f `  s )  ->  U. m  =  U. ( f `  s ) )
8887uneq1d 3328 . . . . . . . . . . . . . . . 16  |-  ( m  =  ( f `  s )  ->  ( U. m  u.  s
)  =  ( U. ( f `  s
)  u.  s ) )
8988eqeq2d 2294 . . . . . . . . . . . . . . 15  |-  ( m  =  ( f `  s )  ->  ( X  =  ( U. m  u.  s )  <->  X  =  ( U. (
f `  s )  u.  s ) ) )
9089ac6sfi 7101 . . . . . . . . . . . . . 14  |-  ( ( t  e.  Fin  /\  A. s  e.  t  E. m  e.  ( ~P u  i^i  Fin ) X  =  ( U. m  u.  s ) )  ->  E. f ( f : t --> ( ~P u  i^i  Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )
9190ex 423 . . . . . . . . . . . . 13  |-  ( t  e.  Fin  ->  ( A. s  e.  t  E. m  e.  ( ~P u  i^i  Fin ) X  =  ( U. m  u.  s )  ->  E. f ( f : t --> ( ~P u  i^i  Fin )  /\  A. s  e.  t  X  =  ( U. ( f `  s
)  u.  s ) ) ) )
9286, 91syl 15 . . . . . . . . . . . 12  |-  ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  ->  ( A. s  e.  t  E. m  e.  ( ~P u  i^i  Fin ) X  =  ( U. m  u.  s )  ->  E. f ( f : t --> ( ~P u  i^i  Fin )  /\  A. s  e.  t  X  =  ( U. ( f `  s
)  u.  s ) ) ) )
9392adantr 451 . . . . . . . . . . 11  |-  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  ->  ( A. s  e.  t  E. m  e.  ( ~P u  i^i  Fin ) X  =  ( U. m  u.  s )  ->  E. f ( f : t --> ( ~P u  i^i  Fin )  /\  A. s  e.  t  X  =  ( U. ( f `  s
)  u.  s ) ) ) )
9493ad2antrl 708 . . . . . . . . . 10  |-  ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  /\  a  e.  ~P ( fi `  x ) )  /\  ( u  e.  ~P ( fi `  x )  /\  a  C_  u
) )  /\  (
( ( t  e.  ( ~P x  i^i 
Fin )  /\  w  =  |^| t )  /\  ( y  e.  w  /\  -.  y  e.  U. ( x  i^i  u
) ) )  /\  w  e.  u )
)  ->  ( A. s  e.  t  E. m  e.  ( ~P u  i^i  Fin ) X  =  ( U. m  u.  s )  ->  E. f
( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) ) )
95 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f : t --> ( ~P u  i^i  Fin )  /\  s  e.  t )  ->  ( f `  s )  e.  ( ~P u  i^i  Fin ) )
96 elin 3358 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f `  s )  e.  ( ~P u  i^i  Fin )  <->  ( (
f `  s )  e.  ~P u  /\  (
f `  s )  e.  Fin ) )
97 elpwi 3633 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f `  s )  e.  ~P u  -> 
( f `  s
)  C_  u )
9897adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( f `  s
)  e.  ~P u  /\  ( f `  s
)  e.  Fin )  ->  ( f `  s
)  C_  u )
9996, 98sylbi 187 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f `  s )  e.  ( ~P u  i^i  Fin )  ->  (
f `  s )  C_  u )
10095, 99syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f : t --> ( ~P u  i^i  Fin )  /\  s  e.  t )  ->  ( f `  s )  C_  u
)
101100ralrimiva 2626 . . . . . . . . . . . . . . . . . 18  |-  ( f : t --> ( ~P u  i^i  Fin )  ->  A. s  e.  t  ( f `  s
)  C_  u )
102 iunss 3943 . . . . . . . . . . . . . . . . . 18  |-  ( U_ s  e.  t  (
f `  s )  C_  u  <->  A. s  e.  t  ( f `  s
)  C_  u )
103101, 102sylibr 203 . . . . . . . . . . . . . . . . 17  |-  ( f : t --> ( ~P u  i^i  Fin )  ->  U_ s  e.  t  ( f `  s
)  C_  u )
104103ad2antrl 708 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  U_ s  e.  t  ( f `  s
)  C_  u )
105 simplrr 737 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  w  e.  u
)
106105snssd 3760 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  { w }  C_  u )
107104, 106unssd 3351 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  ( U_ s  e.  t  ( f `  s )  u.  {
w } )  C_  u )
108 inss2 3390 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ~P u  i^i  Fin )  C_ 
Fin
109108, 95sseldi 3178 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f : t --> ( ~P u  i^i  Fin )  /\  s  e.  t )  ->  ( f `  s )  e.  Fin )
110109ralrimiva 2626 . . . . . . . . . . . . . . . . . . . 20  |-  ( f : t --> ( ~P u  i^i  Fin )  ->  A. s  e.  t  ( f `  s
)  e.  Fin )
111 iunfi 7144 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( t  e.  Fin  /\  A. s  e.  t  ( f `  s )  e.  Fin )  ->  U_ s  e.  t 
( f `  s
)  e.  Fin )
11286, 110, 111syl2an 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  f : t --> ( ~P u  i^i  Fin )
)  ->  U_ s  e.  t  ( f `  s )  e.  Fin )
113112adantlr 695 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( t  e.  ( ~P x  i^i 
Fin )  /\  w  =  |^| t )  /\  ( y  e.  w  /\  -.  y  e.  U. ( x  i^i  u
) ) )  /\  f : t --> ( ~P u  i^i  Fin )
)  ->  U_ s  e.  t  ( f `  s )  e.  Fin )
114113adantlr 695 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  ( y  e.  w  /\  -.  y  e.  U. ( x  i^i  u
) ) )  /\  w  e.  u )  /\  f : t --> ( ~P u  i^i  Fin ) )  ->  U_ s  e.  t  ( f `  s )  e.  Fin )
115114ad2ant2lr 728 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  U_ s  e.  t  ( f `  s
)  e.  Fin )
116 snfi 6941 . . . . . . . . . . . . . . . 16  |-  { w }  e.  Fin
117 unfi 7124 . . . . . . . . . . . . . . . 16  |-  ( (
U_ s  e.  t  ( f `  s
)  e.  Fin  /\  { w }  e.  Fin )  ->  ( U_ s  e.  t  ( f `  s )  u.  {
w } )  e. 
Fin )
118115, 116, 117sylancl 643 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  ( U_ s  e.  t  ( f `  s )  u.  {
w } )  e. 
Fin )
119107, 118jca 518 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  ( ( U_ s  e.  t  (
f `  s )  u.  { w } ) 
C_  u  /\  ( U_ s  e.  t 
( f `  s
)  u.  { w } )  e.  Fin ) )
120 elin 3358 . . . . . . . . . . . . . . 15  |-  ( (
U_ s  e.  t  ( f `  s
)  u.  { w } )  e.  ( ~P u  i^i  Fin ) 
<->  ( ( U_ s  e.  t  ( f `  s )  u.  {
w } )  e. 
~P u  /\  ( U_ s  e.  t 
( f `  s
)  u.  { w } )  e.  Fin ) )
12119elpw2 4175 . . . . . . . . . . . . . . . 16  |-  ( (
U_ s  e.  t  ( f `  s
)  u.  { w } )  e.  ~P u 
<->  ( U_ s  e.  t  ( f `  s )  u.  {
w } )  C_  u )
122121anbi1i 676 . . . . . . . . . . . . . . 15  |-  ( ( ( U_ s  e.  t  ( f `  s )  u.  {
w } )  e. 
~P u  /\  ( U_ s  e.  t 
( f `  s
)  u.  { w } )  e.  Fin ) 
<->  ( ( U_ s  e.  t  ( f `  s )  u.  {
w } )  C_  u  /\  ( U_ s  e.  t  ( f `  s )  u.  {
w } )  e. 
Fin ) )
123120, 122bitr2i 241 . . . . . . . . . . . . . 14  |-  ( ( ( U_ s  e.  t  ( f `  s )  u.  {
w } )  C_  u  /\  ( U_ s  e.  t  ( f `  s )  u.  {
w } )  e. 
Fin )  <->  ( U_ s  e.  t  (
f `  s )  u.  { w } )  e.  ( ~P u  i^i  Fin ) )
124119, 123sylib 188 . . . . . . . . . . . . 13  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  ( U_ s  e.  t  ( f `  s )  u.  {
w } )  e.  ( ~P u  i^i 
Fin ) )
125 ralnex 2553 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( A. s  e.  t  -.  y  e.  ( f `  s )  <->  -.  E. s  e.  t  y  e.  ( f `  s
) )
126125imbi2i 303 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( v  e.  y  ->  A. s  e.  t  -.  y  e.  (
f `  s )
)  <->  ( v  e.  y  ->  -.  E. s  e.  t  y  e.  ( f `  s
) ) )
127126albii 1553 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A. y ( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s
) )  <->  A. y
( v  e.  y  ->  -.  E. s  e.  t  y  e.  ( f `  s
) ) )
128 alinexa 1565 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A. y ( v  e.  y  ->  -.  E. s  e.  t  y  e.  ( f `  s
) )  <->  -.  E. y
( v  e.  y  /\  E. s  e.  t  y  e.  ( f `  s ) ) )
129127, 128bitr2i 241 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -. 
E. y ( v  e.  y  /\  E. s  e.  t  y  e.  ( f `  s
) )  <->  A. y
( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s ) ) )
130 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( s  =  z  ->  (
f `  s )  =  ( f `  z ) )
131130unieqd 3838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( s  =  z  ->  U. (
f `  s )  =  U. ( f `  z ) )
132 id 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( s  =  z  ->  s  =  z )
133131, 132uneq12d 3330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( s  =  z  ->  ( U. ( f `  s
)  u.  s )  =  ( U. (
f `  z )  u.  z ) )
134133eqeq2d 2294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( s  =  z  ->  ( X  =  ( U. ( f `  s
)  u.  s )  <-> 
X  =  ( U. ( f `  z
)  u.  z ) ) )
135134rspcv 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( z  e.  t  ->  ( A. s  e.  t  X  =  ( U. ( f `  s
)  u.  s )  ->  X  =  ( U. ( f `  z )  u.  z
) ) )
136 eleq2 2344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( X  =  ( U. (
f `  z )  u.  z )  ->  (
v  e.  X  <->  v  e.  ( U. ( f `  z )  u.  z
) ) )
137136biimpd 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( X  =  ( U. (
f `  z )  u.  z )  ->  (
v  e.  X  -> 
v  e.  ( U. ( f `  z
)  u.  z ) ) )
138 elun 3316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( v  e.  ( U. (
f `  z )  u.  z )  <->  ( v  e.  U. ( f `  z )  \/  v  e.  z ) )
139 eluni 3830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( v  e.  U. ( f `
 z )  <->  E. w
( v  e.  w  /\  w  e.  (
f `  z )
) )
140139orbi1i 506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( v  e.  U. (
f `  z )  \/  v  e.  z
)  <->  ( E. w
( v  e.  w  /\  w  e.  (
f `  z )
)  \/  v  e.  z ) )
141 df-or 359 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( E. w ( v  e.  w  /\  w  e.  ( f `  z
) )  \/  v  e.  z )  <->  ( -.  E. w ( v  e.  w  /\  w  e.  ( f `  z
) )  ->  v  e.  z ) )
142 alinexa 1565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( A. w ( v  e.  w  ->  -.  w  e.  ( f `  z
) )  <->  -.  E. w
( v  e.  w  /\  w  e.  (
f `  z )
) )
143142imbi1i 315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( A. w ( v  e.  w  ->  -.  w  e.  ( f `  z ) )  -> 
v  e.  z )  <-> 
( -.  E. w
( v  e.  w  /\  w  e.  (
f `  z )
)  ->  v  e.  z ) )
144141, 143bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( E. w ( v  e.  w  /\  w  e.  ( f `  z
) )  \/  v  e.  z )  <->  ( A. w ( v  e.  w  ->  -.  w  e.  ( f `  z
) )  ->  v  e.  z ) )
145138, 140, 1443bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( v  e.  ( U. (
f `  z )  u.  z )  <->  ( A. w ( v  e.  w  ->  -.  w  e.  ( f `  z
) )  ->  v  e.  z ) )
146 eleq2 2344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( y  =  w  ->  (
v  e.  y  <->  v  e.  w ) )
147 eleq1 2343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( y  =  w  ->  (
y  e.  ( f `
 s )  <->  w  e.  ( f `  s
) ) )
148147notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( y  =  w  ->  ( -.  y  e.  (
f `  s )  <->  -.  w  e.  ( f `
 s ) ) )
149148ralbidv 2563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( y  =  w  ->  ( A. s  e.  t  -.  y  e.  (
f `  s )  <->  A. s  e.  t  -.  w  e.  ( f `
 s ) ) )
150146, 149imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  w  ->  (
( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s ) )  <->  ( v  e.  w  ->  A. s  e.  t  -.  w  e.  ( f `  s
) ) ) )
151150spv 1938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( A. y ( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s
) )  ->  (
v  e.  w  ->  A. s  e.  t  -.  w  e.  (
f `  s )
) )
152130eleq2d 2350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( s  =  z  ->  (
w  e.  ( f `
 s )  <->  w  e.  ( f `  z
) ) )
153152notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( s  =  z  ->  ( -.  w  e.  (
f `  s )  <->  -.  w  e.  ( f `
 z ) ) )
154153rspcv 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( z  e.  t  ->  ( A. s  e.  t  -.  w  e.  (
f `  s )  ->  -.  w  e.  ( f `  z ) ) )
155151, 154syl9r 67 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( z  e.  t  ->  ( A. y ( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s
) )  ->  (
v  e.  w  ->  -.  w  e.  (
f `  z )
) ) )
156155alrimdv 1619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  e.  t  ->  ( A. y ( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s
) )  ->  A. w
( v  e.  w  ->  -.  w  e.  ( f `  z ) ) ) )
157156imim1d 69 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  e.  t  ->  (
( A. w ( v  e.  w  ->  -.  w  e.  (
f `  z )
)  ->  v  e.  z )  ->  ( A. y ( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s
) )  ->  v  e.  z ) ) )
158145, 157syl5bi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z  e.  t  ->  (
v  e.  ( U. ( f `  z
)  u.  z )  ->  ( A. y
( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s ) )  ->  v  e.  z ) ) )
159158a1dd 42 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( z  e.  t  ->  (
v  e.  ( U. ( f `  z
)  u.  z )  ->  ( w  = 
|^| t  ->  ( A. y ( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s
) )  ->  v  e.  z ) ) ) )
160137, 159syl9r 67 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( z  e.  t  ->  ( X  =  ( U. ( f `  z
)  u.  z )  ->  ( v  e.  X  ->  ( w  =  |^| t  ->  ( A. y ( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s
) )  ->  v  e.  z ) ) ) ) )
161135, 160syld 40 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  e.  t  ->  ( A. s  e.  t  X  =  ( U. ( f `  s
)  u.  s )  ->  ( v  e.  X  ->  ( w  =  |^| t  ->  ( A. y ( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s
) )  ->  v  e.  z ) ) ) ) )
162161com14 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( w  =  |^| t  -> 
( A. s  e.  t  X  =  ( U. ( f `  s )  u.  s
)  ->  ( v  e.  X  ->  ( z  e.  t  ->  ( A. y ( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s
) )  ->  v  e.  z ) ) ) ) )
163162imp31 421 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( w  =  |^| t  /\  A. s  e.  t  X  =  ( U. ( f `  s )  u.  s
) )  /\  v  e.  X )  ->  (
z  e.  t  -> 
( A. y ( v  e.  y  ->  A. s  e.  t  -.  y  e.  (
f `  s )
)  ->  v  e.  z ) ) )
164163com23 72 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( w  =  |^| t  /\  A. s  e.  t  X  =  ( U. ( f `  s )  u.  s
) )  /\  v  e.  X )  ->  ( A. y ( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s
) )  ->  (
z  e.  t  -> 
v  e.  z ) ) )
165164ralrimdv 2632 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( w  =  |^| t  /\  A. s  e.  t  X  =  ( U. ( f `  s )  u.  s
) )  /\  v  e.  X )  ->  ( A. y ( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s
) )  ->  A. z  e.  t  v  e.  z ) )
166 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  v  e. 
_V
167166elint2 3869 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( v  e.  |^| t  <->  A. z  e.  t  v  e.  z )
168165, 167syl6ibr 218 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( w  =  |^| t  /\  A. s  e.  t  X  =  ( U. ( f `  s )  u.  s
) )  /\  v  e.  X )  ->  ( A. y ( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s
) )  ->  v  e.  |^| t ) )
169 eleq2 2344 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  |^| t  -> 
( v  e.  w  <->  v  e.  |^| t ) )
170169ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( w  =  |^| t  /\  A. s  e.  t  X  =  ( U. ( f `  s )  u.  s
) )  /\  v  e.  X )  ->  (
v  e.  w  <->  v  e.  |^| t ) )
171168, 170sylibrd 225 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( w  =  |^| t  /\  A. s  e.  t  X  =  ( U. ( f `  s )  u.  s
) )  /\  v  e.  X )  ->  ( A. y ( v  e.  y  ->  A. s  e.  t  -.  y  e.  ( f `  s
) )  ->  v  e.  w ) )
172129, 171syl5bi 208 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( w  =  |^| t  /\  A. s  e.  t  X  =  ( U. ( f `  s )  u.  s
) )  /\  v  e.  X )  ->  ( -.  E. y ( v  e.  y  /\  E. s  e.  t  y  e.  ( f `  s
) )  ->  v  e.  w ) )
173172orrd 367 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  =  |^| t  /\  A. s  e.  t  X  =  ( U. ( f `  s )  u.  s
) )  /\  v  e.  X )  ->  ( E. y ( v  e.  y  /\  E. s  e.  t  y  e.  ( f `  s
) )  \/  v  e.  w ) )
174173ex 423 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( w  =  |^| t  /\  A. s  e.  t  X  =  ( U. ( f `  s
)  u.  s ) )  ->  ( v  e.  X  ->  ( E. y ( v  e.  y  /\  E. s  e.  t  y  e.  ( f `  s
) )  \/  v  e.  w ) ) )
175 orc 374 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( E. s  e.  t  y  e.  ( f `  s )  ->  ( E. s  e.  t 
y  e.  ( f `
 s )  \/  y  =  w ) )
176175anim2i 552 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  y  /\  E. s  e.  t  y  e.  ( f `  s ) )  -> 
( v  e.  y  /\  ( E. s  e.  t  y  e.  ( f `  s
)  \/  y  =  w ) ) )
177176eximi 1563 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E. y ( v  e.  y  /\  E. s  e.  t  y  e.  ( f `  s
) )  ->  E. y
( v  e.  y  /\  ( E. s  e.  t  y  e.  ( f `  s
)  \/  y  =  w ) ) )
178 equid 1644 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  w  =  w
179 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  w  e. 
_V
180 equequ1 1648 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  w  ->  (
y  =  w  <->  w  =  w ) )
181146, 180anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  w  ->  (
( v  e.  y  /\  y  =  w )  <->  ( v  e.  w  /\  w  =  w ) ) )
182179, 181spcev 2875 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( v  e.  w  /\  w  =  w )  ->  E. y ( v  e.  y  /\  y  =  w ) )
183178, 182mpan2 652 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v  e.  w  ->  E. y
( v  e.  y  /\  y  =  w ) )
184 olc 373 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  w  ->  ( E. s  e.  t 
y  e.  ( f `
 s )  \/  y  =  w ) )
185184anim2i 552 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( v  e.  y  /\  y  =  w )  ->  ( v  e.  y  /\  ( E. s  e.  t  y  e.  ( f `  s
)  \/  y  =  w ) ) )
186185eximi 1563 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( E. y ( v  e.  y  /\  y  =  w )  ->  E. y
( v  e.  y  /\  ( E. s  e.  t  y  e.  ( f `  s
)  \/  y  =  w ) ) )
187183, 186syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  e.  w  ->  E. y
( v  e.  y  /\  ( E. s  e.  t  y  e.  ( f `  s
)  \/  y  =  w ) ) )
188177, 187jaoi 368 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( E. y ( v  e.  y  /\  E. s  e.  t  y  e.  ( f `  s
) )  \/  v  e.  w )  ->  E. y
( v  e.  y  /\  ( E. s  e.  t  y  e.  ( f `  s
)  \/  y  =  w ) ) )
189 eluni 3830 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  e.  U. ( U_ s  e.  t  (
f `  s )  u.  { w } )  <->  E. y ( v  e.  y  /\  y  e.  ( U_ s  e.  t  ( f `  s )  u.  {
w } ) ) )
190 elun 3316 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  ( U_ s  e.  t  ( f `  s )  u.  {
w } )  <->  ( y  e.  U_ s  e.  t  ( f `  s
)  \/  y  e. 
{ w } ) )
191 eliun 3909 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  U_ s  e.  t  ( f `  s )  <->  E. s  e.  t  y  e.  ( f `  s
) )
192 elsn 3655 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  e.  { w }  <->  y  =  w )
193191, 192orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( y  e.  U_ s  e.  t  ( f `  s )  \/  y  e.  { w } )  <-> 
( E. s  e.  t  y  e.  ( f `  s )  \/  y  =  w ) )
194190, 193bitri 240 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( U_ s  e.  t  ( f `  s )  u.  {
w } )  <->  ( E. s  e.  t  y  e.  ( f `  s
)  \/  y  =  w ) )
195194anbi2i 675 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  y  /\  y  e.  ( U_ s  e.  t  (
f `  s )  u.  { w } ) )  <->  ( v  e.  y  /\  ( E. s  e.  t  y  e.  ( f `  s )  \/  y  =  w ) ) )
196195exbii 1569 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E. y ( v  e.  y  /\  y  e.  ( U_ s  e.  t  ( f `  s )  u.  {
w } ) )  <->  E. y ( v  e.  y  /\  ( E. s  e.  t  y  e.  ( f `  s )  \/  y  =  w ) ) )
197189, 196bitr2i 241 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E. y ( v  e.  y  /\  ( E. s  e.  t  y  e.  ( f `  s )  \/  y  =  w ) )  <->  v  e.  U. ( U_ s  e.  t  ( f `  s )  u.  {
w } ) )
198188, 197sylib 188 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( E. y ( v  e.  y  /\  E. s  e.  t  y  e.  ( f `  s
) )  \/  v  e.  w )  ->  v  e.  U. ( U_ s  e.  t  ( f `  s )  u.  {
w } ) )
199174, 198syl6 29 . . . . . . . . . . . . . . . . . . 19  |-  ( ( w  =  |^| t  /\  A. s  e.  t  X  =  ( U. ( f `  s
)  u.  s ) )  ->  ( v  e.  X  ->  v  e. 
U. ( U_ s  e.  t  ( f `  s )  u.  {
w } ) ) )
200199adantll 694 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) )  -> 
( v  e.  X  ->  v  e.  U. ( U_ s  e.  t 
( f `  s
)  u.  { w } ) ) )
201200adantlr 695 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( t  e.  ( ~P x  i^i 
Fin )  /\  w  =  |^| t )  /\  ( y  e.  w  /\  -.  y  e.  U. ( x  i^i  u
) ) )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) )  -> 
( v  e.  X  ->  v  e.  U. ( U_ s  e.  t 
( f `  s
)  u.  { w } ) ) )
202201adantlr 695 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  ( y  e.  w  /\  -.  y  e.  U. ( x  i^i  u
) ) )  /\  w  e.  u )  /\  A. s  e.  t  X  =  ( U. ( f `  s
)  u.  s ) )  ->  ( v  e.  X  ->  v  e. 
U. ( U_ s  e.  t  ( f `  s )  u.  {
w } ) ) )
203202ad2ant2l 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  ( v  e.  X  ->  v  e.  U. ( U_ s  e.  t  ( f `  s )  u.  {
w } ) ) )
204203ssrdv 3185 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  X  C_  U. ( U_ s  e.  t 
( f `  s
)  u.  { w } ) )
205 elun 3316 . . . . . . . . . . . . . . . . . 18  |-  ( v  e.  ( U_ s  e.  t  ( f `  s )  u.  {
w } )  <->  ( v  e.  U_ s  e.  t  ( f `  s
)  \/  v  e. 
{ w } ) )
206 eliun 3909 . . . . . . . . . . . . . . . . . . 19  |-  ( v  e.  U_ s  e.  t  ( f `  s )  <->  E. s  e.  t  v  e.  ( f `  s
) )
207 elsn 3655 . . . . . . . . . . . . . . . . . . 19  |-  ( v  e.  { w }  <->  v  =  w )
208206, 207orbi12i 507 . . . . . . . . . . . . . . . . . 18  |-  ( ( v  e.  U_ s  e.  t  ( f `  s )  \/  v  e.  { w } )  <-> 
( E. s  e.  t  v  e.  ( f `  s )  \/  v  =  w ) )
209205, 208bitri 240 . . . . . . . . . . . . . . . . 17  |-  ( v  e.  ( U_ s  e.  t  ( f `  s )  u.  {
w } )  <->  ( E. s  e.  t  v  e.  ( f `  s
)  \/  v  =  w ) )
210 nfra1 2593 . . . . . . . . . . . . . . . . . . . 20  |-  F/ s A. s  e.  t  X  =  ( U. ( f `  s
)  u.  s )
211 nfv 1605 . . . . . . . . . . . . . . . . . . . 20  |-  F/ s  v  C_  X
212 rsp 2603 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. s  e.  t  X  =  ( U. (
f `  s )  u.  s )  ->  (
s  e.  t  ->  X  =  ( U. ( f `  s
)  u.  s ) ) )
213 eqimss2 3231 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( X  =  ( U. (
f `  s )  u.  s )  ->  ( U. ( f `  s
)  u.  s ) 
C_  X )
214 elssuni 3855 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v  e.  ( f `  s )  ->  v  C_ 
U. ( f `  s ) )
215 ssun3 3340 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v 
C_  U. ( f `  s )  ->  v  C_  ( U. ( f `
 s )  u.  s ) )
216214, 215syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  e.  ( f `  s )  ->  v  C_  ( U. ( f `
 s )  u.  s ) )
217 sstr 3187 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  C_  ( U. ( f `  s
)  u.  s )  /\  ( U. (
f `  s )  u.  s )  C_  X
)  ->  v  C_  X )
218217expcom 424 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( U. ( f `  s )  u.  s
)  C_  X  ->  ( v  C_  ( U. ( f `  s
)  u.  s )  ->  v  C_  X
) )
219213, 216, 218syl2im 34 . . . . . . . . . . . . . . . . . . . . 21  |-  ( X  =  ( U. (
f `  s )  u.  s )  ->  (
v  e.  ( f `
 s )  -> 
v  C_  X )
)
220212, 219syl6 29 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. s  e.  t  X  =  ( U. (
f `  s )  u.  s )  ->  (
s  e.  t  -> 
( v  e.  ( f `  s )  ->  v  C_  X
) ) )
221210, 211, 220rexlimd 2664 . . . . . . . . . . . . . . . . . . 19  |-  ( A. s  e.  t  X  =  ( U. (
f `  s )  u.  s )  ->  ( E. s  e.  t 
v  e.  ( f `
 s )  -> 
v  C_  X )
)
222221ad2antll 709 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  ( E. s  e.  t  v  e.  ( f `  s
)  ->  v  C_  X ) )
223 elpwi 3633 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( u  e.  ~P ( fi
`  x )  ->  u  C_  ( fi `  x ) )
224223ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( J  =  (
topGen `  ( fi `  x ) )  /\  A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  /\  a  e.  ~P ( fi `  x ) )  /\  ( u  e.  ~P ( fi `  x )  /\  a  C_  u
) )  ->  u  C_  ( fi `  x
) )
225224ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  u  C_  ( fi `  x ) )
226225, 105sseldd 3181 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  w  e.  ( fi `  x ) )
227 elssuni 3855 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  ( fi `  x )  ->  w  C_ 
U. ( fi `  x ) )
228226, 227syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  w  C_  U. ( fi `  x ) )
22960, 61ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  U. ( topGen `
 ( fi `  x ) )  = 
U. ( fi `  x )
23063, 229syl6req 2332 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( J  =  ( topGen `  ( fi `  x ) )  ->  U. ( fi `  x )  =  U. J )
231230, 70syl6eqr 2333 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( J  =  ( topGen `  ( fi `  x ) )  ->  U. ( fi `  x )  =  X )
2322313ad2ant1 976 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( J  =  ( topGen `  ( fi `  x
) )  /\  A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  /\  a  e.  ~P ( fi `  x ) )  ->  U. ( fi `  x
)  =  X )
233232ad3antrrr 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  U. ( fi `  x )  =  X )
234228, 233sseqtrd 3214 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  w  C_  X
)
235 sseq1 3199 . . . . . . . . . . . . . . . . . . 19  |-  ( v  =  w  ->  (
v  C_  X  <->  w  C_  X
) )
236234, 235syl5ibrcom 213 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  ( v  =  w  ->  v  C_  X ) )
237222, 236jaod 369 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  ( ( E. s  e.  t  v  e.  ( f `  s )  \/  v  =  w )  ->  v  C_  X ) )
238209, 237syl5bi 208 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  ( v  e.  ( U_ s  e.  t  ( f `  s )  u.  {
w } )  -> 
v  C_  X )
)
239238ralrimiv 2625 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  A. v  e.  (
U_ s  e.  t  ( f `  s
)  u.  { w } ) v  C_  X )
240 unissb 3857 . . . . . . . . . . . . . . 15  |-  ( U. ( U_ s  e.  t  ( f `  s
)  u.  { w } )  C_  X  <->  A. v  e.  ( U_ s  e.  t  (
f `  s )  u.  { w } ) v  C_  X )
241239, 240sylibr 203 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  U. ( U_ s  e.  t  ( f `  s )  u.  {
w } )  C_  X )
242204, 241eqssd 3196 . . . . . . . . . . . . 13  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  X  =  U. ( U_ s  e.  t  ( f `  s
)  u.  { w } ) )
243 unieq 3836 . . . . . . . . . . . . . . 15  |-  ( b  =  ( U_ s  e.  t  ( f `  s )  u.  {
w } )  ->  U. b  =  U. ( U_ s  e.  t  ( f `  s
)  u.  { w } ) )
244243eqeq2d 2294 . . . . . . . . . . . . . 14  |-  ( b  =  ( U_ s  e.  t  ( f `  s )  u.  {
w } )  -> 
( X  =  U. b 
<->  X  =  U. ( U_ s  e.  t 
( f `  s
)  u.  { w } ) ) )
245244rspcev 2884 . . . . . . . . . . . . 13  |-  ( ( ( U_ s  e.  t  ( f `  s )  u.  {
w } )  e.  ( ~P u  i^i 
Fin )  /\  X  =  U. ( U_ s  e.  t  ( f `  s )  u.  {
w } ) )  ->  E. b  e.  ( ~P u  i^i  Fin ) X  =  U. b )
246124, 242, 245syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  a  C_  u ) )  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  /\  w  e.  u ) )  /\  ( f : t --> ( ~P u  i^i 
Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) ) )  ->  E. b  e.  ( ~P u  i^i  Fin ) X  =  U. b )
247246ex 423 . . . . . . . . . . 11  |-  ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  /\  a  e.  ~P ( fi `  x ) )  /\  ( u  e.  ~P ( fi `  x )  /\  a  C_  u
) )  /\  (
( ( t  e.  ( ~P x  i^i 
Fin )  /\  w  =  |^| t )  /\  ( y  e.  w  /\  -.  y  e.  U. ( x  i^i  u
) ) )  /\  w  e.  u )
)  ->  ( (
f : t --> ( ~P u  i^i  Fin )  /\  A. s  e.  t  X  =  ( U. ( f `  s )  u.  s
) )  ->  E. b  e.  ( ~P u  i^i 
Fin ) X  = 
U. b ) )
248247exlimdv 1664 . . . . . . . . . 10  |-  ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  /\  a  e.  ~P ( fi `  x ) )  /\  ( u  e.  ~P ( fi `  x )  /\  a  C_  u
) )  /\  (
( ( t  e.  ( ~P x  i^i 
Fin )  /\  w  =  |^| t )  /\  ( y  e.  w  /\  -.  y  e.  U. ( x  i^i  u
) ) )  /\  w  e.  u )
)  ->  ( E. f ( f : t --> ( ~P u  i^i  Fin )  /\  A. s  e.  t  X  =  ( U. (
f `  s )  u.  s ) )  ->  E. b  e.  ( ~P u  i^i  Fin ) X  =  U. b
) )
24983, 94, 2483syld 51 . . . . . . . . 9  |-  ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  /\  a  e.  ~P ( fi `  x ) )  /\  ( u  e.  ~P ( fi `  x )  /\  a  C_  u
) )  /\  (
( ( t  e.  ( ~P x  i^i 
Fin )  /\  w  =  |^| t )  /\  ( y  e.  w  /\  -.  y  e.  U. ( x  i^i  u
) ) )  /\  w  e.  u )
)  ->  ( A. s  e.  t  E. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin ) X  =  U. n  ->  E. b  e.  ( ~P u  i^i  Fin ) X  =  U. b ) )
2504, 249syl5bi 208 . . . . . . . 8  |-  ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  /\  a  e.  ~P ( fi `  x ) )  /\  ( u  e.  ~P ( fi `  x )  /\  a  C_  u
) )  /\  (
( ( t  e.  ( ~P x  i^i 
Fin )  /\  w  =  |^| t )  /\  ( y  e.  w  /\  -.  y  e.  U. ( x  i^i  u
) ) )  /\  w  e.  u )
)  ->  ( -.  E. s  e.  t  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n  ->  E. b  e.  ( ~P u  i^i  Fin ) X  =  U. b ) )
251 dfrex2 2556 . . . . . . . 8  |-  ( E. b  e.  ( ~P u  i^i  Fin ) X  =  U. b  <->  -. 
A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b )
252250, 251syl6ib 217 . . . . . . 7  |-  ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  /\  a  e.  ~P ( fi `  x ) )  /\  ( u  e.  ~P ( fi `  x )  /\  a  C_  u
) )  /\  (
( ( t  e.  ( ~P x  i^i 
Fin )  /\  w  =  |^| t )  /\  ( y  e.  w  /\  -.  y  e.  U. ( x  i^i  u
) ) )  /\  w  e.  u )
)  ->  ( -.  E. s  e.  t  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n  ->  -.  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) )
253252con4d 97 . . . . . 6  |-  ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  /\  a  e.  ~P ( fi `  x ) )  /\  ( u  e.  ~P ( fi `  x )  /\  a  C_  u
) )  /\  (
( ( t  e.  ( ~P x  i^i 
Fin )  /\  w  =  |^| t )  /\  ( y  e.  w  /\  -.  y  e.  U. ( x  i^i  u
) ) )  /\  w  e.  u )
)  ->  ( A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b  ->  E. s  e.  t 
A. n  e.  ( ~P ( u  u. 
{ s } )  i^i  Fin )  -.  X  =  U. n
) )
254253exp32 588 . . . . 5  |-  ( ( ( J  =  (
topGen `  ( fi `  x ) )  /\  A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  /\  a  e.  ~P ( fi `  x ) )  /\  ( u  e.  ~P ( fi `  x )  /\  a  C_  u
) )  ->  (
( ( t  e.  ( ~P x  i^i 
Fin )  /\  w  =  |^| t )  /\  ( y  e.  w  /\  -.  y  e.  U. ( x  i^i  u
) ) )  -> 
( w  e.  u  ->  ( A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b  ->  E. s  e.  t  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) ) ) )
255254com24 81 . . . 4  |-  ( ( ( J  =  (
topGen `  ( fi `  x ) )  /\  A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  /\  a  e.  ~P ( fi `  x ) )  /\  ( u  e.  ~P ( fi `  x )  /\  a  C_  u
) )  ->  ( A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b  ->  ( w  e.  u  ->  ( (
( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  ->  E. s  e.  t  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) ) ) )
256255exp32 588 . . 3  |-  ( ( J  =  ( topGen `  ( fi `  x
) )  /\  A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  /\  a  e.  ~P ( fi `  x ) )  -> 
( u  e.  ~P ( fi `  x )  ->  ( a  C_  u  ->  ( A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b  ->  (
w  e.  u  -> 
( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  ( y  e.  w  /\  -.  y  e.  U. ( x  i^i  u
) ) )  ->  E. s  e.  t  A. n  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  -.  X  =  U. n ) ) ) ) ) )
257256imp45 580 . 2  |-  ( ( ( J  =  (
topGen `  ( fi `  x ) )  /\  A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  /\  a  e.  ~P ( fi `  x ) )  /\  ( u  e.  ~P ( fi `  x )  /\  ( a  C_  u  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  ( w  e.  u  ->  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  ->  E. s  e.  t  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) ) )
258257imp31 421 1  |-  ( ( ( ( ( J  =  ( topGen `  ( fi `  x ) )  /\  A. c  e. 
~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  /\  a  e.  ~P ( fi `  x
) )  /\  (
u  e.  ~P ( fi `  x )  /\  ( a  C_  u  /\  A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b ) ) )  /\  w  e.  u
)  /\  ( (
t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) ) )  ->  E. s  e.  t  A. n  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  -.  X  =  U. n )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    /\ w3a 934   A.wal 1527   E.wex 1528    = wceq 1623    e. wcel 1684   A.wral 2543   E.wrex 2544   _Vcvv 2788    \ cdif 3149    u. cun 3150    i^i cin 3151    C_ wss 3152   ~Pcpw 3625   {csn 3640   U.cuni 3827   |^|cint 3862   U_ciun 3905   -->wf 5251   ` cfv 5255   Fincfn 6863   ficfi 7164   topGenctg 13342   TopBasesctb 16635
This theorem is referenced by:  alexsubALTlem4