Step |
Hyp |
Ref |
Expression |
1 |
|
php2 |
|- ( ( A e. _om /\ B C. A ) -> B ~< A ) |
2 |
1
|
ex |
|- ( A e. _om -> ( B C. A -> B ~< A ) ) |
3 |
|
domnsym |
|- ( A ~<_ B -> -. B ~< A ) |
4 |
2 3
|
nsyli |
|- ( A e. _om -> ( A ~<_ B -> -. B C. A ) ) |
5 |
4
|
adantr |
|- ( ( A e. _om /\ B e. On ) -> ( A ~<_ B -> -. B C. A ) ) |
6 |
|
nnord |
|- ( A e. _om -> Ord A ) |
7 |
|
eloni |
|- ( B e. On -> Ord B ) |
8 |
|
ordtri1 |
|- ( ( Ord A /\ Ord B ) -> ( A C_ B <-> -. B e. A ) ) |
9 |
|
ordelpss |
|- ( ( Ord B /\ Ord A ) -> ( B e. A <-> B C. A ) ) |
10 |
9
|
ancoms |
|- ( ( Ord A /\ Ord B ) -> ( B e. A <-> B C. A ) ) |
11 |
10
|
notbid |
|- ( ( Ord A /\ Ord B ) -> ( -. B e. A <-> -. B C. A ) ) |
12 |
8 11
|
bitrd |
|- ( ( Ord A /\ Ord B ) -> ( A C_ B <-> -. B C. A ) ) |
13 |
6 7 12
|
syl2an |
|- ( ( A e. _om /\ B e. On ) -> ( A C_ B <-> -. B C. A ) ) |
14 |
5 13
|
sylibrd |
|- ( ( A e. _om /\ B e. On ) -> ( A ~<_ B -> A C_ B ) ) |
15 |
|
ssdomg |
|- ( B e. On -> ( A C_ B -> A ~<_ B ) ) |
16 |
15
|
adantl |
|- ( ( A e. _om /\ B e. On ) -> ( A C_ B -> A ~<_ B ) ) |
17 |
14 16
|
impbid |
|- ( ( A e. _om /\ B e. On ) -> ( A ~<_ B <-> A C_ B ) ) |