Theorem cfslb2n

Description: Any small collection of small subsets of A cannot have union A , where "small" means smaller than the cofinality. This is a stronger version of cfslb . This is a common application of cofinality: under AC, ( aleph1 ) is regular, so it is not a countable union of countable sets. (Contributed by Mario Carneiro, 24-Jun-2013)

	Ref	Expression
Hypothesis	cfslb.1	$$⊢A\in \mathrm{V}$$
Assertion	cfslb2n	$$⊢\left(\mathrm{Lim}A\wedge \forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\right)\to \left(B\prec \mathrm{cf}\left(A\right)\to \bigcup B\ne A\right)$$

Proof

Step	Hyp	Ref	Expression
1		cfslb.1	$$⊢A\in \mathrm{V}$$
2		limord	$$⊢\mathrm{Lim}A\to \mathrm{Ord}A$$
3		ordsson	$$⊢\mathrm{Ord}A\to A\subseteq \mathrm{On}$$
4		sstr	$$⊢\left(x\subseteq A\wedge A\subseteq \mathrm{On}\right)\to x\subseteq \mathrm{On}$$
5	4	expcom	$$⊢A\subseteq \mathrm{On}\to \left(x\subseteq A\to x\subseteq \mathrm{On}\right)$$
6	2 3 5	3syl	$$⊢\mathrm{Lim}A\to \left(x\subseteq A\to x\subseteq \mathrm{On}\right)$$
7		onsucuni	$$⊢x\subseteq \mathrm{On}\to x\subseteq \mathrm{suc}\bigcup x$$
8	6 7	syl6	$$⊢\mathrm{Lim}A\to \left(x\subseteq A\to x\subseteq \mathrm{suc}\bigcup x\right)$$
9	8	adantrd	$$⊢\mathrm{Lim}A\to \left(\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\to x\subseteq \mathrm{suc}\bigcup x\right)$$
10	9	ralimdv	$$⊢\mathrm{Lim}A\to \left(\forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\to \forall x\in Bx\subseteq \mathrm{suc}\bigcup x\right)$$
11		uniiun	$$⊢\bigcup B=\bigcup _{x\in B}x$$
12		ss2iun	$$⊢\forall x\in Bx\subseteq \mathrm{suc}\bigcup x\to \bigcup _{x\in B}x\subseteq \bigcup _{x\in B}\mathrm{suc}\bigcup x$$
13	11 12	eqsstrid	$$⊢\forall x\in Bx\subseteq \mathrm{suc}\bigcup x\to \bigcup B\subseteq \bigcup _{x\in B}\mathrm{suc}\bigcup x$$
14	10 13	syl6	$$⊢\mathrm{Lim}A\to \left(\forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\to \bigcup B\subseteq \bigcup _{x\in B}\mathrm{suc}\bigcup x\right)$$
15	14	imp	$$⊢\left(\mathrm{Lim}A\wedge \forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\right)\to \bigcup B\subseteq \bigcup _{x\in B}\mathrm{suc}\bigcup x$$
16	1	cfslbn	$$⊢\left(\mathrm{Lim}A\wedge x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\to \bigcup x\in A$$
17	16	3expib	$$⊢\mathrm{Lim}A\to \left(\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\to \bigcup x\in A\right)$$
18		ordsucss	$$⊢\mathrm{Ord}A\to \left(\bigcup x\in A\to \mathrm{suc}\bigcup x\subseteq A\right)$$
19	2 17 18	sylsyld	$$⊢\mathrm{Lim}A\to \left(\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\to \mathrm{suc}\bigcup x\subseteq A\right)$$
20	19	ralimdv	$$⊢\mathrm{Lim}A\to \left(\forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\to \forall x\in B\mathrm{suc}\bigcup x\subseteq A\right)$$
21		iunss	$$⊢\bigcup _{x\in B}\mathrm{suc}\bigcup x\subseteq A\leftrightarrow \forall x\in B\mathrm{suc}\bigcup x\subseteq A$$
22	20 21	imbitrrdi	$$⊢\mathrm{Lim}A\to \left(\forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\to \bigcup _{x\in B}\mathrm{suc}\bigcup x\subseteq A\right)$$
23	22	imp	$$⊢\left(\mathrm{Lim}A\wedge \forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\right)\to \bigcup _{x\in B}\mathrm{suc}\bigcup x\subseteq A$$
24		sseq1	$$⊢\bigcup B=A\to \left(\bigcup B\subseteq \bigcup _{x\in B}\mathrm{suc}\bigcup x\leftrightarrow A\subseteq \bigcup _{x\in B}\mathrm{suc}\bigcup x\right)$$
25		eqss	$$⊢\bigcup _{x\in B}\mathrm{suc}\bigcup x=A\leftrightarrow \left(\bigcup _{x\in B}\mathrm{suc}\bigcup x\subseteq A\wedge A\subseteq \bigcup _{x\in B}\mathrm{suc}\bigcup x\right)$$
26	25	simplbi2com	$$⊢A\subseteq \bigcup _{x\in B}\mathrm{suc}\bigcup x\to \left(\bigcup _{x\in B}\mathrm{suc}\bigcup x\subseteq A\to \bigcup _{x\in B}\mathrm{suc}\bigcup x=A\right)$$
27	24 26	biimtrdi	$$⊢\bigcup B=A\to \left(\bigcup B\subseteq \bigcup _{x\in B}\mathrm{suc}\bigcup x\to \left(\bigcup _{x\in B}\mathrm{suc}\bigcup x\subseteq A\to \bigcup _{x\in B}\mathrm{suc}\bigcup x=A\right)\right)$$
28	27	com3l	$$⊢\bigcup B\subseteq \bigcup _{x\in B}\mathrm{suc}\bigcup x\to \left(\bigcup _{x\in B}\mathrm{suc}\bigcup x\subseteq A\to \left(\bigcup B=A\to \bigcup _{x\in B}\mathrm{suc}\bigcup x=A\right)\right)$$
29	15 23 28	sylc	$$⊢\left(\mathrm{Lim}A\wedge \forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\right)\to \left(\bigcup B=A\to \bigcup _{x\in B}\mathrm{suc}\bigcup x=A\right)$$
30		limsuc	$$⊢\mathrm{Lim}A\to \left(\bigcup x\in A\leftrightarrow \mathrm{suc}\bigcup x\in A\right)$$
31	17 30	sylibd	$$⊢\mathrm{Lim}A\to \left(\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\to \mathrm{suc}\bigcup x\in A\right)$$
32	31	ralimdv	$$⊢\mathrm{Lim}A\to \left(\forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\to \forall x\in B\mathrm{suc}\bigcup x\in A\right)$$
33	32	imp	$$⊢\left(\mathrm{Lim}A\wedge \forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\right)\to \forall x\in B\mathrm{suc}\bigcup x\in A$$
34		r19.29	$$⊢\left(\forall x\in B\mathrm{suc}\bigcup x\in A\wedge \exists x\in By=\mathrm{suc}\bigcup x\right)\to \exists x\in B\left(\mathrm{suc}\bigcup x\in A\wedge y=\mathrm{suc}\bigcup x\right)$$
35		eleq1	$$⊢y=\mathrm{suc}\bigcup x\to \left(y\in A\leftrightarrow \mathrm{suc}\bigcup x\in A\right)$$
36	35	biimparc	$$⊢\left(\mathrm{suc}\bigcup x\in A\wedge y=\mathrm{suc}\bigcup x\right)\to y\in A$$
37	36	rexlimivw	$$⊢\exists x\in B\left(\mathrm{suc}\bigcup x\in A\wedge y=\mathrm{suc}\bigcup x\right)\to y\in A$$
38	34 37	syl	$$⊢\left(\forall x\in B\mathrm{suc}\bigcup x\in A\wedge \exists x\in By=\mathrm{suc}\bigcup x\right)\to y\in A$$
39	38	ex	$$⊢\forall x\in B\mathrm{suc}\bigcup x\in A\to \left(\exists x\in By=\mathrm{suc}\bigcup x\to y\in A\right)$$
40	33 39	syl	$$⊢\left(\mathrm{Lim}A\wedge \forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\right)\to \left(\exists x\in By=\mathrm{suc}\bigcup x\to y\in A\right)$$
41	40	abssdv	$$⊢\left(\mathrm{Lim}A\wedge \forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\right)\to \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}\subseteq A$$
42		vuniex	$$⊢\bigcup x\in \mathrm{V}$$
43	42	sucex	$$⊢\mathrm{suc}\bigcup x\in \mathrm{V}$$
44	43	dfiun2	$$⊢\bigcup _{x\in B}\mathrm{suc}\bigcup x=\bigcup \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}$$
45	44	eqeq1i	$$⊢\bigcup _{x\in B}\mathrm{suc}\bigcup x=A\leftrightarrow \bigcup \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}=A$$
46	1	cfslb	$$⊢\left(\mathrm{Lim}A\wedge \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}\subseteq A\wedge \bigcup \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}=A\right)\to \mathrm{cf}\left(A\right)\preccurlyeq \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}$$
47	46	3expia	$$⊢\left(\mathrm{Lim}A\wedge \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}\subseteq A\right)\to \left(\bigcup \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}=A\to \mathrm{cf}\left(A\right)\preccurlyeq \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}\right)$$
48	45 47	biimtrid	$$⊢\left(\mathrm{Lim}A\wedge \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}\subseteq A\right)\to \left(\bigcup _{x\in B}\mathrm{suc}\bigcup x=A\to \mathrm{cf}\left(A\right)\preccurlyeq \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}\right)$$
49	41 48	syldan	$$⊢\left(\mathrm{Lim}A\wedge \forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\right)\to \left(\bigcup _{x\in B}\mathrm{suc}\bigcup x=A\to \mathrm{cf}\left(A\right)\preccurlyeq \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}\right)$$
50		eqid	$$⊢\left(x\in B⟼\mathrm{suc}\bigcup x\right)=\left(x\in B⟼\mathrm{suc}\bigcup x\right)$$
51	50	rnmpt	$$⊢\mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)=\left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}$$
52	43 50	fnmpti	$$⊢\left(x\in B⟼\mathrm{suc}\bigcup x\right)FnB$$
53		dffn4	$$⊢\left(x\in B⟼\mathrm{suc}\bigcup x\right)FnB\leftrightarrow \left(x\in B⟼\mathrm{suc}\bigcup x\right):B\underset{onto}{⟶}\mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)$$
54	52 53	mpbi	$$⊢\left(x\in B⟼\mathrm{suc}\bigcup x\right):B\underset{onto}{⟶}\mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)$$
55		relsdom	$$⊢\mathrm{Rel}\prec$$
56	55	brrelex1i	$$⊢B\prec \mathrm{cf}\left(A\right)\to B\in \mathrm{V}$$
57		breq1	$$⊢y=B\to \left(y\prec \mathrm{cf}\left(A\right)\leftrightarrow B\prec \mathrm{cf}\left(A\right)\right)$$
58		foeq2	$$⊢y=B\to \left(\left(x\in B⟼\mathrm{suc}\bigcup x\right):y\underset{onto}{⟶}\mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\leftrightarrow \left(x\in B⟼\mathrm{suc}\bigcup x\right):B\underset{onto}{⟶}\mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\right)$$
59		breq2	$$⊢y=B\to \left(\mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\preccurlyeq y\leftrightarrow \mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\preccurlyeq B\right)$$
60	58 59	imbi12d	$$⊢y=B\to \left(\left(\left(x\in B⟼\mathrm{suc}\bigcup x\right):y\underset{onto}{⟶}\mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\to \mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\preccurlyeq y\right)\leftrightarrow \left(\left(x\in B⟼\mathrm{suc}\bigcup x\right):B\underset{onto}{⟶}\mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\to \mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\preccurlyeq B\right)\right)$$
61	57 60	imbi12d	$$⊢y=B\to \left(\left(y\prec \mathrm{cf}\left(A\right)\to \left(\left(x\in B⟼\mathrm{suc}\bigcup x\right):y\underset{onto}{⟶}\mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\to \mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\preccurlyeq y\right)\right)\leftrightarrow \left(B\prec \mathrm{cf}\left(A\right)\to \left(\left(x\in B⟼\mathrm{suc}\bigcup x\right):B\underset{onto}{⟶}\mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\to \mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\preccurlyeq B\right)\right)\right)$$
62		cfon	$$⊢\mathrm{cf}\left(A\right)\in \mathrm{On}$$
63		sdomdom	$$⊢y\prec \mathrm{cf}\left(A\right)\to y\preccurlyeq \mathrm{cf}\left(A\right)$$
64		ondomen	$$⊢\left(\mathrm{cf}\left(A\right)\in \mathrm{On}\wedge y\preccurlyeq \mathrm{cf}\left(A\right)\right)\to y\in \mathrm{dom}\mathrm{card}$$
65	62 63 64	sylancr	$$⊢y\prec \mathrm{cf}\left(A\right)\to y\in \mathrm{dom}\mathrm{card}$$
66		fodomnum	$$⊢y\in \mathrm{dom}\mathrm{card}\to \left(\left(x\in B⟼\mathrm{suc}\bigcup x\right):y\underset{onto}{⟶}\mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\to \mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\preccurlyeq y\right)$$
67	65 66	syl	$$⊢y\prec \mathrm{cf}\left(A\right)\to \left(\left(x\in B⟼\mathrm{suc}\bigcup x\right):y\underset{onto}{⟶}\mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\to \mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\preccurlyeq y\right)$$
68	61 67	vtoclg	$$⊢B\in \mathrm{V}\to \left(B\prec \mathrm{cf}\left(A\right)\to \left(\left(x\in B⟼\mathrm{suc}\bigcup x\right):B\underset{onto}{⟶}\mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\to \mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\preccurlyeq B\right)\right)$$
69	56 68	mpcom	$$⊢B\prec \mathrm{cf}\left(A\right)\to \left(\left(x\in B⟼\mathrm{suc}\bigcup x\right):B\underset{onto}{⟶}\mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\to \mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\preccurlyeq B\right)$$
70	54 69	mpi	$$⊢B\prec \mathrm{cf}\left(A\right)\to \mathrm{ran}\left(x\in B⟼\mathrm{suc}\bigcup x\right)\preccurlyeq B$$
71	51 70	eqbrtrrid	$$⊢B\prec \mathrm{cf}\left(A\right)\to \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}\preccurlyeq B$$
72		domtr	$$⊢\left(\mathrm{cf}\left(A\right)\preccurlyeq \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}\wedge \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}\preccurlyeq B\right)\to \mathrm{cf}\left(A\right)\preccurlyeq B$$
73	71 72	sylan2	$$⊢\left(\mathrm{cf}\left(A\right)\preccurlyeq \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}\wedge B\prec \mathrm{cf}\left(A\right)\right)\to \mathrm{cf}\left(A\right)\preccurlyeq B$$
74		domnsym	$$⊢\mathrm{cf}\left(A\right)\preccurlyeq B\to \neg B\prec \mathrm{cf}\left(A\right)$$
75	73 74	syl	$$⊢\left(\mathrm{cf}\left(A\right)\preccurlyeq \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}\wedge B\prec \mathrm{cf}\left(A\right)\right)\to \neg B\prec \mathrm{cf}\left(A\right)$$
76	75	pm2.01da	$$⊢\mathrm{cf}\left(A\right)\preccurlyeq \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}\to \neg B\prec \mathrm{cf}\left(A\right)$$
77	76	a1i	$$⊢\left(\mathrm{Lim}A\wedge \forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\right)\to \left(\mathrm{cf}\left(A\right)\preccurlyeq \left\{y|\exists x\in By=\mathrm{suc}\bigcup x\right\}\to \neg B\prec \mathrm{cf}\left(A\right)\right)$$
78	29 49 77	3syld	$$⊢\left(\mathrm{Lim}A\wedge \forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\right)\to \left(\bigcup B=A\to \neg B\prec \mathrm{cf}\left(A\right)\right)$$
79	78	necon2ad	$$⊢\left(\mathrm{Lim}A\wedge \forall x\in B\left(x\subseteq A\wedge x\prec \mathrm{cf}\left(A\right)\right)\right)\to \left(B\prec \mathrm{cf}\left(A\right)\to \bigcup B\ne A\right)$$