Metamath Proof Explorer

Theorem infunsdom1

Description: The union of two sets that are strictly dominated by the infinite set X is also dominated by X . This version of infunsdom assumes additionally that A is the smaller of the two. (Contributed by Mario Carneiro, 14-Dec-2013) (Revised by Mario Carneiro, 3-May-2015)

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

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) -> A ~<_ B )
2 domsdomtr 
 |-  ( ( A ~<_ B /\ B ~< _om ) -> A ~< _om )
3 1 2 sylan 
 |-  ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) /\ B ~< _om ) -> A ~< _om )
4 unfi2 
 |-  ( ( A ~< _om /\ B ~< _om ) -> ( A u. B ) ~< _om )
5 3 4 sylancom 
 |-  ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) /\ B ~< _om ) -> ( A u. B ) ~< _om )
6 simpllr 
 |-  ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) /\ B ~< _om ) -> _om ~<_ X )
7 sdomdomtr 
 |-  ( ( ( A u. B ) ~< _om /\ _om ~<_ X ) -> ( A u. B ) ~< X )
8 5 6 7 syl2anc 
 |-  ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) /\ B ~< _om ) -> ( A u. B ) ~< X )
9 omelon 
 |-  _om e. On
10 onenon 
 |-  ( _om e. On -> _om e. dom card )
11 9 10 ax-mp 
 |-  _om e. dom card
12 simpll 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) -> X e. dom card )
13 sdomdom 
 |-  ( B ~< X -> B ~<_ X )
14 13 ad2antll 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) -> B ~<_ X )
15 numdom 
 |-  ( ( X e. dom card /\ B ~<_ X ) -> B e. dom card )
16 12 14 15 syl2anc 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) -> B e. dom card )
17 domtri2 
 |-  ( ( _om e. dom card /\ B e. dom card ) -> ( _om ~<_ B <-> -. B ~< _om ) )
18 11 16 17 sylancr 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) -> ( _om ~<_ B <-> -. B ~< _om ) )
19 18 biimpar 
 |-  ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) /\ -. B ~< _om ) -> _om ~<_ B )
20 uncom 
 |-  ( A u. B ) = ( B u. A )
21 16 adantr 
 |-  ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) /\ _om ~<_ B ) -> B e. dom card )
22 simpr 
 |-  ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) /\ _om ~<_ B ) -> _om ~<_ B )
23 1 adantr 
 |-  ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) /\ _om ~<_ B ) -> A ~<_ B )
24 infunabs 
 |-  ( ( B e. dom card /\ _om ~<_ B /\ A ~<_ B ) -> ( B u. A ) ~~ B )
25 21 22 23 24 syl3anc 
 |-  ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) /\ _om ~<_ B ) -> ( B u. A ) ~~ B )
26 20 25 eqbrtrid 
 |-  ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) /\ _om ~<_ B ) -> ( A u. B ) ~~ B )
27 simplrr 
 |-  ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) /\ _om ~<_ B ) -> B ~< X )
28 ensdomtr 
 |-  ( ( ( A u. B ) ~~ B /\ B ~< X ) -> ( A u. B ) ~< X )
29 26 27 28 syl2anc 
 |-  ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) /\ _om ~<_ B ) -> ( A u. B ) ~< X )
30 19 29 syldan 
 |-  ( ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) /\ -. B ~< _om ) -> ( A u. B ) ~< X )
31 8 30 pm2.61dan 
 |-  ( ( ( X e. dom card /\ _om ~<_ X ) /\ ( A ~<_ B /\ B ~< X ) ) -> ( A u. B ) ~< X )