This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem alexsubALTlem4

Description: Lemma for alexsubALT . If any cover taken from a subbase has a finite subcover, any cover taken from the corresponding base has a finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010) (Revised by Mario Carneiro, 14-Dec-2013)

Ref Expression
Hypothesis alexsubALT.1 
|- X = U. J
Assertion alexsubALTlem4 
|- ( J = ( topGen ` ( fi ` x ) ) -> ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) ) )

Proof

Step Hyp Ref Expression
1 alexsubALT.1 
 |-  X = U. J
2 ralnex 
 |-  ( A. b e. ( ~P a i^i Fin ) -. X = U. b <-> -. E. b e. ( ~P a i^i Fin ) X = U. b )
3 1 alexsubALTlem2 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) -> E. u e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v )
4 elun 
 |-  ( u e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) <-> ( u e. { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } \/ u e. { (/) } ) )
5 sseq2 
 |-  ( z = u -> ( a C_ z <-> a C_ u ) )
6 pweq 
 |-  ( z = u -> ~P z = ~P u )
7 6 ineq1d 
 |-  ( z = u -> ( ~P z i^i Fin ) = ( ~P u i^i Fin ) )
8 7 raleqdv 
 |-  ( z = u -> ( A. b e. ( ~P z i^i Fin ) -. X = U. b <-> A. b e. ( ~P u i^i Fin ) -. X = U. b ) )
9 5 8 anbi12d 
 |-  ( z = u -> ( ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) <-> ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) )
10 9 elrab 
 |-  ( u e. { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } <-> ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) )
11 velsn 
 |-  ( u e. { (/) } <-> u = (/) )
12 10 11 orbi12i 
 |-  ( ( u e. { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } \/ u e. { (/) } ) <-> ( ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) \/ u = (/) ) )
13 4 12 bitri 
 |-  ( u e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) <-> ( ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) \/ u = (/) ) )
14 ralnex 
 |-  ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v <-> -. E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v )
15 simprrl 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> a C_ u )
16 15 unissd 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> U. a C_ U. u )
17 sseq1 
 |-  ( X = U. a -> ( X C_ U. u <-> U. a C_ U. u ) )
18 16 17 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( X = U. a -> X C_ U. u ) )
19 vex 
 |-  x e. _V
20 inss1 
 |-  ( x i^i u ) C_ x
21 19 20 elpwi2 
 |-  ( x i^i u ) e. ~P x
22 unieq 
 |-  ( c = ( x i^i u ) -> U. c = U. ( x i^i u ) )
23 22 eqeq2d 
 |-  ( c = ( x i^i u ) -> ( X = U. c <-> X = U. ( x i^i u ) ) )
24 pweq 
 |-  ( c = ( x i^i u ) -> ~P c = ~P ( x i^i u ) )
25 24 ineq1d 
 |-  ( c = ( x i^i u ) -> ( ~P c i^i Fin ) = ( ~P ( x i^i u ) i^i Fin ) )
26 25 rexeqdv 
 |-  ( c = ( x i^i u ) -> ( E. d e. ( ~P c i^i Fin ) X = U. d <-> E. d e. ( ~P ( x i^i u ) i^i Fin ) X = U. d ) )
27 23 26 imbi12d 
 |-  ( c = ( x i^i u ) -> ( ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) <-> ( X = U. ( x i^i u ) -> E. d e. ( ~P ( x i^i u ) i^i Fin ) X = U. d ) ) )
28 27 rspccv 
 |-  ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( ( x i^i u ) e. ~P x -> ( X = U. ( x i^i u ) -> E. d e. ( ~P ( x i^i u ) i^i Fin ) X = U. d ) ) )
29 21 28 mpi 
 |-  ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( X = U. ( x i^i u ) -> E. d e. ( ~P ( x i^i u ) i^i Fin ) X = U. d ) )
30 inss2 
 |-  ( x i^i u ) C_ u
31 sstr 
 |-  ( ( d C_ ( x i^i u ) /\ ( x i^i u ) C_ u ) -> d C_ u )
32 30 31 mpan2 
 |-  ( d C_ ( x i^i u ) -> d C_ u )
33 32 anim1i 
 |-  ( ( d C_ ( x i^i u ) /\ d e. Fin ) -> ( d C_ u /\ d e. Fin ) )
34 elfpw 
 |-  ( d e. ( ~P ( x i^i u ) i^i Fin ) <-> ( d C_ ( x i^i u ) /\ d e. Fin ) )
35 elfpw 
 |-  ( d e. ( ~P u i^i Fin ) <-> ( d C_ u /\ d e. Fin ) )
36 33 34 35 3imtr4i 
 |-  ( d e. ( ~P ( x i^i u ) i^i Fin ) -> d e. ( ~P u i^i Fin ) )
37 36 anim1i 
 |-  ( ( d e. ( ~P ( x i^i u ) i^i Fin ) /\ X = U. d ) -> ( d e. ( ~P u i^i Fin ) /\ X = U. d ) )
38 37 reximi2 
 |-  ( E. d e. ( ~P ( x i^i u ) i^i Fin ) X = U. d -> E. d e. ( ~P u i^i Fin ) X = U. d )
39 29 38 syl6 
 |-  ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( X = U. ( x i^i u ) -> E. d e. ( ~P u i^i Fin ) X = U. d ) )
40 unieq 
 |-  ( d = b -> U. d = U. b )
41 40 eqeq2d 
 |-  ( d = b -> ( X = U. d <-> X = U. b ) )
42 41 cbvrexvw 
 |-  ( E. d e. ( ~P u i^i Fin ) X = U. d <-> E. b e. ( ~P u i^i Fin ) X = U. b )
43 39 42 imbitrdi 
 |-  ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( X = U. ( x i^i u ) -> E. b e. ( ~P u i^i Fin ) X = U. b ) )
44 dfrex2 
 |-  ( E. b e. ( ~P u i^i Fin ) X = U. b <-> -. A. b e. ( ~P u i^i Fin ) -. X = U. b )
45 43 44 imbitrdi 
 |-  ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( X = U. ( x i^i u ) -> -. A. b e. ( ~P u i^i Fin ) -. X = U. b ) )
46 45 con2d 
 |-  ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( A. b e. ( ~P u i^i Fin ) -. X = U. b -> -. X = U. ( x i^i u ) ) )
47 46 a1d 
 |-  ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( a C_ u -> ( A. b e. ( ~P u i^i Fin ) -. X = U. b -> -. X = U. ( x i^i u ) ) ) )
48 47 3ad2ant2 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) -> ( a C_ u -> ( A. b e. ( ~P u i^i Fin ) -. X = U. b -> -. X = U. ( x i^i u ) ) ) )
49 48 adantr 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ u e. ~P ( fi ` x ) ) -> ( a C_ u -> ( A. b e. ( ~P u i^i Fin ) -. X = U. b -> -. X = U. ( x i^i u ) ) ) )
50 49 impd 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ u e. ~P ( fi ` x ) ) -> ( ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) -> -. X = U. ( x i^i u ) ) )
51 50 impr 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> -. X = U. ( x i^i u ) )
52 20 unissi 
 |-  U. ( x i^i u ) C_ U. x
53 fiuni 
 |-  ( x e. _V -> U. x = U. ( fi ` x ) )
54 53 elv 
 |-  U. x = U. ( fi ` x )
55 fibas 
 |-  ( fi ` x ) e. TopBases
56 unitg 
 |-  ( ( fi ` x ) e. TopBases -> U. ( topGen ` ( fi ` x ) ) = U. ( fi ` x ) )
57 55 56 ax-mp 
 |-  U. ( topGen ` ( fi ` x ) ) = U. ( fi ` x )
58 54 57 eqtr4i 
 |-  U. x = U. ( topGen ` ( fi ` x ) )
59 unieq 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> U. J = U. ( topGen ` ( fi ` x ) ) )
60 58 59 eqtr4id 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> U. x = U. J )
61 60 1 eqtr4di 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> U. x = 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. x = X )
63 62 adantr 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> U. x = X )
64 52 63 sseqtrid 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> U. ( x i^i u ) C_ X )
65 eqcom 
 |-  ( X = U. ( x i^i u ) <-> U. ( x i^i u ) = X )
66 eqss 
 |-  ( U. ( x i^i u ) = X <-> ( U. ( x i^i u ) C_ X /\ X C_ U. ( x i^i u ) ) )
67 66 baib 
 |-  ( U. ( x i^i u ) C_ X -> ( U. ( x i^i u ) = X <-> X C_ U. ( x i^i u ) ) )
68 65 67 bitrid 
 |-  ( U. ( x i^i u ) C_ X -> ( X = U. ( x i^i u ) <-> X C_ U. ( x i^i u ) ) )
69 64 68 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( X = U. ( x i^i u ) <-> X C_ U. ( x i^i u ) ) )
70 51 69 mtbid 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> -. X C_ U. ( x i^i u ) )
71 sstr2 
 |-  ( X C_ U. u -> ( U. u C_ U. ( x i^i u ) -> X C_ U. ( x i^i u ) ) )
72 71 con3rr3 
 |-  ( -. X C_ U. ( x i^i u ) -> ( X C_ U. u -> -. U. u C_ U. ( x i^i u ) ) )
73 70 72 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( X C_ U. u -> -. U. u C_ U. ( x i^i u ) ) )
74 nss 
 |-  ( -. U. u C_ U. ( x i^i u ) <-> E. y ( y e. U. u /\ -. y e. U. ( x i^i u ) ) )
75 df-rex 
 |-  ( E. y e. U. u -. y e. U. ( x i^i u ) <-> E. y ( y e. U. u /\ -. y e. U. ( x i^i u ) ) )
76 74 75 bitr4i 
 |-  ( -. U. u C_ U. ( x i^i u ) <-> E. y e. U. u -. y e. U. ( x i^i u ) )
77 eluni2 
 |-  ( y e. U. u <-> E. w e. u y e. w )
78 elpwi 
 |-  ( u e. ~P ( fi ` x ) -> u C_ ( fi ` x ) )
79 78 sseld 
 |-  ( u e. ~P ( fi ` x ) -> ( w e. u -> w e. ( fi ` x ) ) )
80 79 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( w e. u -> w e. ( fi ` x ) ) )
81 elfi 
 |-  ( ( w e. _V /\ x e. _V ) -> ( w e. ( fi ` x ) <-> E. t e. ( ~P x i^i Fin ) w = |^| t ) )
82 81 el2v 
 |-  ( w e. ( fi ` x ) <-> E. t e. ( ~P x i^i Fin ) w = |^| t )
83 80 82 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( w e. u -> E. t e. ( ~P x i^i Fin ) w = |^| t ) )
84 1 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 )
85 78 adantr 
 |-  ( ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) -> u C_ ( fi ` x ) )
86 85 ad4antlr 
 |-  ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> u C_ ( fi ` x ) )
87 ssfii 
 |-  ( x e. _V -> x C_ ( fi ` x ) )
88 87 elv 
 |-  x C_ ( fi ` x )
89 elinel1 
 |-  ( t e. ( ~P x i^i Fin ) -> t e. ~P x )
90 89 elpwid 
 |-  ( t e. ( ~P x i^i Fin ) -> t C_ x )
91 90 ad2antrr 
 |-  ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) -> t C_ x )
92 91 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> t C_ x )
93 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> s e. t )
94 92 93 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> s e. x )
95 88 94 sselid 
 |-  ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> s e. ( fi ` x ) )
96 95 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> { s } C_ ( fi ` x ) )
97 86 96 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> ( u u. { s } ) C_ ( fi ` x ) )
98 fvex 
 |-  ( fi ` x ) e. _V
99 98 elpw2 
 |-  ( ( u u. { s } ) e. ~P ( fi ` x ) <-> ( u u. { s } ) C_ ( fi ` x ) )
100 97 99 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> ( u u. { s } ) e. ~P ( fi ` x ) )
101 simprl 
 |-  ( ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) -> a C_ u )
102 101 ad4antlr 
 |-  ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> a C_ u )
103 ssun1 
 |-  u C_ ( u u. { s } )
104 102 103 sstrdi 
 |-  ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> a C_ ( u u. { s } ) )
105 unieq 
 |-  ( n = b -> U. n = U. b )
106 105 eqeq2d 
 |-  ( n = b -> ( X = U. n <-> X = U. b ) )
107 106 notbid 
 |-  ( n = b -> ( -. X = U. n <-> -. X = U. b ) )
108 107 cbvralvw 
 |-  ( A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n <-> A. b e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. b )
109 108 biimpi 
 |-  ( A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n -> A. b e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. b )
110 109 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> A. b e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. b )
111 100 104 110 jca32 
 |-  ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> ( ( u u. { s } ) e. ~P ( fi ` x ) /\ ( a C_ ( u u. { s } ) /\ A. b e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. b ) ) )
112 sseq2 
 |-  ( z = ( u u. { s } ) -> ( a C_ z <-> a C_ ( u u. { s } ) ) )
113 pweq 
 |-  ( z = ( u u. { s } ) -> ~P z = ~P ( u u. { s } ) )
114 113 ineq1d 
 |-  ( z = ( u u. { s } ) -> ( ~P z i^i Fin ) = ( ~P ( u u. { s } ) i^i Fin ) )
115 114 raleqdv 
 |-  ( z = ( u u. { s } ) -> ( A. b e. ( ~P z i^i Fin ) -. X = U. b <-> A. b e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. b ) )
116 112 115 anbi12d 
 |-  ( z = ( u u. { s } ) -> ( ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) <-> ( a C_ ( u u. { s } ) /\ A. b e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. b ) ) )
117 116 elrab 
 |-  ( ( u u. { s } ) e. { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } <-> ( ( u u. { s } ) e. ~P ( fi ` x ) /\ ( a C_ ( u u. { s } ) /\ A. b e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. b ) ) )
118 111 117 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> ( u u. { s } ) e. { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } )
119 elun1 
 |-  ( ( u u. { s } ) e. { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } -> ( u u. { s } ) e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) )
120 118 119 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> ( u u. { s } ) e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) )
121 vsnid 
 |-  s e. { s }
122 elun2 
 |-  ( s e. { s } -> s e. ( u u. { s } ) )
123 121 122 ax-mp 
 |-  s e. ( u u. { s } )
124 intss1 
 |-  ( s e. t -> |^| t C_ s )
125 sseq1 
 |-  ( w = |^| t -> ( w C_ s <-> |^| t C_ s ) )
126 124 125 syl5ibrcom 
 |-  ( s e. t -> ( w = |^| t -> w C_ s ) )
127 126 impcom 
 |-  ( ( w = |^| t /\ s e. t ) -> w C_ s )
128 127 ad4ant24 
 |-  ( ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ s e. t ) -> w C_ s )
129 128 adantl 
 |-  ( ( w e. u /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ s e. t ) ) -> w C_ s )
130 129 adantrrr 
 |-  ( ( w e. u /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> w C_ s )
131 130 adantll 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> w C_ s )
132 simprlr 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> y e. w )
133 131 132 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> y e. s )
134 90 ad2antrr 
 |-  ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) -> t C_ x )
135 134 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> t C_ x )
136 simprrl 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> s e. t )
137 135 136 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> s e. x )
138 elin 
 |-  ( s e. ( x i^i u ) <-> ( s e. x /\ s e. u ) )
139 elunii 
 |-  ( ( y e. s /\ s e. ( x i^i u ) ) -> y e. U. ( x i^i u ) )
140 139 ex 
 |-  ( y e. s -> ( s e. ( x i^i u ) -> y e. U. ( x i^i u ) ) )
141 138 140 biimtrrid 
 |-  ( y e. s -> ( ( s e. x /\ s e. u ) -> y e. U. ( x i^i u ) ) )
142 141 expd 
 |-  ( y e. s -> ( s e. x -> ( s e. u -> y e. U. ( x i^i u ) ) ) )
143 133 137 142 sylc 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> ( s e. u -> y e. U. ( x i^i u ) ) )
144 143 con3d 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> ( -. y e. U. ( x i^i u ) -> -. s e. u ) )
145 144 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) ) -> ( ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) -> ( -. y e. U. ( x i^i u ) -> -. s e. u ) ) )
146 145 com23 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) ) -> ( -. y e. U. ( x i^i u ) -> ( ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) -> -. s e. u ) ) )
147 146 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 ) -> ( ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) -> -. s e. u ) ) ) ) )
148 147 imp55 
 |-  ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> -. s e. u )
149 vex 
 |-  s e. _V
150 eleq1w 
 |-  ( v = s -> ( v e. ( u u. { s } ) <-> s e. ( u u. { s } ) ) )
151 elequ1 
 |-  ( v = s -> ( v e. u <-> s e. u ) )
152 151 notbid 
 |-  ( v = s -> ( -. v e. u <-> -. s e. u ) )
153 150 152 anbi12d 
 |-  ( v = s -> ( ( v e. ( u u. { s } ) /\ -. v e. u ) <-> ( s e. ( u u. { s } ) /\ -. s e. u ) ) )
154 149 153 spcev 
 |-  ( ( s e. ( u u. { s } ) /\ -. s e. u ) -> E. v ( v e. ( u u. { s } ) /\ -. v e. u ) )
155 123 148 154 sylancr 
 |-  ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> E. v ( v e. ( u u. { s } ) /\ -. v e. u ) )
156 nss 
 |-  ( -. ( u u. { s } ) C_ u <-> E. v ( v e. ( u u. { s } ) /\ -. v e. u ) )
157 155 156 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> -. ( u u. { s } ) C_ u )
158 eqimss2 
 |-  ( u = ( u u. { s } ) -> ( u u. { s } ) C_ u )
159 158 necon3bi 
 |-  ( -. ( u u. { s } ) C_ u -> u =/= ( u u. { s } ) )
160 157 159 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> u =/= ( u u. { s } ) )
161 160 103 jctil 
 |-  ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> ( u C_ ( u u. { s } ) /\ u =/= ( u u. { s } ) ) )
162 df-pss 
 |-  ( u C. ( u u. { s } ) <-> ( u C_ ( u u. { s } ) /\ u =/= ( u u. { s } ) ) )
163 161 162 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> u C. ( u u. { s } ) )
164 psseq2 
 |-  ( v = ( u u. { s } ) -> ( u C. v <-> u C. ( u u. { s } ) ) )
165 164 rspcev 
 |-  ( ( ( u u. { s } ) e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) /\ u C. ( u u. { s } ) ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v )
166 120 163 165 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v )
167 84 166 rexlimddv 
 |-  ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v )
168 167 exp45 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) -> ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) -> ( y e. w -> ( -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) ) ) )
169 168 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) -> ( t e. ( ~P x i^i Fin ) -> ( w = |^| t -> ( y e. w -> ( -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) ) ) ) )
170 169 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) -> ( E. t e. ( ~P x i^i Fin ) w = |^| t -> ( y e. w -> ( -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) ) ) )
171 170 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( w e. u -> ( E. t e. ( ~P x i^i Fin ) w = |^| t -> ( y e. w -> ( -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) ) ) ) )
172 83 171 mpdd 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( w e. u -> ( y e. w -> ( -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) ) ) )
173 172 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( E. w e. u y e. w -> ( -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) ) )
174 77 173 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( y e. U. u -> ( -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) ) )
175 174 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( E. y e. U. u -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) )
176 76 175 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( -. U. u C_ U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) )
177 18 73 176 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( X = U. a -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) )
178 177 con3d 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( -. E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v -> -. X = U. a ) )
179 14 178 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) )
180 179 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 /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) ) )
181 180 adantr 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) -> ( ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) ) )
182 ssun1 
 |-  { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } C_ ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } )
183 eqimss2 
 |-  ( z = a -> a C_ z )
184 183 biantrurd 
 |-  ( z = a -> ( A. b e. ( ~P z i^i Fin ) -. X = U. b <-> ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) ) )
185 pweq 
 |-  ( z = a -> ~P z = ~P a )
186 185 ineq1d 
 |-  ( z = a -> ( ~P z i^i Fin ) = ( ~P a i^i Fin ) )
187 186 raleqdv 
 |-  ( z = a -> ( A. b e. ( ~P z i^i Fin ) -. X = U. b <-> A. b e. ( ~P a i^i Fin ) -. X = U. b ) )
188 184 187 bitr3d 
 |-  ( z = a -> ( ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) <-> A. b e. ( ~P a i^i Fin ) -. X = U. b ) )
189 simpll3 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> a e. ~P ( fi ` x ) )
190 simplr 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> A. b e. ( ~P a i^i Fin ) -. X = U. b )
191 188 189 190 elrabd 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> a e. { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } )
192 182 191 sselid 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> a e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) )
193 psseq2 
 |-  ( v = a -> ( u C. v <-> u C. a ) )
194 193 notbid 
 |-  ( v = a -> ( -. u C. v <-> -. u C. a ) )
195 194 rspcv 
 |-  ( a e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. u C. a ) )
196 192 195 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 ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. u C. a ) )
197 id 
 |-  ( a = (/) -> a = (/) )
198 0elpw 
 |-  (/) e. ~P a
199 0fi 
 |-  (/) e. Fin
200 198 199 elini 
 |-  (/) e. ( ~P a i^i Fin )
201 197 200 eqeltrdi 
 |-  ( a = (/) -> a e. ( ~P a i^i Fin ) )
202 unieq 
 |-  ( b = a -> U. b = U. a )
203 202 eqeq2d 
 |-  ( b = a -> ( X = U. b <-> X = U. a ) )
204 203 notbid 
 |-  ( b = a -> ( -. X = U. b <-> -. X = U. a ) )
205 204 rspccv 
 |-  ( A. b e. ( ~P a i^i Fin ) -. X = U. b -> ( a e. ( ~P a i^i Fin ) -> -. X = U. a ) )
206 201 205 syl5 
 |-  ( A. b e. ( ~P a i^i Fin ) -. X = U. b -> ( a = (/) -> -. X = U. a ) )
207 206 necon2ad 
 |-  ( A. b e. ( ~P a i^i Fin ) -. X = U. b -> ( X = U. a -> a =/= (/) ) )
208 207 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 ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> ( X = U. a -> a =/= (/) ) )
209 psseq1 
 |-  ( u = (/) -> ( u C. a <-> (/) C. a ) )
210 209 adantl 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> ( u C. a <-> (/) C. a ) )
211 0pss 
 |-  ( (/) C. a <-> a =/= (/) )
212 210 211 bitrdi 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> ( u C. a <-> a =/= (/) ) )
213 208 212 sylibrd 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> ( X = U. a -> u C. a ) )
214 196 213 nsyld 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) )
215 214 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 ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) -> ( u = (/) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) ) )
216 181 215 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 ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) -> ( ( ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) \/ u = (/) ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) ) )
217 13 216 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 ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) -> ( u e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) ) )
218 217 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 ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) -> ( E. u e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) )
219 3 218 mpd 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) -> -. X = U. a )
220 219 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 ) ) -> ( A. b e. ( ~P a i^i Fin ) -. X = U. b -> -. X = U. a ) )
221 2 220 biimtrrid 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) -> ( -. E. b e. ( ~P a i^i Fin ) X = U. b -> -. X = U. a ) )
222 221 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 ) ) -> ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) )
223 222 3exp 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( a e. ~P ( fi ` x ) -> ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) ) ) )
224 223 ralrimdv 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) ) )