MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgcmp Structured version   Visualization version   GIF version
Theorem tgcmp 22896
Description: A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 23540, 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 2732 . . . . 5 βˆͺ (topGenβ€˜π΅) = βˆͺ (topGenβ€˜π΅)
21iscmp 22883 . . . 4 ((topGenβ€˜π΅) ∈ Comp ↔ ((topGenβ€˜π΅) ∈ Top ∧ βˆ€π‘¦ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧)))
32simprbi 497 . . 3 ((topGenβ€˜π΅) ∈ Comp β†’ βˆ€π‘¦ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧))
4 unitg 22461 . . . . . . . 8 (𝐡 ∈ TopBases β†’ βˆͺ (topGenβ€˜π΅) = βˆͺ 𝐡)
5 eqtr3 2758 . . . . . . . 8 ((βˆͺ (topGenβ€˜π΅) = βˆͺ 𝐡 ∧ 𝑋 = βˆͺ 𝐡) β†’ βˆͺ (topGenβ€˜π΅) = 𝑋)
64, 5sylan 580 . . . . . . 7 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ βˆͺ (topGenβ€˜π΅) = 𝑋)
76eqeq1d 2734 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 ↔ 𝑋 = βˆͺ 𝑦))
86eqeq1d 2734 . . . . . . 7 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧 ↔ 𝑋 = βˆͺ 𝑧))
98rexbidv 3178 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧 ↔ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧))
107, 9imbi12d 344 . . . . 5 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ ((βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧) ↔ (𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧)))
1110ralbidv 3177 . . . 4 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧) ↔ βˆ€π‘¦ ∈ 𝒫 (topGenβ€˜π΅)(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧)))
12 bastg 22460 . . . . . . 7 (𝐡 ∈ TopBases β†’ 𝐡 βŠ† (topGenβ€˜π΅))
1312adantr 481 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ 𝐡 βŠ† (topGenβ€˜π΅))
1413sspwd 4614 . . . . 5 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ 𝒫 𝐡 βŠ† 𝒫 (topGenβ€˜π΅))
15 ssralv 4049 . . . . 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 4608 . . . . 5 (𝑒 ∈ 𝒫 (topGenβ€˜π΅) β†’ 𝑒 βŠ† (topGenβ€˜π΅))
20 simprr 771 . . . . . . . . . . 11 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ 𝑋 = βˆͺ 𝑒)
21 simprl 769 . . . . . . . . . . . . . . . . . 18 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ 𝑒 βŠ† (topGenβ€˜π΅))
2221sselda 3981 . . . . . . . . . . . . . . . . 17 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ 𝑑 ∈ 𝑒) β†’ 𝑑 ∈ (topGenβ€˜π΅))
2322adantrr 715 . . . . . . . . . . . . . . . 16 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑑 ∈ 𝑒 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑑 ∈ (topGenβ€˜π΅))
24 simprr 771 . . . . . . . . . . . . . . . 16 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑑 ∈ 𝑒 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ 𝑑)
25 tg2 22459 . . . . . . . . . . . . . . . 16 ((𝑑 ∈ (topGenβ€˜π΅) ∧ 𝑦 ∈ 𝑑) β†’ βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑))
2623, 24, 25syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑑 ∈ 𝑒 ∧ 𝑦 ∈ 𝑑)) β†’ βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑))
2726expr 457 . . . . . . . . . . . . . 14 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ 𝑑 ∈ 𝑒) β†’ (𝑦 ∈ 𝑑 β†’ βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑)))
2827reximdva 3168 . . . . . . . . . . . . 13 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (βˆƒπ‘‘ ∈ 𝑒 𝑦 ∈ 𝑑 β†’ βˆƒπ‘‘ ∈ 𝑒 βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑)))
29 eluni2 4911 . . . . . . . . . . . . 13 (𝑦 ∈ βˆͺ 𝑒 ↔ βˆƒπ‘‘ ∈ 𝑒 𝑦 ∈ 𝑑)
30 elunirab 4923 . . . . . . . . . . . . . 14 (𝑦 ∈ βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ↔ βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑))
31 r19.42v 3190 . . . . . . . . . . . . . . 15 (βˆƒπ‘‘ ∈ 𝑒 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑) ↔ (𝑦 ∈ 𝑀 ∧ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑))
3231rexbii 3094 . . . . . . . . . . . . . 14 (βˆƒπ‘€ ∈ 𝐡 βˆƒπ‘‘ ∈ 𝑒 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑) ↔ βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑))
33 rexcom 3287 . . . . . . . . . . . . . 14 (βˆƒπ‘€ ∈ 𝐡 βˆƒπ‘‘ ∈ 𝑒 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑) ↔ βˆƒπ‘‘ ∈ 𝑒 βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑))
3430, 32, 333bitr2i 298 . . . . . . . . . . . . 13 (𝑦 ∈ βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ↔ βˆƒπ‘‘ ∈ 𝑒 βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑))
3528, 29, 343imtr4g 295 . . . . . . . . . . . 12 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (𝑦 ∈ βˆͺ 𝑒 β†’ 𝑦 ∈ βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑}))
3635ssrdv 3987 . . . . . . . . . . 11 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ βˆͺ 𝑒 βŠ† βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
3720, 36eqsstrd 4019 . . . . . . . . . 10 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ 𝑋 βŠ† βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
38 ssrab2 4076 . . . . . . . . . . . 12 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} βŠ† 𝐡
3938unissi 4916 . . . . . . . . . . 11 βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} βŠ† βˆͺ 𝐡
40 simplr 767 . . . . . . . . . . 11 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ 𝑋 = βˆͺ 𝐡)
4139, 40sseqtrrid 4034 . . . . . . . . . 10 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} βŠ† 𝑋)
4237, 41eqssd 3998 . . . . . . . . 9 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ 𝑋 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
43 elpw2g 5343 . . . . . . . . . . . 12 (𝐡 ∈ TopBases β†’ ({𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∈ 𝒫 𝐡 ↔ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} βŠ† 𝐡))
4443ad2antrr 724 . . . . . . . . . . 11 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ ({𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∈ 𝒫 𝐡 ↔ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} βŠ† 𝐡))
4538, 44mpbiri 257 . . . . . . . . . 10 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∈ 𝒫 𝐡)
46 unieq 4918 . . . . . . . . . . . . 13 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ βˆͺ 𝑦 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
4746eqeq2d 2743 . . . . . . . . . . . 12 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ (𝑋 = βˆͺ 𝑦 ↔ 𝑋 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑}))
48 pweq 4615 . . . . . . . . . . . . . 14 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ 𝒫 𝑦 = 𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
4948ineq1d 4210 . . . . . . . . . . . . 13 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ (𝒫 𝑦 ∩ Fin) = (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin))
5049rexeqdv 3326 . . . . . . . . . . . 12 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ (βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧 ↔ βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧))
5147, 50imbi12d 344 . . . . . . . . . . 11 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ ((𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) ↔ (𝑋 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧)))
5251rspcv 3608 . . . . . . . . . 10 ({𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∈ 𝒫 𝐡 β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ (𝑋 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧)))
5345, 52syl 17 . . . . . . . . 9 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ (𝑋 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧)))
5442, 53mpid 44 . . . . . . . 8 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧))
55 elfpw 9350 . . . . . . . . . . . . 13 (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ↔ (𝑧 βŠ† {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∧ 𝑧 ∈ Fin))
5655simprbi 497 . . . . . . . . . . . 12 (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) β†’ 𝑧 ∈ Fin)
5756ad2antrl 726 . . . . . . . . . . 11 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) β†’ 𝑧 ∈ Fin)
5855simplbi 498 . . . . . . . . . . . . 13 (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) β†’ 𝑧 βŠ† {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
5958ad2antrl 726 . . . . . . . . . . . 12 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) β†’ 𝑧 βŠ† {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
60 ssrab 4069 . . . . . . . . . . . . 13 (𝑧 βŠ† {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ↔ (𝑧 βŠ† 𝐡 ∧ βˆ€π‘€ ∈ 𝑧 βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑))
6160simprbi 497 . . . . . . . . . . . 12 (𝑧 βŠ† {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ βˆ€π‘€ ∈ 𝑧 βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑)
6259, 61syl 17 . . . . . . . . . . 11 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) β†’ βˆ€π‘€ ∈ 𝑧 βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑)
63 sseq2 4007 . . . . . . . . . . . 12 (𝑑 = (π‘“β€˜π‘€) β†’ (𝑀 βŠ† 𝑑 ↔ 𝑀 βŠ† (π‘“β€˜π‘€)))
6463ac6sfi 9283 . . . . . . . . . . 11 ((𝑧 ∈ Fin ∧ βˆ€π‘€ ∈ 𝑧 βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑) β†’ βˆƒπ‘“(𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€)))
6557, 62, 64syl2anc 584 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) β†’ βˆƒπ‘“(𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€)))
66 frn 6721 . . . . . . . . . . . . 13 (𝑓:π‘§βŸΆπ‘’ β†’ ran 𝑓 βŠ† 𝑒)
6766ad2antrl 726 . . . . . . . . . . . 12 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ ran 𝑓 βŠ† 𝑒)
68 ffn 6714 . . . . . . . . . . . . . . 15 (𝑓:π‘§βŸΆπ‘’ β†’ 𝑓 Fn 𝑧)
69 dffn4 6808 . . . . . . . . . . . . . . 15 (𝑓 Fn 𝑧 ↔ 𝑓:𝑧–ontoβ†’ran 𝑓)
7068, 69sylib 217 . . . . . . . . . . . . . 14 (𝑓:π‘§βŸΆπ‘’ β†’ 𝑓:𝑧–ontoβ†’ran 𝑓)
7170adantr 481 . . . . . . . . . . . . 13 ((𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€)) β†’ 𝑓:𝑧–ontoβ†’ran 𝑓)
72 fofi 9334 . . . . . . . . . . . . 13 ((𝑧 ∈ Fin ∧ 𝑓:𝑧–ontoβ†’ran 𝑓) β†’ ran 𝑓 ∈ Fin)
7357, 71, 72syl2an 596 . . . . . . . . . . . 12 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ ran 𝑓 ∈ Fin)
74 elfpw 9350 . . . . . . . . . . . 12 (ran 𝑓 ∈ (𝒫 𝑒 ∩ Fin) ↔ (ran 𝑓 βŠ† 𝑒 ∧ ran 𝑓 ∈ Fin))
7567, 73, 74sylanbrc 583 . . . . . . . . . . 11 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ ran 𝑓 ∈ (𝒫 𝑒 ∩ Fin))
76 simplrr 776 . . . . . . . . . . . . 13 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ 𝑋 = βˆͺ 𝑧)
77 uniiun 5060 . . . . . . . . . . . . . . . 16 βˆͺ 𝑧 = βˆͺ 𝑀 ∈ 𝑧 𝑀
78 ss2iun 5014 . . . . . . . . . . . . . . . 16 (βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€) β†’ βˆͺ 𝑀 ∈ 𝑧 𝑀 βŠ† βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€))
7977, 78eqsstrid 4029 . . . . . . . . . . . . . . 15 (βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€) β†’ βˆͺ 𝑧 βŠ† βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€))
8079ad2antll 727 . . . . . . . . . . . . . 14 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆͺ 𝑧 βŠ† βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€))
81 fniunfv 7242 . . . . . . . . . . . . . . . 16 (𝑓 Fn 𝑧 β†’ βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€) = βˆͺ ran 𝑓)
8268, 81syl 17 . . . . . . . . . . . . . . 15 (𝑓:π‘§βŸΆπ‘’ β†’ βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€) = βˆͺ ran 𝑓)
8382ad2antrl 726 . . . . . . . . . . . . . 14 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€) = βˆͺ ran 𝑓)
8480, 83sseqtrd 4021 . . . . . . . . . . . . 13 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆͺ 𝑧 βŠ† βˆͺ ran 𝑓)
8576, 84eqsstrd 4019 . . . . . . . . . . . 12 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ 𝑋 βŠ† βˆͺ ran 𝑓)
8667unissd 4917 . . . . . . . . . . . . 13 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆͺ ran 𝑓 βŠ† βˆͺ 𝑒)
8720ad2antrr 724 . . . . . . . . . . . . 13 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ 𝑋 = βˆͺ 𝑒)
8886, 87sseqtrrd 4022 . . . . . . . . . . . 12 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆͺ ran 𝑓 βŠ† 𝑋)
8985, 88eqssd 3998 . . . . . . . . . . 11 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ 𝑋 = βˆͺ ran 𝑓)
90 unieq 4918 . . . . . . . . . . . 12 (𝑣 = ran 𝑓 β†’ βˆͺ 𝑣 = βˆͺ ran 𝑓)
9190rspceeqv 3632 . . . . . . . . . . 11 ((ran 𝑓 ∈ (𝒫 𝑒 ∩ Fin) ∧ 𝑋 = βˆͺ ran 𝑓) β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)
9275, 89, 91syl2anc 584 . . . . . . . . . 10 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)
9365, 92exlimddv 1938 . . . . . . . . 9 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)
9493rexlimdvaa 3156 . . . . . . . 8 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣))
9554, 94syld 47 . . . . . . 7 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣))
9695expr 457 . . . . . 6 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ 𝑒 βŠ† (topGenβ€˜π΅)) β†’ (𝑋 = βˆͺ 𝑒 β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
9796com23 86 . . . . 5 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ 𝑒 βŠ† (topGenβ€˜π΅)) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ (𝑋 = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
9819, 97sylan2 593 . . . 4 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ 𝑒 ∈ 𝒫 (topGenβ€˜π΅)) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ (𝑋 = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
9998ralrimdva 3154 . . 3 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ βˆ€π‘’ ∈ 𝒫 (topGenβ€˜π΅)(𝑋 = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
100 tgcl 22463 . . . . . 6 (𝐡 ∈ TopBases β†’ (topGenβ€˜π΅) ∈ Top)
101100adantr 481 . . . . 5 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (topGenβ€˜π΅) ∈ Top)
1021iscmp 22883 . . . . . 6 ((topGenβ€˜π΅) ∈ Comp ↔ ((topGenβ€˜π΅) ∈ Top ∧ βˆ€π‘’ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣)))
103102baib 536 . . . . 5 ((topGenβ€˜π΅) ∈ Top β†’ ((topGenβ€˜π΅) ∈ Comp ↔ βˆ€π‘’ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣)))
104101, 103syl 17 . . . 4 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ ((topGenβ€˜π΅) ∈ Comp ↔ βˆ€π‘’ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣)))
1056eqeq1d 2734 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑒 ↔ 𝑋 = βˆͺ 𝑒))
1066eqeq1d 2734 . . . . . . 7 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣 ↔ 𝑋 = βˆͺ 𝑣))
107106rexbidv 3178 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣 ↔ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣))
108105, 107imbi12d 344 . . . . 5 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ ((βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣) ↔ (𝑋 = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
109108ralbidv 3177 . . . 4 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆ€π‘’ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣) ↔ βˆ€π‘’ ∈ 𝒫 (topGenβ€˜π΅)(𝑋 = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
110104, 109bitrd 278 . . 3 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ ((topGenβ€˜π΅) ∈ Comp ↔ βˆ€π‘’ ∈ 𝒫 (topGenβ€˜π΅)(𝑋 = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
11199, 110sylibrd 258 . 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 396   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432   ∩ cin 3946   βŠ† wss 3947  π’« cpw 4601  βˆͺ cuni 4907  βˆͺ ciun 4996  ran crn 5676   Fn wfn 6535  βŸΆwf 6536  β€“ontoβ†’wfo 6538  β€˜cfv 6540  Fincfn 8935  topGenctg 17379  Topctop 22386  TopBasesctb 22439  Compccmp 22881
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-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
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-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-om 7852  df-1o 8462  df-er 8699  df-en 8936  df-dom 8937  df-fin 8939  df-topgen 17385  df-top 22387  df-bases 22440  df-cmp 22882
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator