Description: Ordering property of the aleph function. Theorem 66 of Suppes p. 229. (Contributed by NM, 25-Oct-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | alephord2i | |- ( B e. On -> ( A e. B -> ( aleph ` A ) e. ( aleph ` B ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | onelon | |- ( ( B e. On /\ A e. B ) -> A e. On ) |
|
2 | alephord2 | |- ( ( A e. On /\ B e. On ) -> ( A e. B <-> ( aleph ` A ) e. ( aleph ` B ) ) ) |
|
3 | 2 | biimpd | |- ( ( A e. On /\ B e. On ) -> ( A e. B -> ( aleph ` A ) e. ( aleph ` B ) ) ) |
4 | 3 | expimpd | |- ( A e. On -> ( ( B e. On /\ A e. B ) -> ( aleph ` A ) e. ( aleph ` B ) ) ) |
5 | 1 4 | mpcom | |- ( ( B e. On /\ A e. B ) -> ( aleph ` A ) e. ( aleph ` B ) ) |
6 | 5 | ex | |- ( B e. On -> ( A e. B -> ( aleph ` A ) e. ( aleph ` B ) ) ) |