Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  2ndcctbss Structured version   Visualization version   GIF version

Theorem 2ndcctbss 21306
 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.)
Hypotheses
Ref Expression
2ndcctbss.1 𝑋 = 𝐵
2ndcctbss.2 𝐽 = (topGen‘𝐵)
2ndcctbss.3 𝑆 = {⟨𝑢, 𝑣⟩ ∣ (𝑢𝑐𝑣𝑐 ∧ ∃𝑤𝐵 (𝑢𝑤𝑤𝑣))}
Assertion
Ref Expression
2ndcctbss ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏𝐵𝐽 = (topGen‘𝑏)))
Distinct variable groups:   𝑏,𝑐,𝑢,𝑣,𝑤,𝐵   𝐽,𝑏,𝑐
Allowed substitution hints:   𝑆(𝑤,𝑣,𝑢,𝑏,𝑐)   𝐽(𝑤,𝑣,𝑢)   𝑋(𝑤,𝑣,𝑢,𝑏,𝑐)

Proof of Theorem 2ndcctbss
Dummy variables 𝑑 𝑓 𝑚 𝑛 𝑜 𝑡 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 476 . . 3 ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) → 𝐽 ∈ 2nd𝜔)
2 is2ndc 21297 . . 3 (𝐽 ∈ 2nd𝜔 ↔ ∃𝑐 ∈ TopBases (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))
31, 2sylib 208 . 2 ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) → ∃𝑐 ∈ TopBases (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))
4 vex 3234 . . . . . . 7 𝑐 ∈ V
54, 4xpex 7004 . . . . . 6 (𝑐 × 𝑐) ∈ V
6 3simpa 1078 . . . . . . . 8 ((𝑢𝑐𝑣𝑐 ∧ ∃𝑤𝐵 (𝑢𝑤𝑤𝑣)) → (𝑢𝑐𝑣𝑐))
76ssopab2i 5032 . . . . . . 7 {⟨𝑢, 𝑣⟩ ∣ (𝑢𝑐𝑣𝑐 ∧ ∃𝑤𝐵 (𝑢𝑤𝑤𝑣))} ⊆ {⟨𝑢, 𝑣⟩ ∣ (𝑢𝑐𝑣𝑐)}
8 2ndcctbss.3 . . . . . . 7 𝑆 = {⟨𝑢, 𝑣⟩ ∣ (𝑢𝑐𝑣𝑐 ∧ ∃𝑤𝐵 (𝑢𝑤𝑤𝑣))}
9 df-xp 5149 . . . . . . 7 (𝑐 × 𝑐) = {⟨𝑢, 𝑣⟩ ∣ (𝑢𝑐𝑣𝑐)}
107, 8, 93sstr4i 3677 . . . . . 6 𝑆 ⊆ (𝑐 × 𝑐)
11 ssdomg 8043 . . . . . 6 ((𝑐 × 𝑐) ∈ V → (𝑆 ⊆ (𝑐 × 𝑐) → 𝑆 ≼ (𝑐 × 𝑐)))
125, 10, 11mp2 9 . . . . 5 𝑆 ≼ (𝑐 × 𝑐)
134xpdom1 8100 . . . . . . . . 9 (𝑐 ≼ ω → (𝑐 × 𝑐) ≼ (ω × 𝑐))
14 omex 8578 . . . . . . . . . 10 ω ∈ V
1514xpdom2 8096 . . . . . . . . 9 (𝑐 ≼ ω → (ω × 𝑐) ≼ (ω × ω))
16 domtr 8050 . . . . . . . . 9 (((𝑐 × 𝑐) ≼ (ω × 𝑐) ∧ (ω × 𝑐) ≼ (ω × ω)) → (𝑐 × 𝑐) ≼ (ω × ω))
1713, 15, 16syl2anc 694 . . . . . . . 8 (𝑐 ≼ ω → (𝑐 × 𝑐) ≼ (ω × ω))
18 xpomen 8876 . . . . . . . 8 (ω × ω) ≈ ω
19 domentr 8056 . . . . . . . 8 (((𝑐 × 𝑐) ≼ (ω × ω) ∧ (ω × ω) ≈ ω) → (𝑐 × 𝑐) ≼ ω)
2017, 18, 19sylancl 695 . . . . . . 7 (𝑐 ≼ ω → (𝑐 × 𝑐) ≼ ω)
2120adantr 480 . . . . . 6 ((𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽) → (𝑐 × 𝑐) ≼ ω)
2221ad2antll 765 . . . . 5 (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → (𝑐 × 𝑐) ≼ ω)
23 domtr 8050 . . . . 5 ((𝑆 ≼ (𝑐 × 𝑐) ∧ (𝑐 × 𝑐) ≼ ω) → 𝑆 ≼ ω)
2412, 22, 23sylancr 696 . . . 4 (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → 𝑆 ≼ ω)
258relopabi 5278 . . . . . . . . 9 Rel 𝑆
26 simpr 476 . . . . . . . . 9 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥𝑆) → 𝑥𝑆)
27 1st2nd 7258 . . . . . . . . 9 ((Rel 𝑆𝑥𝑆) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
2825, 26, 27sylancr 696 . . . . . . . 8 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥𝑆) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
2928, 26eqeltrrd 2731 . . . . . . 7 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥𝑆) → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝑆)
30 df-br 4686 . . . . . . . . 9 ((1st𝑥)𝑆(2nd𝑥) ↔ ⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝑆)
31 fvex 6239 . . . . . . . . . 10 (1st𝑥) ∈ V
32 fvex 6239 . . . . . . . . . 10 (2nd𝑥) ∈ V
33 simpl 472 . . . . . . . . . . . 12 ((𝑢 = (1st𝑥) ∧ 𝑣 = (2nd𝑥)) → 𝑢 = (1st𝑥))
3433eleq1d 2715 . . . . . . . . . . 11 ((𝑢 = (1st𝑥) ∧ 𝑣 = (2nd𝑥)) → (𝑢𝑐 ↔ (1st𝑥) ∈ 𝑐))
35 simpr 476 . . . . . . . . . . . 12 ((𝑢 = (1st𝑥) ∧ 𝑣 = (2nd𝑥)) → 𝑣 = (2nd𝑥))
3635eleq1d 2715 . . . . . . . . . . 11 ((𝑢 = (1st𝑥) ∧ 𝑣 = (2nd𝑥)) → (𝑣𝑐 ↔ (2nd𝑥) ∈ 𝑐))
37 sseq1 3659 . . . . . . . . . . . . 13 (𝑢 = (1st𝑥) → (𝑢𝑤 ↔ (1st𝑥) ⊆ 𝑤))
38 sseq2 3660 . . . . . . . . . . . . 13 (𝑣 = (2nd𝑥) → (𝑤𝑣𝑤 ⊆ (2nd𝑥)))
3937, 38bi2anan9 935 . . . . . . . . . . . 12 ((𝑢 = (1st𝑥) ∧ 𝑣 = (2nd𝑥)) → ((𝑢𝑤𝑤𝑣) ↔ ((1st𝑥) ⊆ 𝑤𝑤 ⊆ (2nd𝑥))))
4039rexbidv 3081 . . . . . . . . . . 11 ((𝑢 = (1st𝑥) ∧ 𝑣 = (2nd𝑥)) → (∃𝑤𝐵 (𝑢𝑤𝑤𝑣) ↔ ∃𝑤𝐵 ((1st𝑥) ⊆ 𝑤𝑤 ⊆ (2nd𝑥))))
4134, 36, 403anbi123d 1439 . . . . . . . . . 10 ((𝑢 = (1st𝑥) ∧ 𝑣 = (2nd𝑥)) → ((𝑢𝑐𝑣𝑐 ∧ ∃𝑤𝐵 (𝑢𝑤𝑤𝑣)) ↔ ((1st𝑥) ∈ 𝑐 ∧ (2nd𝑥) ∈ 𝑐 ∧ ∃𝑤𝐵 ((1st𝑥) ⊆ 𝑤𝑤 ⊆ (2nd𝑥)))))
4231, 32, 41, 8braba 5021 . . . . . . . . 9 ((1st𝑥)𝑆(2nd𝑥) ↔ ((1st𝑥) ∈ 𝑐 ∧ (2nd𝑥) ∈ 𝑐 ∧ ∃𝑤𝐵 ((1st𝑥) ⊆ 𝑤𝑤 ⊆ (2nd𝑥))))
4330, 42bitr3i 266 . . . . . . . 8 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝑆 ↔ ((1st𝑥) ∈ 𝑐 ∧ (2nd𝑥) ∈ 𝑐 ∧ ∃𝑤𝐵 ((1st𝑥) ⊆ 𝑤𝑤 ⊆ (2nd𝑥))))
4443simp3bi 1098 . . . . . . 7 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ 𝑆 → ∃𝑤𝐵 ((1st𝑥) ⊆ 𝑤𝑤 ⊆ (2nd𝑥)))
4529, 44syl 17 . . . . . 6 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥𝑆) → ∃𝑤𝐵 ((1st𝑥) ⊆ 𝑤𝑤 ⊆ (2nd𝑥)))
46 fvi 6294 . . . . . . . 8 (𝐵 ∈ TopBases → ( I ‘𝐵) = 𝐵)
4746ad3antrrr 766 . . . . . . 7 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥𝑆) → ( I ‘𝐵) = 𝐵)
4847rexeqdv 3175 . . . . . 6 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥𝑆) → (∃𝑤 ∈ ( I ‘𝐵)((1st𝑥) ⊆ 𝑤𝑤 ⊆ (2nd𝑥)) ↔ ∃𝑤𝐵 ((1st𝑥) ⊆ 𝑤𝑤 ⊆ (2nd𝑥))))
4945, 48mpbird 247 . . . . 5 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ 𝑥𝑆) → ∃𝑤 ∈ ( I ‘𝐵)((1st𝑥) ⊆ 𝑤𝑤 ⊆ (2nd𝑥)))
5049ralrimiva 2995 . . . 4 (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ∀𝑥𝑆𝑤 ∈ ( I ‘𝐵)((1st𝑥) ⊆ 𝑤𝑤 ⊆ (2nd𝑥)))
51 fvex 6239 . . . . 5 ( I ‘𝐵) ∈ V
52 sseq2 3660 . . . . . 6 (𝑤 = (𝑓𝑥) → ((1st𝑥) ⊆ 𝑤 ↔ (1st𝑥) ⊆ (𝑓𝑥)))
53 sseq1 3659 . . . . . 6 (𝑤 = (𝑓𝑥) → (𝑤 ⊆ (2nd𝑥) ↔ (𝑓𝑥) ⊆ (2nd𝑥)))
5452, 53anbi12d 747 . . . . 5 (𝑤 = (𝑓𝑥) → (((1st𝑥) ⊆ 𝑤𝑤 ⊆ (2nd𝑥)) ↔ ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))))
5551, 54axcc4dom 9301 . . . 4 ((𝑆 ≼ ω ∧ ∀𝑥𝑆𝑤 ∈ ( I ‘𝐵)((1st𝑥) ⊆ 𝑤𝑤 ⊆ (2nd𝑥))) → ∃𝑓(𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))))
5624, 50, 55syl2anc 694 . . 3 (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ∃𝑓(𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))))
5746ad2antrr 762 . . . . . . 7 (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ( I ‘𝐵) = 𝐵)
5857feq3d 6070 . . . . . 6 (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → (𝑓:𝑆⟶( I ‘𝐵) ↔ 𝑓:𝑆𝐵))
5958anbi1d 741 . . . . 5 (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ((𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ↔ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))))
60 2ndctop 21298 . . . . . . . . . . . 12 (𝐽 ∈ 2nd𝜔 → 𝐽 ∈ Top)
6160adantl 481 . . . . . . . . . . 11 ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) → 𝐽 ∈ Top)
6261ad2antrr 762 . . . . . . . . . 10 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → 𝐽 ∈ Top)
63 frn 6091 . . . . . . . . . . . 12 (𝑓:𝑆𝐵 → ran 𝑓𝐵)
6463ad2antrl 764 . . . . . . . . . . 11 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → ran 𝑓𝐵)
65 bastg 20818 . . . . . . . . . . . . 13 (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵))
6665ad3antrrr 766 . . . . . . . . . . . 12 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → 𝐵 ⊆ (topGen‘𝐵))
67 2ndcctbss.2 . . . . . . . . . . . 12 𝐽 = (topGen‘𝐵)
6866, 67syl6sseqr 3685 . . . . . . . . . . 11 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → 𝐵𝐽)
6964, 68sstrd 3646 . . . . . . . . . 10 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → ran 𝑓𝐽)
70 simprrl 821 . . . . . . . . . . . . . . 15 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) → 𝑜𝐽)
71 simprr 811 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽)) → (topGen‘𝑐) = 𝐽)
7271ad2antlr 763 . . . . . . . . . . . . . . 15 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) → (topGen‘𝑐) = 𝐽)
7370, 72eleqtrrd 2733 . . . . . . . . . . . . . 14 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) → 𝑜 ∈ (topGen‘𝑐))
74 simprrr 822 . . . . . . . . . . . . . 14 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) → 𝑡𝑜)
75 tg2 20817 . . . . . . . . . . . . . 14 ((𝑜 ∈ (topGen‘𝑐) ∧ 𝑡𝑜) → ∃𝑑𝑐 (𝑡𝑑𝑑𝑜))
7673, 74, 75syl2anc 694 . . . . . . . . . . . . 13 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) → ∃𝑑𝑐 (𝑡𝑑𝑑𝑜))
77 bastg 20818 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ TopBases → 𝑐 ⊆ (topGen‘𝑐))
7877ad2antrl 764 . . . . . . . . . . . . . . . . . 18 (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → 𝑐 ⊆ (topGen‘𝑐))
7978ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) → 𝑐 ⊆ (topGen‘𝑐))
8067eqeq2i 2663 . . . . . . . . . . . . . . . . . . . . 21 ((topGen‘𝑐) = 𝐽 ↔ (topGen‘𝑐) = (topGen‘𝐵))
8180biimpi 206 . . . . . . . . . . . . . . . . . . . 20 ((topGen‘𝑐) = 𝐽 → (topGen‘𝑐) = (topGen‘𝐵))
8281adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽) → (topGen‘𝑐) = (topGen‘𝐵))
8382ad2antll 765 . . . . . . . . . . . . . . . . . 18 (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → (topGen‘𝑐) = (topGen‘𝐵))
8483ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) → (topGen‘𝑐) = (topGen‘𝐵))
8579, 84sseqtrd 3674 . . . . . . . . . . . . . . . 16 (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) → 𝑐 ⊆ (topGen‘𝐵))
86 simprl 809 . . . . . . . . . . . . . . . 16 (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) → 𝑑𝑐)
8785, 86sseldd 3637 . . . . . . . . . . . . . . 15 (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) → 𝑑 ∈ (topGen‘𝐵))
88 simprrl 821 . . . . . . . . . . . . . . 15 (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) → 𝑡𝑑)
89 tg2 20817 . . . . . . . . . . . . . . 15 ((𝑑 ∈ (topGen‘𝐵) ∧ 𝑡𝑑) → ∃𝑚𝐵 (𝑡𝑚𝑚𝑑))
9087, 88, 89syl2anc 694 . . . . . . . . . . . . . 14 (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) → ∃𝑚𝐵 (𝑡𝑚𝑚𝑑))
9165ad3antrrr 766 . . . . . . . . . . . . . . . . . . 19 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) → 𝐵 ⊆ (topGen‘𝐵))
9291ad2antrr 762 . . . . . . . . . . . . . . . . . 18 ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) → 𝐵 ⊆ (topGen‘𝐵))
9372ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) → (topGen‘𝑐) = 𝐽)
9493, 67syl6req 2702 . . . . . . . . . . . . . . . . . 18 ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) → (topGen‘𝐵) = (topGen‘𝑐))
9592, 94sseqtrd 3674 . . . . . . . . . . . . . . . . 17 ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) → 𝐵 ⊆ (topGen‘𝑐))
96 simprl 809 . . . . . . . . . . . . . . . . 17 ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) → 𝑚𝐵)
9795, 96sseldd 3637 . . . . . . . . . . . . . . . 16 ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) → 𝑚 ∈ (topGen‘𝑐))
98 simprrl 821 . . . . . . . . . . . . . . . 16 ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) → 𝑡𝑚)
99 tg2 20817 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ (topGen‘𝑐) ∧ 𝑡𝑚) → ∃𝑛𝑐 (𝑡𝑛𝑛𝑚))
10097, 98, 99syl2anc 694 . . . . . . . . . . . . . . 15 ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) → ∃𝑛𝑐 (𝑡𝑛𝑛𝑚))
101 ffn 6083 . . . . . . . . . . . . . . . . . . . 20 (𝑓:𝑆𝐵𝑓 Fn 𝑆)
102101ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜)) → 𝑓 Fn 𝑆)
103102ad2antlr 763 . . . . . . . . . . . . . . . . . 18 (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) → 𝑓 Fn 𝑆)
104103ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → 𝑓 Fn 𝑆)
105 simprl 809 . . . . . . . . . . . . . . . . . 18 (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → 𝑛𝑐)
10686ad2antrr 762 . . . . . . . . . . . . . . . . . 18 (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → 𝑑𝑐)
107 simplrl 817 . . . . . . . . . . . . . . . . . . 19 (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → 𝑚𝐵)
108 simprrr 822 . . . . . . . . . . . . . . . . . . 19 (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → 𝑛𝑚)
109 simprr 811 . . . . . . . . . . . . . . . . . . . 20 ((𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑)) → 𝑚𝑑)
110109ad2antlr 763 . . . . . . . . . . . . . . . . . . 19 (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → 𝑚𝑑)
111 sseq2 3660 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑚 → (𝑛𝑤𝑛𝑚))
112 sseq1 3659 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑚 → (𝑤𝑑𝑚𝑑))
113111, 112anbi12d 747 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑚 → ((𝑛𝑤𝑤𝑑) ↔ (𝑛𝑚𝑚𝑑)))
114113rspcev 3340 . . . . . . . . . . . . . . . . . . 19 ((𝑚𝐵 ∧ (𝑛𝑚𝑚𝑑)) → ∃𝑤𝐵 (𝑛𝑤𝑤𝑑))
115107, 108, 110, 114syl12anc 1364 . . . . . . . . . . . . . . . . . 18 (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → ∃𝑤𝐵 (𝑛𝑤𝑤𝑑))
116 df-br 4686 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑆𝑑 ↔ ⟨𝑛, 𝑑⟩ ∈ 𝑆)
117 vex 3234 . . . . . . . . . . . . . . . . . . . 20 𝑛 ∈ V
118 vex 3234 . . . . . . . . . . . . . . . . . . . 20 𝑑 ∈ V
119 simpl 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑢 = 𝑛𝑣 = 𝑑) → 𝑢 = 𝑛)
120119eleq1d 2715 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 = 𝑛𝑣 = 𝑑) → (𝑢𝑐𝑛𝑐))
121 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑢 = 𝑛𝑣 = 𝑑) → 𝑣 = 𝑑)
122121eleq1d 2715 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 = 𝑛𝑣 = 𝑑) → (𝑣𝑐𝑑𝑐))
123 sseq1 3659 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝑛 → (𝑢𝑤𝑛𝑤))
124 sseq2 3660 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = 𝑑 → (𝑤𝑣𝑤𝑑))
125123, 124bi2anan9 935 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑢 = 𝑛𝑣 = 𝑑) → ((𝑢𝑤𝑤𝑣) ↔ (𝑛𝑤𝑤𝑑)))
126125rexbidv 3081 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 = 𝑛𝑣 = 𝑑) → (∃𝑤𝐵 (𝑢𝑤𝑤𝑣) ↔ ∃𝑤𝐵 (𝑛𝑤𝑤𝑑)))
127120, 122, 1263anbi123d 1439 . . . . . . . . . . . . . . . . . . . 20 ((𝑢 = 𝑛𝑣 = 𝑑) → ((𝑢𝑐𝑣𝑐 ∧ ∃𝑤𝐵 (𝑢𝑤𝑤𝑣)) ↔ (𝑛𝑐𝑑𝑐 ∧ ∃𝑤𝐵 (𝑛𝑤𝑤𝑑))))
128117, 118, 127, 8braba 5021 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑆𝑑 ↔ (𝑛𝑐𝑑𝑐 ∧ ∃𝑤𝐵 (𝑛𝑤𝑤𝑑)))
129116, 128bitr3i 266 . . . . . . . . . . . . . . . . . 18 (⟨𝑛, 𝑑⟩ ∈ 𝑆 ↔ (𝑛𝑐𝑑𝑐 ∧ ∃𝑤𝐵 (𝑛𝑤𝑤𝑑)))
130105, 106, 115, 129syl3anbrc 1265 . . . . . . . . . . . . . . . . 17 (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → ⟨𝑛, 𝑑⟩ ∈ 𝑆)
131 fnfvelrn 6396 . . . . . . . . . . . . . . . . 17 ((𝑓 Fn 𝑆 ∧ ⟨𝑛, 𝑑⟩ ∈ 𝑆) → (𝑓‘⟨𝑛, 𝑑⟩) ∈ ran 𝑓)
132104, 130, 131syl2anc 694 . . . . . . . . . . . . . . . 16 (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → (𝑓‘⟨𝑛, 𝑑⟩) ∈ ran 𝑓)
133 simprl 809 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → 𝑛𝑐)
134 simplll 813 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → 𝑑𝑐)
135 simplrl 817 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → 𝑚𝐵)
136 simprrr 822 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → 𝑛𝑚)
137109ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → 𝑚𝑑)
138135, 136, 137, 114syl12anc 1364 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → ∃𝑤𝐵 (𝑛𝑤𝑤𝑑))
139133, 134, 138, 129syl3anbrc 1265 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → ⟨𝑛, 𝑑⟩ ∈ 𝑆)
140 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ⟨𝑛, 𝑑⟩ → (1st𝑥) = (1st ‘⟨𝑛, 𝑑⟩))
141 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ⟨𝑛, 𝑑⟩ → (𝑓𝑥) = (𝑓‘⟨𝑛, 𝑑⟩))
142140, 141sseq12d 3667 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ⟨𝑛, 𝑑⟩ → ((1st𝑥) ⊆ (𝑓𝑥) ↔ (1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩)))
143 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ⟨𝑛, 𝑑⟩ → (2nd𝑥) = (2nd ‘⟨𝑛, 𝑑⟩))
144141, 143sseq12d 3667 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ⟨𝑛, 𝑑⟩ → ((𝑓𝑥) ⊆ (2nd𝑥) ↔ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩)))
145142, 144anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = ⟨𝑛, 𝑑⟩ → (((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)) ↔ ((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩))))
146145rspcv 3336 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑛, 𝑑⟩ ∈ 𝑆 → (∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)) → ((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩))))
147139, 146syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → (∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)) → ((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩))))
148117, 118op1st 7218 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st ‘⟨𝑛, 𝑑⟩) = 𝑛
149148sseq1i 3662 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ↔ 𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩))
150117, 118op2nd 7219 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd ‘⟨𝑛, 𝑑⟩) = 𝑑
151150sseq2i 3663 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩) ↔ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)
152149, 151anbi12i 733 . . . . . . . . . . . . . . . . . . . . . 22 (((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩)) ↔ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑))
153 simprl 809 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → 𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩))
154 simprl 809 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚)) → 𝑡𝑛)
155154ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → 𝑡𝑛)
156153, 155sseldd 3637 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → 𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩))
157 simprr 811 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)
158 simplrr 818 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) → 𝑑𝑜)
159158ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → 𝑑𝑜)
160157, 159sstrd 3646 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)
161156, 160jca 553 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) ∧ (𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑)) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜))
162161ex 449 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → ((𝑛 ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑑) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))
163152, 162syl5bi 232 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → (((1st ‘⟨𝑛, 𝑑⟩) ⊆ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ (2nd ‘⟨𝑛, 𝑑⟩)) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))
164147, 163syldc 48 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)) → ((((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))
165164exp4c 635 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)) → ((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) → ((𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑)) → ((𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚)) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))))
166165ad2antlr 763 . . . . . . . . . . . . . . . . . 18 (((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜)) → ((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) → ((𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑)) → ((𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚)) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))))
167166adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) → ((𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜)) → ((𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑)) → ((𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚)) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))))
168167imp41 618 . . . . . . . . . . . . . . . 16 (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜))
169 eleq2 2719 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑓‘⟨𝑛, 𝑑⟩) → (𝑡𝑏𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩)))
170 sseq1 3659 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑓‘⟨𝑛, 𝑑⟩) → (𝑏𝑜 ↔ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜))
171169, 170anbi12d 747 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑓‘⟨𝑛, 𝑑⟩) → ((𝑡𝑏𝑏𝑜) ↔ (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)))
172171rspcev 3340 . . . . . . . . . . . . . . . 16 (((𝑓‘⟨𝑛, 𝑑⟩) ∈ ran 𝑓 ∧ (𝑡 ∈ (𝑓‘⟨𝑛, 𝑑⟩) ∧ (𝑓‘⟨𝑛, 𝑑⟩) ⊆ 𝑜)) → ∃𝑏 ∈ ran 𝑓(𝑡𝑏𝑏𝑜))
173132, 168, 172syl2anc 694 . . . . . . . . . . . . . . 15 (((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) ∧ (𝑛𝑐 ∧ (𝑡𝑛𝑛𝑚))) → ∃𝑏 ∈ ran 𝑓(𝑡𝑏𝑏𝑜))
174100, 173rexlimddv 3064 . . . . . . . . . . . . . 14 ((((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) ∧ (𝑚𝐵 ∧ (𝑡𝑚𝑚𝑑))) → ∃𝑏 ∈ ran 𝑓(𝑡𝑏𝑏𝑜))
17590, 174rexlimddv 3064 . . . . . . . . . . . . 13 (((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) ∧ (𝑑𝑐 ∧ (𝑡𝑑𝑑𝑜))) → ∃𝑏 ∈ ran 𝑓(𝑡𝑏𝑏𝑜))
17676, 175rexlimddv 3064 . . . . . . . . . . . 12 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) ∧ (𝑜𝐽𝑡𝑜))) → ∃𝑏 ∈ ran 𝑓(𝑡𝑏𝑏𝑜))
177176expr 642 . . . . . . . . . . 11 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → ((𝑜𝐽𝑡𝑜) → ∃𝑏 ∈ ran 𝑓(𝑡𝑏𝑏𝑜)))
178177ralrimivv 2999 . . . . . . . . . 10 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → ∀𝑜𝐽𝑡𝑜𝑏 ∈ ran 𝑓(𝑡𝑏𝑏𝑜))
179 basgen2 20841 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ ran 𝑓𝐽 ∧ ∀𝑜𝐽𝑡𝑜𝑏 ∈ ran 𝑓(𝑡𝑏𝑏𝑜)) → (topGen‘ran 𝑓) = 𝐽)
18062, 69, 178, 179syl3anc 1366 . . . . . . . . 9 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → (topGen‘ran 𝑓) = 𝐽)
181180, 62eqeltrd 2730 . . . . . . . 8 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → (topGen‘ran 𝑓) ∈ Top)
182 tgclb 20822 . . . . . . . 8 (ran 𝑓 ∈ TopBases ↔ (topGen‘ran 𝑓) ∈ Top)
183181, 182sylibr 224 . . . . . . 7 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → ran 𝑓 ∈ TopBases)
184 omelon 8581 . . . . . . . . . 10 ω ∈ On
18524adantr 480 . . . . . . . . . 10 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → 𝑆 ≼ ω)
186 ondomen 8898 . . . . . . . . . 10 ((ω ∈ On ∧ 𝑆 ≼ ω) → 𝑆 ∈ dom card)
187184, 185, 186sylancr 696 . . . . . . . . 9 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → 𝑆 ∈ dom card)
188101ad2antrl 764 . . . . . . . . . 10 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → 𝑓 Fn 𝑆)
189 dffn4 6159 . . . . . . . . . 10 (𝑓 Fn 𝑆𝑓:𝑆onto→ran 𝑓)
190188, 189sylib 208 . . . . . . . . 9 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → 𝑓:𝑆onto→ran 𝑓)
191 fodomnum 8918 . . . . . . . . 9 (𝑆 ∈ dom card → (𝑓:𝑆onto→ran 𝑓 → ran 𝑓𝑆))
192187, 190, 191sylc 65 . . . . . . . 8 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → ran 𝑓𝑆)
193 domtr 8050 . . . . . . . 8 ((ran 𝑓𝑆𝑆 ≼ ω) → ran 𝑓 ≼ ω)
194192, 185, 193syl2anc 694 . . . . . . 7 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → ran 𝑓 ≼ ω)
195180eqcomd 2657 . . . . . . 7 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → 𝐽 = (topGen‘ran 𝑓))
196 breq1 4688 . . . . . . . . 9 (𝑏 = ran 𝑓 → (𝑏 ≼ ω ↔ ran 𝑓 ≼ ω))
197 sseq1 3659 . . . . . . . . 9 (𝑏 = ran 𝑓 → (𝑏𝐵 ↔ ran 𝑓𝐵))
198 fveq2 6229 . . . . . . . . . 10 (𝑏 = ran 𝑓 → (topGen‘𝑏) = (topGen‘ran 𝑓))
199198eqeq2d 2661 . . . . . . . . 9 (𝑏 = ran 𝑓 → (𝐽 = (topGen‘𝑏) ↔ 𝐽 = (topGen‘ran 𝑓)))
200196, 197, 1993anbi123d 1439 . . . . . . . 8 (𝑏 = ran 𝑓 → ((𝑏 ≼ ω ∧ 𝑏𝐵𝐽 = (topGen‘𝑏)) ↔ (ran 𝑓 ≼ ω ∧ ran 𝑓𝐵𝐽 = (topGen‘ran 𝑓))))
201200rspcev 3340 . . . . . . 7 ((ran 𝑓 ∈ TopBases ∧ (ran 𝑓 ≼ ω ∧ ran 𝑓𝐵𝐽 = (topGen‘ran 𝑓))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏𝐵𝐽 = (topGen‘𝑏)))
202183, 194, 64, 195, 201syl13anc 1368 . . . . . 6 ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ (𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥)))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏𝐵𝐽 = (topGen‘𝑏)))
203202ex 449 . . . . 5 (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ((𝑓:𝑆𝐵 ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏𝐵𝐽 = (topGen‘𝑏))))
20459, 203sylbid 230 . . . 4 (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ((𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏𝐵𝐽 = (topGen‘𝑏))))
205204exlimdv 1901 . . 3 (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → (∃𝑓(𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥𝑆 ((1st𝑥) ⊆ (𝑓𝑥) ∧ (𝑓𝑥) ⊆ (2nd𝑥))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏𝐵𝐽 = (topGen‘𝑏))))
20656, 205mpd 15 . 2 (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏𝐵𝐽 = (topGen‘𝑏)))
2073, 206rexlimddv 3064 1 ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏𝐵𝐽 = (topGen‘𝑏)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054   = wceq 1523  ∃wex 1744   ∈ wcel 2030  ∀wral 2941  ∃wrex 2942  Vcvv 3231   ⊆ wss 3607  ⟨cop 4216  ∪ cuni 4468   class class class wbr 4685  {copab 4745   I cid 5052   × cxp 5141  dom cdm 5143  ran crn 5144  Rel wrel 5148  Oncon0 5761   Fn wfn 5921  ⟶wf 5922  –onto→wfo 5924  ‘cfv 5926  ωcom 7107  1st c1st 7208  2nd c2nd 7209   ≈ cen 7994   ≼ cdom 7995  cardccrd 8799  topGenctg 16145  Topctop 20746  TopBasesctb 20797  2nd𝜔c2ndc 21289 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cc 9295 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-oi 8456  df-card 8803  df-acn 8806  df-topgen 16151  df-top 20747  df-bases 20798  df-2ndc 21291 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator