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 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 ) )
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 )