Step |
Hyp |
Ref |
Expression |
1 |
|
sdomdom |
|- ( A ~< B -> A ~<_ B ) |
2 |
|
infunsdom1 |
|- ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) -> ( A u. B ) ~< X ) |
3 |
2
|
anass1rs |
|- ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ B ~< X ) /\ A ~<_ B ) -> ( A u. B ) ~< X ) |
4 |
3
|
adantlrl |
|- ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~< X /\ B ~< X ) ) /\ A ~<_ B ) -> ( A u. B ) ~< X ) |
5 |
1 4
|
sylan2 |
|- ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~< X /\ B ~< X ) ) /\ A ~< B ) -> ( A u. B ) ~< X ) |
6 |
|
simpll |
|- ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~< X /\ B ~< X ) ) -> X e. dom card ) |
7 |
|
sdomdom |
|- ( B ~< X -> B ~<_ X ) |
8 |
7
|
ad2antll |
|- ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~< X /\ B ~< X ) ) -> B ~<_ X ) |
9 |
|
numdom |
|- ( ( X e. dom card /\ B ~<_ X ) -> B e. dom card ) |
10 |
6 8 9
|
syl2anc |
|- ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~< X /\ B ~< X ) ) -> B e. dom card ) |
11 |
|
sdomdom |
|- ( A ~< X -> A ~<_ X ) |
12 |
11
|
ad2antrl |
|- ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~< X /\ B ~< X ) ) -> A ~<_ X ) |
13 |
|
numdom |
|- ( ( X e. dom card /\ A ~<_ X ) -> A e. dom card ) |
14 |
6 12 13
|
syl2anc |
|- ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~< X /\ B ~< X ) ) -> A e. dom card ) |
15 |
|
domtri2 |
|- ( ( B e. dom card /\ A e. dom card ) -> ( B ~<_ A <-> -. A ~< B ) ) |
16 |
10 14 15
|
syl2anc |
|- ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~< X /\ B ~< X ) ) -> ( B ~<_ A <-> -. A ~< B ) ) |
17 |
16
|
biimpar |
|- ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~< X /\ B ~< X ) ) /\ -. A ~< B ) -> B ~<_ A ) |
18 |
|
uncom |
|- ( A u. B ) = ( B u. A ) |
19 |
|
infunsdom1 |
|- ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( B ~<_ A /\ A ~< X ) ) -> ( B u. A ) ~< X ) |
20 |
18 19
|
eqbrtrid |
|- ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( B ~<_ A /\ A ~< X ) ) -> ( A u. B ) ~< X ) |
21 |
20
|
anass1rs |
|- ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ A ~< X ) /\ B ~<_ A ) -> ( A u. B ) ~< X ) |
22 |
21
|
adantlrr |
|- ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~< X /\ B ~< X ) ) /\ B ~<_ A ) -> ( A u. B ) ~< X ) |
23 |
17 22
|
syldan |
|- ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~< X /\ B ~< X ) ) /\ -. A ~< B ) -> ( A u. B ) ~< X ) |
24 |
5 23
|
pm2.61dan |
|- ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~< X /\ B ~< X ) ) -> ( A u. B ) ~< X ) |