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 𝐽 = ( topGen ‘ 𝐵 )
2ndcctbss.2 𝑆 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢𝑐𝑣𝑐 ∧ ∃ 𝑤𝐵 ( 𝑢𝑤𝑤𝑣 ) ) }
Assertion 2ndcctbss ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏𝐵𝐽 = ( topGen ‘ 𝑏 ) ) )

Proof

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