Theorem tgcmp 23419

Description: A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 24063, 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.

Step	Hyp	Ref	Expression
1		eqid 2729	. . . . 5 ⊢ ∪ (topGen‘𝐵) = ∪ (topGen‘𝐵)
2	1	iscmp 23406	. . . 4 ⊢ ((topGen‘𝐵) ∈ Comp ↔ ((topGen‘𝐵) ∈ Top ∧ ∀𝑦 ∈ 𝒫 (topGen‘𝐵)(∪ (topGen‘𝐵) = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑧)))
3	2	simprbi 495	. . 3 ⊢ ((topGen‘𝐵) ∈ Comp → ∀𝑦 ∈ 𝒫 (topGen‘𝐵)(∪ (topGen‘𝐵) = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑧))
4		unitg 22984	. . . . . . . 8 ⊢ (𝐵 ∈ TopBases → ∪ (topGen‘𝐵) = ∪ 𝐵)
5		eqtr3 2755	. . . . . . . 8 ⊢ ((∪ (topGen‘𝐵) = ∪ 𝐵 ∧ 𝑋 = ∪ 𝐵) → ∪ (topGen‘𝐵) = 𝑋)
6	4, 5	sylan 578	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → ∪ (topGen‘𝐵) = 𝑋)
7	6	eqeq1d 2731	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → (∪ (topGen‘𝐵) = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑦))
8	6	eqeq1d 2731	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → (∪ (topGen‘𝐵) = ∪ 𝑧 ↔ 𝑋 = ∪ 𝑧))
9	8	rexbidv 3172	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
10	7, 9	imbi12d 343	. . . . 5 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → ((∪ (topGen‘𝐵) = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑧) ↔ (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
11	10	ralbidv 3171	. . . 4 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)(∪ (topGen‘𝐵) = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑧) ↔ ∀𝑦 ∈ 𝒫 (topGen‘𝐵)(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
12		bastg 22983	. . . . . . 7 ⊢ (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵))
13	12	adantr 479	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → 𝐵 ⊆ (topGen‘𝐵))
14	13	sspwd 4623	. . . . 5 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → 𝒫 𝐵 ⊆ 𝒫 (topGen‘𝐵))
15		ssralv 4060	. . . . 5 ⊢ (𝒫 𝐵 ⊆ 𝒫 (topGen‘𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
16	14, 15	syl 17	. . . 4 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
17	11, 16	sylbid 239	. . 3 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → (∀𝑦 ∈ 𝒫 (topGen‘𝐵)(∪ (topGen‘𝐵) = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑧) → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
18	3, 17	syl5 34	. 2 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → ((topGen‘𝐵) ∈ Comp → ∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
19		elpwi 4617	. . . . 5 ⊢ (𝑢 ∈ 𝒫 (topGen‘𝐵) → 𝑢 ⊆ (topGen‘𝐵))
20		simprr 771	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → 𝑋 = ∪ 𝑢)
21		simprl 769	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → 𝑢 ⊆ (topGen‘𝐵))
22	21	sselda 3991	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ 𝑡 ∈ 𝑢) → 𝑡 ∈ (topGen‘𝐵))
23	22	adantrr 715	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑦 ∈ 𝑡)) → 𝑡 ∈ (topGen‘𝐵))
24		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑦 ∈ 𝑡)) → 𝑦 ∈ 𝑡)
25		tg2 22982	. . . . . . . . . . . . . . . 16 ⊢ ((𝑡 ∈ (topGen‘𝐵) ∧ 𝑦 ∈ 𝑡) → ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡))
26	23, 24, 25	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑡 ∈ 𝑢 ∧ 𝑦 ∈ 𝑡)) → ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡))
27	26	expr 455	. . . . . . . . . . . . . 14 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ 𝑡 ∈ 𝑢) → (𝑦 ∈ 𝑡 → ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡)))
28	27	reximdva 3161	. . . . . . . . . . . . 13 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → (∃𝑡 ∈ 𝑢 𝑦 ∈ 𝑡 → ∃𝑡 ∈ 𝑢 ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡)))
29		eluni2 4922	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∪ 𝑢 ↔ ∃𝑡 ∈ 𝑢 𝑦 ∈ 𝑡)
30		elunirab 4933	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ↔ ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡))
31		r19.42v 3184	. . . . . . . . . . . . . . 15 ⊢ (∃𝑡 ∈ 𝑢 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡) ↔ (𝑦 ∈ 𝑤 ∧ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡))
32	31	rexbii 3087	. . . . . . . . . . . . . 14 ⊢ (∃𝑤 ∈ 𝐵 ∃𝑡 ∈ 𝑢 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡) ↔ ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡))
33		rexcom 3282	. . . . . . . . . . . . . 14 ⊢ (∃𝑤 ∈ 𝐵 ∃𝑡 ∈ 𝑢 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡) ↔ ∃𝑡 ∈ 𝑢 ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡))
34	30, 32, 33	3bitr2i 298	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ↔ ∃𝑡 ∈ 𝑢 ∃𝑤 ∈ 𝐵 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡))
35	28, 29, 34	3imtr4g 295	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → (𝑦 ∈ ∪ 𝑢 → 𝑦 ∈ ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡}))
36	35	ssrdv 3997	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → ∪ 𝑢 ⊆ ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡})
37	20, 36	eqsstrd 4030	. . . . . . . . . 10 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → 𝑋 ⊆ ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡})
38		ssrab2 4086	. . . . . . . . . . . 12 ⊢ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ⊆ 𝐵
39	38	unissi 4927	. . . . . . . . . . 11 ⊢ ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ⊆ ∪ 𝐵
40		simplr 767	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → 𝑋 = ∪ 𝐵)
41	39, 40	sseqtrrid 4045	. . . . . . . . . 10 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ⊆ 𝑋)
42	37, 41	eqssd 4009	. . . . . . . . 9 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → 𝑋 = ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡})
43		elpw2g 5341	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ TopBases → ({𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∈ 𝒫 𝐵 ↔ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ⊆ 𝐵))
44	43	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → ({𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∈ 𝒫 𝐵 ↔ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ⊆ 𝐵))
45	38, 44	mpbiri 257	. . . . . . . . . 10 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∈ 𝒫 𝐵)
46		unieq 4929	. . . . . . . . . . . . 13 ⊢ (𝑦 = {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → ∪ 𝑦 = ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡})
47	46	eqeq2d 2740	. . . . . . . . . . . 12 ⊢ (𝑦 = {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → (𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡}))
48		pweq 4624	. . . . . . . . . . . . . 14 ⊢ (𝑦 = {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → 𝒫 𝑦 = 𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡})
49	48	ineq1d 4222	. . . . . . . . . . . . 13 ⊢ (𝑦 = {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → (𝒫 𝑦 ∩ Fin) = (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin))
50	49	rexeqdv 3320	. . . . . . . . . . . 12 ⊢ (𝑦 = {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin)𝑋 = ∪ 𝑧))
51	47, 50	imbi12d 343	. . . . . . . . . . 11 ⊢ (𝑦 = {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → ((𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) ↔ (𝑋 = ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → ∃𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin)𝑋 = ∪ 𝑧)))
52	51	rspcv 3616	. . . . . . . . . 10 ⊢ ({𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∈ 𝒫 𝐵 → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → (𝑋 = ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → ∃𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin)𝑋 = ∪ 𝑧)))
53	45, 52	syl 17	. . . . . . . . 9 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → (𝑋 = ∪ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → ∃𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin)𝑋 = ∪ 𝑧)))
54	42, 53	mpid 44	. . . . . . . 8 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → ∃𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin)𝑋 = ∪ 𝑧))
55		elfpw 9405	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ↔ (𝑧 ⊆ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∧ 𝑧 ∈ Fin))
56	55	simprbi 495	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) → 𝑧 ∈ Fin)
57	56	ad2antrl 726	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) → 𝑧 ∈ Fin)
58	55	simplbi 496	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) → 𝑧 ⊆ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡})
59	58	ad2antrl 726	. . . . . . . . . . . 12 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) → 𝑧 ⊆ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡})
60		ssrab 4079	. . . . . . . . . . . . 13 ⊢ (𝑧 ⊆ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ↔ (𝑧 ⊆ 𝐵 ∧ ∀𝑤 ∈ 𝑧 ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡))
61	60	simprbi 495	. . . . . . . . . . . 12 ⊢ (𝑧 ⊆ {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} → ∀𝑤 ∈ 𝑧 ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡)
62	59, 61	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) → ∀𝑤 ∈ 𝑧 ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡)
63		sseq2 4018	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑓‘𝑤) → (𝑤 ⊆ 𝑡 ↔ 𝑤 ⊆ (𝑓‘𝑤)))
64	63	ac6sfi 9328	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ Fin ∧ ∀𝑤 ∈ 𝑧 ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡) → ∃𝑓(𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤)))
65	57, 62, 64	syl2anc 582	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) → ∃𝑓(𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤)))
66		frn 6739	. . . . . . . . . . . . 13 ⊢ (𝑓:𝑧⟶𝑢 → ran 𝑓 ⊆ 𝑢)
67	66	ad2antrl 726	. . . . . . . . . . . 12 ⊢ (((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ran 𝑓 ⊆ 𝑢)
68		ffn 6732	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝑧⟶𝑢 → 𝑓 Fn 𝑧)
69		dffn4 6825	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fn 𝑧 ↔ 𝑓:𝑧–onto→ran 𝑓)
70	68, 69	sylib 217	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝑧⟶𝑢 → 𝑓:𝑧–onto→ran 𝑓)
71	70	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤)) → 𝑓:𝑧–onto→ran 𝑓)
72		fofi 9360	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ Fin ∧ 𝑓:𝑧–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
73	57, 71, 72	syl2an 594	. . . . . . . . . . . 12 ⊢ (((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ran 𝑓 ∈ Fin)
74		elfpw 9405	. . . . . . . . . . . 12 ⊢ (ran 𝑓 ∈ (𝒫 𝑢 ∩ Fin) ↔ (ran 𝑓 ⊆ 𝑢 ∧ ran 𝑓 ∈ Fin))
75	67, 73, 74	sylanbrc 581	. . . . . . . . . . 11 ⊢ (((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ran 𝑓 ∈ (𝒫 𝑢 ∩ Fin))
76		simplrr 776	. . . . . . . . . . . . 13 ⊢ (((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → 𝑋 = ∪ 𝑧)
77		uniiun 5071	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑧 = ∪ 𝑤 ∈ 𝑧 𝑤
78		ss2iun 5024	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤) → ∪ 𝑤 ∈ 𝑧 𝑤 ⊆ ∪ 𝑤 ∈ 𝑧 (𝑓‘𝑤))
79	77, 78	eqsstrid 4040	. . . . . . . . . . . . . . 15 ⊢ (∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤) → ∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 (𝑓‘𝑤))
80	79	ad2antll 727	. . . . . . . . . . . . . 14 ⊢ (((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 (𝑓‘𝑤))
81		fniunfv 7267	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 Fn 𝑧 → ∪ 𝑤 ∈ 𝑧 (𝑓‘𝑤) = ∪ ran 𝑓)
82	68, 81	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝑧⟶𝑢 → ∪ 𝑤 ∈ 𝑧 (𝑓‘𝑤) = ∪ ran 𝑓)
83	82	ad2antrl 726	. . . . . . . . . . . . . 14 ⊢ (((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ∪ 𝑤 ∈ 𝑧 (𝑓‘𝑤) = ∪ ran 𝑓)
84	80, 83	sseqtrd 4032	. . . . . . . . . . . . 13 ⊢ (((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ∪ 𝑧 ⊆ ∪ ran 𝑓)
85	76, 84	eqsstrd 4030	. . . . . . . . . . . 12 ⊢ (((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → 𝑋 ⊆ ∪ ran 𝑓)
86	67	unissd 4928	. . . . . . . . . . . . 13 ⊢ (((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ∪ ran 𝑓 ⊆ ∪ 𝑢)
87	20	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → 𝑋 = ∪ 𝑢)
88	86, 87	sseqtrrd 4033	. . . . . . . . . . . 12 ⊢ (((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ∪ ran 𝑓 ⊆ 𝑋)
89	85, 88	eqssd 4009	. . . . . . . . . . 11 ⊢ (((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → 𝑋 = ∪ ran 𝑓)
90		unieq 4929	. . . . . . . . . . . 12 ⊢ (𝑣 = ran 𝑓 → ∪ 𝑣 = ∪ ran 𝑓)
91	90	rspceeqv 3642	. . . . . . . . . . 11 ⊢ ((ran 𝑓 ∈ (𝒫 𝑢 ∩ Fin) ∧ 𝑋 = ∪ ran 𝑓) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣)
92	75, 89, 91	syl2anc 582	. . . . . . . . . 10 ⊢ (((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) ∧ (𝑓:𝑧⟶𝑢 ∧ ∀𝑤 ∈ 𝑧 𝑤 ⊆ (𝑓‘𝑤))) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣)
93	65, 92	exlimddv 1931	. . . . . . . . 9 ⊢ ((((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) ∧ (𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin) ∧ 𝑋 = ∪ 𝑧)) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣)
94	93	rexlimdvaa 3149	. . . . . . . 8 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → (∃𝑧 ∈ (𝒫 {𝑤 ∈ 𝐵 ∣ ∃𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡} ∩ Fin)𝑋 = ∪ 𝑧 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣))
95	54, 94	syld 47	. . . . . . 7 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ (𝑢 ⊆ (topGen‘𝐵) ∧ 𝑋 = ∪ 𝑢)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣))
96	95	expr 455	. . . . . 6 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ 𝑢 ⊆ (topGen‘𝐵)) → (𝑋 = ∪ 𝑢 → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣)))
97	96	com23 86	. . . . 5 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ 𝑢 ⊆ (topGen‘𝐵)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → (𝑋 = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣)))
98	19, 97	sylan2 591	. . . 4 ⊢ (((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) ∧ 𝑢 ∈ 𝒫 (topGen‘𝐵)) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → (𝑋 = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣)))
99	98	ralrimdva 3147	. . 3 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → ∀𝑢 ∈ 𝒫 (topGen‘𝐵)(𝑋 = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣)))
100		tgcl 22986	. . . . . 6 ⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)
101	100	adantr 479	. . . . 5 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → (topGen‘𝐵) ∈ Top)
102	1	iscmp 23406	. . . . . 6 ⊢ ((topGen‘𝐵) ∈ Comp ↔ ((topGen‘𝐵) ∈ Top ∧ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)(∪ (topGen‘𝐵) = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑣)))
103	102	baib 534	. . . . 5 ⊢ ((topGen‘𝐵) ∈ Top → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)(∪ (topGen‘𝐵) = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑣)))
104	101, 103	syl 17	. . . 4 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)(∪ (topGen‘𝐵) = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑣)))
105	6	eqeq1d 2731	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → (∪ (topGen‘𝐵) = ∪ 𝑢 ↔ 𝑋 = ∪ 𝑢))
106	6	eqeq1d 2731	. . . . . . 7 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → (∪ (topGen‘𝐵) = ∪ 𝑣 ↔ 𝑋 = ∪ 𝑣))
107	106	rexbidv 3172	. . . . . 6 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → (∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣))
108	105, 107	imbi12d 343	. . . . 5 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → ((∪ (topGen‘𝐵) = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑣) ↔ (𝑋 = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣)))
109	108	ralbidv 3171	. . . 4 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → (∀𝑢 ∈ 𝒫 (topGen‘𝐵)(∪ (topGen‘𝐵) = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)∪ (topGen‘𝐵) = ∪ 𝑣) ↔ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)(𝑋 = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣)))
110	104, 109	bitrd 278	. . 3 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 (topGen‘𝐵)(𝑋 = ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)𝑋 = ∪ 𝑣)))
111	99, 110	sylibrd 258	. 2 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → (∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → (topGen‘𝐵) ∈ Comp))
112	18, 111	impbid 211	1 ⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1534  ∃wex 1774   ∈ wcel 2100  ∀wral 3054  ∃wrex 3063  {crab 3428   ∩ cin 3958   ⊆ wss 3959  𝒫 cpw 4610  ∪ cuni 4918  ∪ ciun 5006  ran crn 5687   Fn wfn 6553  ⟶wf 6554  –onto→wfo 6556  ‘cfv 6558  Fincfn 8982  topGenctg 17473  Topctop 22909  TopBasesctb 22962  Compccmp 23404

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pow 5373  ax-pr 5437  ax-un 7751

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-ral 3055  df-rex 3064  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3789  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-pss 3979  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-iun 5008  df-br 5157  df-opab 5219  df-mpt 5240  df-tr 5274  df-id 5584  df-eprel 5590  df-po 5598  df-so 5599  df-fr 5641  df-we 5643  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-om 7885  df-1o 8504  df-en 8983  df-dom 8984  df-fin 8986  df-topgen 17479  df-top 22910  df-bases 22963  df-cmp 23405

This theorem is referenced by: (None)