Step |
Hyp |
Ref |
Expression |
1 |
|
ssequn1 |
|- ( A C_ B <-> ( A u. B ) = B ) |
2 |
|
eleq1a |
|- ( B e. On -> ( ( A u. B ) = B -> ( A u. B ) e. On ) ) |
3 |
2
|
adantl |
|- ( ( A e. On /\ B e. On ) -> ( ( A u. B ) = B -> ( A u. B ) e. On ) ) |
4 |
1 3
|
syl5bi |
|- ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A u. B ) e. On ) ) |
5 |
|
ssequn2 |
|- ( B C_ A <-> ( A u. B ) = A ) |
6 |
|
eleq1a |
|- ( A e. On -> ( ( A u. B ) = A -> ( A u. B ) e. On ) ) |
7 |
6
|
adantr |
|- ( ( A e. On /\ B e. On ) -> ( ( A u. B ) = A -> ( A u. B ) e. On ) ) |
8 |
5 7
|
syl5bi |
|- ( ( A e. On /\ B e. On ) -> ( B C_ A -> ( A u. B ) e. On ) ) |
9 |
|
eloni |
|- ( A e. On -> Ord A ) |
10 |
|
eloni |
|- ( B e. On -> Ord B ) |
11 |
|
ordtri2or2 |
|- ( ( Ord A /\ Ord B ) -> ( A C_ B \/ B C_ A ) ) |
12 |
9 10 11
|
syl2an |
|- ( ( A e. On /\ B e. On ) -> ( A C_ B \/ B C_ A ) ) |
13 |
4 8 12
|
mpjaod |
|- ( ( A e. On /\ B e. On ) -> ( A u. B ) e. On ) |