Step |
Hyp |
Ref |
Expression |
1 |
|
olc |
|- ( J = { (/) } -> ( J = (/) \/ J = { (/) } ) ) |
2 |
|
0opn |
|- ( J e. Top -> (/) e. J ) |
3 |
|
n0i |
|- ( (/) e. J -> -. J = (/) ) |
4 |
2 3
|
syl |
|- ( J e. Top -> -. J = (/) ) |
5 |
4
|
pm2.21d |
|- ( J e. Top -> ( J = (/) -> J = { (/) } ) ) |
6 |
|
idd |
|- ( J e. Top -> ( J = { (/) } -> J = { (/) } ) ) |
7 |
5 6
|
jaod |
|- ( J e. Top -> ( ( J = (/) \/ J = { (/) } ) -> J = { (/) } ) ) |
8 |
1 7
|
impbid2 |
|- ( J e. Top -> ( J = { (/) } <-> ( J = (/) \/ J = { (/) } ) ) ) |
9 |
|
uni0b |
|- ( U. J = (/) <-> J C_ { (/) } ) |
10 |
|
sssn |
|- ( J C_ { (/) } <-> ( J = (/) \/ J = { (/) } ) ) |
11 |
9 10
|
bitr2i |
|- ( ( J = (/) \/ J = { (/) } ) <-> U. J = (/) ) |
12 |
8 11
|
bitr2di |
|- ( J e. Top -> ( U. J = (/) <-> J = { (/) } ) ) |