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 ∪ B ≈ ω → A ≈ ω ∨ B ≈ ω

Proof

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