Step |
Hyp |
Ref |
Expression |
1 |
|
eloni |
|- ( A e. On -> Ord A ) |
2 |
|
ordn2lp |
|- ( Ord A -> -. ( A e. B /\ B e. A ) ) |
3 |
|
pm3.13 |
|- ( -. ( A e. B /\ B e. A ) -> ( -. A e. B \/ -. B e. A ) ) |
4 |
1 2 3
|
3syl |
|- ( A e. On -> ( -. A e. B \/ -. B e. A ) ) |
5 |
4
|
adantr |
|- ( ( A e. On /\ B e. On ) -> ( -. A e. B \/ -. B e. A ) ) |
6 |
|
eqimss |
|- ( suc A = suc B -> suc A C_ suc B ) |
7 |
|
sucssel |
|- ( A e. On -> ( suc A C_ suc B -> A e. suc B ) ) |
8 |
6 7
|
syl5 |
|- ( A e. On -> ( suc A = suc B -> A e. suc B ) ) |
9 |
|
elsuci |
|- ( A e. suc B -> ( A e. B \/ A = B ) ) |
10 |
9
|
ord |
|- ( A e. suc B -> ( -. A e. B -> A = B ) ) |
11 |
10
|
com12 |
|- ( -. A e. B -> ( A e. suc B -> A = B ) ) |
12 |
8 11
|
syl9 |
|- ( A e. On -> ( -. A e. B -> ( suc A = suc B -> A = B ) ) ) |
13 |
|
eqimss2 |
|- ( suc A = suc B -> suc B C_ suc A ) |
14 |
|
sucssel |
|- ( B e. On -> ( suc B C_ suc A -> B e. suc A ) ) |
15 |
13 14
|
syl5 |
|- ( B e. On -> ( suc A = suc B -> B e. suc A ) ) |
16 |
|
elsuci |
|- ( B e. suc A -> ( B e. A \/ B = A ) ) |
17 |
16
|
ord |
|- ( B e. suc A -> ( -. B e. A -> B = A ) ) |
18 |
|
eqcom |
|- ( B = A <-> A = B ) |
19 |
17 18
|
syl6ib |
|- ( B e. suc A -> ( -. B e. A -> A = B ) ) |
20 |
19
|
com12 |
|- ( -. B e. A -> ( B e. suc A -> A = B ) ) |
21 |
15 20
|
syl9 |
|- ( B e. On -> ( -. B e. A -> ( suc A = suc B -> A = B ) ) ) |
22 |
12 21
|
jaao |
|- ( ( A e. On /\ B e. On ) -> ( ( -. A e. B \/ -. B e. A ) -> ( suc A = suc B -> A = B ) ) ) |
23 |
5 22
|
mpd |
|- ( ( A e. On /\ B e. On ) -> ( suc A = suc B -> A = B ) ) |
24 |
|
suceq |
|- ( A = B -> suc A = suc B ) |
25 |
23 24
|
impbid1 |
|- ( ( A e. On /\ B e. On ) -> ( suc A = suc B <-> A = B ) ) |