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