Metamath Proof Explorer

Theorem 2ndcomap

Description: A surjective continuous open map maps second-countable spaces to second-countable spaces. (Contributed by Mario Carneiro, 9-Apr-2015)

Ref Expression
Hypotheses 2ndcomap.2 
|- Y = U. K
2ndcomap.3 
|- ( ph -> J e. 2ndc )
2ndcomap.5 
|- ( ph -> F e. ( J Cn K ) )
2ndcomap.6 
|- ( ph -> ran F = Y )
2ndcomap.7 
|- ( ( ph /\ x e. J ) -> ( F " x ) e. K )
Assertion 2ndcomap 
|- ( ph -> K e. 2ndc )

Proof

Step Hyp Ref Expression
1 2ndcomap.2 
 |-  Y = U. K
2 2ndcomap.3 
 |-  ( ph -> J e. 2ndc )
3 2ndcomap.5 
 |-  ( ph -> F e. ( J Cn K ) )
4 2ndcomap.6 
 |-  ( ph -> ran F = Y )
5 2ndcomap.7 
 |-  ( ( ph /\ x e. J ) -> ( F " x ) e. K )
6 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
7 3 6 syl 
 |-  ( ph -> K e. Top )
8 7 ad2antrr 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> K e. Top )
9 simplll 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ x e. b ) -> ph )
10 bastg 
 |-  ( b e. TopBases -> b C_ ( topGen ` b ) )
11 10 ad2antlr 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> b C_ ( topGen ` b ) )
12 simprr 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> ( topGen ` b ) = J )
13 11 12 sseqtrd 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> b C_ J )
14 13 sselda 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ x e. b ) -> x e. J )
15 9 14 5 syl2anc 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ x e. b ) -> ( F " x ) e. K )
16 15 fmpttd 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> ( x e. b |-> ( F " x ) ) : b --> K )
17 16 frnd 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> ran ( x e. b |-> ( F " x ) ) C_ K )
18 elunii 
 |-  ( ( z e. k /\ k e. K ) -> z e. U. K )
19 18 1 eleqtrrdi 
 |-  ( ( z e. k /\ k e. K ) -> z e. Y )
20 19 ancoms 
 |-  ( ( k e. K /\ z e. k ) -> z e. Y )
21 20 adantl 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( k e. K /\ z e. k ) ) -> z e. Y )
22 4 ad3antrrr 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( k e. K /\ z e. k ) ) -> ran F = Y )
23 21 22 eleqtrrd 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( k e. K /\ z e. k ) ) -> z e. ran F )
24 eqid 
 |-  U. J = U. J
25 24 1 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> Y )
26 3 25 syl 
 |-  ( ph -> F : U. J --> Y )
27 26 ad3antrrr 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( k e. K /\ z e. k ) ) -> F : U. J --> Y )
28 ffn 
 |-  ( F : U. J --> Y -> F Fn U. J )
29 fvelrnb 
 |-  ( F Fn U. J -> ( z e. ran F <-> E. t e. U. J ( F ` t ) = z ) )
30 27 28 29 3syl 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( k e. K /\ z e. k ) ) -> ( z e. ran F <-> E. t e. U. J ( F ` t ) = z ) )
31 23 30 mpbid 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( k e. K /\ z e. k ) ) -> E. t e. U. J ( F ` t ) = z )
32 3 ad3antrrr 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) -> F e. ( J Cn K ) )
33 simprll 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) -> k e. K )
34 cnima 
 |-  ( ( F e. ( J Cn K ) /\ k e. K ) -> ( `' F " k ) e. J )
35 32 33 34 syl2anc 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) -> ( `' F " k ) e. J )
36 12 adantr 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) -> ( topGen ` b ) = J )
37 35 36 eleqtrrd 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) -> ( `' F " k ) e. ( topGen ` b ) )
38 simprrl 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) -> t e. U. J )
39 simprrr 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) -> ( F ` t ) = z )
40 simprlr 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) -> z e. k )
41 39 40 eqeltrd 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) -> ( F ` t ) e. k )
42 27 ffnd 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( k e. K /\ z e. k ) ) -> F Fn U. J )
43 42 adantrr 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) -> F Fn U. J )
44 elpreima 
 |-  ( F Fn U. J -> ( t e. ( `' F " k ) <-> ( t e. U. J /\ ( F ` t ) e. k ) ) )
45 43 44 syl 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) -> ( t e. ( `' F " k ) <-> ( t e. U. J /\ ( F ` t ) e. k ) ) )
46 38 41 45 mpbir2and 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) -> t e. ( `' F " k ) )
47 tg2 
 |-  ( ( ( `' F " k ) e. ( topGen ` b ) /\ t e. ( `' F " k ) ) -> E. m e. b ( t e. m /\ m C_ ( `' F " k ) ) )
48 37 46 47 syl2anc 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) -> E. m e. b ( t e. m /\ m C_ ( `' F " k ) ) )
49 simprl 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> m e. b )
50 eqid 
 |-  ( F " m ) = ( F " m )
51 imaeq2 
 |-  ( x = m -> ( F " x ) = ( F " m ) )
52 51 rspceeqv 
 |-  ( ( m e. b /\ ( F " m ) = ( F " m ) ) -> E. x e. b ( F " m ) = ( F " x ) )
53 49 50 52 sylancl 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> E. x e. b ( F " m ) = ( F " x ) )
54 43 adantr 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> F Fn U. J )
55 fnfun 
 |-  ( F Fn U. J -> Fun F )
56 54 55 syl 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> Fun F )
57 simprrr 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> m C_ ( `' F " k ) )
58 funimass2 
 |-  ( ( Fun F /\ m C_ ( `' F " k ) ) -> ( F " m ) C_ k )
59 56 57 58 syl2anc 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> ( F " m ) C_ k )
60 vex 
 |-  k e. _V
61 ssexg 
 |-  ( ( ( F " m ) C_ k /\ k e. _V ) -> ( F " m ) e. _V )
62 59 60 61 sylancl 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> ( F " m ) e. _V )
63 eqid 
 |-  ( x e. b |-> ( F " x ) ) = ( x e. b |-> ( F " x ) )
64 63 elrnmpt 
 |-  ( ( F " m ) e. _V -> ( ( F " m ) e. ran ( x e. b |-> ( F " x ) ) <-> E. x e. b ( F " m ) = ( F " x ) ) )
65 62 64 syl 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> ( ( F " m ) e. ran ( x e. b |-> ( F " x ) ) <-> E. x e. b ( F " m ) = ( F " x ) ) )
66 53 65 mpbird 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> ( F " m ) e. ran ( x e. b |-> ( F " x ) ) )
67 39 adantr 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> ( F ` t ) = z )
68 simprrl 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> t e. m )
69 cnvimass 
 |-  ( `' F " k ) C_ dom F
70 57 69 sstrdi 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> m C_ dom F )
71 funfvima2 
 |-  ( ( Fun F /\ m C_ dom F ) -> ( t e. m -> ( F ` t ) e. ( F " m ) ) )
72 56 70 71 syl2anc 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> ( t e. m -> ( F ` t ) e. ( F " m ) ) )
73 68 72 mpd 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> ( F ` t ) e. ( F " m ) )
74 67 73 eqeltrrd 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> z e. ( F " m ) )
75 eleq2 
 |-  ( w = ( F " m ) -> ( z e. w <-> z e. ( F " m ) ) )
76 sseq1 
 |-  ( w = ( F " m ) -> ( w C_ k <-> ( F " m ) C_ k ) )
77 75 76 anbi12d 
 |-  ( w = ( F " m ) -> ( ( z e. w /\ w C_ k ) <-> ( z e. ( F " m ) /\ ( F " m ) C_ k ) ) )
78 77 rspcev 
 |-  ( ( ( F " m ) e. ran ( x e. b |-> ( F " x ) ) /\ ( z e. ( F " m ) /\ ( F " m ) C_ k ) ) -> E. w e. ran ( x e. b |-> ( F " x ) ) ( z e. w /\ w C_ k ) )
79 66 74 59 78 syl12anc 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) /\ ( m e. b /\ ( t e. m /\ m C_ ( `' F " k ) ) ) ) -> E. w e. ran ( x e. b |-> ( F " x ) ) ( z e. w /\ w C_ k ) )
80 48 79 rexlimddv 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( ( k e. K /\ z e. k ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) ) -> E. w e. ran ( x e. b |-> ( F " x ) ) ( z e. w /\ w C_ k ) )
81 80 anassrs 
 |-  ( ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( k e. K /\ z e. k ) ) /\ ( t e. U. J /\ ( F ` t ) = z ) ) -> E. w e. ran ( x e. b |-> ( F " x ) ) ( z e. w /\ w C_ k ) )
82 31 81 rexlimddv 
 |-  ( ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) /\ ( k e. K /\ z e. k ) ) -> E. w e. ran ( x e. b |-> ( F " x ) ) ( z e. w /\ w C_ k ) )
83 82 ralrimivva 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> A. k e. K A. z e. k E. w e. ran ( x e. b |-> ( F " x ) ) ( z e. w /\ w C_ k ) )
84 basgen2 
 |-  ( ( K e. Top /\ ran ( x e. b |-> ( F " x ) ) C_ K /\ A. k e. K A. z e. k E. w e. ran ( x e. b |-> ( F " x ) ) ( z e. w /\ w C_ k ) ) -> ( topGen ` ran ( x e. b |-> ( F " x ) ) ) = K )
85 8 17 83 84 syl3anc 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> ( topGen ` ran ( x e. b |-> ( F " x ) ) ) = K )
86 85 8 eqeltrd 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> ( topGen ` ran ( x e. b |-> ( F " x ) ) ) e. Top )
87 tgclb 
 |-  ( ran ( x e. b |-> ( F " x ) ) e. TopBases <-> ( topGen ` ran ( x e. b |-> ( F " x ) ) ) e. Top )
88 86 87 sylibr 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> ran ( x e. b |-> ( F " x ) ) e. TopBases )
89 omelon 
 |-  _om e. On
90 simprl 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> b ~<_ _om )
91 ondomen 
 |-  ( ( _om e. On /\ b ~<_ _om ) -> b e. dom card )
92 89 90 91 sylancr 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> b e. dom card )
93 16 ffnd 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> ( x e. b |-> ( F " x ) ) Fn b )
94 dffn4 
 |-  ( ( x e. b |-> ( F " x ) ) Fn b <-> ( x e. b |-> ( F " x ) ) : b -onto-> ran ( x e. b |-> ( F " x ) ) )
95 93 94 sylib 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> ( x e. b |-> ( F " x ) ) : b -onto-> ran ( x e. b |-> ( F " x ) ) )
96 fodomnum 
 |-  ( b e. dom card -> ( ( x e. b |-> ( F " x ) ) : b -onto-> ran ( x e. b |-> ( F " x ) ) -> ran ( x e. b |-> ( F " x ) ) ~<_ b ) )
97 92 95 96 sylc 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> ran ( x e. b |-> ( F " x ) ) ~<_ b )
98 domtr 
 |-  ( ( ran ( x e. b |-> ( F " x ) ) ~<_ b /\ b ~<_ _om ) -> ran ( x e. b |-> ( F " x ) ) ~<_ _om )
99 97 90 98 syl2anc 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> ran ( x e. b |-> ( F " x ) ) ~<_ _om )
100 2ndci 
 |-  ( ( ran ( x e. b |-> ( F " x ) ) e. TopBases /\ ran ( x e. b |-> ( F " x ) ) ~<_ _om ) -> ( topGen ` ran ( x e. b |-> ( F " x ) ) ) e. 2ndc )
101 88 99 100 syl2anc 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> ( topGen ` ran ( x e. b |-> ( F " x ) ) ) e. 2ndc )
102 85 101 eqeltrrd 
 |-  ( ( ( ph /\ b e. TopBases ) /\ ( b ~<_ _om /\ ( topGen ` b ) = J ) ) -> K e. 2ndc )
103 is2ndc 
 |-  ( J e. 2ndc <-> E. b e. TopBases ( b ~<_ _om /\ ( topGen ` b ) = J ) )
104 2 103 sylib 
 |-  ( ph -> E. b e. TopBases ( b ~<_ _om /\ ( topGen ` b ) = J ) )
105 102 104 r19.29a 
 |-  ( ph -> K e. 2ndc )