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

Theorem tgcmp 22145
Description: A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 22789, 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 2738 . . . . 5 (topGen‘𝐵) = (topGen‘𝐵)
21iscmp 22132 . . . 4 ((topGen‘𝐵) ∈ Comp ↔ ((topGen‘𝐵) ∈ Top ∧ ∀𝑦 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧)))
32simprbi 500 . . 3 ((topGen‘𝐵) ∈ Comp → ∀𝑦 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧))
4 unitg 21711 . . . . . . . 8 (𝐵 ∈ TopBases → (topGen‘𝐵) = 𝐵)
5 eqtr3 2760 . . . . . . . 8 (( (topGen‘𝐵) = 𝐵𝑋 = 𝐵) → (topGen‘𝐵) = 𝑋)
64, 5sylan 583 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (topGen‘𝐵) = 𝑋)
76eqeq1d 2740 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ( (topGen‘𝐵) = 𝑦𝑋 = 𝑦))
86eqeq1d 2740 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ( (topGen‘𝐵) = 𝑧𝑋 = 𝑧))
98rexbidv 3206 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
107, 9imbi12d 348 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (( (topGen‘𝐵) = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧) ↔ (𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
1110ralbidv 3109 . . . 4 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧) ↔ ∀𝑦 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
12 bastg 21710 . . . . . . 7 (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵))
1312adantr 484 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → 𝐵 ⊆ (topGen‘𝐵))
1413sspwd 4500 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → 𝒫 𝐵 ⊆ 𝒫 (topGen‘𝐵))
15 ssralv 3941 . . . . 5 (𝒫 𝐵 ⊆ 𝒫 (topGen‘𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
1614, 15syl 17 . . . 4 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
1711, 16sylbid 243 . . 3 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧) → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
183, 17syl5 34 . 2 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ((topGen‘𝐵) ∈ Comp → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
19 elpwi 4494 . . . . 5 (𝑢 ∈ 𝒫 (topGen‘𝐵) → 𝑢 ⊆ (topGen‘𝐵))
20 simprr 773 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑋 = 𝑢)
21 simprl 771 . . . . . . . . . . . . . . . . . 18 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑢 ⊆ (topGen‘𝐵))
2221sselda 3875 . . . . . . . . . . . . . . . . 17 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ 𝑡𝑢) → 𝑡 ∈ (topGen‘𝐵))
2322adantrr 717 . . . . . . . . . . . . . . . 16 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑡𝑢𝑦𝑡)) → 𝑡 ∈ (topGen‘𝐵))
24 simprr 773 . . . . . . . . . . . . . . . 16 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑡𝑢𝑦𝑡)) → 𝑦𝑡)
25 tg2 21709 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (topGen‘𝐵) ∧ 𝑦𝑡) → ∃𝑤𝐵 (𝑦𝑤𝑤𝑡))
2623, 24, 25syl2anc 587 . . . . . . . . . . . . . . 15 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑡𝑢𝑦𝑡)) → ∃𝑤𝐵 (𝑦𝑤𝑤𝑡))
2726expr 460 . . . . . . . . . . . . . 14 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ 𝑡𝑢) → (𝑦𝑡 → ∃𝑤𝐵 (𝑦𝑤𝑤𝑡)))
2827reximdva 3183 . . . . . . . . . . . . 13 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (∃𝑡𝑢 𝑦𝑡 → ∃𝑡𝑢𝑤𝐵 (𝑦𝑤𝑤𝑡)))
29 eluni2 4797 . . . . . . . . . . . . 13 (𝑦 𝑢 ↔ ∃𝑡𝑢 𝑦𝑡)
30 elunirab 4809 . . . . . . . . . . . . . 14 (𝑦 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ↔ ∃𝑤𝐵 (𝑦𝑤 ∧ ∃𝑡𝑢 𝑤𝑡))
31 r19.42v 3253 . . . . . . . . . . . . . . 15 (∃𝑡𝑢 (𝑦𝑤𝑤𝑡) ↔ (𝑦𝑤 ∧ ∃𝑡𝑢 𝑤𝑡))
3231rexbii 3160 . . . . . . . . . . . . . 14 (∃𝑤𝐵𝑡𝑢 (𝑦𝑤𝑤𝑡) ↔ ∃𝑤𝐵 (𝑦𝑤 ∧ ∃𝑡𝑢 𝑤𝑡))
33 rexcom 3258 . . . . . . . . . . . . . 14 (∃𝑤𝐵𝑡𝑢 (𝑦𝑤𝑤𝑡) ↔ ∃𝑡𝑢𝑤𝐵 (𝑦𝑤𝑤𝑡))
3430, 32, 333bitr2i 302 . . . . . . . . . . . . 13 (𝑦 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ↔ ∃𝑡𝑢𝑤𝐵 (𝑦𝑤𝑤𝑡))
3528, 29, 343imtr4g 299 . . . . . . . . . . . 12 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (𝑦 𝑢𝑦 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡}))
3635ssrdv 3881 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑢 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
3720, 36eqsstrd 3913 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑋 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
38 ssrab2 3967 . . . . . . . . . . . 12 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ⊆ 𝐵
3938unissi 4802 . . . . . . . . . . 11 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ⊆ 𝐵
40 simplr 769 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑋 = 𝐵)
4139, 40sseqtrrid 3928 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ⊆ 𝑋)
4237, 41eqssd 3892 . . . . . . . . 9 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑋 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
43 elpw2g 5209 . . . . . . . . . . . 12 (𝐵 ∈ TopBases → ({𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∈ 𝒫 𝐵 ↔ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ⊆ 𝐵))
4443ad2antrr 726 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → ({𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∈ 𝒫 𝐵 ↔ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ⊆ 𝐵))
4538, 44mpbiri 261 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∈ 𝒫 𝐵)
46 unieq 4804 . . . . . . . . . . . . 13 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → 𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
4746eqeq2d 2749 . . . . . . . . . . . 12 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → (𝑋 = 𝑦𝑋 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡}))
48 pweq 4501 . . . . . . . . . . . . . 14 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → 𝒫 𝑦 = 𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
4948ineq1d 4100 . . . . . . . . . . . . 13 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → (𝒫 𝑦 ∩ Fin) = (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin))
5049rexeqdv 3316 . . . . . . . . . . . 12 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧 ↔ ∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧))
5147, 50imbi12d 348 . . . . . . . . . . 11 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → ((𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) ↔ (𝑋 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → ∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧)))
5251rspcv 3519 . . . . . . . . . 10 ({𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∈ 𝒫 𝐵 → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → (𝑋 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → ∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧)))
5345, 52syl 17 . . . . . . . . 9 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → (𝑋 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → ∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧)))
5442, 53mpid 44 . . . . . . . 8 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧))
55 elfpw 8892 . . . . . . . . . . . . 13 (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ↔ (𝑧 ⊆ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∧ 𝑧 ∈ Fin))
5655simprbi 500 . . . . . . . . . . . 12 (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) → 𝑧 ∈ Fin)
5756ad2antrl 728 . . . . . . . . . . 11 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) → 𝑧 ∈ Fin)
5855simplbi 501 . . . . . . . . . . . . 13 (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) → 𝑧 ⊆ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
5958ad2antrl 728 . . . . . . . . . . . 12 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) → 𝑧 ⊆ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
60 ssrab 3960 . . . . . . . . . . . . 13 (𝑧 ⊆ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ↔ (𝑧𝐵 ∧ ∀𝑤𝑧𝑡𝑢 𝑤𝑡))
6160simprbi 500 . . . . . . . . . . . 12 (𝑧 ⊆ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → ∀𝑤𝑧𝑡𝑢 𝑤𝑡)
6259, 61syl 17 . . . . . . . . . . 11 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) → ∀𝑤𝑧𝑡𝑢 𝑤𝑡)
63 sseq2 3901 . . . . . . . . . . . 12 (𝑡 = (𝑓𝑤) → (𝑤𝑡𝑤 ⊆ (𝑓𝑤)))
6463ac6sfi 8829 . . . . . . . . . . 11 ((𝑧 ∈ Fin ∧ ∀𝑤𝑧𝑡𝑢 𝑤𝑡) → ∃𝑓(𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤)))
6557, 62, 64syl2anc 587 . . . . . . . . . 10 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) → ∃𝑓(𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤)))
66 frn 6505 . . . . . . . . . . . . 13 (𝑓:𝑧𝑢 → ran 𝑓𝑢)
6766ad2antrl 728 . . . . . . . . . . . 12 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ran 𝑓𝑢)
68 ffn 6498 . . . . . . . . . . . . . . 15 (𝑓:𝑧𝑢𝑓 Fn 𝑧)
69 dffn4 6592 . . . . . . . . . . . . . . 15 (𝑓 Fn 𝑧𝑓:𝑧onto→ran 𝑓)
7068, 69sylib 221 . . . . . . . . . . . . . 14 (𝑓:𝑧𝑢𝑓:𝑧onto→ran 𝑓)
7170adantr 484 . . . . . . . . . . . . 13 ((𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤)) → 𝑓:𝑧onto→ran 𝑓)
72 fofi 8876 . . . . . . . . . . . . 13 ((𝑧 ∈ Fin ∧ 𝑓:𝑧onto→ran 𝑓) → ran 𝑓 ∈ Fin)
7357, 71, 72syl2an 599 . . . . . . . . . . . 12 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ran 𝑓 ∈ Fin)
74 elfpw 8892 . . . . . . . . . . . 12 (ran 𝑓 ∈ (𝒫 𝑢 ∩ Fin) ↔ (ran 𝑓𝑢 ∧ ran 𝑓 ∈ Fin))
7567, 73, 74sylanbrc 586 . . . . . . . . . . 11 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ran 𝑓 ∈ (𝒫 𝑢 ∩ Fin))
76 simplrr 778 . . . . . . . . . . . . 13 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑋 = 𝑧)
77 uniiun 4941 . . . . . . . . . . . . . . . 16 𝑧 = 𝑤𝑧 𝑤
78 ss2iun 4896 . . . . . . . . . . . . . . . 16 (∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤) → 𝑤𝑧 𝑤 𝑤𝑧 (𝑓𝑤))
7977, 78eqsstrid 3923 . . . . . . . . . . . . . . 15 (∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤) → 𝑧 𝑤𝑧 (𝑓𝑤))
8079ad2antll 729 . . . . . . . . . . . . . 14 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑧 𝑤𝑧 (𝑓𝑤))
81 fniunfv 7011 . . . . . . . . . . . . . . . 16 (𝑓 Fn 𝑧 𝑤𝑧 (𝑓𝑤) = ran 𝑓)
8268, 81syl 17 . . . . . . . . . . . . . . 15 (𝑓:𝑧𝑢 𝑤𝑧 (𝑓𝑤) = ran 𝑓)
8382ad2antrl 728 . . . . . . . . . . . . . 14 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑤𝑧 (𝑓𝑤) = ran 𝑓)
8480, 83sseqtrd 3915 . . . . . . . . . . . . 13 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑧 ran 𝑓)
8576, 84eqsstrd 3913 . . . . . . . . . . . 12 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑋 ran 𝑓)
8667unissd 4803 . . . . . . . . . . . . 13 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ran 𝑓 𝑢)
8720ad2antrr 726 . . . . . . . . . . . . 13 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑋 = 𝑢)
8886, 87sseqtrrd 3916 . . . . . . . . . . . 12 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ran 𝑓𝑋)
8985, 88eqssd 3892 . . . . . . . . . . 11 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑋 = ran 𝑓)
90 unieq 4804 . . . . . . . . . . . 12 (𝑣 = ran 𝑓 𝑣 = ran 𝑓)
9190rspceeqv 3539 . . . . . . . . . . 11 ((ran 𝑓 ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ran 𝑓) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)
9275, 89, 91syl2anc 587 . . . . . . . . . 10 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)
9365, 92exlimddv 1941 . . . . . . . . 9 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)
9493rexlimdvaa 3194 . . . . . . . 8 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣))
9554, 94syld 47 . . . . . . 7 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣))
9695expr 460 . . . . . 6 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ 𝑢 ⊆ (topGen‘𝐵)) → (𝑋 = 𝑢 → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
9796com23 86 . . . . 5 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → (𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
9819, 97sylan2 596 . . . 4 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ 𝑢 ∈ 𝒫 (topGen‘𝐵)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → (𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
9998ralrimdva 3101 . . 3 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∀𝑢 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
100 tgcl 21713 . . . . . 6 (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)
101100adantr 484 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (topGen‘𝐵) ∈ Top)
1021iscmp 22132 . . . . . 6 ((topGen‘𝐵) ∈ Comp ↔ ((topGen‘𝐵) ∈ Top ∧ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣)))
103102baib 539 . . . . 5 ((topGen‘𝐵) ∈ Top → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣)))
104101, 103syl 17 . . . 4 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣)))
1056eqeq1d 2740 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ( (topGen‘𝐵) = 𝑢𝑋 = 𝑢))
1066eqeq1d 2740 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ( (topGen‘𝐵) = 𝑣𝑋 = 𝑣))
107106rexbidv 3206 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣))
108105, 107imbi12d 348 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (( (topGen‘𝐵) = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣) ↔ (𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
109108ralbidv 3109 . . . 4 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑢 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣) ↔ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
110104, 109bitrd 282 . . 3 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
11199, 110sylibrd 262 . 2 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → (topGen‘𝐵) ∈ Comp))
11218, 111impbid 215 1 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1542  wex 1786  wcel 2113  wral 3053  wrex 3054  {crab 3057  cin 3840  wss 3841  𝒫 cpw 4485   cuni 4793   ciun 4878  ran crn 5520   Fn wfn 6328  wf 6329  ontowfo 6331  cfv 6333  Fincfn 8548  topGenctg 16807  Topctop 21637  TopBasesctb 21689  Compccmp 22130
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3399  df-sbc 3680  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-om 7594  df-1o 8124  df-er 8313  df-en 8549  df-dom 8550  df-fin 8552  df-topgen 16813  df-top 21638  df-bases 21690  df-cmp 22131
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator