Metamath Proof Explorer

Theorem 2ndcctbss

Description: If a topology is second-countable, every base has a countable subset which is a base. Exercise 16B2 in Willard. (Contributed by Jeff Hankins, 28-Jan-2010) (Proof shortened by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypotheses 2ndcctbss.1 
|- J = ( topGen ` B )
2ndcctbss.2 
|- S = { <. u , v >. | ( u e. c /\ v e. c /\ E. w e. B ( u C_ w /\ w C_ v ) ) }
Assertion 2ndcctbss 
|- ( ( B e. TopBases /\ J e. 2ndc ) -> E. b e. TopBases ( b ~<_ _om /\ b C_ B /\ J = ( topGen ` b ) ) )

Proof

Step Hyp Ref Expression
1 2ndcctbss.1 
 |-  J = ( topGen ` B )
2 2ndcctbss.2 
 |-  S = { <. u , v >. | ( u e. c /\ v e. c /\ E. w e. B ( u C_ w /\ w C_ v ) ) }
3 simpr 
 |-  ( ( B e. TopBases /\ J e. 2ndc ) -> J e. 2ndc )
4 is2ndc 
 |-  ( J e. 2ndc <-> E. c e. TopBases ( c ~<_ _om /\ ( topGen ` c ) = J ) )
5 3 4 sylib 
 |-  ( ( B e. TopBases /\ J e. 2ndc ) -> E. c e. TopBases ( c ~<_ _om /\ ( topGen ` c ) = J ) )
6 vex 
 |-  c e. _V
7 6 6 xpex 
 |-  ( c X. c ) e. _V
8 3simpa 
 |-  ( ( u e. c /\ v e. c /\ E. w e. B ( u C_ w /\ w C_ v ) ) -> ( u e. c /\ v e. c ) )
9 8 ssopab2i 
 |-  { <. u , v >. | ( u e. c /\ v e. c /\ E. w e. B ( u C_ w /\ w C_ v ) ) } C_ { <. u , v >. | ( u e. c /\ v e. c ) }
10 df-xp 
 |-  ( c X. c ) = { <. u , v >. | ( u e. c /\ v e. c ) }
11 9 2 10 3sstr4i 
 |-  S C_ ( c X. c )
12 ssdomg 
 |-  ( ( c X. c ) e. _V -> ( S C_ ( c X. c ) -> S ~<_ ( c X. c ) ) )
13 7 11 12 mp2 
 |-  S ~<_ ( c X. c )
14 6 xpdom1 
 |-  ( c ~<_ _om -> ( c X. c ) ~<_ ( _om X. c ) )
15 omex 
 |-  _om e. _V
16 15 xpdom2 
 |-  ( c ~<_ _om -> ( _om X. c ) ~<_ ( _om X. _om ) )
17 domtr 
 |-  ( ( ( c X. c ) ~<_ ( _om X. c ) /\ ( _om X. c ) ~<_ ( _om X. _om ) ) -> ( c X. c ) ~<_ ( _om X. _om ) )
18 14 16 17 syl2anc 
 |-  ( c ~<_ _om -> ( c X. c ) ~<_ ( _om X. _om ) )
19 xpomen 
 |-  ( _om X. _om ) ~~ _om
20 domentr 
 |-  ( ( ( c X. c ) ~<_ ( _om X. _om ) /\ ( _om X. _om ) ~~ _om ) -> ( c X. c ) ~<_ _om )
21 18 19 20 sylancl 
 |-  ( c ~<_ _om -> ( c X. c ) ~<_ _om )
22 21 adantr 
 |-  ( ( c ~<_ _om /\ ( topGen ` c ) = J ) -> ( c X. c ) ~<_ _om )
23 22 ad2antll 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> ( c X. c ) ~<_ _om )
24 domtr 
 |-  ( ( S ~<_ ( c X. c ) /\ ( c X. c ) ~<_ _om ) -> S ~<_ _om )
25 13 23 24 sylancr 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> S ~<_ _om )
26 2 relopabiv 
 |-  Rel S
27 simpr 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ x e. S ) -> x e. S )
28 1st2nd 
 |-  ( ( Rel S /\ x e. S ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
29 26 27 28 sylancr 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ x e. S ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
30 29 27 eqeltrrd 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ x e. S ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. e. S )
31 df-br 
 |-  ( ( 1st ` x ) S ( 2nd ` x ) <-> <. ( 1st ` x ) , ( 2nd ` x ) >. e. S )
32 fvex 
 |-  ( 1st ` x ) e. _V
33 fvex 
 |-  ( 2nd ` x ) e. _V
34 simpl 
 |-  ( ( u = ( 1st ` x ) /\ v = ( 2nd ` x ) ) -> u = ( 1st ` x ) )
35 34 eleq1d 
 |-  ( ( u = ( 1st ` x ) /\ v = ( 2nd ` x ) ) -> ( u e. c <-> ( 1st ` x ) e. c ) )
36 simpr 
 |-  ( ( u = ( 1st ` x ) /\ v = ( 2nd ` x ) ) -> v = ( 2nd ` x ) )
37 36 eleq1d 
 |-  ( ( u = ( 1st ` x ) /\ v = ( 2nd ` x ) ) -> ( v e. c <-> ( 2nd ` x ) e. c ) )
38 sseq1 
 |-  ( u = ( 1st ` x ) -> ( u C_ w <-> ( 1st ` x ) C_ w ) )
39 sseq2 
 |-  ( v = ( 2nd ` x ) -> ( w C_ v <-> w C_ ( 2nd ` x ) ) )
40 38 39 bi2anan9 
 |-  ( ( u = ( 1st ` x ) /\ v = ( 2nd ` x ) ) -> ( ( u C_ w /\ w C_ v ) <-> ( ( 1st ` x ) C_ w /\ w C_ ( 2nd ` x ) ) ) )
41 40 rexbidv 
 |-  ( ( u = ( 1st ` x ) /\ v = ( 2nd ` x ) ) -> ( E. w e. B ( u C_ w /\ w C_ v ) <-> E. w e. B ( ( 1st ` x ) C_ w /\ w C_ ( 2nd ` x ) ) ) )
42 35 37 41 3anbi123d 
 |-  ( ( u = ( 1st ` x ) /\ v = ( 2nd ` x ) ) -> ( ( u e. c /\ v e. c /\ E. w e. B ( u C_ w /\ w C_ v ) ) <-> ( ( 1st ` x ) e. c /\ ( 2nd ` x ) e. c /\ E. w e. B ( ( 1st ` x ) C_ w /\ w C_ ( 2nd ` x ) ) ) ) )
43 32 33 42 2 braba 
 |-  ( ( 1st ` x ) S ( 2nd ` x ) <-> ( ( 1st ` x ) e. c /\ ( 2nd ` x ) e. c /\ E. w e. B ( ( 1st ` x ) C_ w /\ w C_ ( 2nd ` x ) ) ) )
44 31 43 bitr3i 
 |-  ( <. ( 1st ` x ) , ( 2nd ` x ) >. e. S <-> ( ( 1st ` x ) e. c /\ ( 2nd ` x ) e. c /\ E. w e. B ( ( 1st ` x ) C_ w /\ w C_ ( 2nd ` x ) ) ) )
45 44 simp3bi 
 |-  ( <. ( 1st ` x ) , ( 2nd ` x ) >. e. S -> E. w e. B ( ( 1st ` x ) C_ w /\ w C_ ( 2nd ` x ) ) )
46 30 45 syl 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ x e. S ) -> E. w e. B ( ( 1st ` x ) C_ w /\ w C_ ( 2nd ` x ) ) )
47 fvi 
 |-  ( B e. TopBases -> ( _I ` B ) = B )
48 47 ad3antrrr 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ x e. S ) -> ( _I ` B ) = B )
49 48 rexeqdv 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ x e. S ) -> ( E. w e. ( _I ` B ) ( ( 1st ` x ) C_ w /\ w C_ ( 2nd ` x ) ) <-> E. w e. B ( ( 1st ` x ) C_ w /\ w C_ ( 2nd ` x ) ) ) )
50 46 49 mpbird 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ x e. S ) -> E. w e. ( _I ` B ) ( ( 1st ` x ) C_ w /\ w C_ ( 2nd ` x ) ) )
51 50 ralrimiva 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> A. x e. S E. w e. ( _I ` B ) ( ( 1st ` x ) C_ w /\ w C_ ( 2nd ` x ) ) )
52 fvex 
 |-  ( _I ` B ) e. _V
53 sseq2 
 |-  ( w = ( f ` x ) -> ( ( 1st ` x ) C_ w <-> ( 1st ` x ) C_ ( f ` x ) ) )
54 sseq1 
 |-  ( w = ( f ` x ) -> ( w C_ ( 2nd ` x ) <-> ( f ` x ) C_ ( 2nd ` x ) ) )
55 53 54 anbi12d 
 |-  ( w = ( f ` x ) -> ( ( ( 1st ` x ) C_ w /\ w C_ ( 2nd ` x ) ) <-> ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) )
56 52 55 axcc4dom 
 |-  ( ( S ~<_ _om /\ A. x e. S E. w e. ( _I ` B ) ( ( 1st ` x ) C_ w /\ w C_ ( 2nd ` x ) ) ) -> E. f ( f : S --> ( _I ` B ) /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) )
57 25 51 56 syl2anc 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> E. f ( f : S --> ( _I ` B ) /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) )
58 47 ad2antrr 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> ( _I ` B ) = B )
59 58 feq3d 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> ( f : S --> ( _I ` B ) <-> f : S --> B ) )
60 59 anbi1d 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> ( ( f : S --> ( _I ` B ) /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) <-> ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) )
61 2ndctop 
 |-  ( J e. 2ndc -> J e. Top )
62 61 adantl 
 |-  ( ( B e. TopBases /\ J e. 2ndc ) -> J e. Top )
63 62 ad2antrr 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> J e. Top )
64 frn 
 |-  ( f : S --> B -> ran f C_ B )
65 64 ad2antrl 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> ran f C_ B )
66 bastg 
 |-  ( B e. TopBases -> B C_ ( topGen ` B ) )
67 66 ad3antrrr 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> B C_ ( topGen ` B ) )
68 67 1 sseqtrrdi 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> B C_ J )
69 65 68 sstrd 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> ran f C_ J )
70 simprrl 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) -> o e. J )
71 simprr 
 |-  ( ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) -> ( topGen ` c ) = J )
72 71 ad2antlr 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) -> ( topGen ` c ) = J )
73 70 72 eleqtrrd 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) -> o e. ( topGen ` c ) )
74 simprrr 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) -> t e. o )
75 tg2 
 |-  ( ( o e. ( topGen ` c ) /\ t e. o ) -> E. d e. c ( t e. d /\ d C_ o ) )
76 73 74 75 syl2anc 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) -> E. d e. c ( t e. d /\ d C_ o ) )
77 bastg 
 |-  ( c e. TopBases -> c C_ ( topGen ` c ) )
78 77 ad2antrl 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> c C_ ( topGen ` c ) )
79 78 ad2antrr 
 |-  ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) -> c C_ ( topGen ` c ) )
80 1 eqeq2i 
 |-  ( ( topGen ` c ) = J <-> ( topGen ` c ) = ( topGen ` B ) )
81 80 biimpi 
 |-  ( ( topGen ` c ) = J -> ( topGen ` c ) = ( topGen ` B ) )
82 81 adantl 
 |-  ( ( c ~<_ _om /\ ( topGen ` c ) = J ) -> ( topGen ` c ) = ( topGen ` B ) )
83 82 ad2antll 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> ( topGen ` c ) = ( topGen ` B ) )
84 83 ad2antrr 
 |-  ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) -> ( topGen ` c ) = ( topGen ` B ) )
85 79 84 sseqtrd 
 |-  ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) -> c C_ ( topGen ` B ) )
86 simprl 
 |-  ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) -> d e. c )
87 85 86 sseldd 
 |-  ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) -> d e. ( topGen ` B ) )
88 simprrl 
 |-  ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) -> t e. d )
89 tg2 
 |-  ( ( d e. ( topGen ` B ) /\ t e. d ) -> E. m e. B ( t e. m /\ m C_ d ) )
90 87 88 89 syl2anc 
 |-  ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) -> E. m e. B ( t e. m /\ m C_ d ) )
91 66 ad3antrrr 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) -> B C_ ( topGen ` B ) )
92 91 ad2antrr 
 |-  ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) -> B C_ ( topGen ` B ) )
93 72 ad2antrr 
 |-  ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) -> ( topGen ` c ) = J )
94 93 1 eqtr2di 
 |-  ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) -> ( topGen ` B ) = ( topGen ` c ) )
95 92 94 sseqtrd 
 |-  ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) -> B C_ ( topGen ` c ) )
96 simprl 
 |-  ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) -> m e. B )
97 95 96 sseldd 
 |-  ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) -> m e. ( topGen ` c ) )
98 simprrl 
 |-  ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) -> t e. m )
99 tg2 
 |-  ( ( m e. ( topGen ` c ) /\ t e. m ) -> E. n e. c ( t e. n /\ n C_ m ) )
100 97 98 99 syl2anc 
 |-  ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) -> E. n e. c ( t e. n /\ n C_ m ) )
101 ffn 
 |-  ( f : S --> B -> f Fn S )
102 101 ad2antrr 
 |-  ( ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) -> f Fn S )
103 102 ad2antlr 
 |-  ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) -> f Fn S )
104 103 ad2antrr 
 |-  ( ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> f Fn S )
105 simprl 
 |-  ( ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> n e. c )
106 86 ad2antrr 
 |-  ( ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> d e. c )
107 simplrl 
 |-  ( ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> m e. B )
108 simprrr 
 |-  ( ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> n C_ m )
109 simprr 
 |-  ( ( m e. B /\ ( t e. m /\ m C_ d ) ) -> m C_ d )
110 109 ad2antlr 
 |-  ( ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> m C_ d )
111 sseq2 
 |-  ( w = m -> ( n C_ w <-> n C_ m ) )
112 sseq1 
 |-  ( w = m -> ( w C_ d <-> m C_ d ) )
113 111 112 anbi12d 
 |-  ( w = m -> ( ( n C_ w /\ w C_ d ) <-> ( n C_ m /\ m C_ d ) ) )
114 113 rspcev 
 |-  ( ( m e. B /\ ( n C_ m /\ m C_ d ) ) -> E. w e. B ( n C_ w /\ w C_ d ) )
115 107 108 110 114 syl12anc 
 |-  ( ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> E. w e. B ( n C_ w /\ w C_ d ) )
116 df-br 
 |-  ( n S d <-> <. n , d >. e. S )
117 vex 
 |-  n e. _V
118 vex 
 |-  d e. _V
119 simpl 
 |-  ( ( u = n /\ v = d ) -> u = n )
120 119 eleq1d 
 |-  ( ( u = n /\ v = d ) -> ( u e. c <-> n e. c ) )
121 simpr 
 |-  ( ( u = n /\ v = d ) -> v = d )
122 121 eleq1d 
 |-  ( ( u = n /\ v = d ) -> ( v e. c <-> d e. c ) )
123 sseq1 
 |-  ( u = n -> ( u C_ w <-> n C_ w ) )
124 sseq2 
 |-  ( v = d -> ( w C_ v <-> w C_ d ) )
125 123 124 bi2anan9 
 |-  ( ( u = n /\ v = d ) -> ( ( u C_ w /\ w C_ v ) <-> ( n C_ w /\ w C_ d ) ) )
126 125 rexbidv 
 |-  ( ( u = n /\ v = d ) -> ( E. w e. B ( u C_ w /\ w C_ v ) <-> E. w e. B ( n C_ w /\ w C_ d ) ) )
127 120 122 126 3anbi123d 
 |-  ( ( u = n /\ v = d ) -> ( ( u e. c /\ v e. c /\ E. w e. B ( u C_ w /\ w C_ v ) ) <-> ( n e. c /\ d e. c /\ E. w e. B ( n C_ w /\ w C_ d ) ) ) )
128 117 118 127 2 braba 
 |-  ( n S d <-> ( n e. c /\ d e. c /\ E. w e. B ( n C_ w /\ w C_ d ) ) )
129 116 128 bitr3i 
 |-  ( <. n , d >. e. S <-> ( n e. c /\ d e. c /\ E. w e. B ( n C_ w /\ w C_ d ) ) )
130 105 106 115 129 syl3anbrc 
 |-  ( ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> <. n , d >. e. S )
131 fnfvelrn 
 |-  ( ( f Fn S /\ <. n , d >. e. S ) -> ( f ` <. n , d >. ) e. ran f )
132 104 130 131 syl2anc 
 |-  ( ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> ( f ` <. n , d >. ) e. ran f )
133 simprl 
 |-  ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> n e. c )
134 simplll 
 |-  ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> d e. c )
135 simplrl 
 |-  ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> m e. B )
136 simprrr 
 |-  ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> n C_ m )
137 109 ad2antlr 
 |-  ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> m C_ d )
138 135 136 137 114 syl12anc 
 |-  ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> E. w e. B ( n C_ w /\ w C_ d ) )
139 133 134 138 129 syl3anbrc 
 |-  ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> <. n , d >. e. S )
140 fveq2 
 |-  ( x = <. n , d >. -> ( 1st ` x ) = ( 1st ` <. n , d >. ) )
141 fveq2 
 |-  ( x = <. n , d >. -> ( f ` x ) = ( f ` <. n , d >. ) )
142 140 141 sseq12d 
 |-  ( x = <. n , d >. -> ( ( 1st ` x ) C_ ( f ` x ) <-> ( 1st ` <. n , d >. ) C_ ( f ` <. n , d >. ) ) )
143 fveq2 
 |-  ( x = <. n , d >. -> ( 2nd ` x ) = ( 2nd ` <. n , d >. ) )
144 141 143 sseq12d 
 |-  ( x = <. n , d >. -> ( ( f ` x ) C_ ( 2nd ` x ) <-> ( f ` <. n , d >. ) C_ ( 2nd ` <. n , d >. ) ) )
145 142 144 anbi12d 
 |-  ( x = <. n , d >. -> ( ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) <-> ( ( 1st ` <. n , d >. ) C_ ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ ( 2nd ` <. n , d >. ) ) ) )
146 145 rspcv 
 |-  ( <. n , d >. e. S -> ( A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) -> ( ( 1st ` <. n , d >. ) C_ ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ ( 2nd ` <. n , d >. ) ) ) )
147 139 146 syl 
 |-  ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> ( A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) -> ( ( 1st ` <. n , d >. ) C_ ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ ( 2nd ` <. n , d >. ) ) ) )
148 117 118 op1st 
 |-  ( 1st ` <. n , d >. ) = n
149 148 sseq1i 
 |-  ( ( 1st ` <. n , d >. ) C_ ( f ` <. n , d >. ) <-> n C_ ( f ` <. n , d >. ) )
150 117 118 op2nd 
 |-  ( 2nd ` <. n , d >. ) = d
151 150 sseq2i 
 |-  ( ( f ` <. n , d >. ) C_ ( 2nd ` <. n , d >. ) <-> ( f ` <. n , d >. ) C_ d )
152 149 151 anbi12i 
 |-  ( ( ( 1st ` <. n , d >. ) C_ ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ ( 2nd ` <. n , d >. ) ) <-> ( n C_ ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ d ) )
153 simprl 
 |-  ( ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) /\ ( n C_ ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ d ) ) -> n C_ ( f ` <. n , d >. ) )
154 simprl 
 |-  ( ( n e. c /\ ( t e. n /\ n C_ m ) ) -> t e. n )
155 154 ad2antlr 
 |-  ( ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) /\ ( n C_ ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ d ) ) -> t e. n )
156 153 155 sseldd 
 |-  ( ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) /\ ( n C_ ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ d ) ) -> t e. ( f ` <. n , d >. ) )
157 simprr 
 |-  ( ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) /\ ( n C_ ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ d ) ) -> ( f ` <. n , d >. ) C_ d )
158 simplrr 
 |-  ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) -> d C_ o )
159 158 ad2antrr 
 |-  ( ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) /\ ( n C_ ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ d ) ) -> d C_ o )
160 157 159 sstrd 
 |-  ( ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) /\ ( n C_ ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ d ) ) -> ( f ` <. n , d >. ) C_ o )
161 156 160 jca 
 |-  ( ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) /\ ( n C_ ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ d ) ) -> ( t e. ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ o ) )
162 161 ex 
 |-  ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> ( ( n C_ ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ d ) -> ( t e. ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ o ) ) )
163 152 162 syl5bi 
 |-  ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> ( ( ( 1st ` <. n , d >. ) C_ ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ ( 2nd ` <. n , d >. ) ) -> ( t e. ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ o ) ) )
164 147 163 syldc 
 |-  ( A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) -> ( ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> ( t e. ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ o ) ) )
165 164 exp4c 
 |-  ( A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) -> ( ( d e. c /\ ( t e. d /\ d C_ o ) ) -> ( ( m e. B /\ ( t e. m /\ m C_ d ) ) -> ( ( n e. c /\ ( t e. n /\ n C_ m ) ) -> ( t e. ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ o ) ) ) ) )
166 165 ad2antlr 
 |-  ( ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) -> ( ( d e. c /\ ( t e. d /\ d C_ o ) ) -> ( ( m e. B /\ ( t e. m /\ m C_ d ) ) -> ( ( n e. c /\ ( t e. n /\ n C_ m ) ) -> ( t e. ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ o ) ) ) ) )
167 166 adantl 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) -> ( ( d e. c /\ ( t e. d /\ d C_ o ) ) -> ( ( m e. B /\ ( t e. m /\ m C_ d ) ) -> ( ( n e. c /\ ( t e. n /\ n C_ m ) ) -> ( t e. ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ o ) ) ) ) )
168 167 imp41 
 |-  ( ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> ( t e. ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ o ) )
169 eleq2 
 |-  ( b = ( f ` <. n , d >. ) -> ( t e. b <-> t e. ( f ` <. n , d >. ) ) )
170 sseq1 
 |-  ( b = ( f ` <. n , d >. ) -> ( b C_ o <-> ( f ` <. n , d >. ) C_ o ) )
171 169 170 anbi12d 
 |-  ( b = ( f ` <. n , d >. ) -> ( ( t e. b /\ b C_ o ) <-> ( t e. ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ o ) ) )
172 171 rspcev 
 |-  ( ( ( f ` <. n , d >. ) e. ran f /\ ( t e. ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ o ) ) -> E. b e. ran f ( t e. b /\ b C_ o ) )
173 132 168 172 syl2anc 
 |-  ( ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) /\ ( n e. c /\ ( t e. n /\ n C_ m ) ) ) -> E. b e. ran f ( t e. b /\ b C_ o ) )
174 100 173 rexlimddv 
 |-  ( ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) -> E. b e. ran f ( t e. b /\ b C_ o ) )
175 90 174 rexlimddv 
 |-  ( ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) /\ ( d e. c /\ ( t e. d /\ d C_ o ) ) ) -> E. b e. ran f ( t e. b /\ b C_ o ) )
176 76 175 rexlimddv 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) /\ ( o e. J /\ t e. o ) ) ) -> E. b e. ran f ( t e. b /\ b C_ o ) )
177 176 expr 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> ( ( o e. J /\ t e. o ) -> E. b e. ran f ( t e. b /\ b C_ o ) ) )
178 177 ralrimivv 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> A. o e. J A. t e. o E. b e. ran f ( t e. b /\ b C_ o ) )
179 basgen2 
 |-  ( ( J e. Top /\ ran f C_ J /\ A. o e. J A. t e. o E. b e. ran f ( t e. b /\ b C_ o ) ) -> ( topGen ` ran f ) = J )
180 63 69 178 179 syl3anc 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> ( topGen ` ran f ) = J )
181 180 63 eqeltrd 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> ( topGen ` ran f ) e. Top )
182 tgclb 
 |-  ( ran f e. TopBases <-> ( topGen ` ran f ) e. Top )
183 181 182 sylibr 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> ran f e. TopBases )
184 omelon 
 |-  _om e. On
185 25 adantr 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> S ~<_ _om )
186 ondomen 
 |-  ( ( _om e. On /\ S ~<_ _om ) -> S e. dom card )
187 184 185 186 sylancr 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> S e. dom card )
188 101 ad2antrl 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> f Fn S )
189 dffn4 
 |-  ( f Fn S <-> f : S -onto-> ran f )
190 188 189 sylib 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> f : S -onto-> ran f )
191 fodomnum 
 |-  ( S e. dom card -> ( f : S -onto-> ran f -> ran f ~<_ S ) )
192 187 190 191 sylc 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> ran f ~<_ S )
193 domtr 
 |-  ( ( ran f ~<_ S /\ S ~<_ _om ) -> ran f ~<_ _om )
194 192 185 193 syl2anc 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> ran f ~<_ _om )
195 180 eqcomd 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> J = ( topGen ` ran f ) )
196 breq1 
 |-  ( b = ran f -> ( b ~<_ _om <-> ran f ~<_ _om ) )
197 sseq1 
 |-  ( b = ran f -> ( b C_ B <-> ran f C_ B ) )
198 fveq2 
 |-  ( b = ran f -> ( topGen ` b ) = ( topGen ` ran f ) )
199 198 eqeq2d 
 |-  ( b = ran f -> ( J = ( topGen ` b ) <-> J = ( topGen ` ran f ) ) )
200 196 197 199 3anbi123d 
 |-  ( b = ran f -> ( ( b ~<_ _om /\ b C_ B /\ J = ( topGen ` b ) ) <-> ( ran f ~<_ _om /\ ran f C_ B /\ J = ( topGen ` ran f ) ) ) )
201 200 rspcev 
 |-  ( ( ran f e. TopBases /\ ( ran f ~<_ _om /\ ran f C_ B /\ J = ( topGen ` ran f ) ) ) -> E. b e. TopBases ( b ~<_ _om /\ b C_ B /\ J = ( topGen ` b ) ) )
202 183 194 65 195 201 syl13anc 
 |-  ( ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) /\ ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) ) -> E. b e. TopBases ( b ~<_ _om /\ b C_ B /\ J = ( topGen ` b ) ) )
203 202 ex 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> ( ( f : S --> B /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) -> E. b e. TopBases ( b ~<_ _om /\ b C_ B /\ J = ( topGen ` b ) ) ) )
204 60 203 sylbid 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> ( ( f : S --> ( _I ` B ) /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) -> E. b e. TopBases ( b ~<_ _om /\ b C_ B /\ J = ( topGen ` b ) ) ) )
205 204 exlimdv 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> ( E. f ( f : S --> ( _I ` B ) /\ A. x e. S ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) -> E. b e. TopBases ( b ~<_ _om /\ b C_ B /\ J = ( topGen ` b ) ) ) )
206 57 205 mpd 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> E. b e. TopBases ( b ~<_ _om /\ b C_ B /\ J = ( topGen ` b ) ) )
207 5 206 rexlimddv 
 |-  ( ( B e. TopBases /\ J e. 2ndc ) -> E. b e. TopBases ( b ~<_ _om /\ b C_ B /\ J = ( topGen ` b ) ) )