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

Theorem tgcmp 23432
Description: A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 24076, 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 2740 . . . . 5 (topGen‘𝐵) = (topGen‘𝐵)
21iscmp 23419 . . . 4 ((topGen‘𝐵) ∈ Comp ↔ ((topGen‘𝐵) ∈ Top ∧ ∀𝑦 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧)))
32simprbi 496 . . 3 ((topGen‘𝐵) ∈ Comp → ∀𝑦 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧))
4 unitg 22997 . . . . . . . 8 (𝐵 ∈ TopBases → (topGen‘𝐵) = 𝐵)
5 eqtr3 2766 . . . . . . . 8 (( (topGen‘𝐵) = 𝐵𝑋 = 𝐵) → (topGen‘𝐵) = 𝑋)
64, 5sylan 579 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (topGen‘𝐵) = 𝑋)
76eqeq1d 2742 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ( (topGen‘𝐵) = 𝑦𝑋 = 𝑦))
86eqeq1d 2742 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ( (topGen‘𝐵) = 𝑧𝑋 = 𝑧))
98rexbidv 3185 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧))
107, 9imbi12d 344 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (( (topGen‘𝐵) = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧) ↔ (𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
1110ralbidv 3184 . . . 4 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧) ↔ ∀𝑦 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
12 bastg 22996 . . . . . . 7 (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵))
1312adantr 480 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → 𝐵 ⊆ (topGen‘𝐵))
1413sspwd 4635 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → 𝒫 𝐵 ⊆ 𝒫 (topGen‘𝐵))
15 ssralv 4077 . . . . 5 (𝒫 𝐵 ⊆ 𝒫 (topGen‘𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
1614, 15syl 17 . . . 4 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
1711, 16sylbid 240 . . 3 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) (topGen‘𝐵) = 𝑧) → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
183, 17syl5 34 . 2 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ((topGen‘𝐵) ∈ Comp → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
19 elpwi 4629 . . . . 5 (𝑢 ∈ 𝒫 (topGen‘𝐵) → 𝑢 ⊆ (topGen‘𝐵))
20 simprr 772 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑋 = 𝑢)
21 simprl 770 . . . . . . . . . . . . . . . . . 18 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑢 ⊆ (topGen‘𝐵))
2221sselda 4008 . . . . . . . . . . . . . . . . 17 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ 𝑡𝑢) → 𝑡 ∈ (topGen‘𝐵))
2322adantrr 716 . . . . . . . . . . . . . . . 16 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑡𝑢𝑦𝑡)) → 𝑡 ∈ (topGen‘𝐵))
24 simprr 772 . . . . . . . . . . . . . . . 16 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑡𝑢𝑦𝑡)) → 𝑦𝑡)
25 tg2 22995 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ (topGen‘𝐵) ∧ 𝑦𝑡) → ∃𝑤𝐵 (𝑦𝑤𝑤𝑡))
2623, 24, 25syl2anc 583 . . . . . . . . . . . . . . 15 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑡𝑢𝑦𝑡)) → ∃𝑤𝐵 (𝑦𝑤𝑤𝑡))
2726expr 456 . . . . . . . . . . . . . 14 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ 𝑡𝑢) → (𝑦𝑡 → ∃𝑤𝐵 (𝑦𝑤𝑤𝑡)))
2827reximdva 3174 . . . . . . . . . . . . 13 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (∃𝑡𝑢 𝑦𝑡 → ∃𝑡𝑢𝑤𝐵 (𝑦𝑤𝑤𝑡)))
29 eluni2 4935 . . . . . . . . . . . . 13 (𝑦 𝑢 ↔ ∃𝑡𝑢 𝑦𝑡)
30 elunirab 4946 . . . . . . . . . . . . . 14 (𝑦 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ↔ ∃𝑤𝐵 (𝑦𝑤 ∧ ∃𝑡𝑢 𝑤𝑡))
31 r19.42v 3197 . . . . . . . . . . . . . . 15 (∃𝑡𝑢 (𝑦𝑤𝑤𝑡) ↔ (𝑦𝑤 ∧ ∃𝑡𝑢 𝑤𝑡))
3231rexbii 3100 . . . . . . . . . . . . . 14 (∃𝑤𝐵𝑡𝑢 (𝑦𝑤𝑤𝑡) ↔ ∃𝑤𝐵 (𝑦𝑤 ∧ ∃𝑡𝑢 𝑤𝑡))
33 rexcom 3296 . . . . . . . . . . . . . 14 (∃𝑤𝐵𝑡𝑢 (𝑦𝑤𝑤𝑡) ↔ ∃𝑡𝑢𝑤𝐵 (𝑦𝑤𝑤𝑡))
3430, 32, 333bitr2i 299 . . . . . . . . . . . . 13 (𝑦 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ↔ ∃𝑡𝑢𝑤𝐵 (𝑦𝑤𝑤𝑡))
3528, 29, 343imtr4g 296 . . . . . . . . . . . 12 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (𝑦 𝑢𝑦 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡}))
3635ssrdv 4014 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑢 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
3720, 36eqsstrd 4047 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑋 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
38 ssrab2 4103 . . . . . . . . . . . 12 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ⊆ 𝐵
3938unissi 4940 . . . . . . . . . . 11 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ⊆ 𝐵
40 simplr 768 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑋 = 𝐵)
4139, 40sseqtrrid 4062 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ⊆ 𝑋)
4237, 41eqssd 4026 . . . . . . . . 9 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → 𝑋 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
43 elpw2g 5351 . . . . . . . . . . . 12 (𝐵 ∈ TopBases → ({𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∈ 𝒫 𝐵 ↔ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ⊆ 𝐵))
4443ad2antrr 725 . . . . . . . . . . 11 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → ({𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∈ 𝒫 𝐵 ↔ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ⊆ 𝐵))
4538, 44mpbiri 258 . . . . . . . . . 10 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∈ 𝒫 𝐵)
46 unieq 4942 . . . . . . . . . . . . 13 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → 𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
4746eqeq2d 2751 . . . . . . . . . . . 12 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → (𝑋 = 𝑦𝑋 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡}))
48 pweq 4636 . . . . . . . . . . . . . 14 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → 𝒫 𝑦 = 𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
4948ineq1d 4240 . . . . . . . . . . . . 13 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → (𝒫 𝑦 ∩ Fin) = (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin))
5049rexeqdv 3335 . . . . . . . . . . . 12 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧 ↔ ∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧))
5147, 50imbi12d 344 . . . . . . . . . . 11 (𝑦 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → ((𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) ↔ (𝑋 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → ∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧)))
5251rspcv 3631 . . . . . . . . . 10 ({𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∈ 𝒫 𝐵 → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → (𝑋 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → ∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧)))
5345, 52syl 17 . . . . . . . . 9 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → (𝑋 = {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → ∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧)))
5442, 53mpid 44 . . . . . . . 8 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧))
55 elfpw 9426 . . . . . . . . . . . . 13 (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ↔ (𝑧 ⊆ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∧ 𝑧 ∈ Fin))
5655simprbi 496 . . . . . . . . . . . 12 (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) → 𝑧 ∈ Fin)
5756ad2antrl 727 . . . . . . . . . . 11 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) → 𝑧 ∈ Fin)
5855simplbi 497 . . . . . . . . . . . . 13 (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) → 𝑧 ⊆ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
5958ad2antrl 727 . . . . . . . . . . . 12 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) → 𝑧 ⊆ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡})
60 ssrab 4096 . . . . . . . . . . . . 13 (𝑧 ⊆ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ↔ (𝑧𝐵 ∧ ∀𝑤𝑧𝑡𝑢 𝑤𝑡))
6160simprbi 496 . . . . . . . . . . . 12 (𝑧 ⊆ {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} → ∀𝑤𝑧𝑡𝑢 𝑤𝑡)
6259, 61syl 17 . . . . . . . . . . 11 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) → ∀𝑤𝑧𝑡𝑢 𝑤𝑡)
63 sseq2 4035 . . . . . . . . . . . 12 (𝑡 = (𝑓𝑤) → (𝑤𝑡𝑤 ⊆ (𝑓𝑤)))
6463ac6sfi 9350 . . . . . . . . . . 11 ((𝑧 ∈ Fin ∧ ∀𝑤𝑧𝑡𝑢 𝑤𝑡) → ∃𝑓(𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤)))
6557, 62, 64syl2anc 583 . . . . . . . . . 10 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) → ∃𝑓(𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤)))
66 frn 6756 . . . . . . . . . . . . 13 (𝑓:𝑧𝑢 → ran 𝑓𝑢)
6766ad2antrl 727 . . . . . . . . . . . 12 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ran 𝑓𝑢)
68 ffn 6749 . . . . . . . . . . . . . . 15 (𝑓:𝑧𝑢𝑓 Fn 𝑧)
69 dffn4 6842 . . . . . . . . . . . . . . 15 (𝑓 Fn 𝑧𝑓:𝑧onto→ran 𝑓)
7068, 69sylib 218 . . . . . . . . . . . . . 14 (𝑓:𝑧𝑢𝑓:𝑧onto→ran 𝑓)
7170adantr 480 . . . . . . . . . . . . 13 ((𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤)) → 𝑓:𝑧onto→ran 𝑓)
72 fofi 9381 . . . . . . . . . . . . 13 ((𝑧 ∈ Fin ∧ 𝑓:𝑧onto→ran 𝑓) → ran 𝑓 ∈ Fin)
7357, 71, 72syl2an 595 . . . . . . . . . . . 12 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ran 𝑓 ∈ Fin)
74 elfpw 9426 . . . . . . . . . . . 12 (ran 𝑓 ∈ (𝒫 𝑢 ∩ Fin) ↔ (ran 𝑓𝑢 ∧ ran 𝑓 ∈ Fin))
7567, 73, 74sylanbrc 582 . . . . . . . . . . 11 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ran 𝑓 ∈ (𝒫 𝑢 ∩ Fin))
76 simplrr 777 . . . . . . . . . . . . 13 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑋 = 𝑧)
77 uniiun 5081 . . . . . . . . . . . . . . . 16 𝑧 = 𝑤𝑧 𝑤
78 ss2iun 5033 . . . . . . . . . . . . . . . 16 (∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤) → 𝑤𝑧 𝑤 𝑤𝑧 (𝑓𝑤))
7977, 78eqsstrid 4057 . . . . . . . . . . . . . . 15 (∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤) → 𝑧 𝑤𝑧 (𝑓𝑤))
8079ad2antll 728 . . . . . . . . . . . . . 14 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑧 𝑤𝑧 (𝑓𝑤))
81 fniunfv 7286 . . . . . . . . . . . . . . . 16 (𝑓 Fn 𝑧 𝑤𝑧 (𝑓𝑤) = ran 𝑓)
8268, 81syl 17 . . . . . . . . . . . . . . 15 (𝑓:𝑧𝑢 𝑤𝑧 (𝑓𝑤) = ran 𝑓)
8382ad2antrl 727 . . . . . . . . . . . . . 14 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑤𝑧 (𝑓𝑤) = ran 𝑓)
8480, 83sseqtrd 4049 . . . . . . . . . . . . 13 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑧 ran 𝑓)
8576, 84eqsstrd 4047 . . . . . . . . . . . 12 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑋 ran 𝑓)
8667unissd 4941 . . . . . . . . . . . . 13 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ran 𝑓 𝑢)
8720ad2antrr 725 . . . . . . . . . . . . 13 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑋 = 𝑢)
8886, 87sseqtrrd 4050 . . . . . . . . . . . 12 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ran 𝑓𝑋)
8985, 88eqssd 4026 . . . . . . . . . . 11 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → 𝑋 = ran 𝑓)
90 unieq 4942 . . . . . . . . . . . 12 (𝑣 = ran 𝑓 𝑣 = ran 𝑓)
9190rspceeqv 3658 . . . . . . . . . . 11 ((ran 𝑓 ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ran 𝑓) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)
9275, 89, 91syl2anc 583 . . . . . . . . . 10 (((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) ∧ (𝑓:𝑧𝑢 ∧ ∀𝑤𝑧 𝑤 ⊆ (𝑓𝑤))) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)
9365, 92exlimddv 1934 . . . . . . . . 9 ((((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin) ∧ 𝑋 = 𝑧)) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)
9493rexlimdvaa 3162 . . . . . . . 8 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (∃𝑧 ∈ (𝒫 {𝑤𝐵 ∣ ∃𝑡𝑢 𝑤𝑡} ∩ Fin)𝑋 = 𝑧 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣))
9554, 94syld 47 . . . . . . 7 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = 𝑢)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣))
9695expr 456 . . . . . 6 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ 𝑢 ⊆ (topGen‘𝐵)) → (𝑋 = 𝑢 → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
9796com23 86 . . . . 5 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → (𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
9819, 97sylan2 592 . . . 4 (((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) ∧ 𝑢 ∈ 𝒫 (topGen‘𝐵)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → (𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
9998ralrimdva 3160 . . 3 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧) → ∀𝑢 ∈ 𝒫 (topGen‘𝐵)(𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
100 tgcl 22999 . . . . . 6 (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)
101100adantr 480 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (topGen‘𝐵) ∈ Top)
1021iscmp 23419 . . . . . 6 ((topGen‘𝐵) ∈ Comp ↔ ((topGen‘𝐵) ∈ Top ∧ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣)))
103102baib 535 . . . . 5 ((topGen‘𝐵) ∈ Top → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣)))
104101, 103syl 17 . . . 4 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)( (topGen‘𝐵) = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣)))
1056eqeq1d 2742 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ( (topGen‘𝐵) = 𝑢𝑋 = 𝑢))
1066eqeq1d 2742 . . . . . . 7 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ( (topGen‘𝐵) = 𝑣𝑋 = 𝑣))
107106rexbidv 3185 . . . . . 6 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣))
108105, 107imbi12d 344 . . . . 5 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → (( (topGen‘𝐵) = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin) (topGen‘𝐵) = 𝑣) ↔ (𝑋 = 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = 𝑣)))
109108ralbidv 3184 . . . 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 212 1 ((𝐵 ∈ TopBases ∧ 𝑋 = 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑦 ∈ 𝒫 𝐵(𝑋 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = 𝑧)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wex 1777  wcel 2108  wral 3067  wrex 3076  {crab 3443  cin 3975  wss 3976  𝒫 cpw 4622   cuni 4931   ciun 5015  ran crn 5701   Fn wfn 6570  wf 6571  ontowfo 6573  cfv 6575  Fincfn 9005  topGenctg 17499  Topctop 22922  TopBasesctb 22975  Compccmp 23417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7772
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-ord 6400  df-on 6401  df-lim 6402  df-suc 6403  df-iota 6527  df-fun 6577  df-fn 6578  df-f 6579  df-f1 6580  df-fo 6581  df-f1o 6582  df-fv 6583  df-om 7906  df-1o 8524  df-en 9006  df-dom 9007  df-fin 9009  df-topgen 17505  df-top 22923  df-bases 22976  df-cmp 23418
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator