Description: Lemma for alephfp . (Contributed by NM, 6-Nov-2004)
Ref | Expression | ||
---|---|---|---|
Hypothesis | alephfplem.1 | |
|
Assertion | alephfplem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alephfplem.1 | |
|
2 | omex | |
|
3 | fr0g | |
|
4 | 2 3 | ax-mp | |
5 | 1 | fveq1i | |
6 | aleph0 | |
|
7 | 4 5 6 | 3eqtr4i | |
8 | alephfnon | |
|
9 | 0elon | |
|
10 | fnfvelrn | |
|
11 | 8 9 10 | mp2an | |
12 | 7 11 | eqeltri | |