Step |
Hyp |
Ref |
Expression |
1 |
|
df-topgen |
⊢ topGen = ( 𝑦 ∈ V ↦ { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑥 ) } ) |
2 |
|
ineq1 |
⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∩ 𝒫 𝑥 ) = ( 𝐵 ∩ 𝒫 𝑥 ) ) |
3 |
2
|
unieqd |
⊢ ( 𝑦 = 𝐵 → ∪ ( 𝑦 ∩ 𝒫 𝑥 ) = ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) |
4 |
3
|
sseq2d |
⊢ ( 𝑦 = 𝐵 → ( 𝑥 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑥 ) ↔ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) ) |
5 |
4
|
abbidv |
⊢ ( 𝑦 = 𝐵 → { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑥 ) } = { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ) |
6 |
|
elex |
⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ V ) |
7 |
|
uniexg |
⊢ ( 𝐵 ∈ 𝑉 → ∪ 𝐵 ∈ V ) |
8 |
|
abssexg |
⊢ ( ∪ 𝐵 ∈ V → { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) } ∈ V ) |
9 |
|
uniin |
⊢ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ⊆ ( ∪ 𝐵 ∩ ∪ 𝒫 𝑥 ) |
10 |
|
sstr |
⊢ ( ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ∧ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ⊆ ( ∪ 𝐵 ∩ ∪ 𝒫 𝑥 ) ) → 𝑥 ⊆ ( ∪ 𝐵 ∩ ∪ 𝒫 𝑥 ) ) |
11 |
9 10
|
mpan2 |
⊢ ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) → 𝑥 ⊆ ( ∪ 𝐵 ∩ ∪ 𝒫 𝑥 ) ) |
12 |
|
ssin |
⊢ ( ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) ↔ 𝑥 ⊆ ( ∪ 𝐵 ∩ ∪ 𝒫 𝑥 ) ) |
13 |
11 12
|
sylibr |
⊢ ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) → ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) ) |
14 |
13
|
ss2abi |
⊢ { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ⊆ { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) } |
15 |
|
ssexg |
⊢ ( ( { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ⊆ { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) } ∧ { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) } ∈ V ) → { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ∈ V ) |
16 |
14 15
|
mpan |
⊢ ( { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) } ∈ V → { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ∈ V ) |
17 |
7 8 16
|
3syl |
⊢ ( 𝐵 ∈ 𝑉 → { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ∈ V ) |
18 |
1 5 6 17
|
fvmptd3 |
⊢ ( 𝐵 ∈ 𝑉 → ( topGen ‘ 𝐵 ) = { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ) |