Step |
Hyp |
Ref |
Expression |
1 |
|
isbasisg |
⊢ ( 𝐵 ∈ 𝐶 → ( 𝐵 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) ) |
2 |
|
dfss3 |
⊢ ( ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) 𝑧 ∈ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) |
3 |
|
elin |
⊢ ( 𝑤 ∈ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) |
4 |
|
velpw |
⊢ ( 𝑤 ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ↔ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) |
5 |
4
|
anbi2i |
⊢ ( ( 𝑤 ∈ 𝐵 ∧ 𝑤 ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) |
6 |
3 5
|
bitri |
⊢ ( 𝑤 ∈ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) |
7 |
6
|
anbi2i |
⊢ ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) ↔ ( 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) |
8 |
|
an12 |
⊢ ( ( 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ↔ ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) |
9 |
7 8
|
bitri |
⊢ ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) ↔ ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) |
10 |
9
|
exbii |
⊢ ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) ↔ ∃ 𝑤 ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) |
11 |
|
eluni |
⊢ ( 𝑧 ∈ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) ) |
12 |
|
df-rex |
⊢ ( ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ↔ ∃ 𝑤 ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) |
13 |
10 11 12
|
3bitr4i |
⊢ ( 𝑧 ∈ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) |
14 |
13
|
ralbii |
⊢ ( ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) 𝑧 ∈ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) |
15 |
2 14
|
bitri |
⊢ ( ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) |
16 |
15
|
2ralbii |
⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) |
17 |
1 16
|
bitrdi |
⊢ ( 𝐵 ∈ 𝐶 → ( 𝐵 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) |