Step |
Hyp |
Ref |
Expression |
1 |
|
alephord2 |
|- ( ( B e. On /\ A e. On ) -> ( B e. A <-> ( aleph ` B ) e. ( aleph ` A ) ) ) |
2 |
1
|
ancoms |
|- ( ( A e. On /\ B e. On ) -> ( B e. A <-> ( aleph ` B ) e. ( aleph ` A ) ) ) |
3 |
2
|
notbid |
|- ( ( A e. On /\ B e. On ) -> ( -. B e. A <-> -. ( aleph ` B ) e. ( aleph ` A ) ) ) |
4 |
|
ontri1 |
|- ( ( A e. On /\ B e. On ) -> ( A C_ B <-> -. B e. A ) ) |
5 |
|
alephon |
|- ( aleph ` A ) e. On |
6 |
|
alephon |
|- ( aleph ` B ) e. On |
7 |
|
ontri1 |
|- ( ( ( aleph ` A ) e. On /\ ( aleph ` B ) e. On ) -> ( ( aleph ` A ) C_ ( aleph ` B ) <-> -. ( aleph ` B ) e. ( aleph ` A ) ) ) |
8 |
5 6 7
|
mp2an |
|- ( ( aleph ` A ) C_ ( aleph ` B ) <-> -. ( aleph ` B ) e. ( aleph ` A ) ) |
9 |
8
|
a1i |
|- ( ( A e. On /\ B e. On ) -> ( ( aleph ` A ) C_ ( aleph ` B ) <-> -. ( aleph ` B ) e. ( aleph ` A ) ) ) |
10 |
3 4 9
|
3bitr4d |
|- ( ( A e. On /\ B e. On ) -> ( A C_ B <-> ( aleph ` A ) C_ ( aleph ` B ) ) ) |