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

Theorem 2ndcctbss 22822
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 22813 . . 3 (𝐽 ∈ 2ndΟ‰ ↔ βˆƒπ‘ ∈ TopBases (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))
31, 2sylib 217 . 2 ((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) β†’ βˆƒπ‘ ∈ TopBases (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))
4 vex 3452 . . . . . . 7 𝑐 ∈ V
54, 4xpex 7692 . . . . . 6 (𝑐 Γ— 𝑐) ∈ V
6 3simpa 1149 . . . . . . . 8 ((𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣)) β†’ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐))
76ssopab2i 5512 . . . . . . 7 {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣))} βŠ† {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)}
8 2ndcctbss.2 . . . . . . 7 𝑆 = {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣))}
9 df-xp 5644 . . . . . . 7 (𝑐 Γ— 𝑐) = {βŸ¨π‘’, π‘£βŸ© ∣ (𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)}
107, 8, 93sstr4i 3992 . . . . . 6 𝑆 βŠ† (𝑐 Γ— 𝑐)
11 ssdomg 8947 . . . . . 6 ((𝑐 Γ— 𝑐) ∈ V β†’ (𝑆 βŠ† (𝑐 Γ— 𝑐) β†’ 𝑆 β‰Ό (𝑐 Γ— 𝑐)))
125, 10, 11mp2 9 . . . . 5 𝑆 β‰Ό (𝑐 Γ— 𝑐)
134xpdom1 9022 . . . . . . . . 9 (𝑐 β‰Ό Ο‰ β†’ (𝑐 Γ— 𝑐) β‰Ό (Ο‰ Γ— 𝑐))
14 omex 9586 . . . . . . . . . 10 Ο‰ ∈ V
1514xpdom2 9018 . . . . . . . . 9 (𝑐 β‰Ό Ο‰ β†’ (Ο‰ Γ— 𝑐) β‰Ό (Ο‰ Γ— Ο‰))
16 domtr 8954 . . . . . . . . 9 (((𝑐 Γ— 𝑐) β‰Ό (Ο‰ Γ— 𝑐) ∧ (Ο‰ Γ— 𝑐) β‰Ό (Ο‰ Γ— Ο‰)) β†’ (𝑐 Γ— 𝑐) β‰Ό (Ο‰ Γ— Ο‰))
1713, 15, 16syl2anc 585 . . . . . . . 8 (𝑐 β‰Ό Ο‰ β†’ (𝑐 Γ— 𝑐) β‰Ό (Ο‰ Γ— Ο‰))
18 xpomen 9958 . . . . . . . 8 (Ο‰ Γ— Ο‰) β‰ˆ Ο‰
19 domentr 8960 . . . . . . . 8 (((𝑐 Γ— 𝑐) β‰Ό (Ο‰ Γ— Ο‰) ∧ (Ο‰ Γ— Ο‰) β‰ˆ Ο‰) β†’ (𝑐 Γ— 𝑐) β‰Ό Ο‰)
2017, 18, 19sylancl 587 . . . . . . 7 (𝑐 β‰Ό Ο‰ β†’ (𝑐 Γ— 𝑐) β‰Ό Ο‰)
2120adantr 482 . . . . . 6 ((𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽) β†’ (𝑐 Γ— 𝑐) β‰Ό Ο‰)
2221ad2antll 728 . . . . 5 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ (𝑐 Γ— 𝑐) β‰Ό Ο‰)
23 domtr 8954 . . . . 5 ((𝑆 β‰Ό (𝑐 Γ— 𝑐) ∧ (𝑐 Γ— 𝑐) β‰Ό Ο‰) β†’ 𝑆 β‰Ό Ο‰)
2412, 22, 23sylancr 588 . . . 4 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ 𝑆 β‰Ό Ο‰)
258relopabiv 5781 . . . . . . . . 9 Rel 𝑆
26 simpr 486 . . . . . . . . 9 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ π‘₯ ∈ 𝑆)
27 1st2nd 7976 . . . . . . . . 9 ((Rel 𝑆 ∧ π‘₯ ∈ 𝑆) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
2825, 26, 27sylancr 588 . . . . . . . 8 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ π‘₯ = ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩)
2928, 26eqeltrrd 2839 . . . . . . 7 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑆)
30 df-br 5111 . . . . . . . . 9 ((1st β€˜π‘₯)𝑆(2nd β€˜π‘₯) ↔ ⟨(1st β€˜π‘₯), (2nd β€˜π‘₯)⟩ ∈ 𝑆)
31 fvex 6860 . . . . . . . . . 10 (1st β€˜π‘₯) ∈ V
32 fvex 6860 . . . . . . . . . 10 (2nd β€˜π‘₯) ∈ V
33 simpl 484 . . . . . . . . . . . 12 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ 𝑒 = (1st β€˜π‘₯))
3433eleq1d 2823 . . . . . . . . . . 11 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ (𝑒 ∈ 𝑐 ↔ (1st β€˜π‘₯) ∈ 𝑐))
35 simpr 486 . . . . . . . . . . . 12 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ 𝑣 = (2nd β€˜π‘₯))
3635eleq1d 2823 . . . . . . . . . . 11 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ (𝑣 ∈ 𝑐 ↔ (2nd β€˜π‘₯) ∈ 𝑐))
37 sseq1 3974 . . . . . . . . . . . . 13 (𝑒 = (1st β€˜π‘₯) β†’ (𝑒 βŠ† 𝑀 ↔ (1st β€˜π‘₯) βŠ† 𝑀))
38 sseq2 3975 . . . . . . . . . . . . 13 (𝑣 = (2nd β€˜π‘₯) β†’ (𝑀 βŠ† 𝑣 ↔ 𝑀 βŠ† (2nd β€˜π‘₯)))
3937, 38bi2anan9 638 . . . . . . . . . . . 12 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ ((𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣) ↔ ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯))))
4039rexbidv 3176 . . . . . . . . . . 11 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ (βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣) ↔ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯))))
4134, 36, 403anbi123d 1437 . . . . . . . . . 10 ((𝑒 = (1st β€˜π‘₯) ∧ 𝑣 = (2nd β€˜π‘₯)) β†’ ((𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣)) ↔ ((1st β€˜π‘₯) ∈ 𝑐 ∧ (2nd β€˜π‘₯) ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)))))
4231, 32, 41, 8braba 5499 . . . . . . . . 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 6922 . . . . . . . 8 (𝐡 ∈ TopBases β†’ ( I β€˜π΅) = 𝐡)
4746ad3antrrr 729 . . . . . . 7 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ ( I β€˜π΅) = 𝐡)
4847rexeqdv 3317 . . . . . 6 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ (βˆƒπ‘€ ∈ ( I β€˜π΅)((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)) ↔ βˆƒπ‘€ ∈ 𝐡 ((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯))))
4945, 48mpbird 257 . . . . 5 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ π‘₯ ∈ 𝑆) β†’ βˆƒπ‘€ ∈ ( I β€˜π΅)((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)))
5049ralrimiva 3144 . . . 4 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ βˆ€π‘₯ ∈ 𝑆 βˆƒπ‘€ ∈ ( I β€˜π΅)((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)))
51 fvex 6860 . . . . 5 ( I β€˜π΅) ∈ V
52 sseq2 3975 . . . . . 6 (𝑀 = (π‘“β€˜π‘₯) β†’ ((1st β€˜π‘₯) βŠ† 𝑀 ↔ (1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯)))
53 sseq1 3974 . . . . . 6 (𝑀 = (π‘“β€˜π‘₯) β†’ (𝑀 βŠ† (2nd β€˜π‘₯) ↔ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))
5452, 53anbi12d 632 . . . . 5 (𝑀 = (π‘“β€˜π‘₯) β†’ (((1st β€˜π‘₯) βŠ† 𝑀 ∧ 𝑀 βŠ† (2nd β€˜π‘₯)) ↔ ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))))
5551, 54axcc4dom 10384 . . . 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 6660 . . . . . 6 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ (𝑓:π‘†βŸΆ( I β€˜π΅) ↔ 𝑓:π‘†βŸΆπ΅))
5958anbi1d 631 . . . . 5 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ ((𝑓:π‘†βŸΆ( I β€˜π΅) ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ↔ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))))
60 2ndctop 22814 . . . . . . . . . . . 12 (𝐽 ∈ 2ndΟ‰ β†’ 𝐽 ∈ Top)
6160adantl 483 . . . . . . . . . . 11 ((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) β†’ 𝐽 ∈ Top)
6261ad2antrr 725 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝐽 ∈ Top)
63 frn 6680 . . . . . . . . . . . 12 (𝑓:π‘†βŸΆπ΅ β†’ ran 𝑓 βŠ† 𝐡)
6463ad2antrl 727 . . . . . . . . . . 11 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ran 𝑓 βŠ† 𝐡)
65 bastg 22332 . . . . . . . . . . . . 13 (𝐡 ∈ TopBases β†’ 𝐡 βŠ† (topGenβ€˜π΅))
6665ad3antrrr 729 . . . . . . . . . . . 12 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝐡 βŠ† (topGenβ€˜π΅))
67 2ndcctbss.1 . . . . . . . . . . . 12 𝐽 = (topGenβ€˜π΅)
6866, 67sseqtrrdi 4000 . . . . . . . . . . 11 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝐡 βŠ† 𝐽)
6964, 68sstrd 3959 . . . . . . . . . 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 2841 . . . . . . . . . . . . . 14 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ π‘œ ∈ (topGenβ€˜π‘))
74 simprrr 781 . . . . . . . . . . . . . 14 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ 𝑑 ∈ π‘œ)
75 tg2 22331 . . . . . . . . . . . . . 14 ((π‘œ ∈ (topGenβ€˜π‘) ∧ 𝑑 ∈ π‘œ) β†’ βˆƒπ‘‘ ∈ 𝑐 (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))
7673, 74, 75syl2anc 585 . . . . . . . . . . . . 13 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ βˆƒπ‘‘ ∈ 𝑐 (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))
77 bastg 22332 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ TopBases β†’ 𝑐 βŠ† (topGenβ€˜π‘))
7877ad2antrl 727 . . . . . . . . . . . . . . . . . 18 (((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) β†’ 𝑐 βŠ† (topGenβ€˜π‘))
7978ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑐 βŠ† (topGenβ€˜π‘))
8067eqeq2i 2750 . . . . . . . . . . . . . . . . . . . . 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 3989 . . . . . . . . . . . . . . . 16 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑐 βŠ† (topGenβ€˜π΅))
86 simprl 770 . . . . . . . . . . . . . . . 16 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑑 ∈ 𝑐)
8785, 86sseldd 3950 . . . . . . . . . . . . . . 15 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑑 ∈ (topGenβ€˜π΅))
88 simprrl 780 . . . . . . . . . . . . . . 15 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ 𝑑 ∈ 𝑑)
89 tg2 22331 . . . . . . . . . . . . . . 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 2794 . . . . . . . . . . . . . . . . . 18 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ (topGenβ€˜π΅) = (topGenβ€˜π‘))
9592, 94sseqtrd 3989 . . . . . . . . . . . . . . . . 17 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ 𝐡 βŠ† (topGenβ€˜π‘))
96 simprl 770 . . . . . . . . . . . . . . . . 17 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ π‘š ∈ 𝐡)
9795, 96sseldd 3950 . . . . . . . . . . . . . . . 16 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ π‘š ∈ (topGenβ€˜π‘))
98 simprrl 780 . . . . . . . . . . . . . . . 16 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ 𝑑 ∈ π‘š)
99 tg2 22331 . . . . . . . . . . . . . . . 16 ((π‘š ∈ (topGenβ€˜π‘) ∧ 𝑑 ∈ π‘š) β†’ βˆƒπ‘› ∈ 𝑐 (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))
10097, 98, 99syl2anc 585 . . . . . . . . . . . . . . 15 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ βˆƒπ‘› ∈ 𝑐 (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))
101 ffn 6673 . . . . . . . . . . . . . . . . . . . 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 3975 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 = π‘š β†’ (𝑛 βŠ† 𝑀 ↔ 𝑛 βŠ† π‘š))
112 sseq1 3974 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 = π‘š β†’ (𝑀 βŠ† 𝑑 ↔ π‘š βŠ† 𝑑))
113111, 112anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑀 = π‘š β†’ ((𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑) ↔ (𝑛 βŠ† π‘š ∧ π‘š βŠ† 𝑑)))
114113rspcev 3584 . . . . . . . . . . . . . . . . . . 19 ((π‘š ∈ 𝐡 ∧ (𝑛 βŠ† π‘š ∧ π‘š βŠ† 𝑑)) β†’ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑))
115107, 108, 110, 114syl12anc 836 . . . . . . . . . . . . . . . . . 18 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑))
116 df-br 5111 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑆𝑑 ↔ βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆)
117 vex 3452 . . . . . . . . . . . . . . . . . . . 20 𝑛 ∈ V
118 vex 3452 . . . . . . . . . . . . . . . . . . . 20 𝑑 ∈ V
119 simpl 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ 𝑒 = 𝑛)
120119eleq1d 2823 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ (𝑒 ∈ 𝑐 ↔ 𝑛 ∈ 𝑐))
121 simpr 486 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ 𝑣 = 𝑑)
122121eleq1d 2823 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ (𝑣 ∈ 𝑐 ↔ 𝑑 ∈ 𝑐))
123 sseq1 3974 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = 𝑛 β†’ (𝑒 βŠ† 𝑀 ↔ 𝑛 βŠ† 𝑀))
124 sseq2 3975 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = 𝑑 β†’ (𝑀 βŠ† 𝑣 ↔ 𝑀 βŠ† 𝑑))
125123, 124bi2anan9 638 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ ((𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣) ↔ (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑)))
126125rexbidv 3176 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ (βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣) ↔ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑)))
127120, 122, 1263anbi123d 1437 . . . . . . . . . . . . . . . . . . . 20 ((𝑒 = 𝑛 ∧ 𝑣 = 𝑑) β†’ ((𝑒 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑒 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑣)) ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑))))
128117, 118, 127, 8braba 5499 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑆𝑑 ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑)))
129116, 128bitr3i 277 . . . . . . . . . . . . . . . . . 18 (βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆 ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ βˆƒπ‘€ ∈ 𝐡 (𝑛 βŠ† 𝑀 ∧ 𝑀 βŠ† 𝑑)))
130105, 106, 115, 129syl3anbrc 1344 . . . . . . . . . . . . . . . . 17 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆)
131 fnfvelrn 7036 . . . . . . . . . . . . . . . . 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 6847 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ (1st β€˜π‘₯) = (1st β€˜βŸ¨π‘›, π‘‘βŸ©))
141 fveq2 6847 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ (π‘“β€˜π‘₯) = (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©))
142140, 141sseq12d 3982 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ↔ (1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©)))
143 fveq2 6847 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ (2nd β€˜π‘₯) = (2nd β€˜βŸ¨π‘›, π‘‘βŸ©))
144141, 143sseq12d 3982 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ ((π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯) ↔ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©)))
145142, 144anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = βŸ¨π‘›, π‘‘βŸ© β†’ (((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)) ↔ ((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©))))
146145rspcv 3580 . . . . . . . . . . . . . . . . . . . . . 22 (βŸ¨π‘›, π‘‘βŸ© ∈ 𝑆 β†’ (βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)) β†’ ((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©))))
147139, 146syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ (βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)) β†’ ((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©))))
148117, 118op1st 7934 . . . . . . . . . . . . . . . . . . . . . . . 24 (1st β€˜βŸ¨π‘›, π‘‘βŸ©) = 𝑛
149148sseq1i 3977 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ↔ 𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©))
150117, 118op2nd 7935 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd β€˜βŸ¨π‘›, π‘‘βŸ©) = 𝑑
151150sseq2i 3978 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©) ↔ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)
152149, 151anbi12i 628 . . . . . . . . . . . . . . . . . . . . . 22 (((1st β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† (2nd β€˜βŸ¨π‘›, π‘‘βŸ©)) ↔ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑))
153 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ 𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©))
154 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š)) β†’ 𝑑 ∈ 𝑛)
155154ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ 𝑑 ∈ 𝑛)
156153, 155sseldd 3950 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ 𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©))
157 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)
158 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ 𝑑 βŠ† π‘œ)
159158ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ)) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) ∧ (𝑛 βŠ† (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† 𝑑)) β†’ 𝑑 βŠ† π‘œ)
160157, 159sstrd 3959 . . . . . . . . . . . . . . . . . . . . . . . 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 2827 . . . . . . . . . . . . . . . . . 18 (𝑏 = (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) β†’ (𝑑 ∈ 𝑏 ↔ 𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©)))
170 sseq1 3974 . . . . . . . . . . . . . . . . . 18 (𝑏 = (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) β†’ (𝑏 βŠ† π‘œ ↔ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ))
171169, 170anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑏 = (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) β†’ ((𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ) ↔ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)))
172171rspcev 3584 . . . . . . . . . . . . . . . 16 (((π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∈ ran 𝑓 ∧ (𝑑 ∈ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) ∧ (π‘“β€˜βŸ¨π‘›, π‘‘βŸ©) βŠ† π‘œ)) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
173132, 168, 172syl2anc 585 . . . . . . . . . . . . . . 15 (((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑑 ∈ 𝑛 ∧ 𝑛 βŠ† π‘š))) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
174100, 173rexlimddv 3159 . . . . . . . . . . . . . 14 ((((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) ∧ (π‘š ∈ 𝐡 ∧ (𝑑 ∈ π‘š ∧ π‘š βŠ† 𝑑))) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
17590, 174rexlimddv 3159 . . . . . . . . . . . . 13 (((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑑 ∈ 𝑑 ∧ 𝑑 βŠ† π‘œ))) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
17676, 175rexlimddv 3159 . . . . . . . . . . . 12 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ ((𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯))) ∧ (π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ))) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
177176expr 458 . . . . . . . . . . 11 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ((π‘œ ∈ 𝐽 ∧ 𝑑 ∈ π‘œ) β†’ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ)))
178177ralrimivv 3196 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ βˆ€π‘œ ∈ 𝐽 βˆ€π‘‘ ∈ π‘œ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ))
179 basgen2 22355 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ ran 𝑓 βŠ† 𝐽 ∧ βˆ€π‘œ ∈ 𝐽 βˆ€π‘‘ ∈ π‘œ βˆƒπ‘ ∈ ran 𝑓(𝑑 ∈ 𝑏 ∧ 𝑏 βŠ† π‘œ)) β†’ (topGenβ€˜ran 𝑓) = 𝐽)
18062, 69, 178, 179syl3anc 1372 . . . . . . . . 9 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ (topGenβ€˜ran 𝑓) = 𝐽)
181180, 62eqeltrd 2838 . . . . . . . 8 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ (topGenβ€˜ran 𝑓) ∈ Top)
182 tgclb 22336 . . . . . . . 8 (ran 𝑓 ∈ TopBases ↔ (topGenβ€˜ran 𝑓) ∈ Top)
183181, 182sylibr 233 . . . . . . 7 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ran 𝑓 ∈ TopBases)
184 omelon 9589 . . . . . . . . . 10 Ο‰ ∈ On
18524adantr 482 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝑆 β‰Ό Ο‰)
186 ondomen 9980 . . . . . . . . . 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 6767 . . . . . . . . . 10 (𝑓 Fn 𝑆 ↔ 𝑓:𝑆–ontoβ†’ran 𝑓)
190188, 189sylib 217 . . . . . . . . 9 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝑓:𝑆–ontoβ†’ran 𝑓)
191 fodomnum 10000 . . . . . . . . 9 (𝑆 ∈ dom card β†’ (𝑓:𝑆–ontoβ†’ran 𝑓 β†’ ran 𝑓 β‰Ό 𝑆))
192187, 190, 191sylc 65 . . . . . . . 8 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ran 𝑓 β‰Ό 𝑆)
193 domtr 8954 . . . . . . . 8 ((ran 𝑓 β‰Ό 𝑆 ∧ 𝑆 β‰Ό Ο‰) β†’ ran 𝑓 β‰Ό Ο‰)
194192, 185, 193syl2anc 585 . . . . . . 7 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ ran 𝑓 β‰Ό Ο‰)
195180eqcomd 2743 . . . . . . 7 ((((𝐡 ∈ TopBases ∧ 𝐽 ∈ 2ndΟ‰) ∧ (𝑐 ∈ TopBases ∧ (𝑐 β‰Ό Ο‰ ∧ (topGenβ€˜π‘) = 𝐽))) ∧ (𝑓:π‘†βŸΆπ΅ ∧ βˆ€π‘₯ ∈ 𝑆 ((1st β€˜π‘₯) βŠ† (π‘“β€˜π‘₯) ∧ (π‘“β€˜π‘₯) βŠ† (2nd β€˜π‘₯)))) β†’ 𝐽 = (topGenβ€˜ran 𝑓))
196 breq1 5113 . . . . . . . . 9 (𝑏 = ran 𝑓 β†’ (𝑏 β‰Ό Ο‰ ↔ ran 𝑓 β‰Ό Ο‰))
197 sseq1 3974 . . . . . . . . 9 (𝑏 = ran 𝑓 β†’ (𝑏 βŠ† 𝐡 ↔ ran 𝑓 βŠ† 𝐡))
198 fveq2 6847 . . . . . . . . . 10 (𝑏 = ran 𝑓 β†’ (topGenβ€˜π‘) = (topGenβ€˜ran 𝑓))
199198eqeq2d 2748 . . . . . . . . 9 (𝑏 = ran 𝑓 β†’ (𝐽 = (topGenβ€˜π‘) ↔ 𝐽 = (topGenβ€˜ran 𝑓)))
200196, 197, 1993anbi123d 1437 . . . . . . . 8 (𝑏 = ran 𝑓 β†’ ((𝑏 β‰Ό Ο‰ ∧ 𝑏 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜π‘)) ↔ (ran 𝑓 β‰Ό Ο‰ ∧ ran 𝑓 βŠ† 𝐡 ∧ 𝐽 = (topGenβ€˜ran 𝑓))))
201200rspcev 3584 . . . . . . 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 3159 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 3065  βˆƒwrex 3074  Vcvv 3448   βŠ† wss 3915  βŸ¨cop 4597   class class class wbr 5110  {copab 5172   I cid 5535   Γ— cxp 5636  dom cdm 5638  ran crn 5639  Rel wrel 5643  Oncon0 6322   Fn wfn 6496  βŸΆwf 6497  β€“ontoβ†’wfo 6499  β€˜cfv 6501  Ο‰com 7807  1st c1st 7924  2nd c2nd 7925   β‰ˆ cen 8887   β‰Ό cdom 8888  cardccrd 9878  topGenctg 17326  Topctop 22258  TopBasesctb 22311  2ndΟ‰c2ndc 22805
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cc 10378
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-oi 9453  df-card 9882  df-acn 9885  df-topgen 17332  df-top 22259  df-bases 22312  df-2ndc 22807
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator