Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∪ 𝐵 = ∪ 𝐶 ) → ∪ 𝐵 = ∪ 𝐶 ) |
2 |
|
uniexg |
⊢ ( 𝐵 ∈ 𝑉 → ∪ 𝐵 ∈ V ) |
3 |
2
|
adantr |
⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∪ 𝐵 = ∪ 𝐶 ) → ∪ 𝐵 ∈ V ) |
4 |
1 3
|
eqeltrrd |
⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∪ 𝐵 = ∪ 𝐶 ) → ∪ 𝐶 ∈ V ) |
5 |
|
uniexb |
⊢ ( 𝐶 ∈ V ↔ ∪ 𝐶 ∈ V ) |
6 |
4 5
|
sylibr |
⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∪ 𝐵 = ∪ 𝐶 ) → 𝐶 ∈ V ) |
7 |
|
tgss3 |
⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V ) → ( ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) ↔ 𝐵 ⊆ ( topGen ‘ 𝐶 ) ) ) |
8 |
6 7
|
syldan |
⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∪ 𝐵 = ∪ 𝐶 ) → ( ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) ↔ 𝐵 ⊆ ( topGen ‘ 𝐶 ) ) ) |
9 |
|
eltg2b |
⊢ ( 𝐶 ∈ V → ( 𝑦 ∈ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝑦 ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) |
10 |
6 9
|
syl |
⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∪ 𝐵 = ∪ 𝐶 ) → ( 𝑦 ∈ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝑦 ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) |
11 |
|
elunii |
⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ ∪ 𝐵 ) |
12 |
11
|
ancoms |
⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ ∪ 𝐵 ) |
13 |
|
biimt |
⊢ ( 𝑥 ∈ ∪ 𝐵 → ( ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ↔ ( 𝑥 ∈ ∪ 𝐵 → ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) ) |
14 |
12 13
|
syl |
⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝑦 ) → ( ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ↔ ( 𝑥 ∈ ∪ 𝐵 → ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) ) |
15 |
14
|
ralbidva |
⊢ ( 𝑦 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝑦 ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ∈ ∪ 𝐵 → ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) ) |
16 |
10 15
|
sylan9bb |
⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ ∪ 𝐵 = ∪ 𝐶 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ∈ ∪ 𝐵 → ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) ) |
17 |
|
ralcom3 |
⊢ ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 ∈ ∪ 𝐵 → ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ∪ 𝐵 ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) |
18 |
16 17
|
bitrdi |
⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ ∪ 𝐵 = ∪ 𝐶 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑥 ∈ ∪ 𝐵 ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) ) |
19 |
18
|
ralbidva |
⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∪ 𝐵 = ∪ 𝐶 ) → ( ∀ 𝑦 ∈ 𝐵 𝑦 ∈ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ ∪ 𝐵 ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) ) |
20 |
|
dfss3 |
⊢ ( 𝐵 ⊆ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑦 ∈ 𝐵 𝑦 ∈ ( topGen ‘ 𝐶 ) ) |
21 |
|
ralcom |
⊢ ( ∀ 𝑥 ∈ ∪ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ ∪ 𝐵 ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) |
22 |
19 20 21
|
3bitr4g |
⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∪ 𝐵 = ∪ 𝐶 ) → ( 𝐵 ⊆ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑥 ∈ ∪ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) ) |
23 |
8 22
|
bitrd |
⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∪ 𝐵 = ∪ 𝐶 ) → ( ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑥 ∈ ∪ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) ) |