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 ( ( 𝐴 ∪ 𝐵 ) ≈ ω → ( 𝐴 ≈ ω ∨ 𝐵 ≈ ω ) )

Proof

Step Hyp Ref Expression
1 unfi2 ⊢ ( ( 𝐴 ≺ ω ∧ 𝐵 ≺ ω ) → ( 𝐴 ∪ 𝐵 ) ≺ ω )
2 sdomnen ⊢ ( ( 𝐴 ∪ 𝐵 ) ≺ ω → ¬ ( 𝐴 ∪ 𝐵 ) ≈ ω )
3 1 2 syl ⊢ ( ( 𝐴 ≺ ω ∧ 𝐵 ≺ ω ) → ¬ ( 𝐴 ∪ 𝐵 ) ≈ ω )
4 3 con2i ⊢ ( ( 𝐴 ∪ 𝐵 ) ≈ ω → ¬ ( 𝐴 ≺ ω ∧ 𝐵 ≺ ω ) )
5 ianor ⊢ ( ¬ ( 𝐴 ≺ ω ∧ 𝐵 ≺ ω ) ↔ ( ¬ 𝐴 ≺ ω ∨ ¬ 𝐵 ≺ ω ) )
6 relen ⊢ Rel ≈
7 6 brrelex1i ⊢ ( ( 𝐴 ∪ 𝐵 ) ≈ ω → ( 𝐴 ∪ 𝐵 ) ∈ V )
8 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
9 ssdomg ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) → 𝐴 ≼ ( 𝐴 ∪ 𝐵 ) ) )
10 7 8 9 mpisyl ⊢ ( ( 𝐴 ∪ 𝐵 ) ≈ ω → 𝐴 ≼ ( 𝐴 ∪ 𝐵 ) )
11 domentr ⊢ ( ( 𝐴 ≼ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ≈ ω ) → 𝐴 ≼ ω )
12 10 11 mpancom ⊢ ( ( 𝐴 ∪ 𝐵 ) ≈ ω → 𝐴 ≼ ω )
13 12 anim1i ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ≈ ω ∧ ¬ 𝐴 ≺ ω ) → ( 𝐴 ≼ ω ∧ ¬ 𝐴 ≺ ω ) )
14 bren2 ⊢ ( 𝐴 ≈ ω ↔ ( 𝐴 ≼ ω ∧ ¬ 𝐴 ≺ ω ) )
15 13 14 sylibr ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ≈ ω ∧ ¬ 𝐴 ≺ ω ) → 𝐴 ≈ ω )
16 15 ex ⊢ ( ( 𝐴 ∪ 𝐵 ) ≈ ω → ( ¬ 𝐴 ≺ ω → 𝐴 ≈ ω ) )
17 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
18 ssdomg ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) → 𝐵 ≼ ( 𝐴 ∪ 𝐵 ) ) )
19 7 17 18 mpisyl ⊢ ( ( 𝐴 ∪ 𝐵 ) ≈ ω → 𝐵 ≼ ( 𝐴 ∪ 𝐵 ) )
20 domentr ⊢ ( ( 𝐵 ≼ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ≈ ω ) → 𝐵 ≼ ω )
21 19 20 mpancom ⊢ ( ( 𝐴 ∪ 𝐵 ) ≈ ω → 𝐵 ≼ ω )
22 21 anim1i ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ≈ ω ∧ ¬ 𝐵 ≺ ω ) → ( 𝐵 ≼ ω ∧ ¬ 𝐵 ≺ ω ) )
23 bren2 ⊢ ( 𝐵 ≈ ω ↔ ( 𝐵 ≼ ω ∧ ¬ 𝐵 ≺ ω ) )
24 22 23 sylibr ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ≈ ω ∧ ¬ 𝐵 ≺ ω ) → 𝐵 ≈ ω )
25 24 ex ⊢ ( ( 𝐴 ∪ 𝐵 ) ≈ ω → ( ¬ 𝐵 ≺ ω → 𝐵 ≈ ω ) )
26 16 25 orim12d ⊢ ( ( 𝐴 ∪ 𝐵 ) ≈ ω → ( ( ¬ 𝐴 ≺ ω ∨ ¬ 𝐵 ≺ ω ) → ( 𝐴 ≈ ω ∨ 𝐵 ≈ ω ) ) )
27 5 26 syl5bi ⊢ ( ( 𝐴 ∪ 𝐵 ) ≈ ω → ( ¬ ( 𝐴 ≺ ω ∧ 𝐵 ≺ ω ) → ( 𝐴 ≈ ω ∨ 𝐵 ≈ ω ) ) )
28 4 27 mpd ⊢ ( ( 𝐴 ∪ 𝐵 ) ≈ ω → ( 𝐴 ≈ ω ∨ 𝐵 ≈ ω ) )