Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( A ~<_ _om /\ A =/= (/) ) -> A =/= (/) ) |
2 |
|
reldom |
|- Rel ~<_ |
3 |
2
|
a1i |
|- ( A ~<_ _om -> Rel ~<_ ) |
4 |
|
brrelex1 |
|- ( ( Rel ~<_ /\ A ~<_ _om ) -> A e. _V ) |
5 |
3 4
|
mpancom |
|- ( A ~<_ _om -> A e. _V ) |
6 |
|
0sdomg |
|- ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) ) |
7 |
5 6
|
syl |
|- ( A ~<_ _om -> ( (/) ~< A <-> A =/= (/) ) ) |
8 |
7
|
adantr |
|- ( ( A ~<_ _om /\ A =/= (/) ) -> ( (/) ~< A <-> A =/= (/) ) ) |
9 |
1 8
|
mpbird |
|- ( ( A ~<_ _om /\ A =/= (/) ) -> (/) ~< A ) |
10 |
|
nnenom |
|- NN ~~ _om |
11 |
10
|
ensymi |
|- _om ~~ NN |
12 |
11
|
a1i |
|- ( A ~<_ _om -> _om ~~ NN ) |
13 |
|
domentr |
|- ( ( A ~<_ _om /\ _om ~~ NN ) -> A ~<_ NN ) |
14 |
12 13
|
mpdan |
|- ( A ~<_ _om -> A ~<_ NN ) |
15 |
14
|
adantr |
|- ( ( A ~<_ _om /\ A =/= (/) ) -> A ~<_ NN ) |
16 |
|
fodomr |
|- ( ( (/) ~< A /\ A ~<_ NN ) -> E. f f : NN -onto-> A ) |
17 |
9 15 16
|
syl2anc |
|- ( ( A ~<_ _om /\ A =/= (/) ) -> E. f f : NN -onto-> A ) |