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	$$⊢\left(A\cup B\right)\approx \mathrm{\omega }\to \left(A\approx \mathrm{\omega }\vee B\approx \mathrm{\omega }\right)$$

Proof

Step	Hyp	Ref	Expression
1		unfi2	$$⊢\left(A\prec \mathrm{\omega }\wedge B\prec \mathrm{\omega }\right)\to \left(A\cup B\right)\prec \mathrm{\omega }$$
2		sdomnen	$$⊢\left(A\cup B\right)\prec \mathrm{\omega }\to \neg \left(A\cup B\right)\approx \mathrm{\omega }$$
3	1 2	syl	$$⊢\left(A\prec \mathrm{\omega }\wedge B\prec \mathrm{\omega }\right)\to \neg \left(A\cup B\right)\approx \mathrm{\omega }$$
4	3	con2i	$$⊢\left(A\cup B\right)\approx \mathrm{\omega }\to \neg \left(A\prec \mathrm{\omega }\wedge B\prec \mathrm{\omega }\right)$$
5		ianor	$$⊢\neg \left(A\prec \mathrm{\omega }\wedge B\prec \mathrm{\omega }\right)\leftrightarrow \left(\neg A\prec \mathrm{\omega }\vee \neg B\prec \mathrm{\omega }\right)$$
6		relen	$$⊢\mathrm{Rel}\approx$$
7	6	brrelex1i	$$⊢\left(A\cup B\right)\approx \mathrm{\omega }\to A\cup B\in \mathrm{V}$$
8		ssun1	$$⊢A\subseteq A\cup B$$
9		ssdomg	$$⊢A\cup B\in \mathrm{V}\to \left(A\subseteq A\cup B\to A\preccurlyeq \left(A\cup B\right)\right)$$
10	7 8 9	mpisyl	$$⊢\left(A\cup B\right)\approx \mathrm{\omega }\to A\preccurlyeq \left(A\cup B\right)$$
11		domentr	$$⊢\left(A\preccurlyeq \left(A\cup B\right)\wedge \left(A\cup B\right)\approx \mathrm{\omega }\right)\to A\preccurlyeq \mathrm{\omega }$$
12	10 11	mpancom	$$⊢\left(A\cup B\right)\approx \mathrm{\omega }\to A\preccurlyeq \mathrm{\omega }$$
13	12	anim1i	$$⊢\left(\left(A\cup B\right)\approx \mathrm{\omega }\wedge \neg A\prec \mathrm{\omega }\right)\to \left(A\preccurlyeq \mathrm{\omega }\wedge \neg A\prec \mathrm{\omega }\right)$$
14		bren2	$$⊢A\approx \mathrm{\omega }\leftrightarrow \left(A\preccurlyeq \mathrm{\omega }\wedge \neg A\prec \mathrm{\omega }\right)$$
15	13 14	sylibr	$$⊢\left(\left(A\cup B\right)\approx \mathrm{\omega }\wedge \neg A\prec \mathrm{\omega }\right)\to A\approx \mathrm{\omega }$$
16	15	ex	$$⊢\left(A\cup B\right)\approx \mathrm{\omega }\to \left(\neg A\prec \mathrm{\omega }\to A\approx \mathrm{\omega }\right)$$
17		ssun2	$$⊢B\subseteq A\cup B$$
18		ssdomg	$$⊢A\cup B\in \mathrm{V}\to \left(B\subseteq A\cup B\to B\preccurlyeq \left(A\cup B\right)\right)$$
19	7 17 18	mpisyl	$$⊢\left(A\cup B\right)\approx \mathrm{\omega }\to B\preccurlyeq \left(A\cup B\right)$$
20		domentr	$$⊢\left(B\preccurlyeq \left(A\cup B\right)\wedge \left(A\cup B\right)\approx \mathrm{\omega }\right)\to B\preccurlyeq \mathrm{\omega }$$
21	19 20	mpancom	$$⊢\left(A\cup B\right)\approx \mathrm{\omega }\to B\preccurlyeq \mathrm{\omega }$$
22	21	anim1i	$$⊢\left(\left(A\cup B\right)\approx \mathrm{\omega }\wedge \neg B\prec \mathrm{\omega }\right)\to \left(B\preccurlyeq \mathrm{\omega }\wedge \neg B\prec \mathrm{\omega }\right)$$
23		bren2	$$⊢B\approx \mathrm{\omega }\leftrightarrow \left(B\preccurlyeq \mathrm{\omega }\wedge \neg B\prec \mathrm{\omega }\right)$$
24	22 23	sylibr	$$⊢\left(\left(A\cup B\right)\approx \mathrm{\omega }\wedge \neg B\prec \mathrm{\omega }\right)\to B\approx \mathrm{\omega }$$
25	24	ex	$$⊢\left(A\cup B\right)\approx \mathrm{\omega }\to \left(\neg B\prec \mathrm{\omega }\to B\approx \mathrm{\omega }\right)$$
26	16 25	orim12d	$$⊢\left(A\cup B\right)\approx \mathrm{\omega }\to \left(\left(\neg A\prec \mathrm{\omega }\vee \neg B\prec \mathrm{\omega }\right)\to \left(A\approx \mathrm{\omega }\vee B\approx \mathrm{\omega }\right)\right)$$
27	5 26	biimtrid	$$⊢\left(A\cup B\right)\approx \mathrm{\omega }\to \left(\neg \left(A\prec \mathrm{\omega }\wedge B\prec \mathrm{\omega }\right)\to \left(A\approx \mathrm{\omega }\vee B\approx \mathrm{\omega }\right)\right)$$
28	4 27	mpd	$$⊢\left(A\cup B\right)\approx \mathrm{\omega }\to \left(A\approx \mathrm{\omega }\vee B\approx \mathrm{\omega }\right)$$