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

Theorem tgcmp 21114
Description: A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 21759, 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 2621 . . . . 5 (topGen‘𝐵) = (topGen‘𝐵)
21iscmp 21101 . . . 4 ((topGen‘𝐵) ∈ Comp ↔ ((topGen‘𝐵) ∈ Top ∧ ∀𝑦 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧)))
32simprbi 480 . . 3 ((topGen‘𝐵) ∈ Comp → ∀𝑦 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧))
4 unitg 20682 . . . . . . . 8 (𝐵 ∈ TopBases → (topGen‘𝐵) = 𝐵)
5 eqtr3 2642 . . . . . . . 8 (( (topGen‘𝐵) = 𝐵𝑋 = 𝐵) → (topGen‘𝐵) = 𝑋)
64, 5sylan 488 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (topGen‘𝐵) = 𝑋)
76eqeq1d 2623 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ( (topGen‘𝐵) = 𝑦𝑋 = 𝑦))
86eqeq1d 2623 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ( (topGen‘𝐵) = 𝑧𝑋 = 𝑧))
98rexbidv 3045 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
107, 9imbi12d 334 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (( (topGen‘𝐵) = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧) ↔ (𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
1110ralbidv 2980 . . . 4 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧) ↔ ∀𝑦 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
12 bastg 20681 . . . . . . 7 (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵))
1312adantr 481 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → 𝐵 ⊆ (topGen‘𝐵))
14 sspwb 4878 . . . . . 6 (𝐵 ⊆ (topGen‘𝐵) ↔ 𝒫 𝐵 ⊆ 𝒫 (topGen‘𝐵))
1513, 14sylib 208 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → 𝒫 𝐵 ⊆ 𝒫 (topGen‘𝐵))
16 ssralv 3645 . . . . 5 (𝒫 𝐵 ⊆ 𝒫 (topGen‘𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
1715, 16syl 17 . . . 4 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
1811, 17sylbid 230 . . 3 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧) → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
193, 18syl5 34 . 2 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ((topGen‘𝐵) ∈ Comp → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
20 elpwi 4140 . . . . 5 (𝑢 ∈ 𝒫 (topGen‘𝐵) → 𝑢 ⊆ (topGen‘𝐵))
21 simprr 795 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑋 = 𝑢)
22 simprl 793 . . . . . . . . . . . . . . . . . 18 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑢 ⊆ (topGen‘𝐵))
2322sselda 3583 . . . . . . . . . . . . . . . . 17 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ 𝑡𝑢) → 𝑡 ∈ (topGen‘𝐵))
2423adantrr 752 . . . . . . . . . . . . . . . 16 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑡𝑢𝑦𝑡)) → 𝑡 ∈ (topGen‘𝐵))
25 simprr 795 . . . . . . . . . . . . . . . 16 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑡𝑢𝑦𝑡)) → 𝑦𝑡)
26 tg2 20680 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (topGen‘𝐵) ∧ 𝑦𝑡) → ∃𝑤𝐵 (𝑦𝑤𝑤𝑡))
2724, 25, 26syl2anc 692 . . . . . . . . . . . . . . 15 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑡𝑢𝑦𝑡)) → ∃𝑤𝐵 (𝑦𝑤𝑤𝑡))
2827expr 642 . . . . . . . . . . . . . 14 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ 𝑡𝑢) → (𝑦𝑡 → ∃𝑤𝐵 (𝑦𝑤𝑤𝑡)))
2928reximdva 3011 . . . . . . . . . . . . 13 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (∃𝑡𝑢 𝑦𝑡 → ∃𝑡𝑢𝑤𝐵 (𝑦𝑤𝑤𝑡)))
30 eluni2 4406 . . . . . . . . . . . . 13 (𝑦 𝑢 ↔ ∃𝑡𝑢 𝑦𝑡)
31 elunirab 4414 . . . . . . . . . . . . . 14 (𝑦 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ↔ ∃𝑤𝐵 (𝑦𝑤 ∧ ∃𝑡𝑢 𝑤𝑡))
32 r19.42v 3084 . . . . . . . . . . . . . . 15 (∃𝑡𝑢 (𝑦𝑤𝑤𝑡) ↔ (𝑦𝑤 ∧ ∃𝑡𝑢 𝑤𝑡))
3332rexbii 3034 . . . . . . . . . . . . . 14 (∃𝑤𝐵𝑡𝑢 (𝑦𝑤𝑤𝑡) ↔ ∃𝑤𝐵 (𝑦𝑤 ∧ ∃𝑡𝑢 𝑤𝑡))
34 rexcom 3091 . . . . . . . . . . . . . 14 (∃𝑤𝐵𝑡𝑢 (𝑦𝑤𝑤𝑡) ↔ ∃𝑡𝑢𝑤𝐵 (𝑦𝑤𝑤𝑡))
3531, 33, 343bitr2i 288 . . . . . . . . . . . . 13 (𝑦 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ↔ ∃𝑡𝑢𝑤𝐵 (𝑦𝑤𝑤𝑡))
3629, 30, 353imtr4g 285 . . . . . . . . . . . 12 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (𝑦 𝑢𝑦 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡}))
3736ssrdv 3589 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑢 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
3821, 37eqsstrd 3618 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑋 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
39 ssrab2 3666 . . . . . . . . . . . 12 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ⊆ 𝐵
4039unissi 4427 . . . . . . . . . . 11 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ⊆ 𝐵
41 simplr 791 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑋 = 𝐵)
4240, 41syl5sseqr 3633 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ⊆ 𝑋)
4338, 42eqssd 3600 . . . . . . . . 9 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑋 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
44 elpw2g 4787 . . . . . . . . . . . 12 (𝐵 ∈ TopBases → ({𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∈ 𝒫 𝐵 ↔ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ⊆ 𝐵))
4544ad2antrr 761 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → ({𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∈ 𝒫 𝐵 ↔ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ⊆ 𝐵))
4639, 45mpbiri 248 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∈ 𝒫 𝐵)
47 unieq 4410 . . . . . . . . . . . . 13 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → 𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
4847eqeq2d 2631 . . . . . . . . . . . 12 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → (𝑋 = 𝑦𝑋 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡}))
49 pweq 4133 . . . . . . . . . . . . . 14 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → 𝒫 𝑦 = 𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
5049ineq1d 3791 . . . . . . . . . . . . 13 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → (𝒫 𝑦 ∩ Fin) = (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin))
5150rexeqdv 3134 . . . . . . . . . . . 12 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧 ↔ ∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧))
5248, 51imbi12d 334 . . . . . . . . . . 11 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → ((𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) ↔ (𝑋 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → ∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧)))
5352rspcv 3291 . . . . . . . . . 10 ({𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∈ 𝒫 𝐵 → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → (𝑋 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → ∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧)))
5446, 53syl 17 . . . . . . . . 9 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → (𝑋 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → ∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧)))
5543, 54mpid 44 . . . . . . . 8 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧))
56 elfpw 8212 . . . . . . . . . . . . 13 (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ↔ (𝑧 ⊆ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∧ 𝑧 ∈ Fin))
5756simprbi 480 . . . . . . . . . . . 12 (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) → 𝑧 ∈ Fin)
5857ad2antrl 763 . . . . . . . . . . 11 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) → 𝑧 ∈ Fin)
5956simplbi 476 . . . . . . . . . . . . 13 (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) → 𝑧 ⊆ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
6059ad2antrl 763 . . . . . . . . . . . 12 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) → 𝑧 ⊆ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
61 ssrab 3659 . . . . . . . . . . . . 13 (𝑧 ⊆ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ↔ (𝑧𝐵 ∧ ∀𝑤𝑧𝑡𝑢 𝑤𝑡))
6261simprbi 480 . . . . . . . . . . . 12 (𝑧 ⊆ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → ∀𝑤𝑧𝑡𝑢 𝑤𝑡)
6360, 62syl 17 . . . . . . . . . . 11 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) → ∀𝑤𝑧𝑡𝑢 𝑤𝑡)
64 sseq2 3606 . . . . . . . . . . . 12 (𝑡 = (𝑓𝑤) → (𝑤𝑡𝑤 ⊆ (𝑓𝑤)))
6564ac6sfi 8148 . . . . . . . . . . 11 ((𝑧 ∈ Fin ∧ ∀𝑤𝑧𝑡𝑢 𝑤𝑡) → ∃𝑓(𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤)))
6658, 63, 65syl2anc 692 . . . . . . . . . 10 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) → ∃𝑓(𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤)))
67 frn 6010 . . . . . . . . . . . . 13 (𝑓:𝑧𝑢 → ran 𝑓𝑢)
6867ad2antrl 763 . . . . . . . . . . . 12 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ran 𝑓𝑢)
69 ffn 6002 . . . . . . . . . . . . . . 15 (𝑓:𝑧𝑢𝑓 Fn 𝑧)
70 dffn4 6078 . . . . . . . . . . . . . . 15 (𝑓 Fn 𝑧𝑓:𝑧onto→ran 𝑓)
7169, 70sylib 208 . . . . . . . . . . . . . 14 (𝑓:𝑧𝑢𝑓:𝑧onto→ran 𝑓)
7271adantr 481 . . . . . . . . . . . . 13 ((𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤)) → 𝑓:𝑧onto→ran 𝑓)
73 fofi 8196 . . . . . . . . . . . . 13 ((𝑧 ∈ Fin ∧ 𝑓:𝑧onto→ran 𝑓) → ran 𝑓 ∈ Fin)
7458, 72, 73syl2an 494 . . . . . . . . . . . 12 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ran 𝑓 ∈ Fin)
75 elfpw 8212 . . . . . . . . . . . 12 (ran 𝑓 ∈ (𝒫 𝑢 ∩ Fin) ↔ (ran 𝑓𝑢 ∧ ran 𝑓 ∈ Fin))
7668, 74, 75sylanbrc 697 . . . . . . . . . . 11 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ran 𝑓 ∈ (𝒫 𝑢 ∩ Fin))
77 simplrr 800 . . . . . . . . . . . . 13 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑋 = 𝑧)
78 uniiun 4539 . . . . . . . . . . . . . . . 16 𝑧 = 𝑤𝑧 𝑤
79 ss2iun 4502 . . . . . . . . . . . . . . . 16 (∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤) → 𝑤𝑧 𝑤 𝑤𝑧 (𝑓𝑤))
8078, 79syl5eqss 3628 . . . . . . . . . . . . . . 15 (∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤) → 𝑧 𝑤𝑧 (𝑓𝑤))
8180ad2antll 764 . . . . . . . . . . . . . 14 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑧 𝑤𝑧 (𝑓𝑤))
82 fniunfv 6459 . . . . . . . . . . . . . . . 16 (𝑓 Fn 𝑧 𝑤𝑧 (𝑓𝑤) = ran 𝑓)
8369, 82syl 17 . . . . . . . . . . . . . . 15 (𝑓:𝑧𝑢 𝑤𝑧 (𝑓𝑤) = ran 𝑓)
8483ad2antrl 763 . . . . . . . . . . . . . 14 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑤𝑧 (𝑓𝑤) = ran 𝑓)
8581, 84sseqtrd 3620 . . . . . . . . . . . . 13 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑧 ran 𝑓)
8677, 85eqsstrd 3618 . . . . . . . . . . . 12 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑋 ran 𝑓)
8768unissd 4428 . . . . . . . . . . . . 13 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ran 𝑓 𝑢)
8821ad2antrr 761 . . . . . . . . . . . . 13 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑋 = 𝑢)
8987, 88sseqtr4d 3621 . . . . . . . . . . . 12 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ran 𝑓𝑋)
9086, 89eqssd 3600 . . . . . . . . . . 11 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑋 = ran 𝑓)
91 unieq 4410 . . . . . . . . . . . . 13 (𝑣 = ran 𝑓 𝑣 = ran 𝑓)
9291eqeq2d 2631 . . . . . . . . . . . 12 (𝑣 = ran 𝑓 → (𝑋 = 𝑣𝑋 = ran 𝑓))
9392rspcev 3295 . . . . . . . . . . 11 ((ran 𝑓 ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ran 𝑓) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)
9476, 90, 93syl2anc 692 . . . . . . . . . 10 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)
9566, 94exlimddv 1860 . . . . . . . . 9 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)
9695rexlimdvaa 3025 . . . . . . . 8 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣))
9755, 96syld 47 . . . . . . 7 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣))
9897expr 642 . . . . . 6 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ 𝑢 ⊆ (topGen‘𝐵)) → (𝑋 = 𝑢 → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
9998com23 86 . . . . 5 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → (𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
10020, 99sylan2 491 . . . 4 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ 𝑢 ∈ 𝒫 (topGen‘𝐵)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → (𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
101100ralrimdva 2963 . . 3 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∀𝑢 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
102 tgcl 20684 . . . . . 6 (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)
103102adantr 481 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (topGen‘𝐵) ∈ Top)
1041iscmp 21101 . . . . . 6 ((topGen‘𝐵) ∈ Comp ↔ ((topGen‘𝐵) ∈ Top ∧ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣)))
105104baib 943 . . . . 5 ((topGen‘𝐵) ∈ Top → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣)))
106103, 105syl 17 . . . 4 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣)))
1076eqeq1d 2623 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ( (topGen‘𝐵) = 𝑢𝑋 = 𝑢))
1086eqeq1d 2623 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ( (topGen‘𝐵) = 𝑣𝑋 = 𝑣))
109108rexbidv 3045 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣))
110107, 109imbi12d 334 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (( (topGen‘𝐵) = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣) ↔ (𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
111110ralbidv 2980 . . . 4 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑢 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣) ↔ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
112106, 111bitrd 268 . . 3 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
113101, 112sylibrd 249 . 2 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → (topGen‘𝐵) ∈ Comp))
11419, 113impbid 202 1 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1987  wral 2907  wrex 2908  {crab 2911  cin 3554  wss 3555  𝒫 cpw 4130   cuni 4402   ciun 4485  ran crn 5075   Fn wfn 5842  wf 5843  ontowfo 5845  cfv 5847  Fincfn 7899  topGenctg 16019  Topctop 20617  TopBasesctb 20620  Compccmp 21099
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-om 7013  df-1o 7505  df-er 7687  df-en 7900  df-dom 7901  df-fin 7903  df-topgen 16025  df-top 20621  df-bases 20622  df-cmp 21100
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator