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

Theorem alexsubALTlem4 18038
Description: Lemma for alexsubALT 18039. If any cover taken from a subbase has a finite subcover, any cover taken from the corresponding base has a 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
alexsubALTlem4  |-  ( J  =  ( topGen `  ( fi `  x ) )  ->  ( A. c  e.  ~P  x ( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d
)  ->  A. a  e.  ~P  ( fi `  x ) ( X  =  U. a  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
) ) )
Distinct variable groups:    a, b,
c, d, x, J    X, a, b, c, d, x

Proof of Theorem alexsubALTlem4
Dummy variables  n  s  t  u  v  w  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ralnex 2680 . . . . 5  |-  ( A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b  <->  -. 
E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b )
2 alexsubALT.1 . . . . . . . 8  |-  X  = 
U. J
32alexsubALTlem2 18036 . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  ->  E. u  e.  ( { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } ) A. v  e.  ( { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } )  -.  u  C.  v )
4 elun 3452 . . . . . . . . . 10  |-  ( u  e.  ( { z  e.  ~P ( fi
`  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } )  <->  ( u  e.  { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  \/  u  e.  { (/)
} ) )
5 sseq2 3334 . . . . . . . . . . . . 13  |-  ( z  =  u  ->  (
a  C_  z  <->  a  C_  u ) )
6 pweq 3766 . . . . . . . . . . . . . . 15  |-  ( z  =  u  ->  ~P z  =  ~P u
)
76ineq1d 3505 . . . . . . . . . . . . . 14  |-  ( z  =  u  ->  ( ~P z  i^i  Fin )  =  ( ~P u  i^i  Fin ) )
87raleqdv 2874 . . . . . . . . . . . . 13  |-  ( z  =  u  ->  ( A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b 
<-> 
A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b ) )
95, 8anbi12d 692 . . . . . . . . . . . 12  |-  ( z  =  u  ->  (
( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b )  <->  ( a  C_  u  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )
109elrab 3056 . . . . . . . . . . 11  |-  ( u  e.  { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  <->  ( u  e.  ~P ( fi `  x )  /\  (
a  C_  u  /\  A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b ) ) )
11 elsn 3793 . . . . . . . . . . 11  |-  ( u  e.  { (/) }  <->  u  =  (/) )
1210, 11orbi12i 508 . . . . . . . . . 10  |-  ( ( u  e.  { z  e.  ~P ( fi
`  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  \/  u  e.  { (/) } )  <-> 
( ( u  e. 
~P ( fi `  x )  /\  (
a  C_  u  /\  A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b ) )  \/  u  =  (/) ) )
134, 12bitri 241 . . . . . . . . 9  |-  ( u  e.  ( { z  e.  ~P ( fi
`  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } )  <->  ( (
u  e.  ~P ( fi `  x )  /\  ( a  C_  u  /\  A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b ) )  \/  u  =  (/) ) )
14 ralnex 2680 . . . . . . . . . . . . 13  |-  ( A. v  e.  ( {
z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } )  -.  u  C.  v  <->  -.  E. v  e.  ( { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } ) u  C.  v )
15 simprrl 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  a  C_  u )
1615unissd 4003 . . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  U. a  C_ 
U. u )
17 sseq1 3333 . . . . . . . . . . . . . . . 16  |-  ( X  =  U. a  -> 
( X  C_  U. u  <->  U. a  C_  U. u
) )
1816, 17syl5ibrcom 214 . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  ( X  =  U. a  ->  X  C_ 
U. u ) )
19 inss1 3525 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  i^i  u )  C_  x
20 vex 2923 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  x  e. 
_V
2120elpw2 4328 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  i^i  u )  e.  ~P x  <->  ( x  i^i  u )  C_  x
)
2219, 21mpbir 201 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  i^i  u )  e. 
~P x
23 unieq 3988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  ( x  i^i  u )  ->  U. c  =  U. ( x  i^i  u ) )
2423eqeq2d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  ( x  i^i  u )  ->  ( X  =  U. c  <->  X  =  U. ( x  i^i  u ) ) )
25 pweq 3766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( c  =  ( x  i^i  u )  ->  ~P c  =  ~P (
x  i^i  u )
)
2625ineq1d 3505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  ( x  i^i  u )  ->  ( ~P c  i^i  Fin )  =  ( ~P (
x  i^i  u )  i^i  Fin ) )
2726rexeqdv 2875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  ( x  i^i  u )  ->  ( E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d  <->  E. d  e.  ( ~P ( x  i^i  u
)  i^i  Fin ) X  =  U. d
) )
2824, 27imbi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  =  ( x  i^i  u )  ->  (
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  <->  ( X  =  U. ( x  i^i  u )  ->  E. d  e.  ( ~P ( x  i^i  u )  i^i 
Fin ) X  = 
U. d ) ) )
2928rspccv 3013 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  ->  (
( x  i^i  u
)  e.  ~P x  ->  ( X  =  U. ( x  i^i  u
)  ->  E. d  e.  ( ~P ( x  i^i  u )  i^i 
Fin ) X  = 
U. d ) ) )
3022, 29mpi 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  ->  ( X  =  U. (
x  i^i  u )  ->  E. d  e.  ( ~P ( x  i^i  u )  i^i  Fin ) X  =  U. d ) )
31 inss2 3526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  i^i  u )  C_  u
32 sstr 3320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( d  C_  ( x  i^i  u )  /\  (
x  i^i  u )  C_  u )  ->  d  C_  u )
3331, 32mpan2 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( d 
C_  ( x  i^i  u )  ->  d  C_  u )
3433anim1i 552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( d  C_  ( x  i^i  u )  /\  d  e.  Fin )  ->  (
d  C_  u  /\  d  e.  Fin )
)
35 elfpw 7370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( d  e.  ( ~P (
x  i^i  u )  i^i  Fin )  <->  ( d  C_  ( x  i^i  u
)  /\  d  e.  Fin ) )
36 elfpw 7370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( d  e.  ( ~P u  i^i  Fin )  <->  ( d  C_  u  /\  d  e. 
Fin ) )
3734, 35, 363imtr4i 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( d  e.  ( ~P (
x  i^i  u )  i^i  Fin )  ->  d  e.  ( ~P u  i^i 
Fin ) )
3837anim1i 552 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( ~P ( x  i^i  u
)  i^i  Fin )  /\  X  =  U. d )  ->  (
d  e.  ( ~P u  i^i  Fin )  /\  X  =  U. d ) )
3938reximi2 2776 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( E. d  e.  ( ~P ( x  i^i  u
)  i^i  Fin ) X  =  U. d  ->  E. d  e.  ( ~P u  i^i  Fin ) X  =  U. d )
4030, 39syl6 31 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  ->  ( X  =  U. (
x  i^i  u )  ->  E. d  e.  ( ~P u  i^i  Fin ) X  =  U. d ) )
41 unieq 3988 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( d  =  b  ->  U. d  =  U. b )
4241eqeq2d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( d  =  b  ->  ( X  =  U. d  <->  X  =  U. b ) )
4342cbvrexv 2897 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( E. d  e.  ( ~P u  i^i  Fin ) X  =  U. d  <->  E. b  e.  ( ~P u  i^i  Fin ) X  =  U. b
)
4440, 43syl6ib 218 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  ->  ( X  =  U. (
x  i^i  u )  ->  E. b  e.  ( ~P u  i^i  Fin ) X  =  U. b ) )
45 dfrex2 2683 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( E. b  e.  ( ~P u  i^i  Fin ) X  =  U. b  <->  -. 
A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b )
4644, 45syl6ib 218 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  ->  ( X  =  U. (
x  i^i  u )  ->  -.  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) )
4746con2d 109 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  ->  ( A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b  ->  -.  X  =  U. ( x  i^i  u
) ) )
4847a1d 23 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. c  e.  ~P  x
( X  =  U. c  ->  E. d  e.  ( ~P c  i^i  Fin ) X  =  U. d )  ->  (
a  C_  u  ->  ( A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b  ->  -.  X  =  U. ( x  i^i  u
) ) ) )
49483ad2ant2 979 . . . . . . . . . . . . . . . . . . . 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 ) )  -> 
( a  C_  u  ->  ( A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b  ->  -.  X  =  U. (
x  i^i  u )
) ) )
5049adantr 452 . . . . . . . . . . . . . . . . . . 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  ->  ( A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b  ->  -.  X  =  U. (
x  i^i  u )
) ) )
5150imp3a 421 . . . . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b
)  ->  -.  X  =  U. ( x  i^i  u ) ) )
5251impr 603 . . . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  -.  X  =  U. ( x  i^i  u ) )
5319unissi 4002 . . . . . . . . . . . . . . . . . . 19  |-  U. (
x  i^i  u )  C_ 
U. x
54 unieq 3988 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( J  =  ( topGen `  ( fi `  x ) )  ->  U. J  =  U. ( topGen `  ( fi `  x ) ) )
55 fiuni 7395 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  _V  ->  U. x  =  U. ( fi `  x ) )
5620, 55ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  U. x  =  U. ( fi `  x )
57 fibas 17001 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( fi
`  x )  e.  TopBases
58 unitg 16991 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( fi `  x )  e.  TopBases  ->  U. ( topGen `  ( fi `  x ) )  =  U. ( fi
`  x ) )
5957, 58ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  U. ( topGen `
 ( fi `  x ) )  = 
U. ( fi `  x )
6056, 59eqtr4i 2431 . . . . . . . . . . . . . . . . . . . . . . 23  |-  U. x  =  U. ( topGen `  ( fi `  x ) )
6154, 60syl6reqr 2459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( J  =  ( topGen `  ( fi `  x ) )  ->  U. x  =  U. J )
6261, 2syl6eqr 2458 . . . . . . . . . . . . . . . . . . . . 21  |-  ( J  =  ( topGen `  ( fi `  x ) )  ->  U. x  =  X )
63623ad2ant1 978 . . . . . . . . . . . . . . . . . . . 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. x  =  X
)
6463adantr 452 . . . . . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  U. x  =  X )
6553, 64syl5sseq 3360 . . . . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  U. (
x  i^i  u )  C_  X )
66 eqcom 2410 . . . . . . . . . . . . . . . . . . 19  |-  ( X  =  U. ( x  i^i  u )  <->  U. (
x  i^i  u )  =  X )
67 eqss 3327 . . . . . . . . . . . . . . . . . . . 20  |-  ( U. ( x  i^i  u
)  =  X  <->  ( U. ( x  i^i  u
)  C_  X  /\  X  C_  U. ( x  i^i  u ) ) )
6867baib 872 . . . . . . . . . . . . . . . . . . 19  |-  ( U. ( x  i^i  u
)  C_  X  ->  ( U. ( x  i^i  u )  =  X  <-> 
X  C_  U. (
x  i^i  u )
) )
6966, 68syl5bb 249 . . . . . . . . . . . . . . . . . 18  |-  ( U. ( x  i^i  u
)  C_  X  ->  ( X  =  U. (
x  i^i  u )  <->  X 
C_  U. ( x  i^i  u ) ) )
7065, 69syl 16 . . . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  ( X  =  U. ( x  i^i  u )  <->  X  C_  U. (
x  i^i  u )
) )
7152, 70mtbid 292 . . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  -.  X  C_ 
U. ( x  i^i  u ) )
72 sstr2 3319 . . . . . . . . . . . . . . . . 17  |-  ( X 
C_  U. u  ->  ( U. u  C_  U. (
x  i^i  u )  ->  X  C_  U. (
x  i^i  u )
) )
7372con3rr3 130 . . . . . . . . . . . . . . . 16  |-  ( -.  X  C_  U. (
x  i^i  u )  ->  ( X  C_  U. u  ->  -.  U. u  C_  U. ( x  i^i  u
) ) )
7471, 73syl 16 . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  ( X  C_ 
U. u  ->  -.  U. u  C_  U. (
x  i^i  u )
) )
75 nss 3370 . . . . . . . . . . . . . . . . 17  |-  ( -. 
U. u  C_  U. (
x  i^i  u )  <->  E. y ( y  e. 
U. u  /\  -.  y  e.  U. (
x  i^i  u )
) )
76 df-rex 2676 . . . . . . . . . . . . . . . . 17  |-  ( E. y  e.  U. u  -.  y  e.  U. (
x  i^i  u )  <->  E. y ( y  e. 
U. u  /\  -.  y  e.  U. (
x  i^i  u )
) )
7775, 76bitr4i 244 . . . . . . . . . . . . . . . 16  |-  ( -. 
U. u  C_  U. (
x  i^i  u )  <->  E. y  e.  U. u  -.  y  e.  U. (
x  i^i  u )
)
78 eluni2 3983 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  U. u  <->  E. w  e.  u  y  e.  w )
79 elpwi 3771 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( u  e.  ~P ( fi
`  x )  ->  u  C_  ( fi `  x ) )
8079sseld 3311 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  e.  ~P ( fi
`  x )  -> 
( w  e.  u  ->  w  e.  ( fi
`  x ) ) )
8180ad2antrl 709 . . . . . . . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  ( w  e.  u  ->  w  e.  ( fi `  x
) ) )
82 vex 2923 . . . . . . . . . . . . . . . . . . . . . 22  |-  w  e. 
_V
83 elfi 7380 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( w  e.  _V  /\  x  e.  _V )  ->  ( w  e.  ( fi `  x )  <->  E. t  e.  ( ~P x  i^i  Fin )
w  =  |^| t
) )
8482, 20, 83mp2an 654 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  ( fi `  x )  <->  E. t  e.  ( ~P x  i^i 
Fin ) w  = 
|^| t )
8581, 84syl6ib 218 . . . . . . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  ( w  e.  u  ->  E. t  e.  ( ~P x  i^i 
Fin ) w  = 
|^| t ) )
862alexsubALTlem3 18037 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( 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 )
8779adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( u  e.  ~P ( fi `  x )  /\  ( a  C_  u  /\  A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b ) )  ->  u  C_  ( fi `  x ) )
8887ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  ->  u  C_  ( fi `  x ) )
89 ssfii 7386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  _V  ->  x  C_  ( fi `  x
) )
9020, 89ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  x  C_  ( fi `  x )
91 inss1 3525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ~P x  i^i  Fin )  C_ 
~P x
9291sseli 3308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( t  e.  ( ~P x  i^i  Fin )  ->  t  e.  ~P x )
9392elpwid 3772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( t  e.  ( ~P x  i^i  Fin )  ->  t  C_  x )
9493ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  ->  t  C_  x )
9594ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  -> 
t  C_  x )
96 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  -> 
s  e.  t )
9795, 96sseldd 3313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  -> 
s  e.  x )
9890, 97sseldi 3310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  -> 
s  e.  ( fi
`  x ) )
9998snssd 3907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  ->  { s }  C_  ( fi `  x ) )
10088, 99unssd 3487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  -> 
( u  u.  {
s } )  C_  ( fi `  x ) )
101 fvex 5705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( fi
`  x )  e. 
_V
102101elpw2 4328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( u  u.  { s } )  e.  ~P ( fi `  x )  <-> 
( u  u.  {
s } )  C_  ( fi `  x ) )
103100, 102sylibr 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  -> 
( u  u.  {
s } )  e. 
~P ( fi `  x ) )
104 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( u  e.  ~P ( fi `  x )  /\  ( a  C_  u  /\  A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b ) )  -> 
a  C_  u )
105104ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  -> 
a  C_  u )
106 ssun1 3474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  u  C_  ( u  u.  { s } )
107105, 106syl6ss 3324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  -> 
a  C_  ( u  u.  { s } ) )
108 unieq 3988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( n  =  b  ->  U. n  =  U. b )
109108eqeq2d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( n  =  b  ->  ( X  =  U. n  <->  X  =  U. b ) )
110109notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( n  =  b  ->  ( -.  X  =  U. n 
<->  -.  X  =  U. b ) )
111110cbvralv 2896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n 
<-> 
A. b  e.  ( ~P ( u  u. 
{ s } )  i^i  Fin )  -.  X  =  U. b
)
112111biimpi 187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n  ->  A. b  e.  ( ~P ( u  u. 
{ s } )  i^i  Fin )  -.  X  =  U. b
)
113112ad2antll 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  ->  A. b  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  -.  X  =  U. b )
114103, 107, 113jca32 522 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  -> 
( ( u  u. 
{ s } )  e.  ~P ( fi
`  x )  /\  ( a  C_  (
u  u.  { s } )  /\  A. b  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. b ) ) )
115 sseq2 3334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( z  =  ( u  u. 
{ s } )  ->  ( a  C_  z 
<->  a  C_  ( u  u.  { s } ) ) )
116 pweq 3766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z  =  ( u  u. 
{ s } )  ->  ~P z  =  ~P ( u  u. 
{ s } ) )
117116ineq1d 3505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( z  =  ( u  u. 
{ s } )  ->  ( ~P z  i^i  Fin )  =  ( ~P ( u  u. 
{ s } )  i^i  Fin ) )
118117raleqdv 2874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( z  =  ( u  u. 
{ s } )  ->  ( A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b  <->  A. b  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. b ) )
119115, 118anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  ( u  u. 
{ s } )  ->  ( ( a 
C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b
)  <->  ( a  C_  ( u  u.  { s } )  /\  A. b  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. b ) ) )
120119elrab 3056 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( u  u.  { s } )  e.  {
z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  <->  ( (
u  u.  { s } )  e.  ~P ( fi `  x )  /\  ( a  C_  ( u  u.  { s } )  /\  A. b  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. b ) ) )
121114, 120sylibr 204 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  -> 
( u  u.  {
s } )  e. 
{ z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) } )
122 elun1 3478 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( u  u.  { s } )  e.  {
z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  ->  ( u  u.  { s } )  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } ) )
123121, 122syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  -> 
( u  u.  {
s } )  e.  ( { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } ) )
124 vex 2923 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  s  e. 
_V
125124snid 3805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  s  e. 
{ s }
126 elun2 3479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( s  e.  { s }  ->  s  e.  ( u  u.  { s } ) )
127125, 126ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  s  e.  ( u  u.  {
s } )
128 intss1 4029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( s  e.  t  ->  |^| t  C_  s )
129 sseq1 3333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( w  =  |^| t  -> 
( w  C_  s  <->  |^| t  C_  s )
)
130128, 129syl5ibrcom 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( s  e.  t  ->  (
w  =  |^| t  ->  w  C_  s )
)
131130impcom 420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( w  =  |^| t  /\  s  e.  t
)  ->  w  C_  s
)
132131adantll 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  s  e.  t )  ->  w  C_  s )
133132adantlr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ( t  e.  ( ~P x  i^i 
Fin )  /\  w  =  |^| t )  /\  y  e.  w )  /\  s  e.  t
)  ->  w  C_  s
)
134133adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( w  e.  u  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  y  e.  w )  /\  s  e.  t
) )  ->  w  C_  s )
135134adantrrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( w  e.  u  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  y  e.  w )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) ) )  ->  w  C_  s
)
136135adantll 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( 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 )  /\  (
s  e.  t  /\  A. n  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  -.  X  =  U. n ) ) )  ->  w  C_  s
)
137 simprlr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( 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 )  /\  (
s  e.  t  /\  A. n  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  -.  X  =  U. n ) ) )  ->  y  e.  w )
138136, 137sseldd 3313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( 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 )  /\  (
s  e.  t  /\  A. n  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  -.  X  =  U. n ) ) )  ->  y  e.  s )
13993ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  y  e.  w )  ->  t  C_  x )
140139ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( 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 )  /\  (
s  e.  t  /\  A. n  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  -.  X  =  U. n ) ) )  ->  t  C_  x )
141 simprrl 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( 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 )  /\  (
s  e.  t  /\  A. n  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  -.  X  =  U. n ) ) )  ->  s  e.  t )
142140, 141sseldd 3313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( 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 )  /\  (
s  e.  t  /\  A. n  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  -.  X  =  U. n ) ) )  ->  s  e.  x )
143 elin 3494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( s  e.  ( x  i^i  u )  <->  ( s  e.  x  /\  s  e.  u ) )
144 elunii 3984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( y  e.  s  /\  s  e.  ( x  i^i  u ) )  -> 
y  e.  U. (
x  i^i  u )
)
145144ex 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( y  e.  s  ->  (
s  e.  ( x  i^i  u )  -> 
y  e.  U. (
x  i^i  u )
) )
146143, 145syl5bir 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( y  e.  s  ->  (
( s  e.  x  /\  s  e.  u
)  ->  y  e.  U. ( x  i^i  u
) ) )
147146exp3a 426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  e.  s  ->  (
s  e.  x  -> 
( s  e.  u  ->  y  e.  U. (
x  i^i  u )
) ) )
148138, 142, 147sylc 58 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( 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 )  /\  (
s  e.  t  /\  A. n  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  -.  X  =  U. n ) ) )  ->  ( s  e.  u  ->  y  e. 
U. ( x  i^i  u ) ) )
149148con3d 127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( 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 )  /\  (
s  e.  t  /\  A. n  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  -.  X  =  U. n ) ) )  ->  ( -.  y  e.  U. (
x  i^i  u )  ->  -.  s  e.  u
) )
150149expr 599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( 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 ) )  -> 
( ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n )  ->  ( -.  y  e.  U. (
x  i^i  u )  ->  -.  s  e.  u
) ) )
151150com23 74 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( 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 )  ->  (
( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n )  ->  -.  s  e.  u )
) )
152151exp32 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( 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 )  ->  (
( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n )  ->  -.  s  e.  u )
) ) ) )
153152imp55 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  ->  -.  s  e.  u
)
154 eleq1 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( v  =  s  ->  (
v  e.  ( u  u.  { s } )  <->  s  e.  ( u  u.  { s } ) ) )
155 elequ1 1724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( v  =  s  ->  (
v  e.  u  <->  s  e.  u ) )
156155notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( v  =  s  ->  ( -.  v  e.  u  <->  -.  s  e.  u ) )
157154, 156anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( v  =  s  ->  (
( v  e.  ( u  u.  { s } )  /\  -.  v  e.  u )  <->  ( s  e.  ( u  u.  { s } )  /\  -.  s  e.  u ) ) )
158124, 157spcev 3007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( s  e.  ( u  u.  { s } )  /\  -.  s  e.  u )  ->  E. v
( v  e.  ( u  u.  { s } )  /\  -.  v  e.  u )
)
159127, 153, 158sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  ->  E. v ( v  e.  ( u  u.  {
s } )  /\  -.  v  e.  u
) )
160 nss 3370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( -.  ( u  u.  {
s } )  C_  u 
<->  E. v ( v  e.  ( u  u. 
{ s } )  /\  -.  v  e.  u ) )
161159, 160sylibr 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  ->  -.  ( u  u.  {
s } )  C_  u )
162 eqimss2 3365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( u  =  ( u  u. 
{ s } )  ->  ( u  u. 
{ s } ) 
C_  u )
163162necon3bi 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( -.  ( u  u.  {
s } )  C_  u  ->  u  =/=  (
u  u.  { s } ) )
164161, 163syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  ->  u  =/=  ( u  u. 
{ s } ) )
165164, 106jctil 524 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  -> 
( u  C_  (
u  u.  { s } )  /\  u  =/=  ( u  u.  {
s } ) ) )
166 df-pss 3300 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( u 
C.  ( u  u. 
{ s } )  <-> 
( u  C_  (
u  u.  { s } )  /\  u  =/=  ( u  u.  {
s } ) ) )
167165, 166sylibr 204 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  ->  u  C.  ( u  u. 
{ s } ) )
168 psseq2 3399 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( v  =  ( u  u. 
{ s } )  ->  ( u  C.  v 
<->  u  C.  ( u  u.  { s } ) ) )
169168rspcev 3016 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( u  u.  {
s } )  e.  ( { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } )  /\  u  C.  ( u  u.  {
s } ) )  ->  E. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } ) u  C.  v )
170123, 167, 169syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( 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 )
) ) )  /\  ( s  e.  t  /\  A. n  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. n ) )  ->  E. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } ) u  C.  v )
17186, 170rexlimddv 2798 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } ) u  C.  v )
172171exp45 598 . . . . . . . . . . . . . . . . . . . . . . 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  /\  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. v  e.  ( { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } ) u  C.  v ) ) ) )
173172exp3a 426 . . . . . . . . . . . . . . . . . . . . . 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  /\  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. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } ) u  C.  v ) ) ) ) )
174173rexlimdv 2793 . . . . . . . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  /\  w  e.  u )  ->  ( E. t  e.  ( ~P x  i^i  Fin )
w  =  |^| t  ->  ( y  e.  w  ->  ( -.  y  e. 
U. ( x  i^i  u )  ->  E. v  e.  ( { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } ) u  C.  v ) ) ) )
175174ex 424 . . . . . . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  ( w  e.  u  ->  ( E. t  e.  ( ~P x  i^i  Fin )
w  =  |^| t  ->  ( y  e.  w  ->  ( -.  y  e. 
U. ( x  i^i  u )  ->  E. v  e.  ( { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } ) u  C.  v ) ) ) ) )
17685, 175mpdd 38 . . . . . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  ( w  e.  u  ->  ( y  e.  w  ->  ( -.  y  e.  U. (
x  i^i  u )  ->  E. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } ) u  C.  v ) ) ) )
177176rexlimdv 2793 . . . . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  ( E. w  e.  u  y  e.  w  ->  ( -.  y  e.  U. (
x  i^i  u )  ->  E. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } ) u  C.  v ) ) )
17878, 177syl5bi 209 . . . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  ( y  e.  U. u  ->  ( -.  y  e.  U. (
x  i^i  u )  ->  E. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } ) u  C.  v ) ) )
179178rexlimdv 2793 . . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  ( E. y  e.  U. u  -.  y  e.  U. (
x  i^i  u )  ->  E. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } ) u  C.  v ) )
18077, 179syl5bi 209 . . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  ( -.  U. u  C_  U. (
x  i^i  u )  ->  E. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } ) u  C.  v ) )
18118, 74, 1803syld 53 . . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  ( X  =  U. a  ->  E. v  e.  ( { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } ) u  C.  v ) )
182181con3d 127 . . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  ( -.  E. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } ) u  C.  v  ->  -.  X  =  U. a ) )
18314, 182syl5bi 209 . . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) ) )  ->  ( A. v  e.  ( {
z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } )  -.  u  C.  v  ->  -.  X  =  U. a ) )
184183ex 424 . . . . . . . . . . 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  /\  A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b ) )  -> 
( A. v  e.  ( { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } )  -.  u  C.  v  ->  -.  X  =  U. a ) ) )
185184adantr 452 . . . . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  ->  (
( u  e.  ~P ( fi `  x )  /\  ( a  C_  u  /\  A. b  e.  ( ~P u  i^i 
Fin )  -.  X  =  U. b ) )  ->  ( A. v  e.  ( { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } )  -.  u  C.  v  ->  -.  X  =  U. a ) ) )
186 ssun1 3474 . . . . . . . . . . . . . 14  |-  { z  e.  ~P ( fi
`  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  C_  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } )
187 simpll3 998 . . . . . . . . . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  /\  u  =  (/) )  ->  a  e.  ~P ( fi `  x ) )
188 simplr 732 . . . . . . . . . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  /\  u  =  (/) )  ->  A. b  e.  ( ~P a  i^i 
Fin )  -.  X  =  U. b )
189 eqimss2 3365 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  a  ->  a  C_  z )
190189biantrurd 495 . . . . . . . . . . . . . . . . 17  |-  ( z  =  a  ->  ( A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b 
<->  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) ) )
191 pweq 3766 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  a  ->  ~P z  =  ~P a
)
192191ineq1d 3505 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  a  ->  ( ~P z  i^i  Fin )  =  ( ~P a  i^i  Fin ) )
193192raleqdv 2874 . . . . . . . . . . . . . . . . 17  |-  ( z  =  a  ->  ( A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b 
<-> 
A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b ) )
194190, 193bitr3d 247 . . . . . . . . . . . . . . . 16  |-  ( z  =  a  ->  (
( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b )  <->  A. b  e.  ( ~P a  i^i 
Fin )  -.  X  =  U. b ) )
195194elrab 3056 . . . . . . . . . . . . . . 15  |-  ( a  e.  { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  <->  ( a  e.  ~P ( fi `  x )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b
) )
196187, 188, 195sylanbrc 646 . . . . . . . . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  /\  u  =  (/) )  ->  a  e.  { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) } )
197186, 196sseldi 3310 . . . . . . . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  /\  u  =  (/) )  ->  a  e.  ( { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } ) )
198 psseq2 3399 . . . . . . . . . . . . . . 15  |-  ( v  =  a  ->  (
u  C.  v  <->  u  C.  a ) )
199198notbid 286 . . . . . . . . . . . . . 14  |-  ( v  =  a  ->  ( -.  u  C.  v  <->  -.  u  C.  a ) )
200199rspcv 3012 . . . . . . . . . . . . 13  |-  ( a  e.  ( { z  e.  ~P ( fi
`  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } )  ->  ( A. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } )  -.  u  C.  v  ->  -.  u  C.  a
) )
201197, 200syl 16 . . . . . . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  /\  u  =  (/) )  ->  ( A. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } )  -.  u  C.  v  ->  -.  u  C.  a
) )
202 id 20 . . . . . . . . . . . . . . . . 17  |-  ( a  =  (/)  ->  a  =  (/) )
203 0elpw 4333 . . . . . . . . . . . . . . . . . 18  |-  (/)  e.  ~P a
204 0fin 7299 . . . . . . . . . . . . . . . . . 18  |-  (/)  e.  Fin
205 elin 3494 . . . . . . . . . . . . . . . . . 18  |-  ( (/)  e.  ( ~P a  i^i 
Fin )  <->  ( (/)  e.  ~P a  /\  (/)  e.  Fin )
)
206203, 204, 205mpbir2an 887 . . . . . . . . . . . . . . . . 17  |-  (/)  e.  ( ~P a  i^i  Fin )
207202, 206syl6eqel 2496 . . . . . . . . . . . . . . . 16  |-  ( a  =  (/)  ->  a  e.  ( ~P a  i^i 
Fin ) )
208 unieq 3988 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  a  ->  U. b  =  U. a )
209208eqeq2d 2419 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  a  ->  ( X  =  U. b  <->  X  =  U. a ) )
210209notbid 286 . . . . . . . . . . . . . . . . 17  |-  ( b  =  a  ->  ( -.  X  =  U. b 
<->  -.  X  =  U. a ) )
211210rspccv 3013 . . . . . . . . . . . . . . . 16  |-  ( A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b  ->  ( a  e.  ( ~P a  i^i  Fin )  ->  -.  X  =  U. a ) )
212207, 211syl5 30 . . . . . . . . . . . . . . 15  |-  ( A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b  ->  ( a  =  (/)  ->  -.  X  =  U. a ) )
213212necon2ad 2619 . . . . . . . . . . . . . 14  |-  ( A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b  ->  ( X  =  U. a  ->  a  =/=  (/) ) )
214213ad2antlr 708 . . . . . . . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  /\  u  =  (/) )  ->  ( X  =  U. a  ->  a  =/=  (/) ) )
215 psseq1 3398 . . . . . . . . . . . . . . 15  |-  ( u  =  (/)  ->  ( u 
C.  a  <->  (/)  C.  a
) )
216215adantl 453 . . . . . . . . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  /\  u  =  (/) )  ->  (
u  C.  a  <->  (/)  C.  a
) )
217 0pss 3629 . . . . . . . . . . . . . 14  |-  ( (/)  C.  a  <->  a  =/=  (/) )
218216, 217syl6bb 253 . . . . . . . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  /\  u  =  (/) )  ->  (
u  C.  a  <->  a  =/=  (/) ) )
219214, 218sylibrd 226 . . . . . . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  /\  u  =  (/) )  ->  ( X  =  U. a  ->  u  C.  a ) )
220201, 219nsyld 134 . . . . . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  /\  u  =  (/) )  ->  ( A. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } )  -.  u  C.  v  ->  -.  X  =  U. a ) )
221220ex 424 . . . . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  ->  (
u  =  (/)  ->  ( A. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } )  -.  u  C.  v  ->  -.  X  =  U. a ) ) )
222185, 221jaod 370 . . . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  ->  (
( ( u  e. 
~P ( fi `  x )  /\  (
a  C_  u  /\  A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b ) )  \/  u  =  (/) )  -> 
( A. v  e.  ( { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } )  -.  u  C.  v  ->  -.  X  =  U. a ) ) )
22313, 222syl5bi 209 . . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  ->  (
u  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } )  ->  ( A. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } )  -.  u  C.  v  ->  -.  X  =  U. a ) ) )
224223rexlimdv 2793 . . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  ->  ( E. u  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } ) A. v  e.  ( { z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) }  u.  { (/) } )  -.  u  C.  v  ->  -.  X  =  U. a ) )
2253, 224mpd 15 . . . . . 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 ) )  /\  A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b )  ->  -.  X  =  U. a
)
226225ex 424 . . . . 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 ) )  -> 
( A. b  e.  ( ~P a  i^i 
Fin )  -.  X  =  U. b  ->  -.  X  =  U. a
) )
2271, 226syl5bir 210 . . . 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 ) )  -> 
( -.  E. b  e.  ( ~P a  i^i 
Fin ) X  = 
U. b  ->  -.  X  =  U. a
) )
228227con4d 99 . . 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 ) )  -> 
( X  =  U. a  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b ) )
2292283exp 1152 . 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 )  ->  ( X  =  U. a  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b ) ) ) )
230229ralrimdv 2759 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. a  e.  ~P  ( fi `  x ) ( X  =  U. a  ->  E. b  e.  ( ~P a  i^i  Fin ) X  =  U. b
) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    /\ w3a 936   E.wex 1547    = wceq 1649    e. wcel 1721    =/= wne 2571   A.wral 2670   E.wrex 2671   {crab 2674   _Vcvv 2920    u. cun 3282    i^i cin 3283    C_ wss 3284    C. wpss 3285   (/)c0 3592   ~Pcpw 3763   {csn 3778   U.cuni 3979   |^|cint 4014   ` cfv 5417   Fincfn 7072   ficfi 7377   topGenctg 13624   TopBasesctb 16921
This theorem is referenced by:  alexsubALT  18039
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-rep 4284  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664  ax-ac2 8303
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-reu 2677  df-rmo 2678  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-pss 3300  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-tp 3786  df-op 3787  df-uni 3980  df-int 4015  df-iun 4059  df-br 4177  df-opab 4231  df-mpt 4232  df-tr 4267  df-eprel 4458  df-id 4462  df-po 4467  df-so 4468  df-fr 4505  df-se 4506  df-we 4507  df-ord 4548  df-on 4549  df-lim 4550  df-suc 4551  df-om 4809  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-isom 5426  df-ov 6047  df-oprab 6048  df-mpt2 6049  df-rpss 6485  df-riota 6512  df-recs 6596  df-rdg 6631  df-1o 6687  df-oadd 6691  df-er 6868  df-en 7073  df-fin 7076  df-fi 7378  df-card 7786  df-ac 7957  df-topgen 13626  df-bases 16924
  Copyright terms: Public domain W3C validator