This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )