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 syl6ib
 |-  ( 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 syl6ib
 |-  ( 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 syl5bb
 |-  ( 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 syl6ib
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ 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 syl5bir
 |-  ( 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 syl5bi
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ 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 syl5bi
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ 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 syl5bi
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ 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 0fin
 |-  (/) 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 syl5bi
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ 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 syl5bir
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ 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 ) ) )