Step |
Hyp |
Ref |
Expression |
1 |
|
ordtri2or2 |
|- ( ( Ord B /\ Ord C ) -> ( B C_ C \/ C C_ B ) ) |
2 |
1
|
orcomd |
|- ( ( Ord B /\ Ord C ) -> ( C C_ B \/ B C_ C ) ) |
3 |
|
ssequn2 |
|- ( C C_ B <-> ( B u. C ) = B ) |
4 |
|
eqeq1 |
|- ( A = ( B u. C ) -> ( A = B <-> ( B u. C ) = B ) ) |
5 |
3 4
|
bitr4id |
|- ( A = ( B u. C ) -> ( C C_ B <-> A = B ) ) |
6 |
|
ssequn1 |
|- ( B C_ C <-> ( B u. C ) = C ) |
7 |
|
eqeq1 |
|- ( A = ( B u. C ) -> ( A = C <-> ( B u. C ) = C ) ) |
8 |
6 7
|
bitr4id |
|- ( A = ( B u. C ) -> ( B C_ C <-> A = C ) ) |
9 |
5 8
|
orbi12d |
|- ( A = ( B u. C ) -> ( ( C C_ B \/ B C_ C ) <-> ( A = B \/ A = C ) ) ) |
10 |
2 9
|
syl5ibcom |
|- ( ( Ord B /\ Ord C ) -> ( A = ( B u. C ) -> ( A = B \/ A = C ) ) ) |