Step |
Hyp |
Ref |
Expression |
1 |
|
df-ni |
|- N. = ( _om \ { (/) } ) |
2 |
|
difss |
|- ( _om \ { (/) } ) C_ _om |
3 |
|
omsson |
|- _om C_ On |
4 |
2 3
|
sstri |
|- ( _om \ { (/) } ) C_ On |
5 |
1 4
|
eqsstri |
|- N. C_ On |
6 |
|
epweon |
|- _E We On |
7 |
|
weso |
|- ( _E We On -> _E Or On ) |
8 |
6 7
|
ax-mp |
|- _E Or On |
9 |
|
soss |
|- ( N. C_ On -> ( _E Or On -> _E Or N. ) ) |
10 |
5 8 9
|
mp2 |
|- _E Or N. |
11 |
|
df-lti |
|- |
12 |
|
soeq1 |
|- ( ( ( _E i^i ( N. X. N. ) ) Or N. ) ) |
13 |
11 12
|
ax-mp |
|- ( ( _E i^i ( N. X. N. ) ) Or N. ) |
14 |
|
soinxp |
|- ( _E Or N. <-> ( _E i^i ( N. X. N. ) ) Or N. ) |
15 |
13 14
|
bitr4i |
|- ( _E Or N. ) |
16 |
10 15
|
mpbir |
|- |