Metamath Proof Explorer

Theorem tgcmp

Description: A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub , which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion tgcmp 
|- ( ( B e. TopBases /\ X = U. B ) -> ( ( topGen ` B ) e. Comp <-> A. y e. ~P B ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. ( topGen ` B ) = U. ( topGen ` B )
2 1 iscmp 
 |-  ( ( topGen ` B ) e. Comp <-> ( ( topGen ` B ) e. Top /\ A. y e. ~P ( topGen ` B ) ( U. ( topGen ` B ) = U. y -> E. z e. ( ~P y i^i Fin ) U. ( topGen ` B ) = U. z ) ) )
3 2 simprbi 
 |-  ( ( topGen ` B ) e. Comp -> A. y e. ~P ( topGen ` B ) ( U. ( topGen ` B ) = U. y -> E. z e. ( ~P y i^i Fin ) U. ( topGen ` B ) = U. z ) )
4 unitg 
 |-  ( B e. TopBases -> U. ( topGen ` B ) = U. B )
5 eqtr3 
 |-  ( ( U. ( topGen ` B ) = U. B /\ X = U. B ) -> U. ( topGen ` B ) = X )
6 4 5 sylan 
 |-  ( ( B e. TopBases /\ X = U. B ) -> U. ( topGen ` B ) = X )
7 6 eqeq1d 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( U. ( topGen ` B ) = U. y <-> X = U. y ) )
8 6 eqeq1d 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( U. ( topGen ` B ) = U. z <-> X = U. z ) )
9 8 rexbidv 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( E. z e. ( ~P y i^i Fin ) U. ( topGen ` B ) = U. z <-> E. z e. ( ~P y i^i Fin ) X = U. z ) )
10 7 9 imbi12d 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( ( U. ( topGen ` B ) = U. y -> E. z e. ( ~P y i^i Fin ) U. ( topGen ` B ) = U. z ) <-> ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )
11 10 ralbidv 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( A. y e. ~P ( topGen ` B ) ( U. ( topGen ` B ) = U. y -> E. z e. ( ~P y i^i Fin ) U. ( topGen ` B ) = U. z ) <-> A. y e. ~P ( topGen ` B ) ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )
12 bastg 
 |-  ( B e. TopBases -> B C_ ( topGen ` B ) )
13 12 adantr 
 |-  ( ( B e. TopBases /\ X = U. B ) -> B C_ ( topGen ` B ) )
14 13 sspwd 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ~P B C_ ~P ( topGen ` B ) )
15 ssralv 
 |-  ( ~P B C_ ~P ( topGen ` B ) -> ( A. y e. ~P ( topGen ` B ) ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) -> A. y e. ~P B ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )
16 14 15 syl 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( A. y e. ~P ( topGen ` B ) ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) -> A. y e. ~P B ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )
17 11 16 sylbid 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( A. y e. ~P ( topGen ` B ) ( U. ( topGen ` B ) = U. y -> E. z e. ( ~P y i^i Fin ) U. ( topGen ` B ) = U. z ) -> A. y e. ~P B ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )
18 3 17 syl5 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( ( topGen ` B ) e. Comp -> A. y e. ~P B ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )
19 elpwi 
 |-  ( u e. ~P ( topGen ` B ) -> u C_ ( topGen ` B ) )
20 simprr 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) -> X = U. u )
21 simprl 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) -> u C_ ( topGen ` B ) )
22 21 sselda 
 |-  ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ t e. u ) -> t e. ( topGen ` B ) )
23 22 adantrr 
 |-  ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( t e. u /\ y e. t ) ) -> t e. ( topGen ` B ) )
24 simprr 
 |-  ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( t e. u /\ y e. t ) ) -> y e. t )
25 tg2 
 |-  ( ( t e. ( topGen ` B ) /\ y e. t ) -> E. w e. B ( y e. w /\ w C_ t ) )
26 23 24 25 syl2anc 
 |-  ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( t e. u /\ y e. t ) ) -> E. w e. B ( y e. w /\ w C_ t ) )
27 26 expr 
 |-  ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ t e. u ) -> ( y e. t -> E. w e. B ( y e. w /\ w C_ t ) ) )
28 27 reximdva 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) -> ( E. t e. u y e. t -> E. t e. u E. w e. B ( y e. w /\ w C_ t ) ) )
29 eluni2 
 |-  ( y e. U. u <-> E. t e. u y e. t )
30 elunirab 
 |-  ( y e. U. { w e. B | E. t e. u w C_ t } <-> E. w e. B ( y e. w /\ E. t e. u w C_ t ) )
31 r19.42v 
 |-  ( E. t e. u ( y e. w /\ w C_ t ) <-> ( y e. w /\ E. t e. u w C_ t ) )
32 31 rexbii 
 |-  ( E. w e. B E. t e. u ( y e. w /\ w C_ t ) <-> E. w e. B ( y e. w /\ E. t e. u w C_ t ) )
33 rexcom 
 |-  ( E. w e. B E. t e. u ( y e. w /\ w C_ t ) <-> E. t e. u E. w e. B ( y e. w /\ w C_ t ) )
34 30 32 33 3bitr2i 
 |-  ( y e. U. { w e. B | E. t e. u w C_ t } <-> E. t e. u E. w e. B ( y e. w /\ w C_ t ) )
35 28 29 34 3imtr4g 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) -> ( y e. U. u -> y e. U. { w e. B | E. t e. u w C_ t } ) )
36 35 ssrdv 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) -> U. u C_ U. { w e. B | E. t e. u w C_ t } )
37 20 36 eqsstrd 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) -> X C_ U. { w e. B | E. t e. u w C_ t } )
38 ssrab2 
 |-  { w e. B | E. t e. u w C_ t } C_ B
39 38 unissi 
 |-  U. { w e. B | E. t e. u w C_ t } C_ U. B
40 simplr 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) -> X = U. B )
41 39 40 sseqtrrid 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) -> U. { w e. B | E. t e. u w C_ t } C_ X )
42 37 41 eqssd 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) -> X = U. { w e. B | E. t e. u w C_ t } )
43 elpw2g 
 |-  ( B e. TopBases -> ( { w e. B | E. t e. u w C_ t } e. ~P B <-> { w e. B | E. t e. u w C_ t } C_ B ) )
44 43 ad2antrr 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) -> ( { w e. B | E. t e. u w C_ t } e. ~P B <-> { w e. B | E. t e. u w C_ t } C_ B ) )
45 38 44 mpbiri 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) -> { w e. B | E. t e. u w C_ t } e. ~P B )
46 unieq 
 |-  ( y = { w e. B | E. t e. u w C_ t } -> U. y = U. { w e. B | E. t e. u w C_ t } )
47 46 eqeq2d 
 |-  ( y = { w e. B | E. t e. u w C_ t } -> ( X = U. y <-> X = U. { w e. B | E. t e. u w C_ t } ) )
48 pweq 
 |-  ( y = { w e. B | E. t e. u w C_ t } -> ~P y = ~P { w e. B | E. t e. u w C_ t } )
49 48 ineq1d 
 |-  ( y = { w e. B | E. t e. u w C_ t } -> ( ~P y i^i Fin ) = ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) )
50 49 rexeqdv 
 |-  ( y = { w e. B | E. t e. u w C_ t } -> ( E. z e. ( ~P y i^i Fin ) X = U. z <-> E. z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) X = U. z ) )
51 47 50 imbi12d 
 |-  ( y = { w e. B | E. t e. u w C_ t } -> ( ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) <-> ( X = U. { w e. B | E. t e. u w C_ t } -> E. z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) X = U. z ) ) )
52 51 rspcv 
 |-  ( { w e. B | E. t e. u w C_ t } e. ~P B -> ( A. y e. ~P B ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) -> ( X = U. { w e. B | E. t e. u w C_ t } -> E. z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) X = U. z ) ) )
53 45 52 syl 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) -> ( A. y e. ~P B ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) -> ( X = U. { w e. B | E. t e. u w C_ t } -> E. z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) X = U. z ) ) )
54 42 53 mpid 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) -> ( A. y e. ~P B ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) -> E. z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) X = U. z ) )
55 elfpw 
 |-  ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) <-> ( z C_ { w e. B | E. t e. u w C_ t } /\ z e. Fin ) )
56 55 simprbi 
 |-  ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) -> z e. Fin )
57 56 ad2antrl 
 |-  ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) -> z e. Fin )
58 55 simplbi 
 |-  ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) -> z C_ { w e. B | E. t e. u w C_ t } )
59 58 ad2antrl 
 |-  ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) -> z C_ { w e. B | E. t e. u w C_ t } )
60 ssrab 
 |-  ( z C_ { w e. B | E. t e. u w C_ t } <-> ( z C_ B /\ A. w e. z E. t e. u w C_ t ) )
61 60 simprbi 
 |-  ( z C_ { w e. B | E. t e. u w C_ t } -> A. w e. z E. t e. u w C_ t )
62 59 61 syl 
 |-  ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) -> A. w e. z E. t e. u w C_ t )
63 sseq2 
 |-  ( t = ( f ` w ) -> ( w C_ t <-> w C_ ( f ` w ) ) )
64 63 ac6sfi 
 |-  ( ( z e. Fin /\ A. w e. z E. t e. u w C_ t ) -> E. f ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) )
65 57 62 64 syl2anc 
 |-  ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) -> E. f ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) )
66 frn 
 |-  ( f : z --> u -> ran f C_ u )
67 66 ad2antrl 
 |-  ( ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) /\ ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) ) -> ran f C_ u )
68 ffn 
 |-  ( f : z --> u -> f Fn z )
69 dffn4 
 |-  ( f Fn z <-> f : z -onto-> ran f )
70 68 69 sylib 
 |-  ( f : z --> u -> f : z -onto-> ran f )
71 70 adantr 
 |-  ( ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) -> f : z -onto-> ran f )
72 fofi 
 |-  ( ( z e. Fin /\ f : z -onto-> ran f ) -> ran f e. Fin )
73 57 71 72 syl2an 
 |-  ( ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) /\ ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) ) -> ran f e. Fin )
74 elfpw 
 |-  ( ran f e. ( ~P u i^i Fin ) <-> ( ran f C_ u /\ ran f e. Fin ) )
75 67 73 74 sylanbrc 
 |-  ( ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) /\ ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) ) -> ran f e. ( ~P u i^i Fin ) )
76 simplrr 
 |-  ( ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) /\ ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) ) -> X = U. z )
77 uniiun 
 |-  U. z = U_ w e. z w
78 ss2iun 
 |-  ( A. w e. z w C_ ( f ` w ) -> U_ w e. z w C_ U_ w e. z ( f ` w ) )
79 77 78 eqsstrid 
 |-  ( A. w e. z w C_ ( f ` w ) -> U. z C_ U_ w e. z ( f ` w ) )
80 79 ad2antll 
 |-  ( ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) /\ ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) ) -> U. z C_ U_ w e. z ( f ` w ) )
81 fniunfv 
 |-  ( f Fn z -> U_ w e. z ( f ` w ) = U. ran f )
82 68 81 syl 
 |-  ( f : z --> u -> U_ w e. z ( f ` w ) = U. ran f )
83 82 ad2antrl 
 |-  ( ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) /\ ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) ) -> U_ w e. z ( f ` w ) = U. ran f )
84 80 83 sseqtrd 
 |-  ( ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) /\ ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) ) -> U. z C_ U. ran f )
85 76 84 eqsstrd 
 |-  ( ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) /\ ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) ) -> X C_ U. ran f )
86 67 unissd 
 |-  ( ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) /\ ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) ) -> U. ran f C_ U. u )
87 20 ad2antrr 
 |-  ( ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) /\ ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) ) -> X = U. u )
88 86 87 sseqtrrd 
 |-  ( ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) /\ ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) ) -> U. ran f C_ X )
89 85 88 eqssd 
 |-  ( ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) /\ ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) ) -> X = U. ran f )
90 unieq 
 |-  ( v = ran f -> U. v = U. ran f )
91 90 rspceeqv 
 |-  ( ( ran f e. ( ~P u i^i Fin ) /\ X = U. ran f ) -> E. v e. ( ~P u i^i Fin ) X = U. v )
92 75 89 91 syl2anc 
 |-  ( ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) /\ ( f : z --> u /\ A. w e. z w C_ ( f ` w ) ) ) -> E. v e. ( ~P u i^i Fin ) X = U. v )
93 65 92 exlimddv 
 |-  ( ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) /\ ( z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) /\ X = U. z ) ) -> E. v e. ( ~P u i^i Fin ) X = U. v )
94 93 rexlimdvaa 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) -> ( E. z e. ( ~P { w e. B | E. t e. u w C_ t } i^i Fin ) X = U. z -> E. v e. ( ~P u i^i Fin ) X = U. v ) )
95 54 94 syld 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ ( u C_ ( topGen ` B ) /\ X = U. u ) ) -> ( A. y e. ~P B ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) -> E. v e. ( ~P u i^i Fin ) X = U. v ) )
96 95 expr 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ u C_ ( topGen ` B ) ) -> ( X = U. u -> ( A. y e. ~P B ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) -> E. v e. ( ~P u i^i Fin ) X = U. v ) ) )
97 96 com23 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ u C_ ( topGen ` B ) ) -> ( A. y e. ~P B ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) -> ( X = U. u -> E. v e. ( ~P u i^i Fin ) X = U. v ) ) )
98 19 97 sylan2 
 |-  ( ( ( B e. TopBases /\ X = U. B ) /\ u e. ~P ( topGen ` B ) ) -> ( A. y e. ~P B ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) -> ( X = U. u -> E. v e. ( ~P u i^i Fin ) X = U. v ) ) )
99 98 ralrimdva 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( A. y e. ~P B ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) -> A. u e. ~P ( topGen ` B ) ( X = U. u -> E. v e. ( ~P u i^i Fin ) X = U. v ) ) )
100 tgcl 
 |-  ( B e. TopBases -> ( topGen ` B ) e. Top )
101 100 adantr 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( topGen ` B ) e. Top )
102 1 iscmp 
 |-  ( ( topGen ` B ) e. Comp <-> ( ( topGen ` B ) e. Top /\ A. u e. ~P ( topGen ` B ) ( U. ( topGen ` B ) = U. u -> E. v e. ( ~P u i^i Fin ) U. ( topGen ` B ) = U. v ) ) )
103 102 baib 
 |-  ( ( topGen ` B ) e. Top -> ( ( topGen ` B ) e. Comp <-> A. u e. ~P ( topGen ` B ) ( U. ( topGen ` B ) = U. u -> E. v e. ( ~P u i^i Fin ) U. ( topGen ` B ) = U. v ) ) )
104 101 103 syl 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( ( topGen ` B ) e. Comp <-> A. u e. ~P ( topGen ` B ) ( U. ( topGen ` B ) = U. u -> E. v e. ( ~P u i^i Fin ) U. ( topGen ` B ) = U. v ) ) )
105 6 eqeq1d 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( U. ( topGen ` B ) = U. u <-> X = U. u ) )
106 6 eqeq1d 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( U. ( topGen ` B ) = U. v <-> X = U. v ) )
107 106 rexbidv 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( E. v e. ( ~P u i^i Fin ) U. ( topGen ` B ) = U. v <-> E. v e. ( ~P u i^i Fin ) X = U. v ) )
108 105 107 imbi12d 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( ( U. ( topGen ` B ) = U. u -> E. v e. ( ~P u i^i Fin ) U. ( topGen ` B ) = U. v ) <-> ( X = U. u -> E. v e. ( ~P u i^i Fin ) X = U. v ) ) )
109 108 ralbidv 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( A. u e. ~P ( topGen ` B ) ( U. ( topGen ` B ) = U. u -> E. v e. ( ~P u i^i Fin ) U. ( topGen ` B ) = U. v ) <-> A. u e. ~P ( topGen ` B ) ( X = U. u -> E. v e. ( ~P u i^i Fin ) X = U. v ) ) )
110 104 109 bitrd 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( ( topGen ` B ) e. Comp <-> A. u e. ~P ( topGen ` B ) ( X = U. u -> E. v e. ( ~P u i^i Fin ) X = U. v ) ) )
111 99 110 sylibrd 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( A. y e. ~P B ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) -> ( topGen ` B ) e. Comp ) )
112 18 111 impbid 
 |-  ( ( B e. TopBases /\ X = U. B ) -> ( ( topGen ` B ) e. Comp <-> A. y e. ~P B ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )