Metamath Proof Explorer

Theorem tgcmp

Description: A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub , which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion tgcmp ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ( topGen ‘ 𝐵 ) ∈ Comp ↔ ∀ 𝑦 ∈ 𝒫 𝐵 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ ( topGen ‘ 𝐵 ) = ∪ ( topGen ‘ 𝐵 )
2 1 iscmp ⊢ ( ( topGen ‘ 𝐵 ) ∈ Comp ↔ ( ( topGen ‘ 𝐵 ) ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 ( topGen ‘ 𝐵 ) ( ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑧 ) ) )
3 2 simprbi ⊢ ( ( topGen ‘ 𝐵 ) ∈ Comp → ∀ 𝑦 ∈ 𝒫 ( topGen ‘ 𝐵 ) ( ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑧 ) )
4 unitg ⊢ ( 𝐵 ∈ TopBases → ∪ ( topGen ‘ 𝐵 ) = ∪ 𝐵 )
5 eqtr3 ⊢ ( ( ∪ ( topGen ‘ 𝐵 ) = ∪ 𝐵 ∧ 𝑋 = ∪ 𝐵 ) → ∪ ( topGen ‘ 𝐵 ) = 𝑋 )
6 4 5 sylan ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ∪ ( topGen ‘ 𝐵 ) = 𝑋 )
7 6 eqeq1d ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑦 ) )
8 6 eqeq1d ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑧 ↔ 𝑋 = ∪ 𝑧 ) )
9 8 rexbidv ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑧 ↔ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
10 7 9 imbi12d ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ( ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑧 ) ↔ ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
11 10 ralbidv ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ∀ 𝑦 ∈ 𝒫 ( topGen ‘ 𝐵 ) ( ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑧 ) ↔ ∀ 𝑦 ∈ 𝒫 ( topGen ‘ 𝐵 ) ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
12 bastg ⊢ ( 𝐵 ∈ TopBases → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
13 12 adantr ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
14 13 sspwd ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → 𝒫 𝐵 ⊆ 𝒫 ( topGen ‘ 𝐵 ) )
15 ssralv ⊢ ( 𝒫 𝐵 ⊆ 𝒫 ( topGen ‘ 𝐵 ) → ( ∀ 𝑦 ∈ 𝒫 ( topGen ‘ 𝐵 ) ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → ∀ 𝑦 ∈ 𝒫 𝐵 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
16 14 15 syl ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ∀ 𝑦 ∈ 𝒫 ( topGen ‘ 𝐵 ) ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → ∀ 𝑦 ∈ 𝒫 𝐵 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
17 11 16 sylbid ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ∀ 𝑦 ∈ 𝒫 ( topGen ‘ 𝐵 ) ( ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑧 ) → ∀ 𝑦 ∈ 𝒫 𝐵 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
18 3 17 syl5 ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ( topGen ‘ 𝐵 ) ∈ Comp → ∀ 𝑦 ∈ 𝒫 𝐵 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
19 elpwi ⊢ ( 𝑢 ∈ 𝒫 ( topGen ‘ 𝐵 ) → 𝑢 ⊆ ( topGen ‘ 𝐵 ) )
20 simprr ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) → 𝑋 = ∪ 𝑢 )
21 simprl ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) → 𝑢 ⊆ ( topGen ‘ 𝐵 ) )
22 21 sselda ⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ 𝑡 ∈ 𝑢 ) → 𝑡 ∈ ( topGen ‘ 𝐵 ) )
23 22 adantrr ⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑡 ∈ 𝑢 ∧ 𝑦 ∈ 𝑡 ) ) → 𝑡 ∈ ( topGen ‘ 𝐵 ) )
24 simprr ⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑡 ∈ 𝑢 ∧ 𝑦 ∈ 𝑡 ) ) → 𝑦 ∈ 𝑡 )
25 tg2 ⊢ ( ( 𝑡 ∈ ( topGen ‘ 𝐵 ) ∧ 𝑦 ∈ 𝑡 ) → ∃ 𝑤 ∈ 𝐵 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡 ) )
26 23 24 25 syl2anc ⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑡 ∈ 𝑢 ∧ 𝑦 ∈ 𝑡 ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡 ) )
27 26 expr ⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ 𝑡 ∈ 𝑢 ) → ( 𝑦 ∈ 𝑡 → ∃ 𝑤 ∈ 𝐵 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡 ) ) )
28 27 reximdva ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) → ( ∃ 𝑡 ∈ 𝑢 𝑦 ∈ 𝑡 → ∃ 𝑡 ∈ 𝑢 ∃ 𝑤 ∈ 𝐵 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡 ) ) )
29 eluni2 ⊢ ( 𝑦 ∈ ∪ 𝑢 ↔ ∃ 𝑡 ∈ 𝑢 𝑦 ∈ 𝑡 )
30 elunirab ⊢ ( 𝑦 ∈ ∪ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ↔ ∃ 𝑤 ∈ 𝐵 ( 𝑦 ∈ 𝑤 ∧ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 ) )
31 r19.42v ⊢ ( ∃ 𝑡 ∈ 𝑢 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡 ) ↔ ( 𝑦 ∈ 𝑤 ∧ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 ) )
32 31 rexbii ⊢ ( ∃ 𝑤 ∈ 𝐵 ∃ 𝑡 ∈ 𝑢 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡 ) ↔ ∃ 𝑤 ∈ 𝐵 ( 𝑦 ∈ 𝑤 ∧ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 ) )
33 rexcom ⊢ ( ∃ 𝑤 ∈ 𝐵 ∃ 𝑡 ∈ 𝑢 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡 ) ↔ ∃ 𝑡 ∈ 𝑢 ∃ 𝑤 ∈ 𝐵 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡 ) )
34 30 32 33 3bitr2i ⊢ ( 𝑦 ∈ ∪ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ↔ ∃ 𝑡 ∈ 𝑢 ∃ 𝑤 ∈ 𝐵 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑡 ) )
35 28 29 34 3imtr4g ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) → ( 𝑦 ∈ ∪ 𝑢 → 𝑦 ∈ ∪ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ) )
36 35 ssrdv ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) → ∪ 𝑢 ⊆ ∪ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } )
37 20 36 eqsstrd ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) → 𝑋 ⊆ ∪ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } )
38 ssrab2 ⊢ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ⊆ 𝐵
39 38 unissi ⊢ ∪ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ⊆ ∪ 𝐵
40 simplr ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) → 𝑋 = ∪ 𝐵 )
41 39 40 sseqtrrid ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) → ∪ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ⊆ 𝑋 )
42 37 41 eqssd ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) → 𝑋 = ∪ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } )
43 elpw2g ⊢ ( 𝐵 ∈ TopBases → ( { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∈ 𝒫 𝐵 ↔ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ⊆ 𝐵 ) )
44 43 ad2antrr ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) → ( { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∈ 𝒫 𝐵 ↔ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ⊆ 𝐵 ) )
45 38 44 mpbiri ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) → { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∈ 𝒫 𝐵 )
46 unieq ⊢ ( 𝑦 = { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } → ∪ 𝑦 = ∪ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } )
47 46 eqeq2d ⊢ ( 𝑦 = { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } → ( 𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ) )
48 pweq ⊢ ( 𝑦 = { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } → 𝒫 𝑦 = 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } )
49 48 ineq1d ⊢ ( 𝑦 = { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } → ( 𝒫 𝑦 ∩ Fin ) = ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) )
50 49 rexeqdv ⊢ ( 𝑦 = { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } → ( ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ↔ ∃ 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
51 47 50 imbi12d ⊢ ( 𝑦 = { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } → ( ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ↔ ( 𝑋 = ∪ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } → ∃ 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
52 51 rspcv ⊢ ( { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∈ 𝒫 𝐵 → ( ∀ 𝑦 ∈ 𝒫 𝐵 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → ( 𝑋 = ∪ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } → ∃ 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
53 45 52 syl ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) → ( ∀ 𝑦 ∈ 𝒫 𝐵 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → ( 𝑋 = ∪ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } → ∃ 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )
54 42 53 mpid ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) → ( ∀ 𝑦 ∈ 𝒫 𝐵 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → ∃ 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
55 elfpw ⊢ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ↔ ( 𝑧 ⊆ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∧ 𝑧 ∈ Fin ) )
56 55 simprbi ⊢ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) → 𝑧 ∈ Fin )
57 56 ad2antrl ⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) → 𝑧 ∈ Fin )
58 55 simplbi ⊢ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) → 𝑧 ⊆ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } )
59 58 ad2antrl ⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) → 𝑧 ⊆ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } )
60 ssrab ⊢ ( 𝑧 ⊆ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ↔ ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑤 ∈ 𝑧 ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 ) )
61 60 simprbi ⊢ ( 𝑧 ⊆ { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } → ∀ 𝑤 ∈ 𝑧 ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 )
62 59 61 syl ⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) → ∀ 𝑤 ∈ 𝑧 ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 )
63 sseq2 ⊢ ( 𝑡 = ( 𝑓 ‘ 𝑤 ) → ( 𝑤 ⊆ 𝑡 ↔ 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
64 63 ac6sfi ⊢ ( ( 𝑧 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑧 ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 ) → ∃ 𝑓 ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
65 57 62 64 syl2anc ⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) → ∃ 𝑓 ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
66 frn ⊢ ( 𝑓 : 𝑧 ⟶ 𝑢 → ran 𝑓 ⊆ 𝑢 )
67 66 ad2antrl ⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) ∧ ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ran 𝑓 ⊆ 𝑢 )
68 ffn ⊢ ( 𝑓 : 𝑧 ⟶ 𝑢 → 𝑓 Fn 𝑧 )
69 dffn4 ⊢ ( 𝑓 Fn 𝑧 ↔ 𝑓 : 𝑧 –onto→ ran 𝑓 )
70 68 69 sylib ⊢ ( 𝑓 : 𝑧 ⟶ 𝑢 → 𝑓 : 𝑧 –onto→ ran 𝑓 )
71 70 adantr ⊢ ( ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) → 𝑓 : 𝑧 –onto→ ran 𝑓 )
72 fofi ⊢ ( ( 𝑧 ∈ Fin ∧ 𝑓 : 𝑧 –onto→ ran 𝑓 ) → ran 𝑓 ∈ Fin )
73 57 71 72 syl2an ⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) ∧ ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ran 𝑓 ∈ Fin )
74 elfpw ⊢ ( ran 𝑓 ∈ ( 𝒫 𝑢 ∩ Fin ) ↔ ( ran 𝑓 ⊆ 𝑢 ∧ ran 𝑓 ∈ Fin ) )
75 67 73 74 sylanbrc ⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) ∧ ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ran 𝑓 ∈ ( 𝒫 𝑢 ∩ Fin ) )
76 simplrr ⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) ∧ ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → 𝑋 = ∪ 𝑧 )
77 uniiun ⊢ ∪ 𝑧 = ∪ 𝑤 ∈ 𝑧 𝑤
78 ss2iun ⊢ ( ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) → ∪ 𝑤 ∈ 𝑧 𝑤 ⊆ ∪ 𝑤 ∈ 𝑧 ( 𝑓 ‘ 𝑤 ) )
79 77 78 eqsstrid ⊢ ( ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) → ∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 ( 𝑓 ‘ 𝑤 ) )
80 79 ad2antll ⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) ∧ ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 ( 𝑓 ‘ 𝑤 ) )
81 fniunfv ⊢ ( 𝑓 Fn 𝑧 → ∪ 𝑤 ∈ 𝑧 ( 𝑓 ‘ 𝑤 ) = ∪ ran 𝑓 )
82 68 81 syl ⊢ ( 𝑓 : 𝑧 ⟶ 𝑢 → ∪ 𝑤 ∈ 𝑧 ( 𝑓 ‘ 𝑤 ) = ∪ ran 𝑓 )
83 82 ad2antrl ⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) ∧ ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∪ 𝑤 ∈ 𝑧 ( 𝑓 ‘ 𝑤 ) = ∪ ran 𝑓 )
84 80 83 sseqtrd ⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) ∧ ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∪ 𝑧 ⊆ ∪ ran 𝑓 )
85 76 84 eqsstrd ⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) ∧ ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → 𝑋 ⊆ ∪ ran 𝑓 )
86 67 unissd ⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) ∧ ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∪ ran 𝑓 ⊆ ∪ 𝑢 )
87 20 ad2antrr ⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) ∧ ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → 𝑋 = ∪ 𝑢 )
88 86 87 sseqtrrd ⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) ∧ ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∪ ran 𝑓 ⊆ 𝑋 )
89 85 88 eqssd ⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) ∧ ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → 𝑋 = ∪ ran 𝑓 )
90 unieq ⊢ ( 𝑣 = ran 𝑓 → ∪ 𝑣 = ∪ ran 𝑓 )
91 90 rspceeqv ⊢ ( ( ran 𝑓 ∈ ( 𝒫 𝑢 ∩ Fin ) ∧ 𝑋 = ∪ ran 𝑓 ) → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑣 )
92 75 89 91 syl2anc ⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) ∧ ( 𝑓 : 𝑧 ⟶ 𝑢 ∧ ∀ 𝑤 ∈ 𝑧 𝑤 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑣 )
93 65 92 exlimddv ⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) ∧ ( 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) ∧ 𝑋 = ∪ 𝑧 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑣 )
94 93 rexlimdvaa ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) → ( ∃ 𝑧 ∈ ( 𝒫 { 𝑤 ∈ 𝐵 ∣ ∃ 𝑡 ∈ 𝑢 𝑤 ⊆ 𝑡 } ∩ Fin ) 𝑋 = ∪ 𝑧 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑣 ) )
95 54 94 syld ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑋 = ∪ 𝑢 ) ) → ( ∀ 𝑦 ∈ 𝒫 𝐵 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑣 ) )
96 95 expr ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ 𝑢 ⊆ ( topGen ‘ 𝐵 ) ) → ( 𝑋 = ∪ 𝑢 → ( ∀ 𝑦 ∈ 𝒫 𝐵 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑣 ) ) )
97 96 com23 ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ 𝑢 ⊆ ( topGen ‘ 𝐵 ) ) → ( ∀ 𝑦 ∈ 𝒫 𝐵 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → ( 𝑋 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑣 ) ) )
98 19 97 sylan2 ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) ∧ 𝑢 ∈ 𝒫 ( topGen ‘ 𝐵 ) ) → ( ∀ 𝑦 ∈ 𝒫 𝐵 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → ( 𝑋 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑣 ) ) )
99 98 ralrimdva ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ∀ 𝑦 ∈ 𝒫 𝐵 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → ∀ 𝑢 ∈ 𝒫 ( topGen ‘ 𝐵 ) ( 𝑋 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑣 ) ) )
100 tgcl ⊢ ( 𝐵 ∈ TopBases → ( topGen ‘ 𝐵 ) ∈ Top )
101 100 adantr ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( topGen ‘ 𝐵 ) ∈ Top )
102 1 iscmp ⊢ ( ( topGen ‘ 𝐵 ) ∈ Comp ↔ ( ( topGen ‘ 𝐵 ) ∈ Top ∧ ∀ 𝑢 ∈ 𝒫 ( topGen ‘ 𝐵 ) ( ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑣 ) ) )
103 102 baib ⊢ ( ( topGen ‘ 𝐵 ) ∈ Top → ( ( topGen ‘ 𝐵 ) ∈ Comp ↔ ∀ 𝑢 ∈ 𝒫 ( topGen ‘ 𝐵 ) ( ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑣 ) ) )
104 101 103 syl ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ( topGen ‘ 𝐵 ) ∈ Comp ↔ ∀ 𝑢 ∈ 𝒫 ( topGen ‘ 𝐵 ) ( ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑣 ) ) )
105 6 eqeq1d ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑢 ↔ 𝑋 = ∪ 𝑢 ) )
106 6 eqeq1d ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑣 ↔ 𝑋 = ∪ 𝑣 ) )
107 106 rexbidv ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑣 ↔ ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑣 ) )
108 105 107 imbi12d ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ( ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑣 ) ↔ ( 𝑋 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑣 ) ) )
109 108 ralbidv ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ∀ 𝑢 ∈ 𝒫 ( topGen ‘ 𝐵 ) ( ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ∪ ( topGen ‘ 𝐵 ) = ∪ 𝑣 ) ↔ ∀ 𝑢 ∈ 𝒫 ( topGen ‘ 𝐵 ) ( 𝑋 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑣 ) ) )
110 104 109 bitrd ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ( topGen ‘ 𝐵 ) ∈ Comp ↔ ∀ 𝑢 ∈ 𝒫 ( topGen ‘ 𝐵 ) ( 𝑋 = ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑣 ) ) )
111 99 110 sylibrd ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ∀ 𝑦 ∈ 𝒫 𝐵 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) → ( topGen ‘ 𝐵 ) ∈ Comp ) )
112 18 111 impbid ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵 ) → ( ( topGen ‘ 𝐵 ) ∈ Comp ↔ ∀ 𝑦 ∈ 𝒫 𝐵 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )