Step |
Hyp |
Ref |
Expression |
1 |
|
elpri |
|- ( A e. { (/) , 1o } -> ( A = (/) \/ A = 1o ) ) |
2 |
|
difeq2 |
|- ( A = (/) -> ( 1o \ A ) = ( 1o \ (/) ) ) |
3 |
|
dif0 |
|- ( 1o \ (/) ) = 1o |
4 |
2 3
|
eqtrdi |
|- ( A = (/) -> ( 1o \ A ) = 1o ) |
5 |
|
difeq2 |
|- ( A = 1o -> ( 1o \ A ) = ( 1o \ 1o ) ) |
6 |
|
difid |
|- ( 1o \ 1o ) = (/) |
7 |
5 6
|
eqtrdi |
|- ( A = 1o -> ( 1o \ A ) = (/) ) |
8 |
4 7
|
orim12i |
|- ( ( A = (/) \/ A = 1o ) -> ( ( 1o \ A ) = 1o \/ ( 1o \ A ) = (/) ) ) |
9 |
8
|
orcomd |
|- ( ( A = (/) \/ A = 1o ) -> ( ( 1o \ A ) = (/) \/ ( 1o \ A ) = 1o ) ) |
10 |
1 9
|
syl |
|- ( A e. { (/) , 1o } -> ( ( 1o \ A ) = (/) \/ ( 1o \ A ) = 1o ) ) |
11 |
|
1on |
|- 1o e. On |
12 |
|
difexg |
|- ( 1o e. On -> ( 1o \ A ) e. _V ) |
13 |
11 12
|
ax-mp |
|- ( 1o \ A ) e. _V |
14 |
13
|
elpr |
|- ( ( 1o \ A ) e. { (/) , 1o } <-> ( ( 1o \ A ) = (/) \/ ( 1o \ A ) = 1o ) ) |
15 |
10 14
|
sylibr |
|- ( A e. { (/) , 1o } -> ( 1o \ A ) e. { (/) , 1o } ) |
16 |
|
df2o3 |
|- 2o = { (/) , 1o } |
17 |
15 16
|
eleqtrrdi |
|- ( A e. { (/) , 1o } -> ( 1o \ A ) e. 2o ) |
18 |
17 16
|
eleq2s |
|- ( A e. 2o -> ( 1o \ A ) e. 2o ) |