Step |
Hyp |
Ref |
Expression |
1 |
|
tgval2 |
⊢ ( 𝐵 ∈ 𝑉 → ( topGen ‘ 𝐵 ) = { 𝑧 ∣ ( 𝑧 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) } ) |
2 |
1
|
eleq2d |
⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ 𝐴 ∈ { 𝑧 ∣ ( 𝑧 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) } ) ) |
3 |
|
elex |
⊢ ( 𝐴 ∈ { 𝑧 ∣ ( 𝑧 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) } → 𝐴 ∈ V ) |
4 |
3
|
adantl |
⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ { 𝑧 ∣ ( 𝑧 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) } ) → 𝐴 ∈ V ) |
5 |
|
uniexg |
⊢ ( 𝐵 ∈ 𝑉 → ∪ 𝐵 ∈ V ) |
6 |
|
ssexg |
⊢ ( ( 𝐴 ⊆ ∪ 𝐵 ∧ ∪ 𝐵 ∈ V ) → 𝐴 ∈ V ) |
7 |
5 6
|
sylan2 |
⊢ ( ( 𝐴 ⊆ ∪ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ V ) |
8 |
7
|
ancoms |
⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝐵 ) → 𝐴 ∈ V ) |
9 |
8
|
adantrr |
⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐴 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) → 𝐴 ∈ V ) |
10 |
|
sseq1 |
⊢ ( 𝑧 = 𝐴 → ( 𝑧 ⊆ ∪ 𝐵 ↔ 𝐴 ⊆ ∪ 𝐵 ) ) |
11 |
|
sseq2 |
⊢ ( 𝑧 = 𝐴 → ( 𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝐴 ) ) |
12 |
11
|
anbi2d |
⊢ ( 𝑧 = 𝐴 → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ↔ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) |
13 |
12
|
rexbidv |
⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) |
14 |
13
|
raleqbi1dv |
⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) |
15 |
10 14
|
anbi12d |
⊢ ( 𝑧 = 𝐴 → ( ( 𝑧 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) ↔ ( 𝐴 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) ) |
16 |
15
|
elabg |
⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ { 𝑧 ∣ ( 𝑧 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) } ↔ ( 𝐴 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) ) |
17 |
4 9 16
|
pm5.21nd |
⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ { 𝑧 ∣ ( 𝑧 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) } ↔ ( 𝐴 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) ) |
18 |
2 17
|
bitrd |
⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ( 𝐴 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴 ) ) ) ) |