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

Theorem tgcmp 22768
Description: A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 23412, 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 2737 . . . . 5 βˆͺ (topGenβ€˜π΅) = βˆͺ (topGenβ€˜π΅)
21iscmp 22755 . . . 4 ((topGenβ€˜π΅) ∈ Comp ↔ ((topGenβ€˜π΅) ∈ Top ∧ βˆ€π‘¦ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧)))
32simprbi 498 . . 3 ((topGenβ€˜π΅) ∈ Comp β†’ βˆ€π‘¦ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧))
4 unitg 22333 . . . . . . . 8 (𝐡 ∈ TopBases β†’ βˆͺ (topGenβ€˜π΅) = βˆͺ 𝐡)
5 eqtr3 2763 . . . . . . . 8 ((βˆͺ (topGenβ€˜π΅) = βˆͺ 𝐡 ∧ 𝑋 = βˆͺ 𝐡) β†’ βˆͺ (topGenβ€˜π΅) = 𝑋)
64, 5sylan 581 . . . . . . 7 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ βˆͺ (topGenβ€˜π΅) = 𝑋)
76eqeq1d 2739 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 ↔ 𝑋 = βˆͺ 𝑦))
86eqeq1d 2739 . . . . . . 7 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧 ↔ 𝑋 = βˆͺ 𝑧))
98rexbidv 3176 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧 ↔ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧))
107, 9imbi12d 345 . . . . 5 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ ((βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧) ↔ (𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧)))
1110ralbidv 3175 . . . 4 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝒫 (topGenβ€˜π΅)(βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑧) ↔ βˆ€π‘¦ ∈ 𝒫 (topGenβ€˜π΅)(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧)))
12 bastg 22332 . . . . . . 7 (𝐡 ∈ TopBases β†’ 𝐡 βŠ† (topGenβ€˜π΅))
1312adantr 482 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ 𝐡 βŠ† (topGenβ€˜π΅))
1413sspwd 4578 . . . . 5 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ 𝒫 𝐡 βŠ† 𝒫 (topGenβ€˜π΅))
15 ssralv 4015 . . . . 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 4572 . . . . 5 (𝑒 ∈ 𝒫 (topGenβ€˜π΅) β†’ 𝑒 βŠ† (topGenβ€˜π΅))
20 simprr 772 . . . . . . . . . . 11 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ 𝑋 = βˆͺ 𝑒)
21 simprl 770 . . . . . . . . . . . . . . . . . 18 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ 𝑒 βŠ† (topGenβ€˜π΅))
2221sselda 3949 . . . . . . . . . . . . . . . . 17 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ 𝑑 ∈ 𝑒) β†’ 𝑑 ∈ (topGenβ€˜π΅))
2322adantrr 716 . . . . . . . . . . . . . . . 16 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑑 ∈ 𝑒 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑑 ∈ (topGenβ€˜π΅))
24 simprr 772 . . . . . . . . . . . . . . . 16 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑑 ∈ 𝑒 ∧ 𝑦 ∈ 𝑑)) β†’ 𝑦 ∈ 𝑑)
25 tg2 22331 . . . . . . . . . . . . . . . 16 ((𝑑 ∈ (topGenβ€˜π΅) ∧ 𝑦 ∈ 𝑑) β†’ βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑))
2623, 24, 25syl2anc 585 . . . . . . . . . . . . . . 15 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑑 ∈ 𝑒 ∧ 𝑦 ∈ 𝑑)) β†’ βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑))
2726expr 458 . . . . . . . . . . . . . 14 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ 𝑑 ∈ 𝑒) β†’ (𝑦 ∈ 𝑑 β†’ βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑)))
2827reximdva 3166 . . . . . . . . . . . . 13 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (βˆƒπ‘‘ ∈ 𝑒 𝑦 ∈ 𝑑 β†’ βˆƒπ‘‘ ∈ 𝑒 βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑)))
29 eluni2 4874 . . . . . . . . . . . . 13 (𝑦 ∈ βˆͺ 𝑒 ↔ βˆƒπ‘‘ ∈ 𝑒 𝑦 ∈ 𝑑)
30 elunirab 4886 . . . . . . . . . . . . . 14 (𝑦 ∈ βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ↔ βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑))
31 r19.42v 3188 . . . . . . . . . . . . . . 15 (βˆƒπ‘‘ ∈ 𝑒 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑) ↔ (𝑦 ∈ 𝑀 ∧ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑))
3231rexbii 3098 . . . . . . . . . . . . . 14 (βˆƒπ‘€ ∈ 𝐡 βˆƒπ‘‘ ∈ 𝑒 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑) ↔ βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑))
33 rexcom 3276 . . . . . . . . . . . . . 14 (βˆƒπ‘€ ∈ 𝐡 βˆƒπ‘‘ ∈ 𝑒 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑) ↔ βˆƒπ‘‘ ∈ 𝑒 βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑))
3430, 32, 333bitr2i 299 . . . . . . . . . . . . 13 (𝑦 ∈ βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ↔ βˆƒπ‘‘ ∈ 𝑒 βˆƒπ‘€ ∈ 𝐡 (𝑦 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑑))
3528, 29, 343imtr4g 296 . . . . . . . . . . . 12 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (𝑦 ∈ βˆͺ 𝑒 β†’ 𝑦 ∈ βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑}))
3635ssrdv 3955 . . . . . . . . . . 11 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ βˆͺ 𝑒 βŠ† βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
3720, 36eqsstrd 3987 . . . . . . . . . 10 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ 𝑋 βŠ† βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
38 ssrab2 4042 . . . . . . . . . . . 12 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} βŠ† 𝐡
3938unissi 4879 . . . . . . . . . . 11 βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} βŠ† βˆͺ 𝐡
40 simplr 768 . . . . . . . . . . 11 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ 𝑋 = βˆͺ 𝐡)
4139, 40sseqtrrid 4002 . . . . . . . . . 10 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} βŠ† 𝑋)
4237, 41eqssd 3966 . . . . . . . . 9 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ 𝑋 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
43 elpw2g 5306 . . . . . . . . . . . 12 (𝐡 ∈ TopBases β†’ ({𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∈ 𝒫 𝐡 ↔ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} βŠ† 𝐡))
4443ad2antrr 725 . . . . . . . . . . 11 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ ({𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∈ 𝒫 𝐡 ↔ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} βŠ† 𝐡))
4538, 44mpbiri 258 . . . . . . . . . 10 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∈ 𝒫 𝐡)
46 unieq 4881 . . . . . . . . . . . . 13 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ βˆͺ 𝑦 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
4746eqeq2d 2748 . . . . . . . . . . . 12 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ (𝑋 = βˆͺ 𝑦 ↔ 𝑋 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑}))
48 pweq 4579 . . . . . . . . . . . . . 14 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ 𝒫 𝑦 = 𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑})
4948ineq1d 4176 . . . . . . . . . . . . 13 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ (𝒫 𝑦 ∩ Fin) = (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin))
5049rexeqdv 3317 . . . . . . . . . . . 12 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ (βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧 ↔ βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧))
5147, 50imbi12d 345 . . . . . . . . . . 11 (𝑦 = {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ ((𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) ↔ (𝑋 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧)))
5251rspcv 3580 . . . . . . . . . 10 ({𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∈ 𝒫 𝐡 β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ (𝑋 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧)))
5345, 52syl 17 . . . . . . . . 9 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ (𝑋 = βˆͺ {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧)))
5442, 53mpid 44 . . . . . . . 8 (((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ βˆƒπ‘§ ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin)𝑋 = βˆͺ 𝑧))
55 elfpw 9305 . . . . . . . . . . . . 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 4035 . . . . . . . . . . . . 13 (𝑧 βŠ† {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ↔ (𝑧 βŠ† 𝐡 ∧ βˆ€π‘€ ∈ 𝑧 βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑))
6160simprbi 498 . . . . . . . . . . . 12 (𝑧 βŠ† {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} β†’ βˆ€π‘€ ∈ 𝑧 βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑)
6259, 61syl 17 . . . . . . . . . . 11 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) β†’ βˆ€π‘€ ∈ 𝑧 βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑)
63 sseq2 3975 . . . . . . . . . . . 12 (𝑑 = (π‘“β€˜π‘€) β†’ (𝑀 βŠ† 𝑑 ↔ 𝑀 βŠ† (π‘“β€˜π‘€)))
6463ac6sfi 9238 . . . . . . . . . . 11 ((𝑧 ∈ Fin ∧ βˆ€π‘€ ∈ 𝑧 βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑) β†’ βˆƒπ‘“(𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€)))
6557, 62, 64syl2anc 585 . . . . . . . . . 10 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) β†’ βˆƒπ‘“(𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€)))
66 frn 6680 . . . . . . . . . . . . 13 (𝑓:π‘§βŸΆπ‘’ β†’ ran 𝑓 βŠ† 𝑒)
6766ad2antrl 727 . . . . . . . . . . . 12 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ ran 𝑓 βŠ† 𝑒)
68 ffn 6673 . . . . . . . . . . . . . . 15 (𝑓:π‘§βŸΆπ‘’ β†’ 𝑓 Fn 𝑧)
69 dffn4 6767 . . . . . . . . . . . . . . 15 (𝑓 Fn 𝑧 ↔ 𝑓:𝑧–ontoβ†’ran 𝑓)
7068, 69sylib 217 . . . . . . . . . . . . . 14 (𝑓:π‘§βŸΆπ‘’ β†’ 𝑓:𝑧–ontoβ†’ran 𝑓)
7170adantr 482 . . . . . . . . . . . . 13 ((𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€)) β†’ 𝑓:𝑧–ontoβ†’ran 𝑓)
72 fofi 9289 . . . . . . . . . . . . 13 ((𝑧 ∈ Fin ∧ 𝑓:𝑧–ontoβ†’ran 𝑓) β†’ ran 𝑓 ∈ Fin)
7357, 71, 72syl2an 597 . . . . . . . . . . . 12 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ ran 𝑓 ∈ Fin)
74 elfpw 9305 . . . . . . . . . . . 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 5023 . . . . . . . . . . . . . . . 16 βˆͺ 𝑧 = βˆͺ 𝑀 ∈ 𝑧 𝑀
78 ss2iun 4977 . . . . . . . . . . . . . . . 16 (βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€) β†’ βˆͺ 𝑀 ∈ 𝑧 𝑀 βŠ† βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€))
7977, 78eqsstrid 3997 . . . . . . . . . . . . . . 15 (βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€) β†’ βˆͺ 𝑧 βŠ† βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€))
8079ad2antll 728 . . . . . . . . . . . . . 14 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆͺ 𝑧 βŠ† βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€))
81 fniunfv 7199 . . . . . . . . . . . . . . . 16 (𝑓 Fn 𝑧 β†’ βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€) = βˆͺ ran 𝑓)
8268, 81syl 17 . . . . . . . . . . . . . . 15 (𝑓:π‘§βŸΆπ‘’ β†’ βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€) = βˆͺ ran 𝑓)
8382ad2antrl 727 . . . . . . . . . . . . . 14 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆͺ 𝑀 ∈ 𝑧 (π‘“β€˜π‘€) = βˆͺ ran 𝑓)
8480, 83sseqtrd 3989 . . . . . . . . . . . . 13 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆͺ 𝑧 βŠ† βˆͺ ran 𝑓)
8576, 84eqsstrd 3987 . . . . . . . . . . . 12 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ 𝑋 βŠ† βˆͺ ran 𝑓)
8667unissd 4880 . . . . . . . . . . . . 13 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆͺ ran 𝑓 βŠ† βˆͺ 𝑒)
8720ad2antrr 725 . . . . . . . . . . . . 13 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ 𝑋 = βˆͺ 𝑒)
8886, 87sseqtrrd 3990 . . . . . . . . . . . 12 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆͺ ran 𝑓 βŠ† 𝑋)
8985, 88eqssd 3966 . . . . . . . . . . 11 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ 𝑋 = βˆͺ ran 𝑓)
90 unieq 4881 . . . . . . . . . . . 12 (𝑣 = ran 𝑓 β†’ βˆͺ 𝑣 = βˆͺ ran 𝑓)
9190rspceeqv 3600 . . . . . . . . . . 11 ((ran 𝑓 ∈ (𝒫 𝑒 ∩ Fin) ∧ 𝑋 = βˆͺ ran 𝑓) β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)
9275, 89, 91syl2anc 585 . . . . . . . . . 10 (((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) ∧ (𝑓:π‘§βŸΆπ‘’ ∧ βˆ€π‘€ ∈ 𝑧 𝑀 βŠ† (π‘“β€˜π‘€))) β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)
9365, 92exlimddv 1939 . . . . . . . . 9 ((((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑋 = βˆͺ 𝑒)) ∧ (𝑧 ∈ (𝒫 {𝑀 ∈ 𝐡 ∣ βˆƒπ‘‘ ∈ 𝑒 𝑀 βŠ† 𝑑} ∩ Fin) ∧ 𝑋 = βˆͺ 𝑧)) β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)
9493rexlimdvaa 3154 . . . . . . . 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 3152 . . 3 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆ€π‘¦ ∈ 𝒫 𝐡(𝑋 = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ (𝒫 𝑦 ∩ Fin)𝑋 = βˆͺ 𝑧) β†’ βˆ€π‘’ ∈ 𝒫 (topGenβ€˜π΅)(𝑋 = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
100 tgcl 22335 . . . . . 6 (𝐡 ∈ TopBases β†’ (topGenβ€˜π΅) ∈ Top)
101100adantr 482 . . . . 5 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (topGenβ€˜π΅) ∈ Top)
1021iscmp 22755 . . . . . 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 2739 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑒 ↔ 𝑋 = βˆͺ 𝑒))
1066eqeq1d 2739 . . . . . . 7 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣 ↔ 𝑋 = βˆͺ 𝑣))
107106rexbidv 3176 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ (βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣 ↔ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣))
108105, 107imbi12d 345 . . . . 5 ((𝐡 ∈ TopBases ∧ 𝑋 = βˆͺ 𝐡) β†’ ((βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)βˆͺ (topGenβ€˜π΅) = βˆͺ 𝑣) ↔ (𝑋 = βˆͺ 𝑒 β†’ βˆƒπ‘£ ∈ (𝒫 𝑒 ∩ Fin)𝑋 = βˆͺ 𝑣)))
109108ralbidv 3175 . . . 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 3065  βˆƒwrex 3074  {crab 3410   ∩ cin 3914   βŠ† wss 3915  π’« cpw 4565  βˆͺ cuni 4870  βˆͺ ciun 4959  ran crn 5639   Fn wfn 6496  βŸΆwf 6497  β€“ontoβ†’wfo 6499  β€˜cfv 6501  Fincfn 8890  topGenctg 17326  Topctop 22258  TopBasesctb 22311  Compccmp 22753
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-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
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-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  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-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-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-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-om 7808  df-1o 8417  df-er 8655  df-en 8891  df-dom 8892  df-fin 8894  df-topgen 17332  df-top 22259  df-bases 22312  df-cmp 22754
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator