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 46 48 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 ) ) )
50 49 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 ) ) )
51 fvex 
 |-  ( _I ` B ) e. _V
52 sseq2 
 |-  ( w = ( f ` x ) -> ( ( 1st ` x ) C_ w <-> ( 1st ` x ) C_ ( f ` x ) ) )
53 sseq1 
 |-  ( w = ( f ` x ) -> ( w C_ ( 2nd ` x ) <-> ( f ` x ) C_ ( 2nd ` x ) ) )
54 52 53 anbi12d 
 |-  ( w = ( f ` x ) -> ( ( ( 1st ` x ) C_ w /\ w C_ ( 2nd ` x ) ) <-> ( ( 1st ` x ) C_ ( f ` x ) /\ ( f ` x ) C_ ( 2nd ` x ) ) ) )
55 51 54 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 ) ) ) )
56 25 50 55 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 ) ) ) )
57 47 ad2antrr 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> ( _I ` B ) = B )
58 57 feq3d 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> ( f : S --> ( _I ` B ) <-> f : S --> B ) )
59 58 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 ) ) ) ) )
60 2ndctop 
 |-  ( J e. 2ndc -> J e. Top )
61 60 adantl 
 |-  ( ( B e. TopBases /\ J e. 2ndc ) -> J e. Top )
62 61 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 )
63 frn 
 |-  ( f : S --> B -> ran f C_ B )
64 63 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 )
65 bastg 
 |-  ( B e. TopBases -> B C_ ( topGen ` B ) )
66 65 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 ) )
67 66 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 )
68 64 67 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 )
69 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 )
70 simprr 
 |-  ( ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) -> ( topGen ` c ) = J )
71 70 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 )
72 69 71 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 ) )
73 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 )
74 tg2 
 |-  ( ( o e. ( topGen ` c ) /\ t e. o ) -> E. d e. c ( t e. d /\ d C_ o ) )
75 72 73 74 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 ) )
76 bastg 
 |-  ( c e. TopBases -> c C_ ( topGen ` c ) )
77 76 ad2antrl 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> c C_ ( topGen ` c ) )
78 77 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 ) )
79 1 eqeq2i 
 |-  ( ( topGen ` c ) = J <-> ( topGen ` c ) = ( topGen ` B ) )
80 79 biimpi 
 |-  ( ( topGen ` c ) = J -> ( topGen ` c ) = ( topGen ` B ) )
81 80 adantl 
 |-  ( ( c ~<_ _om /\ ( topGen ` c ) = J ) -> ( topGen ` c ) = ( topGen ` B ) )
82 81 ad2antll 
 |-  ( ( ( B e. TopBases /\ J e. 2ndc ) /\ ( c e. TopBases /\ ( c ~<_ _om /\ ( topGen ` c ) = J ) ) ) -> ( topGen ` c ) = ( topGen ` B ) )
83 82 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 ) )
84 78 83 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 ) )
85 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 )
86 84 85 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 ) )
87 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 )
88 tg2 
 |-  ( ( d e. ( topGen ` B ) /\ t e. d ) -> E. m e. B ( t e. m /\ m C_ d ) )
89 86 87 88 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 ) )
90 65 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 ) )
91 90 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 ) )
92 71 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 )
93 92 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 ) )
94 91 93 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 ) )
95 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 )
96 94 95 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 ) )
97 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 )
98 tg2 
 |-  ( ( m e. ( topGen ` c ) /\ t e. m ) -> E. n e. c ( t e. n /\ n C_ m ) )
99 96 97 98 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 ) )
100 ffn 
 |-  ( f : S --> B -> f Fn S )
101 100 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 )
102 101 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 )
103 102 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 )
104 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 )
105 85 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 )
106 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 )
107 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 )
108 simprr 
 |-  ( ( m e. B /\ ( t e. m /\ m C_ d ) ) -> m C_ d )
109 108 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 )
110 sseq2 
 |-  ( w = m -> ( n C_ w <-> n C_ m ) )
111 sseq1 
 |-  ( w = m -> ( w C_ d <-> m C_ d ) )
112 110 111 anbi12d 
 |-  ( w = m -> ( ( n C_ w /\ w C_ d ) <-> ( n C_ m /\ m C_ d ) ) )
113 112 rspcev 
 |-  ( ( m e. B /\ ( n C_ m /\ m C_ d ) ) -> E. w e. B ( n C_ w /\ w C_ d ) )
114 106 107 109 113 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 ) )
115 df-br 
 |-  ( n S d <-> <. n , d >. e. S )
116 vex 
 |-  n e. _V
117 vex 
 |-  d e. _V
118 simpl 
 |-  ( ( u = n /\ v = d ) -> u = n )
119 118 eleq1d 
 |-  ( ( u = n /\ v = d ) -> ( u e. c <-> n e. c ) )
120 simpr 
 |-  ( ( u = n /\ v = d ) -> v = d )
121 120 eleq1d 
 |-  ( ( u = n /\ v = d ) -> ( v e. c <-> d e. c ) )
122 sseq1 
 |-  ( u = n -> ( u C_ w <-> n C_ w ) )
123 sseq2 
 |-  ( v = d -> ( w C_ v <-> w C_ d ) )
124 122 123 bi2anan9 
 |-  ( ( u = n /\ v = d ) -> ( ( u C_ w /\ w C_ v ) <-> ( n C_ w /\ w C_ d ) ) )
125 124 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 ) ) )
126 119 121 125 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 ) ) ) )
127 116 117 126 2 braba 
 |-  ( n S d <-> ( n e. c /\ d e. c /\ E. w e. B ( n C_ w /\ w C_ d ) ) )
128 115 127 bitr3i 
 |-  ( <. n , d >. e. S <-> ( n e. c /\ d e. c /\ E. w e. B ( n C_ w /\ w C_ d ) ) )
129 104 105 114 128 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 )
130 fnfvelrn 
 |-  ( ( f Fn S /\ <. n , d >. e. S ) -> ( f ` <. n , d >. ) e. ran f )
131 103 129 130 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 )
132 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 )
133 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 )
134 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 )
135 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 )
136 108 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 )
137 134 135 136 113 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 ) )
138 132 133 137 128 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 )
139 fveq2 
 |-  ( x = <. n , d >. -> ( 1st ` x ) = ( 1st ` <. n , d >. ) )
140 fveq2 
 |-  ( x = <. n , d >. -> ( f ` x ) = ( f ` <. n , d >. ) )
141 139 140 sseq12d 
 |-  ( x = <. n , d >. -> ( ( 1st ` x ) C_ ( f ` x ) <-> ( 1st ` <. n , d >. ) C_ ( f ` <. n , d >. ) ) )
142 fveq2 
 |-  ( x = <. n , d >. -> ( 2nd ` x ) = ( 2nd ` <. n , d >. ) )
143 140 142 sseq12d 
 |-  ( x = <. n , d >. -> ( ( f ` x ) C_ ( 2nd ` x ) <-> ( f ` <. n , d >. ) C_ ( 2nd ` <. n , d >. ) ) )
144 141 143 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 >. ) ) ) )
145 144 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 >. ) ) ) )
146 138 145 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 >. ) ) ) )
147 116 117 op1st 
 |-  ( 1st ` <. n , d >. ) = n
148 147 sseq1i 
 |-  ( ( 1st ` <. n , d >. ) C_ ( f ` <. n , d >. ) <-> n C_ ( f ` <. n , d >. ) )
149 116 117 op2nd 
 |-  ( 2nd ` <. n , d >. ) = d
150 149 sseq2i 
 |-  ( ( f ` <. n , d >. ) C_ ( 2nd ` <. n , d >. ) <-> ( f ` <. n , d >. ) C_ d )
151 148 150 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 ) )
152 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 >. ) )
153 simprl 
 |-  ( ( n e. c /\ ( t e. n /\ n C_ m ) ) -> t e. n )
154 153 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 )
155 152 154 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 >. ) )
156 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 )
157 simplrr 
 |-  ( ( ( d e. c /\ ( t e. d /\ d C_ o ) ) /\ ( m e. B /\ ( t e. m /\ m C_ d ) ) ) -> d C_ o )
158 157 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 )
159 156 158 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 )
160 155 159 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 ) )
161 160 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 ) ) )
162 151 161 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 ) ) )
163 146 162 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 ) ) )
164 163 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 ) ) ) ) )
165 164 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 ) ) ) ) )
166 165 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 ) ) ) ) )
167 166 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 ) )
168 eleq2 
 |-  ( b = ( f ` <. n , d >. ) -> ( t e. b <-> t e. ( f ` <. n , d >. ) ) )
169 sseq1 
 |-  ( b = ( f ` <. n , d >. ) -> ( b C_ o <-> ( f ` <. n , d >. ) C_ o ) )
170 168 169 anbi12d 
 |-  ( b = ( f ` <. n , d >. ) -> ( ( t e. b /\ b C_ o ) <-> ( t e. ( f ` <. n , d >. ) /\ ( f ` <. n , d >. ) C_ o ) ) )
171 170 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 ) )
172 131 167 171 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 ) )
173 99 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 ) ) ) /\ ( 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 ) )
174 89 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 ) ) ) -> E. b e. ran f ( t e. b /\ b C_ o ) )
175 75 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 ) ) ) -> E. b e. ran f ( t e. b /\ b C_ o ) )
176 175 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 ) ) )
177 176 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 ) )
178 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 )
179 62 68 177 178 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 )
180 179 62 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 )
181 tgclb 
 |-  ( ran f e. TopBases <-> ( topGen ` ran f ) e. Top )
182 180 181 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 )
183 omelon 
 |-  _om e. On
184 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 )
185 ondomen 
 |-  ( ( _om e. On /\ S ~<_ _om ) -> S e. dom card )
186 183 184 185 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 )
187 100 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 )
188 dffn4 
 |-  ( f Fn S <-> f : S -onto-> ran f )
189 187 188 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 )
190 fodomnum 
 |-  ( S e. dom card -> ( f : S -onto-> ran f -> ran f ~<_ S ) )
191 186 189 190 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 )
192 domtr 
 |-  ( ( ran f ~<_ S /\ S ~<_ _om ) -> ran f ~<_ _om )
193 191 184 192 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 )
194 179 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 ) )
195 breq1 
 |-  ( b = ran f -> ( b ~<_ _om <-> ran f ~<_ _om ) )
196 sseq1 
 |-  ( b = ran f -> ( b C_ B <-> ran f C_ B ) )
197 fveq2 
 |-  ( b = ran f -> ( topGen ` b ) = ( topGen ` ran f ) )
198 197 eqeq2d 
 |-  ( b = ran f -> ( J = ( topGen ` b ) <-> J = ( topGen ` ran f ) ) )
199 195 196 198 3anbi123d 
 |-  ( b = ran f -> ( ( b ~<_ _om /\ b C_ B /\ J = ( topGen ` b ) ) <-> ( ran f ~<_ _om /\ ran f C_ B /\ J = ( topGen ` ran f ) ) ) )
200 199 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 ) ) )
201 182 193 64 194 200 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 ) ) )
202 201 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 ) ) ) )
203 59 202 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 ) ) ) )
204 203 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 ) ) ) )
205 56 204 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 ) ) )
206 5 205 rexlimddv 
 |-  ( ( B e. TopBases /\ J e. 2ndc ) -> E. b e. TopBases ( b ~<_ _om /\ b C_ B /\ J = ( topGen ` b ) ) )