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

Theorem alexsubALTlem4 17744
Description: Lemma for alexsubALT 17745. 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 2553 . . . . 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 17742 . . . . . . 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 3316 . . . . . . . . . 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 3200 . . . . . . . . . . . . 13  |-  ( z  =  u  ->  (
a  C_  z  <->  a  C_  u ) )
6 pweq 3628 . . . . . . . . . . . . . . 15  |-  ( z  =  u  ->  ~P z  =  ~P u
)
76ineq1d 3369 . . . . . . . . . . . . . 14  |-  ( z  =  u  ->  ( ~P z  i^i  Fin )  =  ( ~P u  i^i  Fin ) )
87raleqdv 2742 . . . . . . . . . . . . 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 691 . . . . . . . . . . . 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 2923 . . . . . . . . . . 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 3655 . . . . . . . . . . 11  |-  ( u  e.  { (/) }  <->  u  =  (/) )
1210, 11orbi12i 507 . . . . . . . . . 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 240 . . . . . . . . 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 2553 . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . . . . 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 )
16 uniss 3848 . . . . . . . . . . . . . . . . 17  |-  ( a 
C_  u  ->  U. a  C_ 
U. u )
1715, 16syl 15 . . . . . . . . . . . . . . . 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 )
18 sseq1 3199 . . . . . . . . . . . . . . . 16  |-  ( X  =  U. a  -> 
( X  C_  U. u  <->  U. a  C_  U. u
) )
1917, 18syl5ibrcom 213 . . . . . . . . . . . . . . 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 ) )
20 inss1 3389 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  i^i  u )  C_  x
21 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  x  e. 
_V
2221elpw2 4175 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  i^i  u )  e.  ~P x  <->  ( x  i^i  u )  C_  x
)
2320, 22mpbir 200 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  i^i  u )  e. 
~P x
24 unieq 3836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  ( x  i^i  u )  ->  U. c  =  U. ( x  i^i  u ) )
2524eqeq2d 2294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  ( x  i^i  u )  ->  ( X  =  U. c  <->  X  =  U. ( x  i^i  u ) ) )
26 pweq 3628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( c  =  ( x  i^i  u )  ->  ~P c  =  ~P (
x  i^i  u )
)
2726ineq1d 3369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  ( x  i^i  u )  ->  ( ~P c  i^i  Fin )  =  ( ~P (
x  i^i  u )  i^i  Fin ) )
2827rexeqdv 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
2925, 28imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
3029rspccv 2881 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
3123, 30mpi 16 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
32 inss2 3390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  i^i  u )  C_  u
33 sstr 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( d  C_  ( x  i^i  u )  /\  (
x  i^i  u )  C_  u )  ->  d  C_  u )
3432, 33mpan2 652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( d 
C_  ( x  i^i  u )  ->  d  C_  u )
3534anim1i 551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( d  C_  ( x  i^i  u )  /\  d  e.  Fin )  ->  (
d  C_  u  /\  d  e.  Fin )
)
36 elfpw 7157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( d  e.  ( ~P (
x  i^i  u )  i^i  Fin )  <->  ( d  C_  ( x  i^i  u
)  /\  d  e.  Fin ) )
37 elfpw 7157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( d  e.  ( ~P u  i^i  Fin )  <->  ( d  C_  u  /\  d  e. 
Fin ) )
3835, 36, 373imtr4i 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( d  e.  ( ~P (
x  i^i  u )  i^i  Fin )  ->  d  e.  ( ~P u  i^i 
Fin ) )
3938anim1i 551 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( d  e.  ( ~P ( x  i^i  u
)  i^i  Fin )  /\  X  =  U. d )  ->  (
d  e.  ( ~P u  i^i  Fin )  /\  X  =  U. d ) )
4039reximi2 2649 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
4131, 40syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
42 unieq 3836 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( d  =  b  ->  U. d  =  U. b )
4342eqeq2d 2294 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( d  =  b  ->  ( X  =  U. d  <->  X  =  U. b ) )
4443cbvrexv 2765 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( E. d  e.  ( ~P u  i^i  Fin ) X  =  U. d  <->  E. b  e.  ( ~P u  i^i  Fin ) X  =  U. b
)
4541, 44syl6ib 217 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
46 dfrex2 2556 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( E. b  e.  ( ~P u  i^i  Fin ) X  =  U. b  <->  -. 
A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b )
4745, 46syl6ib 217 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
4847con2d 107 . . . . . . . . . . . . . . . . . . . . . 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
) ) )
4948a1d 22 . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
50493ad2ant2 977 . . . . . . . . . . . . . . . . . . . 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 )
) ) )
5150adantr 451 . . . . . . . . . . . . . . . . . . 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 )
) ) )
5251imp3a 420 . . . . . . . . . . . . . . . . . 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 ) ) )
5352impr 602 . . . . . . . . . . . . . . . . 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 ) )
54 uniss 3848 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  i^i  u ) 
C_  x  ->  U. (
x  i^i  u )  C_ 
U. x )
5520, 54ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  U. (
x  i^i  u )  C_ 
U. x
56 unieq 3836 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( J  =  ( topGen `  ( fi `  x ) )  ->  U. J  =  U. ( topGen `  ( fi `  x ) ) )
57 fiuni 7181 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  _V  ->  U. x  =  U. ( fi `  x ) )
5821, 57ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  U. x  =  U. ( fi `  x )
59 fibas 16715 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( fi
`  x )  e.  TopBases
60 unitg 16705 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( fi `  x )  e.  TopBases  ->  U. ( topGen `  ( fi `  x ) )  =  U. ( fi
`  x ) )
6159, 60ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  U. ( topGen `
 ( fi `  x ) )  = 
U. ( fi `  x )
6258, 61eqtr4i 2306 . . . . . . . . . . . . . . . . . . . . . . 23  |-  U. x  =  U. ( topGen `  ( fi `  x ) )
6356, 62syl6reqr 2334 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( J  =  ( topGen `  ( fi `  x ) )  ->  U. x  =  U. J )
6463, 2syl6eqr 2333 . . . . . . . . . . . . . . . . . . . . 21  |-  ( J  =  ( topGen `  ( fi `  x ) )  ->  U. x  =  X )
65643ad2ant1 976 . . . . . . . . . . . . . . . . . . . 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
)
6665adantr 451 . . . . . . . . . . . . . . . . . . 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 )
6755, 66syl5sseq 3226 . . . . . . . . . . . . . . . . . 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 )
68 eqcom 2285 . . . . . . . . . . . . . . . . . . 19  |-  ( X  =  U. ( x  i^i  u )  <->  U. (
x  i^i  u )  =  X )
69 eqss 3194 . . . . . . . . . . . . . . . . . . . 20  |-  ( U. ( x  i^i  u
)  =  X  <->  ( U. ( x  i^i  u
)  C_  X  /\  X  C_  U. ( x  i^i  u ) ) )
7069baib 871 . . . . . . . . . . . . . . . . . . 19  |-  ( U. ( x  i^i  u
)  C_  X  ->  ( U. ( x  i^i  u )  =  X  <-> 
X  C_  U. (
x  i^i  u )
) )
7168, 70syl5bb 248 . . . . . . . . . . . . . . . . . 18  |-  ( U. ( x  i^i  u
)  C_  X  ->  ( X  =  U. (
x  i^i  u )  <->  X 
C_  U. ( x  i^i  u ) ) )
7267, 71syl 15 . . . . . . . . . . . . . . . . 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 )
) )
7353, 72mtbid 291 . . . . . . . . . . . . . . . 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 ) )
74 sstr2 3186 . . . . . . . . . . . . . . . . 17  |-  ( X 
C_  U. u  ->  ( U. u  C_  U. (
x  i^i  u )  ->  X  C_  U. (
x  i^i  u )
) )
7574con3rr3 128 . . . . . . . . . . . . . . . 16  |-  ( -.  X  C_  U. (
x  i^i  u )  ->  ( X  C_  U. u  ->  -.  U. u  C_  U. ( x  i^i  u
) ) )
7673, 75syl 15 . . . . . . . . . . . . . . 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 )
) )
77 nss 3236 . . . . . . . . . . . . . . . . 17  |-  ( -. 
U. u  C_  U. (
x  i^i  u )  <->  E. y ( y  e. 
U. u  /\  -.  y  e.  U. (
x  i^i  u )
) )
78 df-rex 2549 . . . . . . . . . . . . . . . . 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 )
) )
7977, 78bitr4i 243 . . . . . . . . . . . . . . . 16  |-  ( -. 
U. u  C_  U. (
x  i^i  u )  <->  E. y  e.  U. u  -.  y  e.  U. (
x  i^i  u )
)
80 eluni2 3831 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  U. u  <->  E. w  e.  u  y  e.  w )
81 elpwi 3633 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( u  e.  ~P ( fi
`  x )  ->  u  C_  ( fi `  x ) )
8281sseld 3179 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  e.  ~P ( fi
`  x )  -> 
( w  e.  u  ->  w  e.  ( fi
`  x ) ) )
8382ad2antrl 708 . . . . . . . . . . . . . . . . . . . . 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
) ) )
84 vex 2791 . . . . . . . . . . . . . . . . . . . . . 22  |-  w  e. 
_V
85 elfi 7167 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( w  e.  _V  /\  x  e.  _V )  ->  ( w  e.  ( fi `  x )  <->  E. t  e.  ( ~P x  i^i  Fin )
w  =  |^| t
) )
8684, 21, 85mp2an 653 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  ( fi `  x )  <->  E. t  e.  ( ~P x  i^i 
Fin ) w  = 
|^| t )
8783, 86syl6ib 217 . . . . . . . . . . . . . . . . . . . 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 ) )
882alexsubALTlem3 17743 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
8981adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( u  e.  ~P ( fi `  x )  /\  ( a  C_  u  /\  A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b ) )  ->  u  C_  ( fi `  x ) )
9089ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )  ->  u  C_  ( fi `  x
) )
9190ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  u  C_  ( fi `  x ) )
92 ssfii 7172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  e.  _V  ->  x  C_  ( fi `  x
) )
9321, 92ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  x  C_  ( fi `  x )
94 inss1 3389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ~P x  i^i  Fin )  C_ 
~P x
9594sseli 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( t  e.  ( ~P x  i^i  Fin )  ->  t  e.  ~P x )
96 elpwi 3633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( t  e.  ~P x  -> 
t  C_  x )
9795, 96syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( t  e.  ( ~P x  i^i  Fin )  ->  t  C_  x )
9897ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  (
y  e.  w  /\  -.  y  e.  U. (
x  i^i  u )
) )  ->  t  C_  x )
9998ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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  /\  -.  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 )
100 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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  /\  -.  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 )
10199, 100sseldd 3181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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  /\  -.  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 )
10293, 101sseldi 3178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  ( fi
`  x ) )
103102snssd 3760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 }  C_  ( fi `  x ) )
10491, 103unssd 3351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  -> 
( u  u.  {
s } )  C_  ( fi `  x ) )
105 fvex 5539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( fi
`  x )  e. 
_V
106105elpw2 4175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( u  u.  { s } )  e.  ~P ( fi `  x )  <-> 
( u  u.  {
s } )  C_  ( fi `  x ) )
107104, 106sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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  u.  {
s } )  e. 
~P ( fi `  x ) )
108 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( u  e.  ~P ( fi `  x )  /\  ( a  C_  u  /\  A. b  e.  ( ~P u  i^i  Fin )  -.  X  =  U. b ) )  -> 
a  C_  u )
109108ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )  ->  a  C_  u )
110109ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  -> 
a  C_  u )
111 ssun1 3338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  u  C_  ( u  u.  { s } )
112110, 111syl6ss 3191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  -> 
a  C_  ( u  u.  { s } ) )
113 unieq 3836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( n  =  b  ->  U. n  =  U. b )
114113eqeq2d 2294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( n  =  b  ->  ( X  =  U. n  <->  X  =  U. b ) )
115114notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( n  =  b  ->  ( -.  X  =  U. n 
<->  -.  X  =  U. b ) )
116115cbvralv 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 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
)
117116biimpi 186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 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
)
118117ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  A. b  e.  ( ~P ( u  u.  {
s } )  i^i 
Fin )  -.  X  =  U. b )
119107, 112, 118jca32 521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 } )  e.  ~P ( fi
`  x )  /\  ( a  C_  (
u  u.  { s } )  /\  A. b  e.  ( ~P ( u  u.  { s } )  i^i  Fin )  -.  X  =  U. b ) ) )
120 sseq2 3200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z  =  ( u  u. 
{ s } )  ->  ( a  C_  z 
<->  a  C_  ( u  u.  { s } ) ) )
121 pweq 3628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  ( u  u. 
{ s } )  ->  ~P z  =  ~P ( u  u. 
{ s } ) )
122121ineq1d 3369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  =  ( u  u. 
{ s } )  ->  ( ~P z  i^i  Fin )  =  ( ~P ( u  u. 
{ s } )  i^i  Fin ) )
123122raleqdv 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 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 ) )
124120, 123anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 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 ) ) )
125124elrab 2923 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 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 ) ) )
126119, 125sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. 
{ z  e.  ~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i 
Fin )  -.  X  =  U. b ) } )
127 elun1 3342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 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.  { (/) } ) )
128126, 127syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  ( { z  e. 
~P ( fi `  x )  |  ( a  C_  z  /\  A. b  e.  ( ~P z  i^i  Fin )  -.  X  =  U. b ) }  u.  {
(/) } ) )
129 vex 2791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  s  e. 
_V
130129snid 3667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  s  e. 
{ s }
131 elun2 3343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( s  e.  { s }  ->  s  e.  ( u  u.  { s } ) )
132130, 131ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  s  e.  ( u  u.  {
s } )
133 intss1 3877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( s  e.  t  ->  |^| t  C_  s )
134 sseq1 3199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( w  =  |^| t  -> 
( w  C_  s  <->  |^| t  C_  s )
)
135133, 134syl5ibrcom 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( s  e.  t  ->  (
w  =  |^| t  ->  w  C_  s )
)
136135impcom 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( w  =  |^| t  /\  s  e.  t
)  ->  w  C_  s
)
137136adantll 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  s  e.  t )  ->  w  C_  s )
138137adantlr 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( ( t  e.  ( ~P x  i^i 
Fin )  /\  w  =  |^| t )  /\  y  e.  w )  /\  s  e.  t
)  ->  w  C_  s
)
139138adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( w  e.  u  /\  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  y  e.  w )  /\  s  e.  t
) )  ->  w  C_  s )
140139adantrrr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( 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
)
141140adantll 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( ( 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
)
142 simprlr 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( ( 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 )
143141, 142sseldd 3181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( ( 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 )
14497ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( t  e.  ( ~P x  i^i  Fin )  /\  w  =  |^| t )  /\  y  e.  w )  ->  t  C_  x )
145144ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( ( 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 )
146 simprrl 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( ( 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 )
147145, 146sseldd 3181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( ( 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 )
148 elin 3358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( s  e.  ( x  i^i  u )  <->  ( s  e.  x  /\  s  e.  u ) )
149 elunii 3832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( y  e.  s  /\  s  e.  ( x  i^i  u ) )  -> 
y  e.  U. (
x  i^i  u )
)
150149ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( y  e.  s  ->  (
s  e.  ( x  i^i  u )  -> 
y  e.  U. (
x  i^i  u )
) )
151148, 150syl5bir 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( y  e.  s  ->  (
( s  e.  x  /\  s  e.  u
)  ->  y  e.  U. ( x  i^i  u
) ) )
152151exp3a 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( y  e.  s  ->  (
s  e.  x  -> 
( s  e.  u  ->  y  e.  U. (
x  i^i  u )
) ) )
153143, 147, 152sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  u  ->  y  e. 
U. ( x  i^i  u ) ) )
154153con3d 125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  U. (
x  i^i  u )  ->  -.  s  e.  u
) )
155154expr 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )  ->  ( -.  y  e.  U. (
x  i^i  u )  ->  -.  s  e.  u
) ) )
156155com23 72 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  -> 
( -.  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 )
) )
157156exp32 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  u )
) ) ) )
158157imp55 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
159 eleq1 2343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( v  =  s  ->  (
v  e.  ( u  u.  { s } )  <->  s  e.  ( u  u.  { s } ) ) )
160 elequ1 1687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( v  =  s  ->  (
v  e.  u  <->  s  e.  u ) )
161160notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( v  =  s  ->  ( -.  v  e.  u  <->  -.  s  e.  u ) )
162159, 161anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( v  =  s  ->  (
( v  e.  ( u  u.  { s } )  /\  -.  v  e.  u )  <->  ( s  e.  ( u  u.  { s } )  /\  -.  s  e.  u ) ) )
163129, 162spcev 2875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( s  e.  ( u  u.  { s } )  /\  -.  s  e.  u )  ->  E. v
( v  e.  ( u  u.  { s } )  /\  -.  v  e.  u )
)
164132, 158, 163sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  E. v ( v  e.  ( u  u.  {
s } )  /\  -.  v  e.  u
) )
165 nss 3236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( -.  ( u  u.  {
s } )  C_  u 
<->  E. v ( v  e.  ( u  u. 
{ s } )  /\  -.  v  e.  u ) )
166164, 165sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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  u.  {
s } )  C_  u )
167 eqimss2 3231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( u  =  ( u  u. 
{ s } )  ->  ( u  u. 
{ s } ) 
C_  u )
168167necon3bi 2487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( -.  ( u  u.  {
s } )  C_  u  ->  u  =/=  (
u  u.  { s } ) )
169166, 168syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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  u. 
{ s } ) )
170169, 111jctil 523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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  C_  (
u  u.  { s } )  /\  u  =/=  ( u  u.  {
s } ) ) )
171 df-pss 3168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( u 
C.  ( u  u. 
{ s } )  <-> 
( u  C_  (
u  u.  { s } )  /\  u  =/=  ( u  u.  {
s } ) ) )
172170, 171sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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  C.  ( u  u. 
{ s } ) )
173 psseq2 3264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( v  =  ( u  u. 
{ s } )  ->  ( u  C.  v 
<->  u  C.  ( u  u.  { s } ) ) )
174173rspcev 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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  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 )
175128, 172, 174syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  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 )
176175exp32 588 . . . . . . . . . . . . . . . . . . . . . . . . . 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  ->  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 2666 . . . . . . . . . . . . . . . . . . . . . . . . 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  ->  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 ) )
17888, 177mpd 14 . . . . . . . . . . . . . . . . . . . . . . . 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 )
179178exp45 597 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
180179exp3a 425 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
181180rexlimdv 2666 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
182181ex 423 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
18387, 182mpdd 36 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
184183rexlimdv 2666 . . . . . . . . . . . . . . . . . 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 ) ) )
18580, 184syl5bi 208 . . . . . . . . . . . . . . . . 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 ) ) )
186185rexlimdv 2666 . . . . . . . . . . . . . . . 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 ) )
18779, 186syl5bi 208 . . . . . . . . . . . . . . 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 ) )
18819, 76, 1873syld 51 . . . . . . . . . . . . . 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 ) )
189188con3d 125 . . . . . . . . . . . . 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 ) )
19014, 189syl5bi 208 . . . . . . . . . . . 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 ) )
191190ex 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  /\  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 ) ) )
192191adantr 451 . . . . . . . . . 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 ) ) )
193 ssun1 3338 . . . . . . . . . . . . . 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.  { (/) } )
194 simpll3 996 . . . . . . . . . . . . . . 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 ) )
195 simplr 731 . . . . . . . . . . . . . . 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 )
196 eqimss2 3231 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  a  ->  a  C_  z )
197196biantrurd 494 . . . . . . . . . . . . . . . . 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 ) ) )
198 pweq 3628 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  a  ->  ~P z  =  ~P a
)
199198ineq1d 3369 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  a  ->  ( ~P z  i^i  Fin )  =  ( ~P a  i^i  Fin ) )
200199raleqdv 2742 . . . . . . . . . . . . . . . . 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 ) )
201197, 200bitr3d 246 . . . . . . . . . . . . . . . 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 ) )
202201elrab 2923 . . . . . . . . . . . . . . 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
) )
203194, 195, 202sylanbrc 645 . . . . . . . . . . . . . 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 ) } )
204193, 203sseldi 3178 . . . . . . . . . . . . 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.  {
(/) } ) )
205 psseq2 3264 . . . . . . . . . . . . . . 15  |-  ( v  =  a  ->  (
u  C.  v  <->  u  C.  a ) )
206205notbid 285 . . . . . . . . . . . . . 14  |-  ( v  =  a  ->  ( -.  u  C.  v  <->  -.  u  C.  a ) )
207206rspcv 2880 . . . . . . . . . . . . 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
) )
208204, 207syl 15 . . . . . . . . . . . 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
) )
209 id 19 . . . . . . . . . . . . . . . . 17  |-  ( a  =  (/)  ->  a  =  (/) )
210 0elpw 4180 . . . . . . . . . . . . . . . . . 18  |-  (/)  e.  ~P a
211 0fin 7087 . . . . . . . . . . . . . . . . . 18  |-  (/)  e.  Fin
212 elin 3358 . . . . . . . . . . . . . . . . . 18  |-  ( (/)  e.  ( ~P a  i^i 
Fin )  <->  ( (/)  e.  ~P a  /\  (/)  e.  Fin )
)
213210, 211, 212mpbir2an 886 . . . . . . . . . . . . . . . . 17  |-  (/)  e.  ( ~P a  i^i  Fin )
214209, 213syl6eqel 2371 . . . . . . . . . . . . . . . 16  |-  ( a  =  (/)  ->  a  e.  ( ~P a  i^i 
Fin ) )
215 unieq 3836 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  a  ->  U. b  =  U. a )
216215eqeq2d 2294 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  a  ->  ( X  =  U. b  <->  X  =  U. a ) )
217216notbid 285 . . . . . . . . . . . . . . . . 17  |-  ( b  =  a  ->  ( -.  X  =  U. b 
<->  -.  X  =  U. a ) )
218217rspccv 2881 . . . . . . . . . . . . . . . 16  |-  ( A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b  ->  ( a  e.  ( ~P a  i^i  Fin )  ->  -.  X  =  U. a ) )
219214, 218syl5 28 . . . . . . . . . . . . . . 15  |-  ( A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b  ->  ( a  =  (/)  ->  -.  X  =  U. a ) )
220219necon2ad 2494 . . . . . . . . . . . . . 14  |-  ( A. b  e.  ( ~P a  i^i  Fin )  -.  X  =  U. b  ->  ( X  =  U. a  ->  a  =/=  (/) ) )
221220ad2antlr 707 . . . . . . . . . . . . 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  =/=  (/) ) )
222 psseq1 3263 . . . . . . . . . . . . . . 15  |-  ( u  =  (/)  ->  ( u 
C.  a  <->  (/)  C.  a
) )
223222adantl 452 . . . . . . . . . . . . . 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
) )
224 0pss 3492 . . . . . . . . . . . . . 14  |-  ( (/)  C.  a  <->  a  =/=  (/) )
225223, 224syl6bb 252 . . . . . . . . . . . . 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  =/=  (/) ) )
226221, 225sylibrd 225 . . . . . . . . . . . 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 ) )
227208, 226nsyld 132 . . . . . . . . . . 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 ) )
228227ex 423 . . . . . . . . . 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 ) ) )
229192, 228jaod 369 . . . . . . . . 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 ) ) )
23013, 229syl5bi 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 ) )  /\  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 ) ) )
231230rexlimdv 2666 . . . . . . 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 ) )
2323, 231mpd 14 . . . . . 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
)
233232ex 423 . . . . 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
) )
2341, 233syl5bir 209 . . . 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
) )
235234con4d 97 . . 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 ) )
2362353exp 1150 . 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 ) ) ) )
237236ralrimdv 2632 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