Metamath Proof Explorer


Theorem infunsdom

Description: The union of two sets that are strictly dominated by the infinite set X is also strictly dominated by X . (Contributed by Mario Carneiro, 3-May-2015)

Ref Expression
Assertion infunsdom
|- ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~< X /\ B ~< X ) ) -> ( A u. B ) ~< X )

Proof

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 )