Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( A u. B ) = ( A u. B ) |
2 |
|
ordequn |
|- ( ( Ord A /\ Ord B ) -> ( ( A u. B ) = ( A u. B ) -> ( ( A u. B ) = A \/ ( A u. B ) = B ) ) ) |
3 |
1 2
|
mpi |
|- ( ( Ord A /\ Ord B ) -> ( ( A u. B ) = A \/ ( A u. B ) = B ) ) |
4 |
|
ordeq |
|- ( ( A u. B ) = A -> ( Ord ( A u. B ) <-> Ord A ) ) |
5 |
4
|
biimprcd |
|- ( Ord A -> ( ( A u. B ) = A -> Ord ( A u. B ) ) ) |
6 |
|
ordeq |
|- ( ( A u. B ) = B -> ( Ord ( A u. B ) <-> Ord B ) ) |
7 |
6
|
biimprcd |
|- ( Ord B -> ( ( A u. B ) = B -> Ord ( A u. B ) ) ) |
8 |
5 7
|
jaao |
|- ( ( Ord A /\ Ord B ) -> ( ( ( A u. B ) = A \/ ( A u. B ) = B ) -> Ord ( A u. B ) ) ) |
9 |
3 8
|
mpd |
|- ( ( Ord A /\ Ord B ) -> Ord ( A u. B ) ) |