Theorem cfslbn

Description: Any subset of A smaller than its cofinality has union less than A . (This is the contrapositive to cfslb .) (Contributed by Mario Carneiro, 24-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cfslb.1	$$⊢A\in \mathrm{V}$$
2		uniss	$$⊢B\subseteq A\to \bigcup B\subseteq \bigcup A$$
3		limuni	$$⊢\mathrm{Lim}A\to A=\bigcup A$$
4	3	sseq2d	$$⊢\mathrm{Lim}A\to \left(\bigcup B\subseteq A\leftrightarrow \bigcup B\subseteq \bigcup A\right)$$
5	2 4	imbitrrid	$$⊢\mathrm{Lim}A\to \left(B\subseteq A\to \bigcup B\subseteq A\right)$$
6	5	imp	$$⊢\left(\mathrm{Lim}A\wedge B\subseteq A\right)\to \bigcup B\subseteq A$$
7		limord	$$⊢\mathrm{Lim}A\to \mathrm{Ord}A$$
8		ordsson	$$⊢\mathrm{Ord}A\to A\subseteq \mathrm{On}$$
9	7 8	syl	$$⊢\mathrm{Lim}A\to A\subseteq \mathrm{On}$$
10		sstr2	$$⊢B\subseteq A\to \left(A\subseteq \mathrm{On}\to B\subseteq \mathrm{On}\right)$$
11	9 10	syl5com	$$⊢\mathrm{Lim}A\to \left(B\subseteq A\to B\subseteq \mathrm{On}\right)$$
12		ssorduni	$$⊢B\subseteq \mathrm{On}\to \mathrm{Ord}\bigcup B$$
13	11 12	syl6	$$⊢\mathrm{Lim}A\to \left(B\subseteq A\to \mathrm{Ord}\bigcup B\right)$$
14	13 7	jctird	$$⊢\mathrm{Lim}A\to \left(B\subseteq A\to \left(\mathrm{Ord}\bigcup B\wedge \mathrm{Ord}A\right)\right)$$
15		ordsseleq	$$⊢\left(\mathrm{Ord}\bigcup B\wedge \mathrm{Ord}A\right)\to \left(\bigcup B\subseteq A\leftrightarrow \left(\bigcup B\in A\vee \bigcup B=A\right)\right)$$
16	14 15	syl6	$$⊢\mathrm{Lim}A\to \left(B\subseteq A\to \left(\bigcup B\subseteq A\leftrightarrow \left(\bigcup B\in A\vee \bigcup B=A\right)\right)\right)$$
17	16	imp	$$⊢\left(\mathrm{Lim}A\wedge B\subseteq A\right)\to \left(\bigcup B\subseteq A\leftrightarrow \left(\bigcup B\in A\vee \bigcup B=A\right)\right)$$
18	6 17	mpbid	$$⊢\left(\mathrm{Lim}A\wedge B\subseteq A\right)\to \left(\bigcup B\in A\vee \bigcup B=A\right)$$
19	18	ord	$$⊢\left(\mathrm{Lim}A\wedge B\subseteq A\right)\to \left(\neg \bigcup B\in A\to \bigcup B=A\right)$$
20	1	cfslb	$$⊢\left(\mathrm{Lim}A\wedge B\subseteq A\wedge \bigcup B=A\right)\to \mathrm{cf}\left(A\right)\preccurlyeq B$$
21		domnsym	$$⊢\mathrm{cf}\left(A\right)\preccurlyeq B\to \neg B\prec \mathrm{cf}\left(A\right)$$
22	20 21	syl	$$⊢\left(\mathrm{Lim}A\wedge B\subseteq A\wedge \bigcup B=A\right)\to \neg B\prec \mathrm{cf}\left(A\right)$$
23	22	3expia	$$⊢\left(\mathrm{Lim}A\wedge B\subseteq A\right)\to \left(\bigcup B=A\to \neg B\prec \mathrm{cf}\left(A\right)\right)$$
24	19 23	syld	$$⊢\left(\mathrm{Lim}A\wedge B\subseteq A\right)\to \left(\neg \bigcup B\in A\to \neg B\prec \mathrm{cf}\left(A\right)\right)$$
25	24	con4d	$$⊢\left(\mathrm{Lim}A\wedge B\subseteq A\right)\to \left(B\prec \mathrm{cf}\left(A\right)\to \bigcup B\in A\right)$$
26	25	3impia	$$⊢\left(\mathrm{Lim}A\wedge B\subseteq A\wedge B\prec \mathrm{cf}\left(A\right)\right)\to \bigcup B\in A$$