Metamath Proof Explorer


Theorem alexsubb

Description: Biconditional form of the Alexander Subbase Theorem alexsub . (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Assertion alexsubb ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → ( ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ Comp ↔ ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ( topGen ‘ ( fi ‘ 𝐵 ) ) = ( topGen ‘ ( fi ‘ 𝐵 ) )
2 1 iscmp ( ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ Comp ↔ ( ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ Top ∧ ∀ 𝑥 ∈ 𝒫 ( topGen ‘ ( fi ‘ 𝐵 ) ) ( ( topGen ‘ ( fi ‘ 𝐵 ) ) = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ( topGen ‘ ( fi ‘ 𝐵 ) ) = 𝑦 ) ) )
3 2 simprbi ( ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ Comp → ∀ 𝑥 ∈ 𝒫 ( topGen ‘ ( fi ‘ 𝐵 ) ) ( ( topGen ‘ ( fi ‘ 𝐵 ) ) = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ( topGen ‘ ( fi ‘ 𝐵 ) ) = 𝑦 ) )
4 simpr ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → 𝑋 = 𝐵 )
5 elex ( 𝑋 ∈ UFL → 𝑋 ∈ V )
6 5 adantr ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → 𝑋 ∈ V )
7 4 6 eqeltrrd ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → 𝐵 ∈ V )
8 uniexb ( 𝐵 ∈ V ↔ 𝐵 ∈ V )
9 7 8 sylibr ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → 𝐵 ∈ V )
10 fiuni ( 𝐵 ∈ V → 𝐵 = ( fi ‘ 𝐵 ) )
11 9 10 syl ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → 𝐵 = ( fi ‘ 𝐵 ) )
12 fibas ( fi ‘ 𝐵 ) ∈ TopBases
13 unitg ( ( fi ‘ 𝐵 ) ∈ TopBases → ( topGen ‘ ( fi ‘ 𝐵 ) ) = ( fi ‘ 𝐵 ) )
14 12 13 mp1i ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → ( topGen ‘ ( fi ‘ 𝐵 ) ) = ( fi ‘ 𝐵 ) )
15 11 4 14 3eqtr4d ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → 𝑋 = ( topGen ‘ ( fi ‘ 𝐵 ) ) )
16 15 eqeq1d ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → ( 𝑋 = 𝑥 ( topGen ‘ ( fi ‘ 𝐵 ) ) = 𝑥 ) )
17 15 eqeq1d ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → ( 𝑋 = 𝑦 ( topGen ‘ ( fi ‘ 𝐵 ) ) = 𝑦 ) )
18 17 rexbidv ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → ( ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ↔ ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ( topGen ‘ ( fi ‘ 𝐵 ) ) = 𝑦 ) )
19 16 18 imbi12d ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → ( ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ↔ ( ( topGen ‘ ( fi ‘ 𝐵 ) ) = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ( topGen ‘ ( fi ‘ 𝐵 ) ) = 𝑦 ) ) )
20 19 ralbidv ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → ( ∀ 𝑥 ∈ 𝒫 ( topGen ‘ ( fi ‘ 𝐵 ) ) ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝒫 ( topGen ‘ ( fi ‘ 𝐵 ) ) ( ( topGen ‘ ( fi ‘ 𝐵 ) ) = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ( topGen ‘ ( fi ‘ 𝐵 ) ) = 𝑦 ) ) )
21 ssfii ( 𝐵 ∈ V → 𝐵 ⊆ ( fi ‘ 𝐵 ) )
22 9 21 syl ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → 𝐵 ⊆ ( fi ‘ 𝐵 ) )
23 bastg ( ( fi ‘ 𝐵 ) ∈ TopBases → ( fi ‘ 𝐵 ) ⊆ ( topGen ‘ ( fi ‘ 𝐵 ) ) )
24 12 23 ax-mp ( fi ‘ 𝐵 ) ⊆ ( topGen ‘ ( fi ‘ 𝐵 ) )
25 22 24 sstrdi ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → 𝐵 ⊆ ( topGen ‘ ( fi ‘ 𝐵 ) ) )
26 25 sspwd ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → 𝒫 𝐵 ⊆ 𝒫 ( topGen ‘ ( fi ‘ 𝐵 ) ) )
27 ssralv ( 𝒫 𝐵 ⊆ 𝒫 ( topGen ‘ ( fi ‘ 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝒫 ( topGen ‘ ( fi ‘ 𝐵 ) ) ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) → ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ) )
28 26 27 syl ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → ( ∀ 𝑥 ∈ 𝒫 ( topGen ‘ ( fi ‘ 𝐵 ) ) ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) → ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ) )
29 20 28 sylbird ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → ( ∀ 𝑥 ∈ 𝒫 ( topGen ‘ ( fi ‘ 𝐵 ) ) ( ( topGen ‘ ( fi ‘ 𝐵 ) ) = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) ( topGen ‘ ( fi ‘ 𝐵 ) ) = 𝑦 ) → ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ) )
30 3 29 syl5 ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → ( ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ Comp → ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ) )
31 simpll ( ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) ∧ ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ) → 𝑋 ∈ UFL )
32 simplr ( ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) ∧ ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ) → 𝑋 = 𝐵 )
33 eqidd ( ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) ∧ ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ) → ( topGen ‘ ( fi ‘ 𝐵 ) ) = ( topGen ‘ ( fi ‘ 𝐵 ) ) )
34 velpw ( 𝑧 ∈ 𝒫 𝐵𝑧𝐵 )
35 unieq ( 𝑥 = 𝑧 𝑥 = 𝑧 )
36 35 eqeq2d ( 𝑥 = 𝑧 → ( 𝑋 = 𝑥𝑋 = 𝑧 ) )
37 pweq ( 𝑥 = 𝑧 → 𝒫 𝑥 = 𝒫 𝑧 )
38 37 ineq1d ( 𝑥 = 𝑧 → ( 𝒫 𝑥 ∩ Fin ) = ( 𝒫 𝑧 ∩ Fin ) )
39 38 rexeqdv ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ↔ ∃ 𝑦 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑋 = 𝑦 ) )
40 36 39 imbi12d ( 𝑥 = 𝑧 → ( ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ↔ ( 𝑋 = 𝑧 → ∃ 𝑦 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑋 = 𝑦 ) ) )
41 40 rspccv ( ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) → ( 𝑧 ∈ 𝒫 𝐵 → ( 𝑋 = 𝑧 → ∃ 𝑦 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑋 = 𝑦 ) ) )
42 41 adantl ( ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) ∧ ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ) → ( 𝑧 ∈ 𝒫 𝐵 → ( 𝑋 = 𝑧 → ∃ 𝑦 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑋 = 𝑦 ) ) )
43 34 42 syl5bir ( ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) ∧ ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ) → ( 𝑧𝐵 → ( 𝑋 = 𝑧 → ∃ 𝑦 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑋 = 𝑦 ) ) )
44 43 imp32 ( ( ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) ∧ ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ) ∧ ( 𝑧𝐵𝑋 = 𝑧 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑋 = 𝑦 )
45 unieq ( 𝑦 = 𝑤 𝑦 = 𝑤 )
46 45 eqeq2d ( 𝑦 = 𝑤 → ( 𝑋 = 𝑦𝑋 = 𝑤 ) )
47 46 cbvrexvw ( ∃ 𝑦 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑋 = 𝑦 ↔ ∃ 𝑤 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑋 = 𝑤 )
48 44 47 sylib ( ( ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) ∧ ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ) ∧ ( 𝑧𝐵𝑋 = 𝑧 ) ) → ∃ 𝑤 ∈ ( 𝒫 𝑧 ∩ Fin ) 𝑋 = 𝑤 )
49 31 32 33 48 alexsub ( ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) ∧ ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ) → ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ Comp )
50 49 ex ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → ( ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) → ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ Comp ) )
51 30 50 impbid ( ( 𝑋 ∈ UFL ∧ 𝑋 = 𝐵 ) → ( ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ Comp ↔ ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑋 = 𝑥 → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = 𝑦 ) ) )