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

Theorem 2ndcctbss 22966
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 485 . . 3 ((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) β†’ 𝐽 ∈ 2ndΟ‰)
2 is2ndc 22957 . . 3 (𝐽 ∈ 2ndΟ‰ ↔ βˆƒπ‘ ∈ TopBases (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))
31, 2sylib 217 . 2 ((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) β†’ βˆƒπ‘ ∈ TopBases (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))
4 vex 3478 . . . . . . 7 𝑐 ∈ V
54, 4xpex 7742 . . . . . 6 (𝑐 Γ— 𝑐) ∈ V
6 3simpa 1148 . . . . . . . 8 ((𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣)) β†’ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐))
76ssopab2i 5550 . . . . . . 7 {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣))} βŠ† {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)}
8 2ndcctbss.2 . . . . . . 7 𝑆 = {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣))}
9 df-xp 5682 . . . . . . 7 (𝑐 Γ— 𝑐) = {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)}
107, 8, 93sstr4i 4025 . . . . . 6 𝑆 βŠ† (𝑐 Γ— 𝑐)
11 ssdomg 8998 . . . . . 6 ((𝑐 Γ— 𝑐) ∈ V β†’ (𝑆 βŠ† (𝑐 Γ— 𝑐) β†’ 𝑆 β‰Ό (𝑐 Γ— 𝑐)))
125, 10, 11mp2 9 . . . . 5 𝑆 β‰Ό (𝑐 Γ— 𝑐)
134xpdom1 9073 . . . . . . . . 9 (𝑐 β‰Ό Ο‰ β†’ (𝑐 Γ— 𝑐) β‰Ό (Ο‰ Γ— 𝑐))
14 omex 9640 . . . . . . . . . 10 Ο‰ ∈ V
1514xpdom2 9069 . . . . . . . . 9 (𝑐 β‰Ό Ο‰ β†’ (Ο‰ Γ— 𝑐) β‰Ό (Ο‰ Γ— Ο‰))
16 domtr 9005 . . . . . . . . 9 (((𝑐 Γ— 𝑐) β‰Ό (Ο‰ Γ— 𝑐) ∧ (Ο‰ Γ— 𝑐) β‰Ό (Ο‰ Γ— Ο‰)) β†’ (𝑐 Γ— 𝑐) β‰Ό (Ο‰ Γ— Ο‰))
1713, 15, 16syl2anc 584 . . . . . . . 8 (𝑐 β‰Ό Ο‰ β†’ (𝑐 Γ— 𝑐) β‰Ό (Ο‰ Γ— Ο‰))
18 xpomen 10012 . . . . . . . 8 (Ο‰ Γ— Ο‰) β‰ˆ Ο‰
19 domentr 9011 . . . . . . . 8 (((𝑐 Γ— 𝑐) β‰Ό (Ο‰ Γ— Ο‰) ∧ (Ο‰ Γ— Ο‰) β‰ˆ Ο‰) β†’ (𝑐 Γ— 𝑐) β‰Ό Ο‰)
2017, 18, 19sylancl 586 . . . . . . 7 (𝑐 β‰Ό Ο‰ β†’ (𝑐 Γ— 𝑐) β‰Ό Ο‰)
2120adantr 481 . . . . . 6 ((𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽) β†’ (𝑐 Γ— 𝑐) β‰Ό Ο‰)
2221ad2antll 727 . . . . 5 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ (𝑐 Γ— 𝑐) β‰Ό Ο‰)
23 domtr 9005 . . . . 5 ((𝑆 β‰Ό (𝑐 Γ— 𝑐) ∧ (𝑐 Γ— 𝑐) β‰Ό Ο‰) β†’ 𝑆 β‰Ό Ο‰)
2412, 22, 23sylancr 587 . . . 4 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ 𝑆 β‰Ό Ο‰)
258relopabiv 5820 . . . . . . . . 9 Rel 𝑆
26 simpr 485 . . . . . . . . 9 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ π‘₯ ∈ 𝑆)
27 1st2nd 8027 . . . . . . . . 9 ((Rel 𝑆 ∧ π‘₯ ∈ 𝑆) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
2825, 26, 27sylancr 587 . . . . . . . 8 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
2928, 26eqeltrrd 2834 . . . . . . 7 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑆)
30 df-br 5149 . . . . . . . . 9 ((1st β€˜π‘₯)𝑆(2nd β€˜π‘₯) ↔ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑆)
31 fvex 6904 . . . . . . . . . 10 (1st β€˜π‘₯) ∈ V
32 fvex 6904 . . . . . . . . . 10 (2nd β€˜π‘₯) ∈ V
33 simpl 483 . . . . . . . . . . . 12 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ 𝑒 = (1st β€˜π‘₯))
3433eleq1d 2818 . . . . . . . . . . 11 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ (𝑒 ∈ 𝑐 ↔ (1st β€˜π‘₯) ∈ 𝑐))
35 simpr 485 . . . . . . . . . . . 12 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ 𝑣 = (2nd β€˜π‘₯))
3635eleq1d 2818 . . . . . . . . . . 11 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ (𝑣 ∈ 𝑐 ↔ (2nd β€˜π‘₯) ∈ 𝑐))
37 sseq1 4007 . . . . . . . . . . . . 13 (𝑒 = (1st β€˜π‘₯) β†’ (𝑒 βŠ† 𝑀 ↔ (1st β€˜π‘₯) βŠ† 𝑀))
38 sseq2 4008 . . . . . . . . . . . . 13 (𝑣 = (2nd β€˜π‘₯) β†’ (𝑀 βŠ† 𝑣 ↔ 𝑀 βŠ† (2nd β€˜π‘₯)))
3937, 38bi2anan9 637 . . . . . . . . . . . 12 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ ((𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣) ↔ ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯))))
4039rexbidv 3178 . . . . . . . . . . 11 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ (βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣) ↔ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯))))
4134, 36, 403anbi123d 1436 . . . . . . . . . 10 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ ((𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣)) ↔ ((1st β€˜π‘₯) ∈ 𝑐 ∧ (2nd β€˜π‘₯) ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)))))
4231, 32, 41, 8braba 5537 . . . . . . . . 9 ((1st β€˜π‘₯)𝑆(2nd β€˜π‘₯) ↔ ((1st β€˜π‘₯) ∈ 𝑐 ∧ (2nd β€˜π‘₯) ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯))))
4330, 42bitr3i 276 . . . . . . . 8 (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑆 ↔ ((1st β€˜π‘₯) ∈ 𝑐 ∧ (2nd β€˜π‘₯) ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯))))
4443simp3bi 1147 . . . . . . 7 (⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑆 β†’ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)))
4529, 44syl 17 . . . . . 6 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)))
46 fvi 6967 . . . . . . . 8 (𝐡 ∈ TopBases β†’ ( I β€˜π΅) = 𝐡)
4746ad3antrrr 728 . . . . . . 7 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ ( I β€˜π΅) = 𝐡)
4847rexeqdv 3326 . . . . . 6 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ (βˆƒπ‘€ ∈ ( I β€˜π΅)((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)) ↔ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯))))
4945, 48mpbird 256 . . . . 5 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ βˆƒπ‘€ ∈ ( I β€˜π΅)((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)))
5049ralrimiva 3146 . . . 4 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ βˆ€π‘₯ ∈ 𝑆 βˆƒπ‘€ ∈ ( I β€˜π΅)((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)))
51 fvex 6904 . . . . 5 ( I β€˜π΅) ∈ V
52 sseq2 4008 . . . . . 6 (𝑀 = (π‘“β€˜π‘₯) β†’ ((1st β€˜π‘₯) βŠ† 𝑀 ↔ (1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯)))
53 sseq1 4007 . . . . . 6 (𝑀 = (π‘“β€˜π‘₯) β†’ (𝑀 βŠ† (2nd β€˜π‘₯) ↔ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))
5452, 53anbi12d 631 . . . . 5 (𝑀 = (π‘“β€˜π‘₯) β†’ (((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)) ↔ ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))))
5551, 54axcc4dom 10438 . . . 4 ((𝑆 β‰Ό Ο‰ ∧ βˆ€π‘₯ ∈ 𝑆 βˆƒπ‘€ ∈ ( I β€˜π΅)((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯))) β†’ βˆƒπ‘“(𝑓:π‘†βŸΆ( I β€˜π΅) ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))))
5624, 50, 55syl2anc 584 . . 3 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ βˆƒπ‘“(𝑓:π‘†βŸΆ( I β€˜π΅) ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))))
5746ad2antrr 724 . . . . . . 7 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ ( I β€˜π΅) = 𝐡)
5857feq3d 6704 . . . . . 6 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ (𝑓:π‘†βŸΆ( I β€˜π΅) ↔ 𝑓:π‘†βŸΆπ΅))
5958anbi1d 630 . . . . 5 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ ((𝑓:π‘†βŸΆ( I β€˜π΅) ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ↔ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))))
60 2ndctop 22958 . . . . . . . . . . . 12 (𝐽 ∈ 2ndΟ‰ β†’ 𝐽 ∈ Top)
6160adantl 482 . . . . . . . . . . 11 ((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) β†’ 𝐽 ∈ Top)
6261ad2antrr 724 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝐽 ∈ Top)
63 frn 6724 . . . . . . . . . . . 12 (𝑓:π‘†βŸΆπ΅ β†’ ran 𝑓 βŠ† 𝐡)
6463ad2antrl 726 . . . . . . . . . . 11 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ran 𝑓 βŠ† 𝐡)
65 bastg 22476 . . . . . . . . . . . . 13 (𝐡 ∈ TopBases β†’ 𝐡 βŠ† (topGenβ€˜π΅))
6665ad3antrrr 728 . . . . . . . . . . . 12 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝐡 βŠ† (topGenβ€˜π΅))
67 2ndcctbss.1 . . . . . . . . . . . 12 𝐽 = (topGenβ€˜π΅)
6866, 67sseqtrrdi 4033 . . . . . . . . . . 11 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝐡 βŠ† 𝐽)
6964, 68sstrd 3992 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ran 𝑓 βŠ† 𝐽)
70 simprrl 779 . . . . . . . . . . . . . . 15 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ π‘œ ∈ 𝐽)
71 simprr 771 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽)) β†’ (topGenβ€˜π‘) = 𝐽)
7271ad2antlr 725 . . . . . . . . . . . . . . 15 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ (topGenβ€˜π‘) = 𝐽)
7370, 72eleqtrrd 2836 . . . . . . . . . . . . . 14 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ π‘œ ∈ (topGenβ€˜π‘))
74 simprrr 780 . . . . . . . . . . . . . 14 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ 𝑑 ∈ π‘œ)
75 tg2 22475 . . . . . . . . . . . . . 14 ((π‘œ ∈ (topGenβ€˜π‘) ∧ 𝑑 ∈ π‘œ) β†’ βˆƒπ‘‘ ∈ 𝑐 (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))
7673, 74, 75syl2anc 584 . . . . . . . . . . . . 13 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ βˆƒπ‘‘ ∈ 𝑐 (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))
77 bastg 22476 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ TopBases β†’ 𝑐 βŠ† (topGenβ€˜π‘))
7877ad2antrl 726 . . . . . . . . . . . . . . . . . 18 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ 𝑐 βŠ† (topGenβ€˜π‘))
7978ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑐 βŠ† (topGenβ€˜π‘))
8067eqeq2i 2745 . . . . . . . . . . . . . . . . . . . . 21 ((topGenβ€˜π‘) = 𝐽 ↔ (topGenβ€˜π‘) = (topGenβ€˜π΅))
8180biimpi 215 . . . . . . . . . . . . . . . . . . . 20 ((topGenβ€˜π‘) = 𝐽 β†’ (topGenβ€˜π‘) = (topGenβ€˜π΅))
8281adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽) β†’ (topGenβ€˜π‘) = (topGenβ€˜π΅))
8382ad2antll 727 . . . . . . . . . . . . . . . . . 18 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ (topGenβ€˜π‘) = (topGenβ€˜π΅))
8483ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ (topGenβ€˜π‘) = (topGenβ€˜π΅))
8579, 84sseqtrd 4022 . . . . . . . . . . . . . . . 16 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑐 βŠ† (topGenβ€˜π΅))
86 simprl 769 . . . . . . . . . . . . . . . 16 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑑 ∈ 𝑐)
8785, 86sseldd 3983 . . . . . . . . . . . . . . 15 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑑 ∈ (topGenβ€˜π΅))
88 simprrl 779 . . . . . . . . . . . . . . 15 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑑 ∈ 𝑑)
89 tg2 22475 . . . . . . . . . . . . . . 15 ((𝑑 ∈ (topGenβ€˜π΅) ∧ 𝑑 ∈ 𝑑) β†’ βˆƒπ‘š ∈ 𝐡 (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))
9087, 88, 89syl2anc 584 . . . . . . . . . . . . . 14 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ βˆƒπ‘š ∈ 𝐡 (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))
9165ad3antrrr 728 . . . . . . . . . . . . . . . . . . 19 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ 𝐡 βŠ† (topGenβ€˜π΅))
9291ad2antrr 724 . . . . . . . . . . . . . . . . . 18 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ 𝐡 βŠ† (topGenβ€˜π΅))
9372ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ (topGenβ€˜π‘) = 𝐽)
9493, 67eqtr2di 2789 . . . . . . . . . . . . . . . . . 18 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ (topGenβ€˜π΅) = (topGenβ€˜π‘))
9592, 94sseqtrd 4022 . . . . . . . . . . . . . . . . 17 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ 𝐡 βŠ† (topGenβ€˜π‘))
96 simprl 769 . . . . . . . . . . . . . . . . 17 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ π‘š ∈ 𝐡)
9795, 96sseldd 3983 . . . . . . . . . . . . . . . 16 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ π‘š ∈ (topGenβ€˜π‘))
98 simprrl 779 . . . . . . . . . . . . . . . 16 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ 𝑑 ∈ π‘š)
99 tg2 22475 . . . . . . . . . . . . . . . 16 ((π‘š ∈ (topGenβ€˜π‘) ∧ 𝑑 ∈ π‘š) β†’ βˆƒπ‘› ∈ 𝑐 (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))
10097, 98, 99syl2anc 584 . . . . . . . . . . . . . . 15 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ βˆƒπ‘› ∈ 𝑐 (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))
101 ffn 6717 . . . . . . . . . . . . . . . . . . . 20 (𝑓:π‘†βŸΆπ΅ β†’ 𝑓 Fn 𝑆)
102101ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ)) β†’ 𝑓 Fn 𝑆)
103102ad2antlr 725 . . . . . . . . . . . . . . . . . 18 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑓 Fn 𝑆)
104103ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ 𝑓 Fn 𝑆)
105 simprl 769 . . . . . . . . . . . . . . . . . 18 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ 𝑛 ∈ 𝑐)
10686ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ 𝑑 ∈ 𝑐)
107 simplrl 775 . . . . . . . . . . . . . . . . . . 19 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ π‘š ∈ 𝐡)
108 simprrr 780 . . . . . . . . . . . . . . . . . . 19 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ 𝑛 βŠ† π‘š)
109 simprr 771 . . . . . . . . . . . . . . . . . . . 20 ((π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑)) β†’ π‘š βŠ† 𝑑)
110109ad2antlr 725 . . . . . . . . . . . . . . . . . . 19 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ π‘š βŠ† 𝑑)
111 sseq2 4008 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 = π‘š β†’ (𝑛 βŠ† 𝑀 ↔ 𝑛 βŠ† π‘š))
112 sseq1 4007 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 = π‘š β†’ (𝑀 βŠ† 𝑑 ↔ π‘š βŠ† 𝑑))
113111, 112anbi12d 631 . . . . . . . . . . . . . . . . . . . 20 (𝑀 = π‘š β†’ ((𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑) ↔ (𝑛 βŠ† π‘š ∧ π‘š βŠ† 𝑑)))
114113rspcev 3612 . . . . . . . . . . . . . . . . . . 19 ((π‘š ∈ 𝐡 ∧ (𝑛 βŠ† π‘š ∧ π‘š βŠ† 𝑑)) β†’ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑))
115107, 108, 110, 114syl12anc 835 . . . . . . . . . . . . . . . . . 18 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑))
116 df-br 5149 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑆𝑑 ↔ βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆)
117 vex 3478 . . . . . . . . . . . . . . . . . . . 20 𝑛 ∈ V
118 vex 3478 . . . . . . . . . . . . . . . . . . . 20 𝑑 ∈ V
119 simpl 483 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ 𝑒 = 𝑛)
120119eleq1d 2818 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ (𝑒 ∈ 𝑐 ↔ 𝑛 ∈ 𝑐))
121 simpr 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ 𝑣 = 𝑑)
122121eleq1d 2818 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ (𝑣 ∈ 𝑐 ↔ 𝑑 ∈ 𝑐))
123 sseq1 4007 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = 𝑛 β†’ (𝑒 βŠ† 𝑀 ↔ 𝑛 βŠ† 𝑀))
124 sseq2 4008 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = 𝑑 β†’ (𝑀 βŠ† 𝑣 ↔ 𝑀 βŠ† 𝑑))
125123, 124bi2anan9 637 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ ((𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣) ↔ (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑)))
126125rexbidv 3178 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ (βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣) ↔ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑)))
127120, 122, 1263anbi123d 1436 . . . . . . . . . . . . . . . . . . . 20 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ ((𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣)) ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑))))
128117, 118, 127, 8braba 5537 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑆𝑑 ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑)))
129116, 128bitr3i 276 . . . . . . . . . . . . . . . . . 18 (βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆 ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑)))
130105, 106, 115, 129syl3anbrc 1343 . . . . . . . . . . . . . . . . 17 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆)
131 fnfvelrn 7082 . . . . . . . . . . . . . . . . 17 ((𝑓 Fn 𝑆 ∧ βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆) β†’ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∈ ran 𝑓)
132104, 130, 131syl2anc 584 . . . . . . . . . . . . . . . 16 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∈ ran 𝑓)
133 simprl 769 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ 𝑛 ∈ 𝑐)
134 simplll 773 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ 𝑑 ∈ 𝑐)
135 simplrl 775 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ π‘š ∈ 𝐡)
136 simprrr 780 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ 𝑛 βŠ† π‘š)
137109ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ π‘š βŠ† 𝑑)
138135, 136, 137, 114syl12anc 835 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑))
139133, 134, 138, 129syl3anbrc 1343 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆)
140 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ (1st β€˜π‘₯) = (1st β€˜βŸ¨π‘›, π‘‘βŸ©))
141 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ (π‘“β€˜π‘₯) = (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©))
142140, 141sseq12d 4015 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ↔ (1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©)))
143 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ (2nd β€˜π‘₯) = (2nd β€˜βŸ¨π‘›, π‘‘βŸ©))
144141, 143sseq12d 4015 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ ((π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯) ↔ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©)))
145142, 144anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ (((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)) ↔ ((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©))))
146145rspcv 3608 . . . . . . . . . . . . . . . . . . . . . 22 (βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆 β†’ (βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)) β†’ ((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©))))
147139, 146syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ (βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)) β†’ ((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©))))
148117, 118op1st 7985 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st β€˜βŸ¨π‘›, π‘‘βŸ©) = 𝑛
149148sseq1i 4010 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ↔ 𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©))
150117, 118op2nd 7986 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd β€˜βŸ¨π‘›, π‘‘βŸ©) = 𝑑
151150sseq2i 4011 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©) ↔ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)
152149, 151anbi12i 627 . . . . . . . . . . . . . . . . . . . . . 22 (((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©)) ↔ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑))
153 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ 𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©))
154 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š)) β†’ 𝑑 ∈ 𝑛)
155154ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ 𝑑 ∈ 𝑛)
156153, 155sseldd 3983 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ 𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©))
157 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)
158 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ 𝑑 βŠ† π‘œ)
159158ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ 𝑑 βŠ† π‘œ)
160157, 159sstrd 3992 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)
161156, 160jca 512 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ))
162161ex 413 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ ((𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)))
163152, 162biimtrid 241 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ (((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©)) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)))
164147, 163syldc 48 . . . . . . . . . . . . . . . . . . . 20 (βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)) β†’ ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)))
165164exp4c 433 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)) β†’ ((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) β†’ ((π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑)) β†’ ((𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š)) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)))))
166165ad2antlr 725 . . . . . . . . . . . . . . . . . 18 (((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ)) β†’ ((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) β†’ ((π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑)) β†’ ((𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š)) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)))))
167166adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ ((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) β†’ ((π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑)) β†’ ((𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š)) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)))))
168167imp41 426 . . . . . . . . . . . . . . . 16 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ))
169 eleq2 2822 . . . . . . . . . . . . . . . . . 18 (𝑏 = (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) β†’ (𝑑 ∈ 𝑏 ↔ 𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©)))
170 sseq1 4007 . . . . . . . . . . . . . . . . . 18 (𝑏 = (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) β†’ (𝑏 βŠ† π‘œ ↔ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ))
171169, 170anbi12d 631 . . . . . . . . . . . . . . . . 17 (𝑏 = (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) β†’ ((𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ) ↔ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)))
172171rspcev 3612 . . . . . . . . . . . . . . . 16 (((π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∈ ran 𝑓 ∧ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
173132, 168, 172syl2anc 584 . . . . . . . . . . . . . . 15 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
174100, 173rexlimddv 3161 . . . . . . . . . . . . . 14 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
17590, 174rexlimddv 3161 . . . . . . . . . . . . 13 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
17676, 175rexlimddv 3161 . . . . . . . . . . . 12 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
177176expr 457 . . . . . . . . . . 11 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ((π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ)))
178177ralrimivv 3198 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ βˆ€π‘œ ∈ 𝐽 βˆ€π‘‘ ∈ π‘œ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
179 basgen2 22499 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ ran 𝑓 βŠ† 𝐽 ∧ βˆ€π‘œ ∈ 𝐽 βˆ€π‘‘ ∈ π‘œ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ)) β†’ (topGenβ€˜ran 𝑓) = 𝐽)
18062, 69, 178, 179syl3anc 1371 . . . . . . . . 9 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ (topGenβ€˜ran 𝑓) = 𝐽)
181180, 62eqeltrd 2833 . . . . . . . 8 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ (topGenβ€˜ran 𝑓) ∈ Top)
182 tgclb 22480 . . . . . . . 8 (ran 𝑓 ∈ TopBases ↔ (topGenβ€˜ran 𝑓) ∈ Top)
183181, 182sylibr 233 . . . . . . 7 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ran 𝑓 ∈ TopBases)
184 omelon 9643 . . . . . . . . . 10 Ο‰ ∈ On
18524adantr 481 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝑆 β‰Ό Ο‰)
186 ondomen 10034 . . . . . . . . . 10 ((Ο‰ ∈ On ∧ 𝑆 β‰Ό Ο‰) β†’ 𝑆 ∈ dom card)
187184, 185, 186sylancr 587 . . . . . . . . 9 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝑆 ∈ dom card)
188101ad2antrl 726 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝑓 Fn 𝑆)
189 dffn4 6811 . . . . . . . . . 10 (𝑓 Fn 𝑆 ↔ 𝑓:𝑆–ontoβ†’ran 𝑓)
190188, 189sylib 217 . . . . . . . . 9 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝑓:𝑆–ontoβ†’ran 𝑓)
191 fodomnum 10054 . . . . . . . . 9 (𝑆 ∈ dom card β†’ (𝑓:𝑆–ontoβ†’ran 𝑓 β†’ ran 𝑓 β‰Ό 𝑆))
192187, 190, 191sylc 65 . . . . . . . 8 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ran 𝑓 β‰Ό 𝑆)
193 domtr 9005 . . . . . . . 8 ((ran 𝑓 β‰Ό 𝑆 ∧ 𝑆 β‰Ό Ο‰) β†’ ran 𝑓 β‰Ό Ο‰)
194192, 185, 193syl2anc 584 . . . . . . 7 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ran 𝑓 β‰Ό Ο‰)
195180eqcomd 2738 . . . . . . 7 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝐽 = (topGenβ€˜ran 𝑓))
196 breq1 5151 . . . . . . . . 9 (𝑏 = ran 𝑓 β†’ (𝑏 β‰Ό Ο‰ ↔ ran 𝑓 β‰Ό Ο‰))
197 sseq1 4007 . . . . . . . . 9 (𝑏 = ran 𝑓 β†’ (𝑏 βŠ† 𝐡 ↔ ran 𝑓 βŠ† 𝐡))
198 fveq2 6891 . . . . . . . . . 10 (𝑏 = ran 𝑓 β†’ (topGenβ€˜π‘) = (topGenβ€˜ran 𝑓))
199198eqeq2d 2743 . . . . . . . . 9 (𝑏 = ran 𝑓 β†’ (𝐽 = (topGenβ€˜π‘) ↔ 𝐽 = (topGenβ€˜ran 𝑓)))
200196, 197, 1993anbi123d 1436 . . . . . . . 8 (𝑏 = ran 𝑓 β†’ ((𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘)) ↔ (ran 𝑓 β‰Ό Ο‰ ∧ ran 𝑓 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜ran 𝑓))))
201200rspcev 3612 . . . . . . 7 ((ran 𝑓 ∈ TopBases ∧ (ran 𝑓 β‰Ό Ο‰ ∧ ran 𝑓 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜ran 𝑓))) β†’ βˆƒπ‘ ∈ TopBases (𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘)))
202183, 194, 64, 195, 201syl13anc 1372 . . . . . 6 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ βˆƒπ‘ ∈ TopBases (𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘)))
203202ex 413 . . . . 5 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) β†’ βˆƒπ‘ ∈ TopBases (𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘))))
20459, 203sylbid 239 . . . 4 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ ((𝑓:π‘†βŸΆ( I β€˜π΅) ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) β†’ βˆƒπ‘ ∈ TopBases (𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘))))
205204exlimdv 1936 . . 3 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ (βˆƒπ‘“(𝑓:π‘†βŸΆ( I β€˜π΅) ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) β†’ βˆƒπ‘ ∈ TopBases (𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘))))
20656, 205mpd 15 . 2 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ βˆƒπ‘ ∈ TopBases (𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘)))
2073, 206rexlimddv 3161 1 ((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) β†’ βˆƒπ‘ ∈ TopBases (𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3474   βŠ† wss 3948  βŸ¨cop 4634   class class class wbr 5148  {copab 5210   I cid 5573   Γ— cxp 5674  dom cdm 5676  ran crn 5677  Rel wrel 5681  Oncon0 6364   Fn wfn 6538  βŸΆwf 6539  β€“ontoβ†’wfo 6541  β€˜cfv 6543  Ο‰com 7857  1st c1st 7975  2nd c2nd 7976   β‰ˆ cen 8938   β‰Ό cdom 8939  cardccrd 9932  topGenctg 17385  Topctop 22402  TopBasesctb 22455  2ndΟ‰c2ndc 22949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cc 10432
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-oi 9507  df-card 9936  df-acn 9939  df-topgen 17391  df-top 22403  df-bases 22456  df-2ndc 22951
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator