MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgcmp Structured version   Visualization version   GIF version
Theorem tgcmp 22905
Description: A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 23549, which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015.)
Assertion
Ref Expression
tgcmp ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ ((topGenβ€˜π΅) ∈ Comp ↔ βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧)))
Distinct variable groups:   𝑦,𝑧,𝐡   𝑦,𝑋,𝑧
Proof of Theorem tgcmp
Dummy variables 𝑑 𝑓 𝑒 𝑣 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2733 . . . . 5 βˆͺ (topGenβ€˜π΅) = βˆͺ (topGenβ€˜π΅)
21iscmp 22892 . . . 4 ((topGenβ€˜π΅) ∈ Comp ↔ ((topGenβ€˜π΅) ∈ Top ∧ βˆ€π‘¦ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧)))
32simprbi 498 . . 3 ((topGenβ€˜π΅) ∈ Comp β†’ βˆ€π‘¦ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧))
4 unitg 22470 . . . . . . . 8 (𝐡 ∈ TopBases β†’ βˆͺ (topGenβ€˜π΅) = βˆͺ 𝐡)
5 eqtr3 2759 . . . . . . . 8 ((βˆͺ (topGenβ€˜π΅) = βˆͺ 𝐡 ∧ 𝑋 = βˆͺ 𝐡) β†’ βˆͺ (topGenβ€˜π΅) = 𝑋)
64, 5sylan 581 . . . . . . 7 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ βˆͺ (topGenβ€˜π΅) = 𝑋)
76eqeq1d 2735 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 ↔ 𝑋 = βˆͺ 𝑦))
86eqeq1d 2735 . . . . . . 7 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧 ↔ 𝑋 = βˆͺ 𝑧))
98rexbidv 3179 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧 ↔ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧))
107, 9imbi12d 345 . . . . 5 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ ((βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧) ↔ (𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧)))
1110ralbidv 3178 . . . 4 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧) ↔ βˆ€π‘¦ ∈ 𝒫 (topGenβ€˜π΅)(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧)))
12 bastg 22469 . . . . . . 7 (𝐡 ∈ TopBases β†’ 𝐡 βŠ† (topGenβ€˜π΅))
1312adantr 482 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ 𝐡 βŠ† (topGenβ€˜π΅))
1413sspwd 4616 . . . . 5 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ 𝒫 𝐡 βŠ† 𝒫 (topGenβ€˜π΅))
15 ssralv 4051 . . . . 5 (𝒫 𝐡 βŠ† 𝒫 (topGenβ€˜π΅) β†’ (βˆ€π‘¦ ∈ 𝒫 (topGenβ€˜π΅)(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧)))
1614, 15syl 17 . . . 4 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝒫 (topGenβ€˜π΅)(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧)))
1711, 16sylbid 239 . . 3 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧) β†’ βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧)))
183, 17syl5 34 . 2 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ ((topGenβ€˜π΅) ∈ Comp β†’ βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧)))
19 elpwi 4610 . . . . 5 (𝑒 ∈ 𝒫 (topGenβ€˜π΅) β†’ 𝑒 βŠ† (topGenβ€˜π΅))
20 simprr 772 . . . . . . . . . . 11 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ 𝑋 = βˆͺ 𝑒)
21 simprl 770 . . . . . . . . . . . . . . . . . 18 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ 𝑒 βŠ† (topGenβ€˜π΅))
2221sselda 3983 . . . . . . . . . . . . . . . . 17 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ 𝑑 ∈ 𝑒) β†’ 𝑑 ∈ (topGenβ€˜π΅))
2322adantrr 716 . . . . . . . . . . . . . . . 16 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑑 ∈ 𝑒 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑑 ∈ (topGenβ€˜π΅))
24 simprr 772 . . . . . . . . . . . . . . . 16 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑑 ∈ 𝑒 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ 𝑑)
25 tg2 22468 . . . . . . . . . . . . . . . 16 ((𝑑 ∈ (topGenβ€˜π΅) ∧ 𝑦 ∈ 𝑑) β†’ βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑))
2623, 24, 25syl2anc 585 . . . . . . . . . . . . . . 15 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑑 ∈ 𝑒 ∧ 𝑦 ∈ 𝑑)) β†’ βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑))
2726expr 458 . . . . . . . . . . . . . 14 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ 𝑑 ∈ 𝑒) β†’ (𝑦 ∈ 𝑑 β†’ βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑)))
2827reximdva 3169 . . . . . . . . . . . . 13 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (βˆƒπ‘‘ ∈ 𝑒 𝑦 ∈ 𝑑 β†’ βˆƒπ‘‘ ∈ 𝑒 βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑)))
29 eluni2 4913 . . . . . . . . . . . . 13 (𝑦 ∈ βˆͺ 𝑒 ↔ βˆƒπ‘‘ ∈ 𝑒 𝑦 ∈ 𝑑)
30 elunirab 4925 . . . . . . . . . . . . . 14 (𝑦 ∈ βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ↔ βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑))
31 r19.42v 3191 . . . . . . . . . . . . . . 15 (βˆƒπ‘‘ ∈ 𝑒 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑) ↔ (𝑦 ∈ 𝑀 ∧ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑))
3231rexbii 3095 . . . . . . . . . . . . . 14 (βˆƒπ‘€ ∈ 𝐡 βˆƒπ‘‘ ∈ 𝑒 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑) ↔ βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑))
33 rexcom 3288 . . . . . . . . . . . . . 14 (βˆƒπ‘€ ∈ 𝐡 βˆƒπ‘‘ ∈ 𝑒 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑) ↔ βˆƒπ‘‘ ∈ 𝑒 βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑))
3430, 32, 333bitr2i 299 . . . . . . . . . . . . 13 (𝑦 ∈ βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ↔ βˆƒπ‘‘ ∈ 𝑒 βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑))
3528, 29, 343imtr4g 296 . . . . . . . . . . . 12 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (𝑦 ∈ βˆͺ 𝑒 β†’ 𝑦 ∈ βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑}))
3635ssrdv 3989 . . . . . . . . . . 11 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ βˆͺ 𝑒 βŠ† βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
3720, 36eqsstrd 4021 . . . . . . . . . 10 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ 𝑋 βŠ† βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
38 ssrab2 4078 . . . . . . . . . . . 12 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} βŠ† 𝐡
3938unissi 4918 . . . . . . . . . . 11 βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} βŠ† βˆͺ 𝐡
40 simplr 768 . . . . . . . . . . 11 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ 𝑋 = βˆͺ 𝐡)
4139, 40sseqtrrid 4036 . . . . . . . . . 10 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} βŠ† 𝑋)
4237, 41eqssd 4000 . . . . . . . . 9 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ 𝑋 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
43 elpw2g 5345 . . . . . . . . . . . 12 (𝐡 ∈ TopBases β†’ ({𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∈ 𝒫 𝐡 ↔ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} βŠ† 𝐡))
4443ad2antrr 725 . . . . . . . . . . 11 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ ({𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∈ 𝒫 𝐡 ↔ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} βŠ† 𝐡))
4538, 44mpbiri 258 . . . . . . . . . 10 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∈ 𝒫 𝐡)
46 unieq 4920 . . . . . . . . . . . . 13 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ βˆͺ 𝑦 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
4746eqeq2d 2744 . . . . . . . . . . . 12 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ (𝑋 = βˆͺ 𝑦 ↔ 𝑋 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑}))
48 pweq 4617 . . . . . . . . . . . . . 14 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ 𝒫 𝑦 = 𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
4948ineq1d 4212 . . . . . . . . . . . . 13 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ (𝒫 𝑦 ∩ Fin) = (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin))
5049rexeqdv 3327 . . . . . . . . . . . 12 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ (βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧 ↔ βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧))
5147, 50imbi12d 345 . . . . . . . . . . 11 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ ((𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) ↔ (𝑋 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧)))
5251rspcv 3609 . . . . . . . . . 10 ({𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∈ 𝒫 𝐡 β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ (𝑋 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧)))
5345, 52syl 17 . . . . . . . . 9 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ (𝑋 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧)))
5442, 53mpid 44 . . . . . . . 8 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧))
55 elfpw 9354 . . . . . . . . . . . . 13 (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ↔ (𝑧 βŠ† {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∧ 𝑧 ∈ Fin))
5655simprbi 498 . . . . . . . . . . . 12 (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) β†’ 𝑧 ∈ Fin)
5756ad2antrl 727 . . . . . . . . . . 11 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) β†’ 𝑧 ∈ Fin)
5855simplbi 499 . . . . . . . . . . . . 13 (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) β†’ 𝑧 βŠ† {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
5958ad2antrl 727 . . . . . . . . . . . 12 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) β†’ 𝑧 βŠ† {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
60 ssrab 4071 . . . . . . . . . . . . 13 (𝑧 βŠ† {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ↔ (𝑧 βŠ† 𝐡 ∧ βˆ€π‘€ ∈ 𝑧 βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑))
6160simprbi 498 . . . . . . . . . . . 12 (𝑧 βŠ† {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ βˆ€π‘€ ∈ 𝑧 βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑)
6259, 61syl 17 . . . . . . . . . . 11 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) β†’ βˆ€π‘€ ∈ 𝑧 βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑)
63 sseq2 4009 . . . . . . . . . . . 12 (𝑑 = (π‘“β€˜π‘€) β†’ (𝑀 βŠ† 𝑑 ↔ 𝑀 βŠ† (π‘“β€˜π‘€)))
6463ac6sfi 9287 . . . . . . . . . . 11 ((𝑧 ∈ Fin ∧ βˆ€π‘€ ∈ 𝑧 βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑) β†’ βˆƒπ‘“(𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€)))
6557, 62, 64syl2anc 585 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) β†’ βˆƒπ‘“(𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€)))
66 frn 6725 . . . . . . . . . . . . 13 (𝑓:π‘§βŸΆπ‘’ β†’ ran 𝑓 βŠ† 𝑒)
6766ad2antrl 727 . . . . . . . . . . . 12 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ ran 𝑓 βŠ† 𝑒)
68 ffn 6718 . . . . . . . . . . . . . . 15 (𝑓:π‘§βŸΆπ‘’ β†’ 𝑓 Fn 𝑧)
69 dffn4 6812 . . . . . . . . . . . . . . 15 (𝑓 Fn 𝑧 ↔ 𝑓:𝑧–ontoβ†’ran 𝑓)
7068, 69sylib 217 . . . . . . . . . . . . . 14 (𝑓:π‘§βŸΆπ‘’ β†’ 𝑓:𝑧–ontoβ†’ran 𝑓)
7170adantr 482 . . . . . . . . . . . . 13 ((𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€)) β†’ 𝑓:𝑧–ontoβ†’ran 𝑓)
72 fofi 9338 . . . . . . . . . . . . 13 ((𝑧 ∈ Fin ∧ 𝑓:𝑧–ontoβ†’ran 𝑓) β†’ ran 𝑓 ∈ Fin)
7357, 71, 72syl2an 597 . . . . . . . . . . . 12 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ ran 𝑓 ∈ Fin)
74 elfpw 9354 . . . . . . . . . . . 12 (ran 𝑓 ∈ (𝒫 𝑒 ∩ Fin) ↔ (ran 𝑓 βŠ† 𝑒 ∧ ran 𝑓 ∈ Fin))
7567, 73, 74sylanbrc 584 . . . . . . . . . . 11 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ ran 𝑓 ∈ (𝒫 𝑒 ∩ Fin))
76 simplrr 777 . . . . . . . . . . . . 13 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ 𝑋 = βˆͺ 𝑧)
77 uniiun 5062 . . . . . . . . . . . . . . . 16 βˆͺ 𝑧 = βˆͺ 𝑀 ∈ 𝑧 𝑀
78 ss2iun 5016 . . . . . . . . . . . . . . . 16 (βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€) β†’ βˆͺ 𝑀 ∈ 𝑧 𝑀 βŠ† βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€))
7977, 78eqsstrid 4031 . . . . . . . . . . . . . . 15 (βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€) β†’ βˆͺ 𝑧 βŠ† βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€))
8079ad2antll 728 . . . . . . . . . . . . . 14 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆͺ 𝑧 βŠ† βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€))
81 fniunfv 7246 . . . . . . . . . . . . . . . 16 (𝑓 Fn 𝑧 β†’ βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€) = βˆͺ ran 𝑓)
8268, 81syl 17 . . . . . . . . . . . . . . 15 (𝑓:π‘§βŸΆπ‘’ β†’ βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€) = βˆͺ ran 𝑓)
8382ad2antrl 727 . . . . . . . . . . . . . 14 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€) = βˆͺ ran 𝑓)
8480, 83sseqtrd 4023 . . . . . . . . . . . . 13 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆͺ 𝑧 βŠ† βˆͺ ran 𝑓)
8576, 84eqsstrd 4021 . . . . . . . . . . . 12 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ 𝑋 βŠ† βˆͺ ran 𝑓)
8667unissd 4919 . . . . . . . . . . . . 13 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆͺ ran 𝑓 βŠ† βˆͺ 𝑒)
8720ad2antrr 725 . . . . . . . . . . . . 13 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ 𝑋 = βˆͺ 𝑒)
8886, 87sseqtrrd 4024 . . . . . . . . . . . 12 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆͺ ran 𝑓 βŠ† 𝑋)
8985, 88eqssd 4000 . . . . . . . . . . 11 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ 𝑋 = βˆͺ ran 𝑓)
90 unieq 4920 . . . . . . . . . . . 12 (𝑣 = ran 𝑓 β†’ βˆͺ 𝑣 = βˆͺ ran 𝑓)
9190rspceeqv 3634 . . . . . . . . . . 11 ((ran 𝑓 ∈ (𝒫 𝑒 ∩ Fin) ∧ 𝑋 = βˆͺ ran 𝑓) β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)
9275, 89, 91syl2anc 585 . . . . . . . . . 10 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)
9365, 92exlimddv 1939 . . . . . . . . 9 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)
9493rexlimdvaa 3157 . . . . . . . 8 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣))
9554, 94syld 47 . . . . . . 7 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣))
9695expr 458 . . . . . 6 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ 𝑒 βŠ† (topGenβ€˜π΅)) β†’ (𝑋 = βˆͺ 𝑒 β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
9796com23 86 . . . . 5 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ 𝑒 βŠ† (topGenβ€˜π΅)) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ (𝑋 = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
9819, 97sylan2 594 . . . 4 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ 𝑒 ∈ 𝒫 (topGenβ€˜π΅)) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ (𝑋 = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
9998ralrimdva 3155 . . 3 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ βˆ€π‘’ ∈ 𝒫 (topGenβ€˜π΅)(𝑋 = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
100 tgcl 22472 . . . . . 6 (𝐡 ∈ TopBases β†’ (topGenβ€˜π΅) ∈ Top)
101100adantr 482 . . . . 5 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (topGenβ€˜π΅) ∈ Top)
1021iscmp 22892 . . . . . 6 ((topGenβ€˜π΅) ∈ Comp ↔ ((topGenβ€˜π΅) ∈ Top ∧ βˆ€π‘’ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣)))
103102baib 537 . . . . 5 ((topGenβ€˜π΅) ∈ Top β†’ ((topGenβ€˜π΅) ∈ Comp ↔ βˆ€π‘’ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣)))
104101, 103syl 17 . . . 4 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ ((topGenβ€˜π΅) ∈ Comp ↔ βˆ€π‘’ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣)))
1056eqeq1d 2735 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑒 ↔ 𝑋 = βˆͺ 𝑒))
1066eqeq1d 2735 . . . . . . 7 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣 ↔ 𝑋 = βˆͺ 𝑣))
107106rexbidv 3179 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣 ↔ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣))
108105, 107imbi12d 345 . . . . 5 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ ((βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣) ↔ (𝑋 = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
109108ralbidv 3178 . . . 4 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆ€π‘’ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣) ↔ βˆ€π‘’ ∈ 𝒫 (topGenβ€˜π΅)(𝑋 = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
110104, 109bitrd 279 . . 3 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ ((topGenβ€˜π΅) ∈ Comp ↔ βˆ€π‘’ ∈ 𝒫 (topGenβ€˜π΅)(𝑋 = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
11199, 110sylibrd 259 . 2 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ (topGenβ€˜π΅) ∈ Comp))
11218, 111impbid 211 1 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ ((topGenβ€˜π΅) ∈ Comp ↔ βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433   ∩ cin 3948   βŠ† wss 3949  π’« cpw 4603  βˆͺ cuni 4909  βˆͺ ciun 4998  ran crn 5678   Fn wfn 6539  βŸΆwf 6540  β€“ontoβ†’wfo 6542  β€˜cfv 6544  Fincfn 8939  topGenctg 17383  Topctop 22395  TopBasesctb 22448  Compccmp 22890
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-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
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-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  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-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-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-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-om 7856  df-1o 8466  df-er 8703  df-en 8940  df-dom 8941  df-fin 8943  df-topgen 17389  df-top 22396  df-bases 22449  df-cmp 22891
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator