Metamath Proof Explorer

Theorem cdainflem

Description: Any partition of omega into two pieces (which may be disjoint) contains an infinite subset. (Contributed by Mario Carneiro, 11-Feb-2013)

Ref Expression
Assertion cdainflem 
|- ( ( A u. B ) ~~ _om -> ( A ~~ _om \/ B ~~ _om ) )

Proof

Step Hyp Ref Expression
1 unfi2 
 |-  ( ( A ~< _om /\ B ~< _om ) -> ( A u. B ) ~< _om )
2 sdomnen 
 |-  ( ( A u. B ) ~< _om -> -. ( A u. B ) ~~ _om )
3 1 2 syl 
 |-  ( ( A ~< _om /\ B ~< _om ) -> -. ( A u. B ) ~~ _om )
4 3 con2i 
 |-  ( ( A u. B ) ~~ _om -> -. ( A ~< _om /\ B ~< _om ) )
5 ianor 
 |-  ( -. ( A ~< _om /\ B ~< _om ) <-> ( -. A ~< _om \/ -. B ~< _om ) )
6 relen 
 |-  Rel ~~
7 6 brrelex1i 
 |-  ( ( A u. B ) ~~ _om -> ( A u. B ) e. _V )
8 ssun1 
 |-  A C_ ( A u. B )
9 ssdomg 
 |-  ( ( A u. B ) e. _V -> ( A C_ ( A u. B ) -> A ~<_ ( A u. B ) ) )
10 7 8 9 mpisyl 
 |-  ( ( A u. B ) ~~ _om -> A ~<_ ( A u. B ) )
11 domentr 
 |-  ( ( A ~<_ ( A u. B ) /\ ( A u. B ) ~~ _om ) -> A ~<_ _om )
12 10 11 mpancom 
 |-  ( ( A u. B ) ~~ _om -> A ~<_ _om )
13 12 anim1i 
 |-  ( ( ( A u. B ) ~~ _om /\ -. A ~< _om ) -> ( A ~<_ _om /\ -. A ~< _om ) )
14 bren2 
 |-  ( A ~~ _om <-> ( A ~<_ _om /\ -. A ~< _om ) )
15 13 14 sylibr 
 |-  ( ( ( A u. B ) ~~ _om /\ -. A ~< _om ) -> A ~~ _om )
16 15 ex 
 |-  ( ( A u. B ) ~~ _om -> ( -. A ~< _om -> A ~~ _om ) )
17 ssun2 
 |-  B C_ ( A u. B )
18 ssdomg 
 |-  ( ( A u. B ) e. _V -> ( B C_ ( A u. B ) -> B ~<_ ( A u. B ) ) )
19 7 17 18 mpisyl 
 |-  ( ( A u. B ) ~~ _om -> B ~<_ ( A u. B ) )
20 domentr 
 |-  ( ( B ~<_ ( A u. B ) /\ ( A u. B ) ~~ _om ) -> B ~<_ _om )
21 19 20 mpancom 
 |-  ( ( A u. B ) ~~ _om -> B ~<_ _om )
22 21 anim1i 
 |-  ( ( ( A u. B ) ~~ _om /\ -. B ~< _om ) -> ( B ~<_ _om /\ -. B ~< _om ) )
23 bren2 
 |-  ( B ~~ _om <-> ( B ~<_ _om /\ -. B ~< _om ) )
24 22 23 sylibr 
 |-  ( ( ( A u. B ) ~~ _om /\ -. B ~< _om ) -> B ~~ _om )
25 24 ex 
 |-  ( ( A u. B ) ~~ _om -> ( -. B ~< _om -> B ~~ _om ) )
26 16 25 orim12d 
 |-  ( ( A u. B ) ~~ _om -> ( ( -. A ~< _om \/ -. B ~< _om ) -> ( A ~~ _om \/ B ~~ _om ) ) )
27 5 26 syl5bi 
 |-  ( ( A u. B ) ~~ _om -> ( -. ( A ~< _om /\ B ~< _om ) -> ( A ~~ _om \/ B ~~ _om ) ) )
28 4 27 mpd 
 |-  ( ( A u. B ) ~~ _om -> ( A ~~ _om \/ B ~~ _om ) )