This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrrid ⊢ ( ( ( 𝑋 ∈ 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 ) 𝑋 = ∪ 𝑦 ) ) )