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

Theorem 2ndcctbss 22959
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 𝐽 = (topGenβ€˜π΅)
2ndcctbss.2 𝑆 = {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣))}
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 486 . . 3 ((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) β†’ 𝐽 ∈ 2ndΟ‰)
2 is2ndc 22950 . . 3 (𝐽 ∈ 2ndΟ‰ ↔ βˆƒπ‘ ∈ TopBases (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))
31, 2sylib 217 . 2 ((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) β†’ βˆƒπ‘ ∈ TopBases (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))
4 vex 3479 . . . . . . 7 𝑐 ∈ V
54, 4xpex 7740 . . . . . 6 (𝑐 Γ— 𝑐) ∈ V
6 3simpa 1149 . . . . . . . 8 ((𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣)) β†’ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐))
76ssopab2i 5551 . . . . . . 7 {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣))} βŠ† {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)}
8 2ndcctbss.2 . . . . . . 7 𝑆 = {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣))}
9 df-xp 5683 . . . . . . 7 (𝑐 Γ— 𝑐) = {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)}
107, 8, 93sstr4i 4026 . . . . . 6 𝑆 βŠ† (𝑐 Γ— 𝑐)
11 ssdomg 8996 . . . . . 6 ((𝑐 Γ— 𝑐) ∈ V β†’ (𝑆 βŠ† (𝑐 Γ— 𝑐) β†’ 𝑆 β‰Ό (𝑐 Γ— 𝑐)))
125, 10, 11mp2 9 . . . . 5 𝑆 β‰Ό (𝑐 Γ— 𝑐)
134xpdom1 9071 . . . . . . . . 9 (𝑐 β‰Ό Ο‰ β†’ (𝑐 Γ— 𝑐) β‰Ό (Ο‰ Γ— 𝑐))
14 omex 9638 . . . . . . . . . 10 Ο‰ ∈ V
1514xpdom2 9067 . . . . . . . . 9 (𝑐 β‰Ό Ο‰ β†’ (Ο‰ Γ— 𝑐) β‰Ό (Ο‰ Γ— Ο‰))
16 domtr 9003 . . . . . . . . 9 (((𝑐 Γ— 𝑐) β‰Ό (Ο‰ Γ— 𝑐) ∧ (Ο‰ Γ— 𝑐) β‰Ό (Ο‰ Γ— Ο‰)) β†’ (𝑐 Γ— 𝑐) β‰Ό (Ο‰ Γ— Ο‰))
1713, 15, 16syl2anc 585 . . . . . . . 8 (𝑐 β‰Ό Ο‰ β†’ (𝑐 Γ— 𝑐) β‰Ό (Ο‰ Γ— Ο‰))
18 xpomen 10010 . . . . . . . 8 (Ο‰ Γ— Ο‰) β‰ˆ Ο‰
19 domentr 9009 . . . . . . . 8 (((𝑐 Γ— 𝑐) β‰Ό (Ο‰ Γ— Ο‰) ∧ (Ο‰ Γ— Ο‰) β‰ˆ Ο‰) β†’ (𝑐 Γ— 𝑐) β‰Ό Ο‰)
2017, 18, 19sylancl 587 . . . . . . 7 (𝑐 β‰Ό Ο‰ β†’ (𝑐 Γ— 𝑐) β‰Ό Ο‰)
2120adantr 482 . . . . . 6 ((𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽) β†’ (𝑐 Γ— 𝑐) β‰Ό Ο‰)
2221ad2antll 728 . . . . 5 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ (𝑐 Γ— 𝑐) β‰Ό Ο‰)
23 domtr 9003 . . . . 5 ((𝑆 β‰Ό (𝑐 Γ— 𝑐) ∧ (𝑐 Γ— 𝑐) β‰Ό Ο‰) β†’ 𝑆 β‰Ό Ο‰)
2412, 22, 23sylancr 588 . . . 4 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ 𝑆 β‰Ό Ο‰)
258relopabiv 5821 . . . . . . . . 9 Rel 𝑆
26 simpr 486 . . . . . . . . 9 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ π‘₯ ∈ 𝑆)
27 1st2nd 8025 . . . . . . . . 9 ((Rel 𝑆 ∧ π‘₯ ∈ 𝑆) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
2825, 26, 27sylancr 588 . . . . . . . 8 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
2928, 26eqeltrrd 2835 . . . . . . 7 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑆)
30 df-br 5150 . . . . . . . . 9 ((1st β€˜π‘₯)𝑆(2nd β€˜π‘₯) ↔ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑆)
31 fvex 6905 . . . . . . . . . 10 (1st β€˜π‘₯) ∈ V
32 fvex 6905 . . . . . . . . . 10 (2nd β€˜π‘₯) ∈ V
33 simpl 484 . . . . . . . . . . . 12 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ 𝑒 = (1st β€˜π‘₯))
3433eleq1d 2819 . . . . . . . . . . 11 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ (𝑒 ∈ 𝑐 ↔ (1st β€˜π‘₯) ∈ 𝑐))
35 simpr 486 . . . . . . . . . . . 12 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ 𝑣 = (2nd β€˜π‘₯))
3635eleq1d 2819 . . . . . . . . . . 11 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ (𝑣 ∈ 𝑐 ↔ (2nd β€˜π‘₯) ∈ 𝑐))
37 sseq1 4008 . . . . . . . . . . . . 13 (𝑒 = (1st β€˜π‘₯) β†’ (𝑒 βŠ† 𝑀 ↔ (1st β€˜π‘₯) βŠ† 𝑀))
38 sseq2 4009 . . . . . . . . . . . . 13 (𝑣 = (2nd β€˜π‘₯) β†’ (𝑀 βŠ† 𝑣 ↔ 𝑀 βŠ† (2nd β€˜π‘₯)))
3937, 38bi2anan9 638 . . . . . . . . . . . 12 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ ((𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣) ↔ ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯))))
4039rexbidv 3179 . . . . . . . . . . 11 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ (βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣) ↔ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯))))
4134, 36, 403anbi123d 1437 . . . . . . . . . 10 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ ((𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣)) ↔ ((1st β€˜π‘₯) ∈ 𝑐 ∧ (2nd β€˜π‘₯) ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)))))
4231, 32, 41, 8braba 5538 . . . . . . . . 9 ((1st β€˜π‘₯)𝑆(2nd β€˜π‘₯) ↔ ((1st β€˜π‘₯) ∈ 𝑐 ∧ (2nd β€˜π‘₯) ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯))))
4330, 42bitr3i 277 . . . . . . . 8 (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑆 ↔ ((1st β€˜π‘₯) ∈ 𝑐 ∧ (2nd β€˜π‘₯) ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯))))
4443simp3bi 1148 . . . . . . 7 (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑆 β†’ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)))
4529, 44syl 17 . . . . . 6 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)))
46 fvi 6968 . . . . . . . 8 (𝐡 ∈ TopBases β†’ ( I β€˜π΅) = 𝐡)
4746ad3antrrr 729 . . . . . . 7 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ ( I β€˜π΅) = 𝐡)
4847rexeqdv 3327 . . . . . 6 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ (βˆƒπ‘€ ∈ ( I β€˜π΅)((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)) ↔ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯))))
4945, 48mpbird 257 . . . . 5 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ βˆƒπ‘€ ∈ ( I β€˜π΅)((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)))
5049ralrimiva 3147 . . . 4 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ βˆ€π‘₯ ∈ 𝑆 βˆƒπ‘€ ∈ ( I β€˜π΅)((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)))
51 fvex 6905 . . . . 5 ( I β€˜π΅) ∈ V
52 sseq2 4009 . . . . . 6 (𝑀 = (π‘“β€˜π‘₯) β†’ ((1st β€˜π‘₯) βŠ† 𝑀 ↔ (1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯)))
53 sseq1 4008 . . . . . 6 (𝑀 = (π‘“β€˜π‘₯) β†’ (𝑀 βŠ† (2nd β€˜π‘₯) ↔ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))
5452, 53anbi12d 632 . . . . 5 (𝑀 = (π‘“β€˜π‘₯) β†’ (((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)) ↔ ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))))
5551, 54axcc4dom 10436 . . . 4 ((𝑆 β‰Ό Ο‰ ∧ βˆ€π‘₯ ∈ 𝑆 βˆƒπ‘€ ∈ ( I β€˜π΅)((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯))) β†’ βˆƒπ‘“(𝑓:π‘†βŸΆ( I β€˜π΅) ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))))
5624, 50, 55syl2anc 585 . . 3 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ βˆƒπ‘“(𝑓:π‘†βŸΆ( I β€˜π΅) ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))))
5746ad2antrr 725 . . . . . . 7 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ ( I β€˜π΅) = 𝐡)
5857feq3d 6705 . . . . . 6 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ (𝑓:π‘†βŸΆ( I β€˜π΅) ↔ 𝑓:π‘†βŸΆπ΅))
5958anbi1d 631 . . . . 5 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ ((𝑓:π‘†βŸΆ( I β€˜π΅) ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ↔ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))))
60 2ndctop 22951 . . . . . . . . . . . 12 (𝐽 ∈ 2ndΟ‰ β†’ 𝐽 ∈ Top)
6160adantl 483 . . . . . . . . . . 11 ((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) β†’ 𝐽 ∈ Top)
6261ad2antrr 725 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝐽 ∈ Top)
63 frn 6725 . . . . . . . . . . . 12 (𝑓:π‘†βŸΆπ΅ β†’ ran 𝑓 βŠ† 𝐡)
6463ad2antrl 727 . . . . . . . . . . 11 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ran 𝑓 βŠ† 𝐡)
65 bastg 22469 . . . . . . . . . . . . 13 (𝐡 ∈ TopBases β†’ 𝐡 βŠ† (topGenβ€˜π΅))
6665ad3antrrr 729 . . . . . . . . . . . 12 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝐡 βŠ† (topGenβ€˜π΅))
67 2ndcctbss.1 . . . . . . . . . . . 12 𝐽 = (topGenβ€˜π΅)
6866, 67sseqtrrdi 4034 . . . . . . . . . . 11 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝐡 βŠ† 𝐽)
6964, 68sstrd 3993 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ran 𝑓 βŠ† 𝐽)
70 simprrl 780 . . . . . . . . . . . . . . 15 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ π‘œ ∈ 𝐽)
71 simprr 772 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽)) β†’ (topGenβ€˜π‘) = 𝐽)
7271ad2antlr 726 . . . . . . . . . . . . . . 15 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ (topGenβ€˜π‘) = 𝐽)
7370, 72eleqtrrd 2837 . . . . . . . . . . . . . 14 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ π‘œ ∈ (topGenβ€˜π‘))
74 simprrr 781 . . . . . . . . . . . . . 14 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ 𝑑 ∈ π‘œ)
75 tg2 22468 . . . . . . . . . . . . . 14 ((π‘œ ∈ (topGenβ€˜π‘) ∧ 𝑑 ∈ π‘œ) β†’ βˆƒπ‘‘ ∈ 𝑐 (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))
7673, 74, 75syl2anc 585 . . . . . . . . . . . . 13 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ βˆƒπ‘‘ ∈ 𝑐 (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))
77 bastg 22469 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ TopBases β†’ 𝑐 βŠ† (topGenβ€˜π‘))
7877ad2antrl 727 . . . . . . . . . . . . . . . . . 18 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ 𝑐 βŠ† (topGenβ€˜π‘))
7978ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑐 βŠ† (topGenβ€˜π‘))
8067eqeq2i 2746 . . . . . . . . . . . . . . . . . . . . 21 ((topGenβ€˜π‘) = 𝐽 ↔ (topGenβ€˜π‘) = (topGenβ€˜π΅))
8180biimpi 215 . . . . . . . . . . . . . . . . . . . 20 ((topGenβ€˜π‘) = 𝐽 β†’ (topGenβ€˜π‘) = (topGenβ€˜π΅))
8281adantl 483 . . . . . . . . . . . . . . . . . . 19 ((𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽) β†’ (topGenβ€˜π‘) = (topGenβ€˜π΅))
8382ad2antll 728 . . . . . . . . . . . . . . . . . 18 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ (topGenβ€˜π‘) = (topGenβ€˜π΅))
8483ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ (topGenβ€˜π‘) = (topGenβ€˜π΅))
8579, 84sseqtrd 4023 . . . . . . . . . . . . . . . 16 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑐 βŠ† (topGenβ€˜π΅))
86 simprl 770 . . . . . . . . . . . . . . . 16 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑑 ∈ 𝑐)
8785, 86sseldd 3984 . . . . . . . . . . . . . . 15 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑑 ∈ (topGenβ€˜π΅))
88 simprrl 780 . . . . . . . . . . . . . . 15 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑑 ∈ 𝑑)
89 tg2 22468 . . . . . . . . . . . . . . 15 ((𝑑 ∈ (topGenβ€˜π΅) ∧ 𝑑 ∈ 𝑑) β†’ βˆƒπ‘š ∈ 𝐡 (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))
9087, 88, 89syl2anc 585 . . . . . . . . . . . . . 14 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ βˆƒπ‘š ∈ 𝐡 (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))
9165ad3antrrr 729 . . . . . . . . . . . . . . . . . . 19 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ 𝐡 βŠ† (topGenβ€˜π΅))
9291ad2antrr 725 . . . . . . . . . . . . . . . . . 18 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ 𝐡 βŠ† (topGenβ€˜π΅))
9372ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ (topGenβ€˜π‘) = 𝐽)
9493, 67eqtr2di 2790 . . . . . . . . . . . . . . . . . 18 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ (topGenβ€˜π΅) = (topGenβ€˜π‘))
9592, 94sseqtrd 4023 . . . . . . . . . . . . . . . . 17 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ 𝐡 βŠ† (topGenβ€˜π‘))
96 simprl 770 . . . . . . . . . . . . . . . . 17 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ π‘š ∈ 𝐡)
9795, 96sseldd 3984 . . . . . . . . . . . . . . . 16 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ π‘š ∈ (topGenβ€˜π‘))
98 simprrl 780 . . . . . . . . . . . . . . . 16 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ 𝑑 ∈ π‘š)
99 tg2 22468 . . . . . . . . . . . . . . . 16 ((π‘š ∈ (topGenβ€˜π‘) ∧ 𝑑 ∈ π‘š) β†’ βˆƒπ‘› ∈ 𝑐 (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))
10097, 98, 99syl2anc 585 . . . . . . . . . . . . . . 15 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ βˆƒπ‘› ∈ 𝑐 (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))
101 ffn 6718 . . . . . . . . . . . . . . . . . . . 20 (𝑓:π‘†βŸΆπ΅ β†’ 𝑓 Fn 𝑆)
102101ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ)) β†’ 𝑓 Fn 𝑆)
103102ad2antlr 726 . . . . . . . . . . . . . . . . . 18 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑓 Fn 𝑆)
104103ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ 𝑓 Fn 𝑆)
105 simprl 770 . . . . . . . . . . . . . . . . . 18 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ 𝑛 ∈ 𝑐)
10686ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ 𝑑 ∈ 𝑐)
107 simplrl 776 . . . . . . . . . . . . . . . . . . 19 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ π‘š ∈ 𝐡)
108 simprrr 781 . . . . . . . . . . . . . . . . . . 19 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ 𝑛 βŠ† π‘š)
109 simprr 772 . . . . . . . . . . . . . . . . . . . 20 ((π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑)) β†’ π‘š βŠ† 𝑑)
110109ad2antlr 726 . . . . . . . . . . . . . . . . . . 19 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ π‘š βŠ† 𝑑)
111 sseq2 4009 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 = π‘š β†’ (𝑛 βŠ† 𝑀 ↔ 𝑛 βŠ† π‘š))
112 sseq1 4008 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 = π‘š β†’ (𝑀 βŠ† 𝑑 ↔ π‘š βŠ† 𝑑))
113111, 112anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑀 = π‘š β†’ ((𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑) ↔ (𝑛 βŠ† π‘š ∧ π‘š βŠ† 𝑑)))
114113rspcev 3613 . . . . . . . . . . . . . . . . . . 19 ((π‘š ∈ 𝐡 ∧ (𝑛 βŠ† π‘š ∧ π‘š βŠ† 𝑑)) β†’ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑))
115107, 108, 110, 114syl12anc 836 . . . . . . . . . . . . . . . . . 18 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑))
116 df-br 5150 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑆𝑑 ↔ βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆)
117 vex 3479 . . . . . . . . . . . . . . . . . . . 20 𝑛 ∈ V
118 vex 3479 . . . . . . . . . . . . . . . . . . . 20 𝑑 ∈ V
119 simpl 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ 𝑒 = 𝑛)
120119eleq1d 2819 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ (𝑒 ∈ 𝑐 ↔ 𝑛 ∈ 𝑐))
121 simpr 486 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ 𝑣 = 𝑑)
122121eleq1d 2819 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ (𝑣 ∈ 𝑐 ↔ 𝑑 ∈ 𝑐))
123 sseq1 4008 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = 𝑛 β†’ (𝑒 βŠ† 𝑀 ↔ 𝑛 βŠ† 𝑀))
124 sseq2 4009 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = 𝑑 β†’ (𝑀 βŠ† 𝑣 ↔ 𝑀 βŠ† 𝑑))
125123, 124bi2anan9 638 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ ((𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣) ↔ (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑)))
126125rexbidv 3179 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ (βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣) ↔ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑)))
127120, 122, 1263anbi123d 1437 . . . . . . . . . . . . . . . . . . . 20 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ ((𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣)) ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑))))
128117, 118, 127, 8braba 5538 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑆𝑑 ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑)))
129116, 128bitr3i 277 . . . . . . . . . . . . . . . . . 18 (βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆 ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑)))
130105, 106, 115, 129syl3anbrc 1344 . . . . . . . . . . . . . . . . 17 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆)
131 fnfvelrn 7083 . . . . . . . . . . . . . . . . 17 ((𝑓 Fn 𝑆 ∧ βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆) β†’ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∈ ran 𝑓)
132104, 130, 131syl2anc 585 . . . . . . . . . . . . . . . 16 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∈ ran 𝑓)
133 simprl 770 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ 𝑛 ∈ 𝑐)
134 simplll 774 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ 𝑑 ∈ 𝑐)
135 simplrl 776 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ π‘š ∈ 𝐡)
136 simprrr 781 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ 𝑛 βŠ† π‘š)
137109ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ π‘š βŠ† 𝑑)
138135, 136, 137, 114syl12anc 836 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑))
139133, 134, 138, 129syl3anbrc 1344 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆)
140 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ (1st β€˜π‘₯) = (1st β€˜βŸ¨π‘›, π‘‘βŸ©))
141 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ (π‘“β€˜π‘₯) = (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©))
142140, 141sseq12d 4016 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ↔ (1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©)))
143 fveq2 6892 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ (2nd β€˜π‘₯) = (2nd β€˜βŸ¨π‘›, π‘‘βŸ©))
144141, 143sseq12d 4016 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ ((π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯) ↔ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©)))
145142, 144anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ (((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)) ↔ ((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©))))
146145rspcv 3609 . . . . . . . . . . . . . . . . . . . . . 22 (βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆 β†’ (βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)) β†’ ((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©))))
147139, 146syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ (βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)) β†’ ((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©))))
148117, 118op1st 7983 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st β€˜βŸ¨π‘›, π‘‘βŸ©) = 𝑛
149148sseq1i 4011 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ↔ 𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©))
150117, 118op2nd 7984 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd β€˜βŸ¨π‘›, π‘‘βŸ©) = 𝑑
151150sseq2i 4012 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©) ↔ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)
152149, 151anbi12i 628 . . . . . . . . . . . . . . . . . . . . . 22 (((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©)) ↔ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑))
153 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ 𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©))
154 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š)) β†’ 𝑑 ∈ 𝑛)
155154ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ 𝑑 ∈ 𝑛)
156153, 155sseldd 3984 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ 𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©))
157 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)
158 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ 𝑑 βŠ† π‘œ)
159158ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ 𝑑 βŠ† π‘œ)
160157, 159sstrd 3993 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)
161156, 160jca 513 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ))
162161ex 414 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ ((𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)))
163152, 162biimtrid 241 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ (((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©)) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)))
164147, 163syldc 48 . . . . . . . . . . . . . . . . . . . 20 (βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)) β†’ ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)))
165164exp4c 434 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)) β†’ ((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) β†’ ((π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑)) β†’ ((𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š)) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)))))
166165ad2antlr 726 . . . . . . . . . . . . . . . . . 18 (((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ)) β†’ ((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) β†’ ((π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑)) β†’ ((𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š)) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)))))
167166adantl 483 . . . . . . . . . . . . . . . . 17 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ ((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) β†’ ((π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑)) β†’ ((𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š)) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)))))
168167imp41 427 . . . . . . . . . . . . . . . 16 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ))
169 eleq2 2823 . . . . . . . . . . . . . . . . . 18 (𝑏 = (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) β†’ (𝑑 ∈ 𝑏 ↔ 𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©)))
170 sseq1 4008 . . . . . . . . . . . . . . . . . 18 (𝑏 = (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) β†’ (𝑏 βŠ† π‘œ ↔ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ))
171169, 170anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑏 = (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) β†’ ((𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ) ↔ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)))
172171rspcev 3613 . . . . . . . . . . . . . . . 16 (((π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∈ ran 𝑓 ∧ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
173132, 168, 172syl2anc 585 . . . . . . . . . . . . . . 15 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
174100, 173rexlimddv 3162 . . . . . . . . . . . . . 14 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
17590, 174rexlimddv 3162 . . . . . . . . . . . . 13 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
17676, 175rexlimddv 3162 . . . . . . . . . . . 12 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
177176expr 458 . . . . . . . . . . 11 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ((π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ)))
178177ralrimivv 3199 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ βˆ€π‘œ ∈ 𝐽 βˆ€π‘‘ ∈ π‘œ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
179 basgen2 22492 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ ran 𝑓 βŠ† 𝐽 ∧ βˆ€π‘œ ∈ 𝐽 βˆ€π‘‘ ∈ π‘œ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ)) β†’ (topGenβ€˜ran 𝑓) = 𝐽)
18062, 69, 178, 179syl3anc 1372 . . . . . . . . 9 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ (topGenβ€˜ran 𝑓) = 𝐽)
181180, 62eqeltrd 2834 . . . . . . . 8 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ (topGenβ€˜ran 𝑓) ∈ Top)
182 tgclb 22473 . . . . . . . 8 (ran 𝑓 ∈ TopBases ↔ (topGenβ€˜ran 𝑓) ∈ Top)
183181, 182sylibr 233 . . . . . . 7 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ran 𝑓 ∈ TopBases)
184 omelon 9641 . . . . . . . . . 10 Ο‰ ∈ On
18524adantr 482 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝑆 β‰Ό Ο‰)
186 ondomen 10032 . . . . . . . . . 10 ((Ο‰ ∈ On ∧ 𝑆 β‰Ό Ο‰) β†’ 𝑆 ∈ dom card)
187184, 185, 186sylancr 588 . . . . . . . . 9 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝑆 ∈ dom card)
188101ad2antrl 727 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝑓 Fn 𝑆)
189 dffn4 6812 . . . . . . . . . 10 (𝑓 Fn 𝑆 ↔ 𝑓:𝑆–ontoβ†’ran 𝑓)
190188, 189sylib 217 . . . . . . . . 9 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝑓:𝑆–ontoβ†’ran 𝑓)
191 fodomnum 10052 . . . . . . . . 9 (𝑆 ∈ dom card β†’ (𝑓:𝑆–ontoβ†’ran 𝑓 β†’ ran 𝑓 β‰Ό 𝑆))
192187, 190, 191sylc 65 . . . . . . . 8 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ran 𝑓 β‰Ό 𝑆)
193 domtr 9003 . . . . . . . 8 ((ran 𝑓 β‰Ό 𝑆 ∧ 𝑆 β‰Ό Ο‰) β†’ ran 𝑓 β‰Ό Ο‰)
194192, 185, 193syl2anc 585 . . . . . . 7 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ran 𝑓 β‰Ό Ο‰)
195180eqcomd 2739 . . . . . . 7 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝐽 = (topGenβ€˜ran 𝑓))
196 breq1 5152 . . . . . . . . 9 (𝑏 = ran 𝑓 β†’ (𝑏 β‰Ό Ο‰ ↔ ran 𝑓 β‰Ό Ο‰))
197 sseq1 4008 . . . . . . . . 9 (𝑏 = ran 𝑓 β†’ (𝑏 βŠ† 𝐡 ↔ ran 𝑓 βŠ† 𝐡))
198 fveq2 6892 . . . . . . . . . 10 (𝑏 = ran 𝑓 β†’ (topGenβ€˜π‘) = (topGenβ€˜ran 𝑓))
199198eqeq2d 2744 . . . . . . . . 9 (𝑏 = ran 𝑓 β†’ (𝐽 = (topGenβ€˜π‘) ↔ 𝐽 = (topGenβ€˜ran 𝑓)))
200196, 197, 1993anbi123d 1437 . . . . . . . 8 (𝑏 = ran 𝑓 β†’ ((𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘)) ↔ (ran 𝑓 β‰Ό Ο‰ ∧ ran 𝑓 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜ran 𝑓))))
201200rspcev 3613 . . . . . . 7 ((ran 𝑓 ∈ TopBases ∧ (ran 𝑓 β‰Ό Ο‰ ∧ ran 𝑓 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜ran 𝑓))) β†’ βˆƒπ‘ ∈ TopBases (𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘)))
202183, 194, 64, 195, 201syl13anc 1373 . . . . . 6 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ βˆƒπ‘ ∈ TopBases (𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘)))
203202ex 414 . . . . 5 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) β†’ βˆƒπ‘ ∈ TopBases (𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘))))
20459, 203sylbid 239 . . . 4 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ ((𝑓:π‘†βŸΆ( I β€˜π΅) ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) β†’ βˆƒπ‘ ∈ TopBases (𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘))))
205204exlimdv 1937 . . 3 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ (βˆƒπ‘“(𝑓:π‘†βŸΆ( I β€˜π΅) ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) β†’ βˆƒπ‘ ∈ TopBases (𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘))))
20656, 205mpd 15 . 2 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ βˆƒπ‘ ∈ TopBases (𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘)))
2073, 206rexlimddv 3162 1 ((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) β†’ βˆƒπ‘ ∈ TopBases (𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   βŠ† wss 3949  βŸ¨cop 4635   class class class wbr 5149  {copab 5211   I cid 5574   Γ— cxp 5675  dom cdm 5677  ran crn 5678  Rel wrel 5682  Oncon0 6365   Fn wfn 6539  βŸΆwf 6540  β€“ontoβ†’wfo 6542  β€˜cfv 6544  Ο‰com 7855  1st c1st 7973  2nd c2nd 7974   β‰ˆ cen 8936   β‰Ό cdom 8937  cardccrd 9930  topGenctg 17383  Topctop 22395  TopBasesctb 22448  2ndΟ‰c2ndc 22942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cc 10430
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-oi 9505  df-card 9934  df-acn 9937  df-topgen 17389  df-top 22396  df-bases 22449  df-2ndc 22944
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator