Metamath Proof Explorer

Theorem alexsubALT

Description: The Alexander Subbase Theorem: a space is compact iff it has a subbase such that any cover taken from the subbase has a finite subcover. (Contributed by Jeff Hankins, 24-Jan-2010) (Revised by Mario Carneiro, 11-Feb-2015) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 alexsubALT.1 
 |-  X = U. J
2 1 alexsubALTlem1 
 |-  ( J e. Comp -> E. x ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
3 1 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 ) ) )
4 velpw 
 |-  ( c e. ~P J <-> c C_ J )
5 eleq2 
 |-  ( X = U. c -> ( t e. X <-> t e. U. c ) )
6 5 3ad2ant3 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( t e. X <-> t e. U. c ) )
7 eluni 
 |-  ( t e. U. c <-> E. w ( t e. w /\ w e. c ) )
8 ssel 
 |-  ( c C_ J -> ( w e. c -> w e. J ) )
9 eleq2 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> ( w e. J <-> w e. ( topGen ` ( fi ` x ) ) ) )
10 tg2 
 |-  ( ( w e. ( topGen ` ( fi ` x ) ) /\ t e. w ) -> E. y e. ( fi ` x ) ( t e. y /\ y C_ w ) )
11 10 ex 
 |-  ( w e. ( topGen ` ( fi ` x ) ) -> ( t e. w -> E. y e. ( fi ` x ) ( t e. y /\ y C_ w ) ) )
12 9 11 syl6bi 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> ( w e. J -> ( t e. w -> E. y e. ( fi ` x ) ( t e. y /\ y C_ w ) ) ) )
13 8 12 sylan9r 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J ) -> ( w e. c -> ( t e. w -> E. y e. ( fi ` x ) ( t e. y /\ y C_ w ) ) ) )
14 13 3impia 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ w e. c ) -> ( t e. w -> E. y e. ( fi ` x ) ( t e. y /\ y C_ w ) ) )
15 sseq2 
 |-  ( z = w -> ( y C_ z <-> y C_ w ) )
16 15 rspcev 
 |-  ( ( w e. c /\ y C_ w ) -> E. z e. c y C_ z )
17 16 ex 
 |-  ( w e. c -> ( y C_ w -> E. z e. c y C_ z ) )
18 17 3ad2ant3 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ w e. c ) -> ( y C_ w -> E. z e. c y C_ z ) )
19 18 anim2d 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ w e. c ) -> ( ( t e. y /\ y C_ w ) -> ( t e. y /\ E. z e. c y C_ z ) ) )
20 19 reximdv 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ w e. c ) -> ( E. y e. ( fi ` x ) ( t e. y /\ y C_ w ) -> E. y e. ( fi ` x ) ( t e. y /\ E. z e. c y C_ z ) ) )
21 14 20 syld 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ w e. c ) -> ( t e. w -> E. y e. ( fi ` x ) ( t e. y /\ E. z e. c y C_ z ) ) )
22 21 3expia 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J ) -> ( w e. c -> ( t e. w -> E. y e. ( fi ` x ) ( t e. y /\ E. z e. c y C_ z ) ) ) )
23 22 com23 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J ) -> ( t e. w -> ( w e. c -> E. y e. ( fi ` x ) ( t e. y /\ E. z e. c y C_ z ) ) ) )
24 23 impd 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J ) -> ( ( t e. w /\ w e. c ) -> E. y e. ( fi ` x ) ( t e. y /\ E. z e. c y C_ z ) ) )
25 24 exlimdv 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J ) -> ( E. w ( t e. w /\ w e. c ) -> E. y e. ( fi ` x ) ( t e. y /\ E. z e. c y C_ z ) ) )
26 7 25 syl5bi 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J ) -> ( t e. U. c -> E. y e. ( fi ` x ) ( t e. y /\ E. z e. c y C_ z ) ) )
27 26 3adant3 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( t e. U. c -> E. y e. ( fi ` x ) ( t e. y /\ E. z e. c y C_ z ) ) )
28 6 27 sylbid 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( t e. X -> E. y e. ( fi ` x ) ( t e. y /\ E. z e. c y C_ z ) ) )
29 ssel 
 |-  ( y C_ z -> ( t e. y -> t e. z ) )
30 elunii 
 |-  ( ( t e. z /\ z e. c ) -> t e. U. c )
31 30 expcom 
 |-  ( z e. c -> ( t e. z -> t e. U. c ) )
32 6 biimprd 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( t e. U. c -> t e. X ) )
33 31 32 sylan9r 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ z e. c ) -> ( t e. z -> t e. X ) )
34 29 33 syl9r 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ z e. c ) -> ( y C_ z -> ( t e. y -> t e. X ) ) )
35 34 rexlimdva 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( E. z e. c y C_ z -> ( t e. y -> t e. X ) ) )
36 35 com23 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( t e. y -> ( E. z e. c y C_ z -> t e. X ) ) )
37 36 impd 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( ( t e. y /\ E. z e. c y C_ z ) -> t e. X ) )
38 37 rexlimdvw 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( E. y e. ( fi ` x ) ( t e. y /\ E. z e. c y C_ z ) -> t e. X ) )
39 28 38 impbid 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( t e. X <-> E. y e. ( fi ` x ) ( t e. y /\ E. z e. c y C_ z ) ) )
40 elunirab 
 |-  ( t e. U. { y e. ( fi ` x ) | E. z e. c y C_ z } <-> E. y e. ( fi ` x ) ( t e. y /\ E. z e. c y C_ z ) )
41 39 40 bitr4di 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( t e. X <-> t e. U. { y e. ( fi ` x ) | E. z e. c y C_ z } ) )
42 41 eqrdv 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> X = U. { y e. ( fi ` x ) | E. z e. c y C_ z } )
43 ssrab2 
 |-  { y e. ( fi ` x ) | E. z e. c y C_ z } C_ ( fi ` x )
44 fvex 
 |-  ( fi ` x ) e. _V
45 44 elpw2 
 |-  ( { y e. ( fi ` x ) | E. z e. c y C_ z } e. ~P ( fi ` x ) <-> { y e. ( fi ` x ) | E. z e. c y C_ z } C_ ( fi ` x ) )
46 43 45 mpbir 
 |-  { y e. ( fi ` x ) | E. z e. c y C_ z } e. ~P ( fi ` x )
47 unieq 
 |-  ( a = { y e. ( fi ` x ) | E. z e. c y C_ z } -> U. a = U. { y e. ( fi ` x ) | E. z e. c y C_ z } )
48 47 eqeq2d 
 |-  ( a = { y e. ( fi ` x ) | E. z e. c y C_ z } -> ( X = U. a <-> X = U. { y e. ( fi ` x ) | E. z e. c y C_ z } ) )
49 pweq 
 |-  ( a = { y e. ( fi ` x ) | E. z e. c y C_ z } -> ~P a = ~P { y e. ( fi ` x ) | E. z e. c y C_ z } )
50 49 ineq1d 
 |-  ( a = { y e. ( fi ` x ) | E. z e. c y C_ z } -> ( ~P a i^i Fin ) = ( ~P { y e. ( fi ` x ) | E. z e. c y C_ z } i^i Fin ) )
51 50 rexeqdv 
 |-  ( a = { y e. ( fi ` x ) | E. z e. c y C_ z } -> ( E. b e. ( ~P a i^i Fin ) X = U. b <-> E. b e. ( ~P { y e. ( fi ` x ) | E. z e. c y C_ z } i^i Fin ) X = U. b ) )
52 48 51 imbi12d 
 |-  ( a = { y e. ( fi ` x ) | E. z e. c y C_ z } -> ( ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) <-> ( X = U. { y e. ( fi ` x ) | E. z e. c y C_ z } -> E. b e. ( ~P { y e. ( fi ` x ) | E. z e. c y C_ z } i^i Fin ) X = U. b ) ) )
53 52 rspcv 
 |-  ( { y e. ( fi ` x ) | E. z e. c y C_ z } e. ~P ( fi ` x ) -> ( A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) -> ( X = U. { y e. ( fi ` x ) | E. z e. c y C_ z } -> E. b e. ( ~P { y e. ( fi ` x ) | E. z e. c y C_ z } i^i Fin ) X = U. b ) ) )
54 46 53 ax-mp 
 |-  ( A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) -> ( X = U. { y e. ( fi ` x ) | E. z e. c y C_ z } -> E. b e. ( ~P { y e. ( fi ` x ) | E. z e. c y C_ z } i^i Fin ) X = U. b ) )
55 42 54 syl5com 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) -> E. b e. ( ~P { y e. ( fi ` x ) | E. z e. c y C_ z } i^i Fin ) X = U. b ) )
56 elfpw 
 |-  ( b e. ( ~P { y e. ( fi ` x ) | E. z e. c y C_ z } i^i Fin ) <-> ( b C_ { y e. ( fi ` x ) | E. z e. c y C_ z } /\ b e. Fin ) )
57 ssel 
 |-  ( b C_ { y e. ( fi ` x ) | E. z e. c y C_ z } -> ( t e. b -> t e. { y e. ( fi ` x ) | E. z e. c y C_ z } ) )
58 sseq1 
 |-  ( y = t -> ( y C_ z <-> t C_ z ) )
59 58 rexbidv 
 |-  ( y = t -> ( E. z e. c y C_ z <-> E. z e. c t C_ z ) )
60 59 elrab 
 |-  ( t e. { y e. ( fi ` x ) | E. z e. c y C_ z } <-> ( t e. ( fi ` x ) /\ E. z e. c t C_ z ) )
61 60 simprbi 
 |-  ( t e. { y e. ( fi ` x ) | E. z e. c y C_ z } -> E. z e. c t C_ z )
62 57 61 syl6 
 |-  ( b C_ { y e. ( fi ` x ) | E. z e. c y C_ z } -> ( t e. b -> E. z e. c t C_ z ) )
63 62 ralrimiv 
 |-  ( b C_ { y e. ( fi ` x ) | E. z e. c y C_ z } -> A. t e. b E. z e. c t C_ z )
64 sseq2 
 |-  ( z = ( f ` t ) -> ( t C_ z <-> t C_ ( f ` t ) ) )
65 64 ac6sfi 
 |-  ( ( b e. Fin /\ A. t e. b E. z e. c t C_ z ) -> E. f ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) )
66 65 ex 
 |-  ( b e. Fin -> ( A. t e. b E. z e. c t C_ z -> E. f ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) ) )
67 63 66 syl5 
 |-  ( b e. Fin -> ( b C_ { y e. ( fi ` x ) | E. z e. c y C_ z } -> E. f ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) ) )
68 67 adantl 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) -> ( b C_ { y e. ( fi ` x ) | E. z e. c y C_ z } -> E. f ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) ) )
69 simprll 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> f : b --> c )
70 frn 
 |-  ( f : b --> c -> ran f C_ c )
71 69 70 syl 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> ran f C_ c )
72 simplr 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> b e. Fin )
73 ffn 
 |-  ( f : b --> c -> f Fn b )
74 dffn4 
 |-  ( f Fn b <-> f : b -onto-> ran f )
75 73 74 sylib 
 |-  ( f : b --> c -> f : b -onto-> ran f )
76 75 adantr 
 |-  ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) -> f : b -onto-> ran f )
77 76 ad2antrl 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> f : b -onto-> ran f )
78 fodomfi 
 |-  ( ( b e. Fin /\ f : b -onto-> ran f ) -> ran f ~<_ b )
79 72 77 78 syl2anc 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> ran f ~<_ b )
80 domfi 
 |-  ( ( b e. Fin /\ ran f ~<_ b ) -> ran f e. Fin )
81 72 79 80 syl2anc 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> ran f e. Fin )
82 71 81 jca 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> ( ran f C_ c /\ ran f e. Fin ) )
83 elin 
 |-  ( ran f e. ( ~P c i^i Fin ) <-> ( ran f e. ~P c /\ ran f e. Fin ) )
84 vex 
 |-  c e. _V
85 84 elpw2 
 |-  ( ran f e. ~P c <-> ran f C_ c )
86 85 anbi1i 
 |-  ( ( ran f e. ~P c /\ ran f e. Fin ) <-> ( ran f C_ c /\ ran f e. Fin ) )
87 83 86 bitr2i 
 |-  ( ( ran f C_ c /\ ran f e. Fin ) <-> ran f e. ( ~P c i^i Fin ) )
88 82 87 sylib 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> ran f e. ( ~P c i^i Fin ) )
89 simprr 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> X = U. b )
90 uniiun 
 |-  U. b = U_ t e. b t
91 simprlr 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> A. t e. b t C_ ( f ` t ) )
92 ss2iun 
 |-  ( A. t e. b t C_ ( f ` t ) -> U_ t e. b t C_ U_ t e. b ( f ` t ) )
93 91 92 syl 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> U_ t e. b t C_ U_ t e. b ( f ` t ) )
94 90 93 eqsstrid 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> U. b C_ U_ t e. b ( f ` t ) )
95 fniunfv 
 |-  ( f Fn b -> U_ t e. b ( f ` t ) = U. ran f )
96 69 73 95 3syl 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> U_ t e. b ( f ` t ) = U. ran f )
97 94 96 sseqtrd 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> U. b C_ U. ran f )
98 89 97 eqsstrd 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> X C_ U. ran f )
99 simpll2 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> c C_ J )
100 71 99 sstrd 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> ran f C_ J )
101 uniss 
 |-  ( ran f C_ J -> U. ran f C_ U. J )
102 101 1 sseqtrrdi 
 |-  ( ran f C_ J -> U. ran f C_ X )
103 100 102 syl 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> U. ran f C_ X )
104 98 103 eqssd 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> X = U. ran f )
105 unieq 
 |-  ( d = ran f -> U. d = U. ran f )
106 105 eqeq2d 
 |-  ( d = ran f -> ( X = U. d <-> X = U. ran f ) )
107 106 rspcev 
 |-  ( ( ran f e. ( ~P c i^i Fin ) /\ X = U. ran f ) -> E. d e. ( ~P c i^i Fin ) X = U. d )
108 88 104 107 syl2anc 
 |-  ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) /\ ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) /\ X = U. b ) ) -> E. d e. ( ~P c i^i Fin ) X = U. d )
109 108 exp32 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) -> ( ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) -> ( X = U. b -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
110 109 exlimdv 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) -> ( E. f ( f : b --> c /\ A. t e. b t C_ ( f ` t ) ) -> ( X = U. b -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
111 68 110 syld 
 |-  ( ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) /\ b e. Fin ) -> ( b C_ { y e. ( fi ` x ) | E. z e. c y C_ z } -> ( X = U. b -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
112 111 ex 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( b e. Fin -> ( b C_ { y e. ( fi ` x ) | E. z e. c y C_ z } -> ( X = U. b -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) ) )
113 112 com23 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( b C_ { y e. ( fi ` x ) | E. z e. c y C_ z } -> ( b e. Fin -> ( X = U. b -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) ) )
114 113 impd 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( ( b C_ { y e. ( fi ` x ) | E. z e. c y C_ z } /\ b e. Fin ) -> ( X = U. b -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
115 56 114 syl5bi 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( b e. ( ~P { y e. ( fi ` x ) | E. z e. c y C_ z } i^i Fin ) -> ( X = U. b -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
116 115 rexlimdv 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( E. b e. ( ~P { y e. ( fi ` x ) | E. z e. c y C_ z } i^i Fin ) X = U. b -> E. d e. ( ~P c i^i Fin ) X = U. d ) )
117 55 116 syld 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ c C_ J /\ X = U. c ) -> ( A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) -> E. d e. ( ~P c i^i Fin ) X = U. d ) )
118 117 3exp 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> ( c C_ J -> ( X = U. c -> ( A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) ) )
119 118 com34 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> ( c C_ J -> ( A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) -> ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) ) )
120 119 com23 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> ( A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) -> ( c C_ J -> ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) ) )
121 4 120 syl7bi 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> ( A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) -> ( c e. ~P J -> ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) ) )
122 121 ralrimdv 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> ( A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) -> A. c e. ~P J ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
123 fibas 
 |-  ( fi ` x ) e. TopBases
124 tgcl 
 |-  ( ( fi ` x ) e. TopBases -> ( topGen ` ( fi ` x ) ) e. Top )
125 123 124 ax-mp 
 |-  ( topGen ` ( fi ` x ) ) e. Top
126 eleq1 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> ( J e. Top <-> ( topGen ` ( fi ` x ) ) e. Top ) )
127 125 126 mpbiri 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> J e. Top )
128 122 127 jctild 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> ( A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) -> ( J e. Top /\ A. c e. ~P J ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) ) )
129 1 iscmp 
 |-  ( J e. Comp <-> ( J e. Top /\ A. c e. ~P J ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )
130 128 129 syl6ibr 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> ( A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) -> J e. Comp ) )
131 3 130 syld 
 |-  ( J = ( topGen ` ( fi ` x ) ) -> ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> J e. Comp ) )
132 131 imp 
 |-  ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) -> J e. Comp )
133 132 exlimiv 
 |-  ( E. x ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) -> J e. Comp )
134 2 133 impbii 
 |-  ( J e. Comp <-> E. x ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) )