Metamath Proof Explorer

Theorem alexsubALTlem3

Description: Lemma for alexsubALT . If a point is covered by a collection taken from the base with no finite subcover, a set from the subbase can be added that covers the point so that the resulting collection has no finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010) (Revised by Mario Carneiro, 14-Dec-2013)

Ref Expression
Hypothesis alexsubALT.1 
|- X = U. J
Assertion alexsubALTlem3 
|- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) -> E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n )

Proof

Step Hyp Ref Expression
1 alexsubALT.1 
 |-  X = U. J
2 dfrex2 
 |-  ( E. n e. ( ~P ( u u. { s } ) i^i Fin ) X = U. n <-> -. A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n )
3 2 ralbii 
 |-  ( A. s e. t E. n e. ( ~P ( u u. { s } ) i^i Fin ) X = U. n <-> A. s e. t -. A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n )
4 ralnex 
 |-  ( A. s e. t -. A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n <-> -. E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n )
5 3 4 bitr2i 
 |-  ( -. E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n <-> A. s e. t E. n e. ( ~P ( u u. { s } ) i^i Fin ) X = U. n )
6 elin 
 |-  ( n e. ( ~P ( u u. { s } ) i^i Fin ) <-> ( n e. ~P ( u u. { s } ) /\ n e. Fin ) )
7 elpwi 
 |-  ( n e. ~P ( u u. { s } ) -> n C_ ( u u. { s } ) )
8 7 adantr 
 |-  ( ( n e. ~P ( u u. { s } ) /\ n e. Fin ) -> n C_ ( u u. { s } ) )
9 uncom 
 |-  ( u u. { s } ) = ( { s } u. u )
10 8 9 sseqtrdi 
 |-  ( ( n e. ~P ( u u. { s } ) /\ n e. Fin ) -> n C_ ( { s } u. u ) )
11 ssundif 
 |-  ( n C_ ( { s } u. u ) <-> ( n \ { s } ) C_ u )
12 10 11 sylib 
 |-  ( ( n e. ~P ( u u. { s } ) /\ n e. Fin ) -> ( n \ { s } ) C_ u )
13 diffi 
 |-  ( n e. Fin -> ( n \ { s } ) e. Fin )
14 13 adantl 
 |-  ( ( n e. ~P ( u u. { s } ) /\ n e. Fin ) -> ( n \ { s } ) e. Fin )
15 12 14 jca 
 |-  ( ( n e. ~P ( u u. { s } ) /\ n e. Fin ) -> ( ( n \ { s } ) C_ u /\ ( n \ { s } ) e. Fin ) )
16 6 15 sylbi 
 |-  ( n e. ( ~P ( u u. { s } ) i^i Fin ) -> ( ( n \ { s } ) C_ u /\ ( n \ { s } ) e. Fin ) )
17 16 adantr 
 |-  ( ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) -> ( ( n \ { s } ) C_ u /\ ( n \ { s } ) e. Fin ) )
18 17 ad2antll 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> ( ( n \ { s } ) C_ u /\ ( n \ { s } ) e. Fin ) )
19 elin 
 |-  ( ( n \ { s } ) e. ( ~P u i^i Fin ) <-> ( ( n \ { s } ) e. ~P u /\ ( n \ { s } ) e. Fin ) )
20 vex 
 |-  u e. _V
21 20 elpw2 
 |-  ( ( n \ { s } ) e. ~P u <-> ( n \ { s } ) C_ u )
22 21 anbi1i 
 |-  ( ( ( n \ { s } ) e. ~P u /\ ( n \ { s } ) e. Fin ) <-> ( ( n \ { s } ) C_ u /\ ( n \ { s } ) e. Fin ) )
23 19 22 bitr2i 
 |-  ( ( ( n \ { s } ) C_ u /\ ( n \ { s } ) e. Fin ) <-> ( n \ { s } ) e. ( ~P u i^i Fin ) )
24 18 23 sylib 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> ( n \ { s } ) e. ( ~P u i^i Fin ) )
25 simprrr 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> X = U. n )
26 eldif 
 |-  ( x e. ( n \ { s } ) <-> ( x e. n /\ -. x e. { s } ) )
27 26 simplbi2 
 |-  ( x e. n -> ( -. x e. { s } -> x e. ( n \ { s } ) ) )
28 elun 
 |-  ( x e. ( ( n \ { s } ) u. { s } ) <-> ( x e. ( n \ { s } ) \/ x e. { s } ) )
29 orcom 
 |-  ( ( x e. { s } \/ x e. ( n \ { s } ) ) <-> ( x e. ( n \ { s } ) \/ x e. { s } ) )
30 28 29 bitr4i 
 |-  ( x e. ( ( n \ { s } ) u. { s } ) <-> ( x e. { s } \/ x e. ( n \ { s } ) ) )
31 df-or 
 |-  ( ( x e. { s } \/ x e. ( n \ { s } ) ) <-> ( -. x e. { s } -> x e. ( n \ { s } ) ) )
32 30 31 bitr2i 
 |-  ( ( -. x e. { s } -> x e. ( n \ { s } ) ) <-> x e. ( ( n \ { s } ) u. { s } ) )
33 27 32 sylib 
 |-  ( x e. n -> x e. ( ( n \ { s } ) u. { s } ) )
34 33 ssriv 
 |-  n C_ ( ( n \ { s } ) u. { s } )
35 uniss 
 |-  ( n C_ ( ( n \ { s } ) u. { s } ) -> U. n C_ U. ( ( n \ { s } ) u. { s } ) )
36 34 35 mp1i 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. n C_ U. ( ( n \ { s } ) u. { s } ) )
37 uniun 
 |-  U. ( ( n \ { s } ) u. { s } ) = ( U. ( n \ { s } ) u. U. { s } )
38 vex 
 |-  s e. _V
39 38 unisn 
 |-  U. { s } = s
40 39 uneq2i 
 |-  ( U. ( n \ { s } ) u. U. { s } ) = ( U. ( n \ { s } ) u. s )
41 37 40 eqtri 
 |-  U. ( ( n \ { s } ) u. { s } ) = ( U. ( n \ { s } ) u. s )
42 36 41 sseqtrdi 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. n C_ ( U. ( n \ { s } ) u. s ) )
43 25 42 eqsstrd 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> X C_ ( U. ( n \ { s } ) u. s ) )
44 difss 
 |-  ( n \ { s } ) C_ n
45 44 unissi 
 |-  U. ( n \ { s } ) C_ U. n
46 sseq2 
 |-  ( X = U. n -> ( U. ( n \ { s } ) C_ X <-> U. ( n \ { s } ) C_ U. n ) )
47 45 46 mpbiri 
 |-  ( X = U. n -> U. ( n \ { s } ) C_ X )
48 47 adantl 
 |-  ( ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) -> U. ( n \ { s } ) C_ X )
49 48 ad2antll 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. ( n \ { s } ) C_ X )
50 elinel1 
 |-  ( t e. ( ~P x i^i Fin ) -> t e. ~P x )
51 50 elpwid 
 |-  ( t e. ( ~P x i^i Fin ) -> t C_ x )
52 51 ad3antrrr 
 |-  ( ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) -> t C_ x )
53 52 ad2antlr 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> t C_ x )
54 simprl 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> s e. t )
55 53 54 sseldd 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> s e. x )
56 elssuni 
 |-  ( s e. x -> s C_ U. x )
57 55 56 syl 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> s C_ U. x )
58 fibas 
 |-  ( fi ` x ) e. TopBases
59 unitg 
 |-  ( ( fi ` x ) e. TopBases -> U. ( topGen ` ( fi ` x ) ) = U. ( fi ` x ) )
60 58 59 mp1i 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. ( topGen ` ( fi ` x ) ) = U. ( fi ` x ) )
61 unieq 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> U. J = U. ( topGen ` ( fi ` x ) ) )
62 61 3ad2ant1 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) -> U. J = U. ( topGen ` ( fi ` x ) ) )
63 62 ad3antrrr 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. J = U. ( topGen ` ( fi ` x ) ) )
64 vex 
 |-  x e. _V
65 fiuni 
 |-  ( x e. _V -> U. x = U. ( fi ` x ) )
66 64 65 mp1i 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. x = U. ( fi ` x ) )
67 60 63 66 3eqtr4rd 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. x = U. J )
68 67 1 eqtr4di 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> U. x = X )
69 57 68 sseqtrd 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> s C_ X )
70 49 69 unssd 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> ( U. ( n \ { s } ) u. s ) C_ X )
71 43 70 eqssd 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> X = ( U. ( n \ { s } ) u. s ) )
72 unieq 
 |-  ( m = ( n \ { s } ) -> U. m = U. ( n \ { s } ) )
73 72 uneq1d 
 |-  ( m = ( n \ { s } ) -> ( U. m u. s ) = ( U. ( n \ { s } ) u. s ) )
74 73 rspceeqv 
 |-  ( ( ( n \ { s } ) e. ( ~P u i^i Fin ) /\ X = ( U. ( n \ { s } ) u. s ) ) -> E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) )
75 24 71 74 syl2anc 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( s e. t /\ ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) ) ) -> E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) )
76 75 expr 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ s e. t ) -> ( ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) -> E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) ) )
77 76 expd 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ s e. t ) -> ( n e. ( ~P ( u u. { s } ) i^i Fin ) -> ( X = U. n -> E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) ) ) )
78 77 rexlimdv 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ s e. t ) -> ( E. n e. ( ~P ( u u. { s } ) i^i Fin ) X = U. n -> E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) ) )
79 78 ralimdva 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( A. s e. t E. n e. ( ~P ( u u. { s } ) i^i Fin ) X = U. n -> A. s e. t E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) ) )
80 elinel2 
 |-  ( t e. ( ~P x i^i Fin ) -> t e. Fin )
81 80 adantr 
 |-  ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) -> t e. Fin )
82 unieq 
 |-  ( m = ( f ` s ) -> U. m = U. ( f ` s ) )
83 82 uneq1d 
 |-  ( m = ( f ` s ) -> ( U. m u. s ) = ( U. ( f ` s ) u. s ) )
84 83 eqeq2d 
 |-  ( m = ( f ` s ) -> ( X = ( U. m u. s ) <-> X = ( U. ( f ` s ) u. s ) ) )
85 84 ac6sfi 
 |-  ( ( t e. Fin /\ A. s e. t E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) ) -> E. f ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) )
86 85 ex 
 |-  ( t e. Fin -> ( A. s e. t E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) -> E. f ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) )
87 81 86 syl 
 |-  ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) -> ( A. s e. t E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) -> E. f ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) )
88 87 adantr 
 |-  ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) -> ( A. s e. t E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) -> E. f ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) )
89 88 ad2antrl 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( A. s e. t E. m e. ( ~P u i^i Fin ) X = ( U. m u. s ) -> E. f ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) )
90 ffvelrn 
 |-  ( ( f : t --> ( ~P u i^i Fin ) /\ s e. t ) -> ( f ` s ) e. ( ~P u i^i Fin ) )
91 elin 
 |-  ( ( f ` s ) e. ( ~P u i^i Fin ) <-> ( ( f ` s ) e. ~P u /\ ( f ` s ) e. Fin ) )
92 elpwi 
 |-  ( ( f ` s ) e. ~P u -> ( f ` s ) C_ u )
93 92 adantr 
 |-  ( ( ( f ` s ) e. ~P u /\ ( f ` s ) e. Fin ) -> ( f ` s ) C_ u )
94 91 93 sylbi 
 |-  ( ( f ` s ) e. ( ~P u i^i Fin ) -> ( f ` s ) C_ u )
95 90 94 syl 
 |-  ( ( f : t --> ( ~P u i^i Fin ) /\ s e. t ) -> ( f ` s ) C_ u )
96 95 ralrimiva 
 |-  ( f : t --> ( ~P u i^i Fin ) -> A. s e. t ( f ` s ) C_ u )
97 iunss 
 |-  ( U_ s e. t ( f ` s ) C_ u <-> A. s e. t ( f ` s ) C_ u )
98 96 97 sylibr 
 |-  ( f : t --> ( ~P u i^i Fin ) -> U_ s e. t ( f ` s ) C_ u )
99 98 ad2antrl 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> U_ s e. t ( f ` s ) C_ u )
100 simplrr 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> w e. u )
101 100 snssd 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> { w } C_ u )
102 99 101 unssd 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( U_ s e. t ( f ` s ) u. { w } ) C_ u )
103 90 elin2d 
 |-  ( ( f : t --> ( ~P u i^i Fin ) /\ s e. t ) -> ( f ` s ) e. Fin )
104 103 ralrimiva 
 |-  ( f : t --> ( ~P u i^i Fin ) -> A. s e. t ( f ` s ) e. Fin )
105 iunfi 
 |-  ( ( t e. Fin /\ A. s e. t ( f ` s ) e. Fin ) -> U_ s e. t ( f ` s ) e. Fin )
106 81 104 105 syl2an 
 |-  ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ f : t --> ( ~P u i^i Fin ) ) -> U_ s e. t ( f ` s ) e. Fin )
107 106 ad4ant14 
 |-  ( ( ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) /\ f : t --> ( ~P u i^i Fin ) ) -> U_ s e. t ( f ` s ) e. Fin )
108 107 ad2ant2lr 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> U_ s e. t ( f ` s ) e. Fin )
109 snfi 
 |-  { w } e. Fin
110 unfi 
 |-  ( ( U_ s e. t ( f ` s ) e. Fin /\ { w } e. Fin ) -> ( U_ s e. t ( f ` s ) u. { w } ) e. Fin )
111 108 109 110 sylancl 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( U_ s e. t ( f ` s ) u. { w } ) e. Fin )
112 102 111 jca 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( ( U_ s e. t ( f ` s ) u. { w } ) C_ u /\ ( U_ s e. t ( f ` s ) u. { w } ) e. Fin ) )
113 elin 
 |-  ( ( U_ s e. t ( f ` s ) u. { w } ) e. ( ~P u i^i Fin ) <-> ( ( U_ s e. t ( f ` s ) u. { w } ) e. ~P u /\ ( U_ s e. t ( f ` s ) u. { w } ) e. Fin ) )
114 20 elpw2 
 |-  ( ( U_ s e. t ( f ` s ) u. { w } ) e. ~P u <-> ( U_ s e. t ( f ` s ) u. { w } ) C_ u )
115 114 anbi1i 
 |-  ( ( ( U_ s e. t ( f ` s ) u. { w } ) e. ~P u /\ ( U_ s e. t ( f ` s ) u. { w } ) e. Fin ) <-> ( ( U_ s e. t ( f ` s ) u. { w } ) C_ u /\ ( U_ s e. t ( f ` s ) u. { w } ) e. Fin ) )
116 113 115 bitr2i 
 |-  ( ( ( U_ s e. t ( f ` s ) u. { w } ) C_ u /\ ( U_ s e. t ( f ` s ) u. { w } ) e. Fin ) <-> ( U_ s e. t ( f ` s ) u. { w } ) e. ( ~P u i^i Fin ) )
117 112 116 sylib 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( U_ s e. t ( f ` s ) u. { w } ) e. ( ~P u i^i Fin ) )
118 ralnex 
 |-  ( A. s e. t -. y e. ( f ` s ) <-> -. E. s e. t y e. ( f ` s ) )
119 118 imbi2i 
 |-  ( ( v e. y -> A. s e. t -. y e. ( f ` s ) ) <-> ( v e. y -> -. E. s e. t y e. ( f ` s ) ) )
120 119 albii 
 |-  ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) <-> A. y ( v e. y -> -. E. s e. t y e. ( f ` s ) ) )
121 alinexa 
 |-  ( A. y ( v e. y -> -. E. s e. t y e. ( f ` s ) ) <-> -. E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) )
122 120 121 bitr2i 
 |-  ( -. E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) <-> A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) )
123 fveq2 
 |-  ( s = z -> ( f ` s ) = ( f ` z ) )
124 123 unieqd 
 |-  ( s = z -> U. ( f ` s ) = U. ( f ` z ) )
125 id 
 |-  ( s = z -> s = z )
126 124 125 uneq12d 
 |-  ( s = z -> ( U. ( f ` s ) u. s ) = ( U. ( f ` z ) u. z ) )
127 126 eqeq2d 
 |-  ( s = z -> ( X = ( U. ( f ` s ) u. s ) <-> X = ( U. ( f ` z ) u. z ) ) )
128 127 rspcv 
 |-  ( z e. t -> ( A. s e. t X = ( U. ( f ` s ) u. s ) -> X = ( U. ( f ` z ) u. z ) ) )
129 eleq2 
 |-  ( X = ( U. ( f ` z ) u. z ) -> ( v e. X <-> v e. ( U. ( f ` z ) u. z ) ) )
130 129 biimpd 
 |-  ( X = ( U. ( f ` z ) u. z ) -> ( v e. X -> v e. ( U. ( f ` z ) u. z ) ) )
131 elun 
 |-  ( v e. ( U. ( f ` z ) u. z ) <-> ( v e. U. ( f ` z ) \/ v e. z ) )
132 eluni 
 |-  ( v e. U. ( f ` z ) <-> E. w ( v e. w /\ w e. ( f ` z ) ) )
133 132 orbi1i 
 |-  ( ( v e. U. ( f ` z ) \/ v e. z ) <-> ( E. w ( v e. w /\ w e. ( f ` z ) ) \/ v e. z ) )
134 df-or 
 |-  ( ( E. w ( v e. w /\ w e. ( f ` z ) ) \/ v e. z ) <-> ( -. E. w ( v e. w /\ w e. ( f ` z ) ) -> v e. z ) )
135 alinexa 
 |-  ( A. w ( v e. w -> -. w e. ( f ` z ) ) <-> -. E. w ( v e. w /\ w e. ( f ` z ) ) )
136 135 imbi1i 
 |-  ( ( A. w ( v e. w -> -. w e. ( f ` z ) ) -> v e. z ) <-> ( -. E. w ( v e. w /\ w e. ( f ` z ) ) -> v e. z ) )
137 134 136 bitr4i 
 |-  ( ( E. w ( v e. w /\ w e. ( f ` z ) ) \/ v e. z ) <-> ( A. w ( v e. w -> -. w e. ( f ` z ) ) -> v e. z ) )
138 131 133 137 3bitri 
 |-  ( v e. ( U. ( f ` z ) u. z ) <-> ( A. w ( v e. w -> -. w e. ( f ` z ) ) -> v e. z ) )
139 eleq2 
 |-  ( y = w -> ( v e. y <-> v e. w ) )
140 eleq1w 
 |-  ( y = w -> ( y e. ( f ` s ) <-> w e. ( f ` s ) ) )
141 140 notbid 
 |-  ( y = w -> ( -. y e. ( f ` s ) <-> -. w e. ( f ` s ) ) )
142 141 ralbidv 
 |-  ( y = w -> ( A. s e. t -. y e. ( f ` s ) <-> A. s e. t -. w e. ( f ` s ) ) )
143 139 142 imbi12d 
 |-  ( y = w -> ( ( v e. y -> A. s e. t -. y e. ( f ` s ) ) <-> ( v e. w -> A. s e. t -. w e. ( f ` s ) ) ) )
144 143 spvv 
 |-  ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> ( v e. w -> A. s e. t -. w e. ( f ` s ) ) )
145 123 eleq2d 
 |-  ( s = z -> ( w e. ( f ` s ) <-> w e. ( f ` z ) ) )
146 145 notbid 
 |-  ( s = z -> ( -. w e. ( f ` s ) <-> -. w e. ( f ` z ) ) )
147 146 rspcv 
 |-  ( z e. t -> ( A. s e. t -. w e. ( f ` s ) -> -. w e. ( f ` z ) ) )
148 144 147 syl9r 
 |-  ( z e. t -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> ( v e. w -> -. w e. ( f ` z ) ) ) )
149 148 alrimdv 
 |-  ( z e. t -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> A. w ( v e. w -> -. w e. ( f ` z ) ) ) )
150 149 imim1d 
 |-  ( z e. t -> ( ( A. w ( v e. w -> -. w e. ( f ` z ) ) -> v e. z ) -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. z ) ) )
151 138 150 syl5bi 
 |-  ( z e. t -> ( v e. ( U. ( f ` z ) u. z ) -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. z ) ) )
152 151 a1dd 
 |-  ( z e. t -> ( v e. ( U. ( f ` z ) u. z ) -> ( w = |^| t -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. z ) ) ) )
153 130 152 syl9r 
 |-  ( z e. t -> ( X = ( U. ( f ` z ) u. z ) -> ( v e. X -> ( w = |^| t -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. z ) ) ) ) )
154 128 153 syld 
 |-  ( z e. t -> ( A. s e. t X = ( U. ( f ` s ) u. s ) -> ( v e. X -> ( w = |^| t -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. z ) ) ) ) )
155 154 com14 
 |-  ( w = |^| t -> ( A. s e. t X = ( U. ( f ` s ) u. s ) -> ( v e. X -> ( z e. t -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. z ) ) ) ) )
156 155 imp31 
 |-  ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( z e. t -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. z ) ) )
157 156 com23 
 |-  ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> ( z e. t -> v e. z ) ) )
158 157 ralrimdv 
 |-  ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> A. z e. t v e. z ) )
159 vex 
 |-  v e. _V
160 159 elint2 
 |-  ( v e. |^| t <-> A. z e. t v e. z )
161 158 160 syl6ibr 
 |-  ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. |^| t ) )
162 eleq2 
 |-  ( w = |^| t -> ( v e. w <-> v e. |^| t ) )
163 162 ad2antrr 
 |-  ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( v e. w <-> v e. |^| t ) )
164 161 163 sylibrd 
 |-  ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> v e. w ) )
165 122 164 syl5bi 
 |-  ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( -. E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) -> v e. w ) )
166 165 orrd 
 |-  ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) \/ v e. w ) )
167 166 ex 
 |-  ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) -> ( v e. X -> ( E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) \/ v e. w ) ) )
168 orc 
 |-  ( E. s e. t y e. ( f ` s ) -> ( E. s e. t y e. ( f ` s ) \/ y = w ) )
169 168 anim2i 
 |-  ( ( v e. y /\ E. s e. t y e. ( f ` s ) ) -> ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) )
170 169 eximi 
 |-  ( E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) -> E. y ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) )
171 equid 
 |-  w = w
172 vex 
 |-  w e. _V
173 equequ1 
 |-  ( y = w -> ( y = w <-> w = w ) )
174 139 173 anbi12d 
 |-  ( y = w -> ( ( v e. y /\ y = w ) <-> ( v e. w /\ w = w ) ) )
175 172 174 spcev 
 |-  ( ( v e. w /\ w = w ) -> E. y ( v e. y /\ y = w ) )
176 171 175 mpan2 
 |-  ( v e. w -> E. y ( v e. y /\ y = w ) )
177 olc 
 |-  ( y = w -> ( E. s e. t y e. ( f ` s ) \/ y = w ) )
178 177 anim2i 
 |-  ( ( v e. y /\ y = w ) -> ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) )
179 178 eximi 
 |-  ( E. y ( v e. y /\ y = w ) -> E. y ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) )
180 176 179 syl 
 |-  ( v e. w -> E. y ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) )
181 170 180 jaoi 
 |-  ( ( E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) \/ v e. w ) -> E. y ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) )
182 eluni 
 |-  ( v e. U. ( U_ s e. t ( f ` s ) u. { w } ) <-> E. y ( v e. y /\ y e. ( U_ s e. t ( f ` s ) u. { w } ) ) )
183 elun 
 |-  ( y e. ( U_ s e. t ( f ` s ) u. { w } ) <-> ( y e. U_ s e. t ( f ` s ) \/ y e. { w } ) )
184 eliun 
 |-  ( y e. U_ s e. t ( f ` s ) <-> E. s e. t y e. ( f ` s ) )
185 velsn 
 |-  ( y e. { w } <-> y = w )
186 184 185 orbi12i 
 |-  ( ( y e. U_ s e. t ( f ` s ) \/ y e. { w } ) <-> ( E. s e. t y e. ( f ` s ) \/ y = w ) )
187 183 186 bitri 
 |-  ( y e. ( U_ s e. t ( f ` s ) u. { w } ) <-> ( E. s e. t y e. ( f ` s ) \/ y = w ) )
188 187 anbi2i 
 |-  ( ( v e. y /\ y e. ( U_ s e. t ( f ` s ) u. { w } ) ) <-> ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) )
189 188 exbii 
 |-  ( E. y ( v e. y /\ y e. ( U_ s e. t ( f ` s ) u. { w } ) ) <-> E. y ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) )
190 182 189 bitr2i 
 |-  ( E. y ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) <-> v e. U. ( U_ s e. t ( f ` s ) u. { w } ) )
191 181 190 sylib 
 |-  ( ( E. y ( v e. y /\ E. s e. t y e. ( f ` s ) ) \/ v e. w ) -> v e. U. ( U_ s e. t ( f ` s ) u. { w } ) )
192 167 191 syl6 
 |-  ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) -> ( v e. X -> v e. U. ( U_ s e. t ( f ` s ) u. { w } ) ) )
193 192 ad5ant25 
 |-  ( ( ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) -> ( v e. X -> v e. U. ( U_ s e. t ( f ` s ) u. { w } ) ) )
194 193 ad2ant2l 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( v e. X -> v e. U. ( U_ s e. t ( f ` s ) u. { w } ) ) )
195 194 ssrdv 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> X C_ U. ( U_ s e. t ( f ` s ) u. { w } ) )
196 elun 
 |-  ( v e. ( U_ s e. t ( f ` s ) u. { w } ) <-> ( v e. U_ s e. t ( f ` s ) \/ v e. { w } ) )
197 eliun 
 |-  ( v e. U_ s e. t ( f ` s ) <-> E. s e. t v e. ( f ` s ) )
198 velsn 
 |-  ( v e. { w } <-> v = w )
199 197 198 orbi12i 
 |-  ( ( v e. U_ s e. t ( f ` s ) \/ v e. { w } ) <-> ( E. s e. t v e. ( f ` s ) \/ v = w ) )
200 196 199 bitri 
 |-  ( v e. ( U_ s e. t ( f ` s ) u. { w } ) <-> ( E. s e. t v e. ( f ` s ) \/ v = w ) )
201 nfra1 
 |-  F/ s A. s e. t X = ( U. ( f ` s ) u. s )
202 nfv 
 |-  F/ s v C_ X
203 rsp 
 |-  ( A. s e. t X = ( U. ( f ` s ) u. s ) -> ( s e. t -> X = ( U. ( f ` s ) u. s ) ) )
204 eqimss2 
 |-  ( X = ( U. ( f ` s ) u. s ) -> ( U. ( f ` s ) u. s ) C_ X )
205 elssuni 
 |-  ( v e. ( f ` s ) -> v C_ U. ( f ` s ) )
206 ssun3 
 |-  ( v C_ U. ( f ` s ) -> v C_ ( U. ( f ` s ) u. s ) )
207 205 206 syl 
 |-  ( v e. ( f ` s ) -> v C_ ( U. ( f ` s ) u. s ) )
208 sstr 
 |-  ( ( v C_ ( U. ( f ` s ) u. s ) /\ ( U. ( f ` s ) u. s ) C_ X ) -> v C_ X )
209 208 expcom 
 |-  ( ( U. ( f ` s ) u. s ) C_ X -> ( v C_ ( U. ( f ` s ) u. s ) -> v C_ X ) )
210 204 207 209 syl2im 
 |-  ( X = ( U. ( f ` s ) u. s ) -> ( v e. ( f ` s ) -> v C_ X ) )
211 203 210 syl6 
 |-  ( A. s e. t X = ( U. ( f ` s ) u. s ) -> ( s e. t -> ( v e. ( f ` s ) -> v C_ X ) ) )
212 201 202 211 rexlimd 
 |-  ( A. s e. t X = ( U. ( f ` s ) u. s ) -> ( E. s e. t v e. ( f ` s ) -> v C_ X ) )
213 212 ad2antll 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( E. s e. t v e. ( f ` s ) -> v C_ X ) )
214 elpwi 
 |-  ( u e. ~P ( fi ` x ) -> u C_ ( fi ` x ) )
215 214 ad2antrl 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) -> u C_ ( fi ` x ) )
216 215 ad2antrr 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> u C_ ( fi ` x ) )
217 216 100 sseldd 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> w e. ( fi ` x ) )
218 elssuni 
 |-  ( w e. ( fi ` x ) -> w C_ U. ( fi ` x ) )
219 217 218 syl 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> w C_ U. ( fi ` x ) )
220 58 59 ax-mp 
 |-  U. ( topGen ` ( fi ` x ) ) = U. ( fi ` x )
221 61 220 eqtr2di 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> U. ( fi ` x ) = U. J )
222 221 1 eqtr4di 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> U. ( fi ` x ) = X )
223 222 3ad2ant1 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) -> U. ( fi ` x ) = X )
224 223 ad3antrrr 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> U. ( fi ` x ) = X )
225 219 224 sseqtrd 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> w C_ X )
226 sseq1 
 |-  ( v = w -> ( v C_ X <-> w C_ X ) )
227 225 226 syl5ibrcom 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( v = w -> v C_ X ) )
228 213 227 jaod 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( ( E. s e. t v e. ( f ` s ) \/ v = w ) -> v C_ X ) )
229 200 228 syl5bi 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> ( v e. ( U_ s e. t ( f ` s ) u. { w } ) -> v C_ X ) )
230 229 ralrimiv 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> A. v e. ( U_ s e. t ( f ` s ) u. { w } ) v C_ X )
231 unissb 
 |-  ( U. ( U_ s e. t ( f ` s ) u. { w } ) C_ X <-> A. v e. ( U_ s e. t ( f ` s ) u. { w } ) v C_ X )
232 230 231 sylibr 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> U. ( U_ s e. t ( f ` s ) u. { w } ) C_ X )
233 195 232 eqssd 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> X = U. ( U_ s e. t ( f ` s ) u. { w } ) )
234 unieq 
 |-  ( b = ( U_ s e. t ( f ` s ) u. { w } ) -> U. b = U. ( U_ s e. t ( f ` s ) u. { w } ) )
235 234 rspceeqv 
 |-  ( ( ( U_ s e. t ( f ` s ) u. { w } ) e. ( ~P u i^i Fin ) /\ X = U. ( U_ s e. t ( f ` s ) u. { w } ) ) -> E. b e. ( ~P u i^i Fin ) X = U. b )
236 117 233 235 syl2anc 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) /\ ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) ) -> E. b e. ( ~P u i^i Fin ) X = U. b )
237 236 ex 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) -> E. b e. ( ~P u i^i Fin ) X = U. b ) )
238 237 exlimdv 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( E. f ( f : t --> ( ~P u i^i Fin ) /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) -> E. b e. ( ~P u i^i Fin ) X = U. b ) )
239 79 89 238 3syld 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( A. s e. t E. n e. ( ~P ( u u. { s } ) i^i Fin ) X = U. n -> E. b e. ( ~P u i^i Fin ) X = U. b ) )
240 5 239 syl5bi 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( -. E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n -> E. b e. ( ~P u i^i Fin ) X = U. b ) )
241 dfrex2 
 |-  ( E. b e. ( ~P u i^i Fin ) X = U. b <-> -. A. b e. ( ~P u i^i Fin ) -. X = U. b )
242 240 241 syl6ib 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( -. E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n -> -. A. b e. ( ~P u i^i Fin ) -. X = U. b ) )
243 242 con4d 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) /\ w e. u ) ) -> ( A. b e. ( ~P u i^i Fin ) -. X = U. b -> E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) )
244 243 exp32 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ a C_ u ) ) -> ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) -> ( w e. u -> ( A. b e. ( ~P u i^i Fin ) -. X = U. b -> E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) )
245 244 com24 
 |-  ( ( ( 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 ) ) ) )
246 245 exp32 
 |-  ( ( 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 ) ) ) ) ) )
247 246 imp45 
 |-  ( ( ( 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 ) ) )
248 247 imp31 
 |-  ( ( ( ( ( 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 )