Metamath Proof Explorer

Theorem tgval2

Description: Definition of a topology generated by a basis in Munkres p. 78. Later we show (in tgcl ) that ( topGenB ) is indeed a topology (on U. B , see unitg ). See also tgval and tgval3 . (Contributed by NM, 15-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

Ref Expression
Assertion tgval2 ( 𝐵 ∈ 𝑉 → ( topGen ‘ 𝐵 ) = { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) } )

Proof

Step Hyp Ref Expression
1 tgval ⊢ ( 𝐵 ∈ 𝑉 → ( topGen ‘ 𝐵 ) = { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } )
2 inss1 ⊢ ( 𝐵 ∩ 𝒫 𝑥 ) ⊆ 𝐵
3 2 unissi ⊢ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ⊆ ∪ 𝐵
4 3 sseli ⊢ ( 𝑦 ∈ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) → 𝑦 ∈ ∪ 𝐵 )
5 4 pm4.71ri ⊢ ( 𝑦 ∈ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ↔ ( 𝑦 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
6 5 ralbii ⊢ ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
7 r19.26 ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ 𝐵 ∧ 𝑦 ∈ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
8 6 7 bitri ⊢ ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ↔ ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
9 dfss3 ⊢ ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) )
10 dfss3 ⊢ ( 𝑥 ⊆ ∪ 𝐵 ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ 𝐵 )
11 elin ⊢ ( 𝑧 ∈ ( 𝐵 ∩ 𝒫 𝑥 ) ↔ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝒫 𝑥 ) )
12 11 anbi2i ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( 𝐵 ∩ 𝒫 𝑥 ) ) ↔ ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝒫 𝑥 ) ) )
13 an12 ⊢ ( ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝒫 𝑥 ) ) ↔ ( 𝑧 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝒫 𝑥 ) ) )
14 12 13 bitri ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( 𝐵 ∩ 𝒫 𝑥 ) ) ↔ ( 𝑧 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝒫 𝑥 ) ) )
15 14 exbii ⊢ ( ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( 𝐵 ∩ 𝒫 𝑥 ) ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝒫 𝑥 ) ) )
16 eluni ⊢ ( 𝑦 ∈ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ↔ ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
17 df-rex ⊢ ( ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝒫 𝑥 ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝒫 𝑥 ) ) )
18 15 16 17 3bitr4i ⊢ ( 𝑦 ∈ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝒫 𝑥 ) )
19 velpw ⊢ ( 𝑧 ∈ 𝒫 𝑥 ↔ 𝑧 ⊆ 𝑥 )
20 19 anbi2i ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝒫 𝑥 ) ↔ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
21 20 rexbii ⊢ ( ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝒫 𝑥 ) ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
22 18 21 bitr2i ⊢ ( ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ↔ 𝑦 ∈ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) )
23 22 ralbii ⊢ ( ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) )
24 10 23 anbi12i ⊢ ( ( 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
25 8 9 24 3bitr4i ⊢ ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ↔ ( 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) )
26 25 abbii ⊢ { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } = { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) }
27 1 26 eqtrdi ⊢ ( 𝐵 ∈ 𝑉 → ( topGen ‘ 𝐵 ) = { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) } )