Step |
Hyp |
Ref |
Expression |
1 |
|
cfon |
|- ( cf ` A ) e. On |
2 |
|
eleq1 |
|- ( ( cf ` A ) = A -> ( ( cf ` A ) e. On <-> A e. On ) ) |
3 |
1 2
|
mpbii |
|- ( ( cf ` A ) = A -> A e. On ) |
4 |
3
|
3ad2ant2 |
|- ( ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A ~P x ~< A ) -> A e. On ) |
5 |
|
idd |
|- ( A e. On -> ( A =/= (/) -> A =/= (/) ) ) |
6 |
|
idd |
|- ( A e. On -> ( ( cf ` A ) = A -> ( cf ` A ) = A ) ) |
7 |
|
inawinalem |
|- ( A e. On -> ( A. x e. A ~P x ~< A -> A. x e. A E. y e. A x ~< y ) ) |
8 |
5 6 7
|
3anim123d |
|- ( A e. On -> ( ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A ~P x ~< A ) -> ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A E. y e. A x ~< y ) ) ) |
9 |
4 8
|
mpcom |
|- ( ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A ~P x ~< A ) -> ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A E. y e. A x ~< y ) ) |
10 |
|
elina |
|- ( A e. Inacc <-> ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A ~P x ~< A ) ) |
11 |
|
elwina |
|- ( A e. InaccW <-> ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A E. y e. A x ~< y ) ) |
12 |
9 10 11
|
3imtr4i |
|- ( A e. Inacc -> A e. InaccW ) |