Step |
Hyp |
Ref |
Expression |
1 |
|
oe0lem.1 |
|- ( ( ph /\ A = (/) ) -> ps ) |
2 |
|
oe0lem.2 |
|- ( ( ( A e. On /\ ph ) /\ (/) e. A ) -> ps ) |
3 |
1
|
ex |
|- ( ph -> ( A = (/) -> ps ) ) |
4 |
3
|
adantl |
|- ( ( A e. On /\ ph ) -> ( A = (/) -> ps ) ) |
5 |
|
on0eln0 |
|- ( A e. On -> ( (/) e. A <-> A =/= (/) ) ) |
6 |
5
|
adantr |
|- ( ( A e. On /\ ph ) -> ( (/) e. A <-> A =/= (/) ) ) |
7 |
2
|
ex |
|- ( ( A e. On /\ ph ) -> ( (/) e. A -> ps ) ) |
8 |
6 7
|
sylbird |
|- ( ( A e. On /\ ph ) -> ( A =/= (/) -> ps ) ) |
9 |
4 8
|
pm2.61dne |
|- ( ( A e. On /\ ph ) -> ps ) |