MPE Home 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  ontowfo 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