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 unisnv 
 |-  U. { s } = s
39 38 uneq2i 
 |-  ( U. ( n \ { s } ) u. U. { s } ) = ( U. ( n \ { s } ) u. s )
40 37 39 eqtri 
 |-  U. ( ( n \ { s } ) u. { s } ) = ( U. ( n \ { s } ) u. s )
41 36 40 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 ) )
42 25 41 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 ) )
43 difss 
 |-  ( n \ { s } ) C_ n
44 43 unissi 
 |-  U. ( n \ { s } ) C_ U. n
45 sseq2 
 |-  ( X = U. n -> ( U. ( n \ { s } ) C_ X <-> U. ( n \ { s } ) C_ U. n ) )
46 44 45 mpbiri 
 |-  ( X = U. n -> U. ( n \ { s } ) C_ X )
47 46 adantl 
 |-  ( ( n e. ( ~P ( u u. { s } ) i^i Fin ) /\ X = U. n ) -> U. ( n \ { s } ) C_ X )
48 47 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 )
49 elinel1 
 |-  ( t e. ( ~P x i^i Fin ) -> t e. ~P x )
50 49 elpwid 
 |-  ( t e. ( ~P x i^i Fin ) -> t C_ x )
51 50 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 )
52 51 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 )
53 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 )
54 52 53 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 )
55 elssuni 
 |-  ( s e. x -> s C_ U. x )
56 54 55 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 )
57 fibas 
 |-  ( fi ` x ) e. TopBases
58 unitg 
 |-  ( ( fi ` x ) e. TopBases -> U. ( topGen ` ( fi ` x ) ) = U. ( fi ` x ) )
59 57 58 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 ) )
60 unieq 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> U. J = U. ( topGen ` ( fi ` x ) ) )
61 60 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 ) ) )
62 61 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 ) ) )
63 vex 
 |-  x e. _V
64 fiuni 
 |-  ( x e. _V -> U. x = U. ( fi ` x ) )
65 63 64 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 ) )
66 59 62 65 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 )
67 66 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 )
68 56 67 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 )
69 48 68 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 )
70 42 69 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 ) )
71 unieq 
 |-  ( m = ( n \ { s } ) -> U. m = U. ( n \ { s } ) )
72 71 uneq1d 
 |-  ( m = ( n \ { s } ) -> ( U. m u. s ) = ( U. ( n \ { s } ) u. s ) )
73 72 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 ) )
74 24 70 73 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 ) )
75 74 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 ) ) )
76 75 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 ) ) ) )
77 76 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 ) ) )
78 77 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 ) ) )
79 elinel2 
 |-  ( t e. ( ~P x i^i Fin ) -> t e. Fin )
80 79 adantr 
 |-  ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) -> t e. Fin )
81 unieq 
 |-  ( m = ( f ` s ) -> U. m = U. ( f ` s ) )
82 81 uneq1d 
 |-  ( m = ( f ` s ) -> ( U. m u. s ) = ( U. ( f ` s ) u. s ) )
83 82 eqeq2d 
 |-  ( m = ( f ` s ) -> ( X = ( U. m u. s ) <-> X = ( U. ( f ` s ) u. s ) ) )
84 83 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 ) ) )
85 84 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 ) ) ) )
86 80 85 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 ) ) ) )
87 86 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 ) ) ) )
88 87 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 ) ) ) )
89 ffvelcdm 
 |-  ( ( f : t --> ( ~P u i^i Fin ) /\ s e. t ) -> ( f ` s ) e. ( ~P u i^i Fin ) )
90 elin 
 |-  ( ( f ` s ) e. ( ~P u i^i Fin ) <-> ( ( f ` s ) e. ~P u /\ ( f ` s ) e. Fin ) )
91 elpwi 
 |-  ( ( f ` s ) e. ~P u -> ( f ` s ) C_ u )
92 91 adantr 
 |-  ( ( ( f ` s ) e. ~P u /\ ( f ` s ) e. Fin ) -> ( f ` s ) C_ u )
93 90 92 sylbi 
 |-  ( ( f ` s ) e. ( ~P u i^i Fin ) -> ( f ` s ) C_ u )
94 89 93 syl 
 |-  ( ( f : t --> ( ~P u i^i Fin ) /\ s e. t ) -> ( f ` s ) C_ u )
95 94 ralrimiva 
 |-  ( f : t --> ( ~P u i^i Fin ) -> A. s e. t ( f ` s ) C_ u )
96 iunss 
 |-  ( U_ s e. t ( f ` s ) C_ u <-> A. s e. t ( f ` s ) C_ u )
97 95 96 sylibr 
 |-  ( f : t --> ( ~P u i^i Fin ) -> U_ s e. t ( f ` s ) C_ u )
98 97 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 )
99 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 )
100 99 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 )
101 98 100 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 )
102 89 elin2d 
 |-  ( ( f : t --> ( ~P u i^i Fin ) /\ s e. t ) -> ( f ` s ) e. Fin )
103 102 ralrimiva 
 |-  ( f : t --> ( ~P u i^i Fin ) -> A. s e. t ( f ` s ) e. Fin )
104 iunfi 
 |-  ( ( t e. Fin /\ A. s e. t ( f ` s ) e. Fin ) -> U_ s e. t ( f ` s ) e. Fin )
105 80 103 104 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 )
106 105 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 )
107 106 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 )
108 snfi 
 |-  { w } e. Fin
109 unfi 
 |-  ( ( U_ s e. t ( f ` s ) e. Fin /\ { w } e. Fin ) -> ( U_ s e. t ( f ` s ) u. { w } ) e. Fin )
110 107 108 109 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 )
111 101 110 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 ) )
112 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 ) )
113 20 elpw2 
 |-  ( ( U_ s e. t ( f ` s ) u. { w } ) e. ~P u <-> ( U_ s e. t ( f ` s ) u. { w } ) C_ u )
114 113 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 ) )
115 112 114 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 ) )
116 111 115 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 ) )
117 ralnex 
 |-  ( A. s e. t -. y e. ( f ` s ) <-> -. E. s e. t y e. ( f ` s ) )
118 117 imbi2i 
 |-  ( ( v e. y -> A. s e. t -. y e. ( f ` s ) ) <-> ( v e. y -> -. E. s e. t y e. ( f ` s ) ) )
119 118 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 ) ) )
120 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 ) ) )
121 119 120 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 ) ) )
122 fveq2 
 |-  ( s = z -> ( f ` s ) = ( f ` z ) )
123 122 unieqd 
 |-  ( s = z -> U. ( f ` s ) = U. ( f ` z ) )
124 id 
 |-  ( s = z -> s = z )
125 123 124 uneq12d 
 |-  ( s = z -> ( U. ( f ` s ) u. s ) = ( U. ( f ` z ) u. z ) )
126 125 eqeq2d 
 |-  ( s = z -> ( X = ( U. ( f ` s ) u. s ) <-> X = ( U. ( f ` z ) u. z ) ) )
127 126 rspcv 
 |-  ( z e. t -> ( A. s e. t X = ( U. ( f ` s ) u. s ) -> X = ( U. ( f ` z ) u. z ) ) )
128 eleq2 
 |-  ( X = ( U. ( f ` z ) u. z ) -> ( v e. X <-> v e. ( U. ( f ` z ) u. z ) ) )
129 128 biimpd 
 |-  ( X = ( U. ( f ` z ) u. z ) -> ( v e. X -> v e. ( U. ( f ` z ) u. z ) ) )
130 elun 
 |-  ( v e. ( U. ( f ` z ) u. z ) <-> ( v e. U. ( f ` z ) \/ v e. z ) )
131 eluni 
 |-  ( v e. U. ( f ` z ) <-> E. w ( v e. w /\ w e. ( f ` z ) ) )
132 131 orbi1i 
 |-  ( ( v e. U. ( f ` z ) \/ v e. z ) <-> ( E. w ( v e. w /\ w e. ( f ` z ) ) \/ v e. z ) )
133 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 ) )
134 alinexa 
 |-  ( A. w ( v e. w -> -. w e. ( f ` z ) ) <-> -. E. w ( v e. w /\ w e. ( f ` z ) ) )
135 134 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 ) )
136 133 135 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 ) )
137 130 132 136 3bitri 
 |-  ( v e. ( U. ( f ` z ) u. z ) <-> ( A. w ( v e. w -> -. w e. ( f ` z ) ) -> v e. z ) )
138 eleq2 
 |-  ( y = w -> ( v e. y <-> v e. w ) )
139 eleq1w 
 |-  ( y = w -> ( y e. ( f ` s ) <-> w e. ( f ` s ) ) )
140 139 notbid 
 |-  ( y = w -> ( -. y e. ( f ` s ) <-> -. w e. ( f ` s ) ) )
141 140 ralbidv 
 |-  ( y = w -> ( A. s e. t -. y e. ( f ` s ) <-> A. s e. t -. w e. ( f ` s ) ) )
142 138 141 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 ) ) ) )
143 142 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 ) ) )
144 122 eleq2d 
 |-  ( s = z -> ( w e. ( f ` s ) <-> w e. ( f ` z ) ) )
145 144 notbid 
 |-  ( s = z -> ( -. w e. ( f ` s ) <-> -. w e. ( f ` z ) ) )
146 145 rspcv 
 |-  ( z e. t -> ( A. s e. t -. w e. ( f ` s ) -> -. w e. ( f ` z ) ) )
147 143 146 syl9r 
 |-  ( z e. t -> ( A. y ( v e. y -> A. s e. t -. y e. ( f ` s ) ) -> ( v e. w -> -. w e. ( f ` z ) ) ) )
148 147 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 ) ) ) )
149 148 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 ) ) )
150 137 149 biimtrid 
 |-  ( 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 ) ) )
151 150 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 ) ) ) )
152 129 151 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 ) ) ) ) )
153 127 152 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 ) ) ) ) )
154 153 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 ) ) ) ) )
155 154 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 ) ) )
156 155 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 ) ) )
157 156 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 ) )
158 vex 
 |-  v e. _V
159 158 elint2 
 |-  ( v e. |^| t <-> A. z e. t v e. z )
160 157 159 imbitrrdi 
 |-  ( ( ( 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 ) )
161 eleq2 
 |-  ( w = |^| t -> ( v e. w <-> v e. |^| t ) )
162 161 ad2antrr 
 |-  ( ( ( w = |^| t /\ A. s e. t X = ( U. ( f ` s ) u. s ) ) /\ v e. X ) -> ( v e. w <-> v e. |^| t ) )
163 160 162 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 ) )
164 121 163 biimtrid 
 |-  ( ( ( 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 ) )
165 164 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 ) )
166 165 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 ) ) )
167 orc 
 |-  ( E. s e. t y e. ( f ` s ) -> ( E. s e. t y e. ( f ` s ) \/ y = w ) )
168 167 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 ) ) )
169 168 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 ) ) )
170 equid 
 |-  w = w
171 vex 
 |-  w e. _V
172 equequ1 
 |-  ( y = w -> ( y = w <-> w = w ) )
173 138 172 anbi12d 
 |-  ( y = w -> ( ( v e. y /\ y = w ) <-> ( v e. w /\ w = w ) ) )
174 171 173 spcev 
 |-  ( ( v e. w /\ w = w ) -> E. y ( v e. y /\ y = w ) )
175 170 174 mpan2 
 |-  ( v e. w -> E. y ( v e. y /\ y = w ) )
176 olc 
 |-  ( y = w -> ( E. s e. t y e. ( f ` s ) \/ y = w ) )
177 176 anim2i 
 |-  ( ( v e. y /\ y = w ) -> ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) )
178 177 eximi 
 |-  ( E. y ( v e. y /\ y = w ) -> E. y ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) )
179 175 178 syl 
 |-  ( v e. w -> E. y ( v e. y /\ ( E. s e. t y e. ( f ` s ) \/ y = w ) ) )
180 169 179 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 ) ) )
181 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 } ) ) )
182 elun 
 |-  ( y e. ( U_ s e. t ( f ` s ) u. { w } ) <-> ( y e. U_ s e. t ( f ` s ) \/ y e. { w } ) )
183 eliun 
 |-  ( y e. U_ s e. t ( f ` s ) <-> E. s e. t y e. ( f ` s ) )
184 velsn 
 |-  ( y e. { w } <-> y = w )
185 183 184 orbi12i 
 |-  ( ( y e. U_ s e. t ( f ` s ) \/ y e. { w } ) <-> ( E. s e. t y e. ( f ` s ) \/ y = w ) )
186 182 185 bitri 
 |-  ( y e. ( U_ s e. t ( f ` s ) u. { w } ) <-> ( E. s e. t y e. ( f ` s ) \/ y = w ) )
187 186 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 ) ) )
188 187 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 ) ) )
189 181 188 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 } ) )
190 180 189 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 } ) )
191 166 190 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 } ) ) )
192 191 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 } ) ) )
193 192 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 } ) ) )
194 193 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 } ) )
195 elun 
 |-  ( v e. ( U_ s e. t ( f ` s ) u. { w } ) <-> ( v e. U_ s e. t ( f ` s ) \/ v e. { w } ) )
196 eliun 
 |-  ( v e. U_ s e. t ( f ` s ) <-> E. s e. t v e. ( f ` s ) )
197 velsn 
 |-  ( v e. { w } <-> v = w )
198 196 197 orbi12i 
 |-  ( ( v e. U_ s e. t ( f ` s ) \/ v e. { w } ) <-> ( E. s e. t v e. ( f ` s ) \/ v = w ) )
199 195 198 bitri 
 |-  ( v e. ( U_ s e. t ( f ` s ) u. { w } ) <-> ( E. s e. t v e. ( f ` s ) \/ v = w ) )
200 nfra1 
 |-  F/ s A. s e. t X = ( U. ( f ` s ) u. s )
201 nfv 
 |-  F/ s v C_ X
202 rsp 
 |-  ( A. s e. t X = ( U. ( f ` s ) u. s ) -> ( s e. t -> X = ( U. ( f ` s ) u. s ) ) )
203 eqimss2 
 |-  ( X = ( U. ( f ` s ) u. s ) -> ( U. ( f ` s ) u. s ) C_ X )
204 elssuni 
 |-  ( v e. ( f ` s ) -> v C_ U. ( f ` s ) )
205 ssun3 
 |-  ( v C_ U. ( f ` s ) -> v C_ ( U. ( f ` s ) u. s ) )
206 204 205 syl 
 |-  ( v e. ( f ` s ) -> v C_ ( U. ( f ` s ) u. s ) )
207 sstr 
 |-  ( ( v C_ ( U. ( f ` s ) u. s ) /\ ( U. ( f ` s ) u. s ) C_ X ) -> v C_ X )
208 207 expcom 
 |-  ( ( U. ( f ` s ) u. s ) C_ X -> ( v C_ ( U. ( f ` s ) u. s ) -> v C_ X ) )
209 203 206 208 syl2im 
 |-  ( X = ( U. ( f ` s ) u. s ) -> ( v e. ( f ` s ) -> v C_ X ) )
210 202 209 syl6 
 |-  ( A. s e. t X = ( U. ( f ` s ) u. s ) -> ( s e. t -> ( v e. ( f ` s ) -> v C_ X ) ) )
211 200 201 210 rexlimd 
 |-  ( A. s e. t X = ( U. ( f ` s ) u. s ) -> ( E. s e. t v e. ( f ` s ) -> v C_ X ) )
212 211 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 ) )
213 elpwi 
 |-  ( u e. ~P ( fi ` x ) -> u C_ ( fi ` x ) )
214 213 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 ) )
215 214 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 ) )
216 215 99 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 ) )
217 elssuni 
 |-  ( w e. ( fi ` x ) -> w C_ U. ( fi ` x ) )
218 216 217 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 ) )
219 57 58 ax-mp 
 |-  U. ( topGen ` ( fi ` x ) ) = U. ( fi ` x )
220 60 219 eqtr2di 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> U. ( fi ` x ) = U. J )
221 220 1 eqtr4di 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> U. ( fi ` x ) = X )
222 221 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 )
223 222 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 )
224 218 223 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 )
225 sseq1 
 |-  ( v = w -> ( v C_ X <-> w C_ X ) )
226 224 225 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 ) )
227 212 226 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 ) )
228 199 227 biimtrid 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ 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 ) )
229 228 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 )
230 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 )
231 229 230 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 )
232 194 231 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 } ) )
233 unieq 
 |-  ( b = ( U_ s e. t ( f ` s ) u. { w } ) -> U. b = U. ( U_ s e. t ( f ` s ) u. { w } ) )
234 233 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 )
235 116 232 234 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 )
236 235 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 ) )
237 236 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 ) )
238 78 88 237 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 ) )
239 5 238 biimtrid 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ 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 ) )
240 dfrex2 
 |-  ( E. b e. ( ~P u i^i Fin ) X = U. b <-> -. A. b e. ( ~P u i^i Fin ) -. X = U. b )
241 239 240 imbitrdi 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ 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 ) )
242 241 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 ) )
243 242 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 ) ) ) )
244 243 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 ) ) ) )
245 244 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 ) ) ) ) ) )
246 245 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 ) ) )
247 246 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 )