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 e. _V
	Assertion	cfslbn	\|- ( ( Lim A /\ B C_ A /\ B ~< ( cf ` A ) ) -> U. B e. A )

Proof

Step	Hyp	Ref	Expression
1		cfslb.1	\|- A e. _V
2		uniss	\|- ( B C_ A -> U. B C_ U. A )
3		limuni	\|- ( Lim A -> A = U. A )
4	3	sseq2d	\|- ( Lim A -> ( U. B C_ A <-> U. B C_ U. A ) )
5	2 4	imbitrrid	\|- ( Lim A -> ( B C_ A -> U. B C_ A ) )
6	5	imp	\|- ( ( Lim A /\ B C_ A ) -> U. B C_ A )
7		limord	\|- ( Lim A -> Ord A )
8		ordsson	\|- ( Ord A -> A C_ On )
9	7 8	syl	\|- ( Lim A -> A C_ On )
10		sstr2	\|- ( B C_ A -> ( A C_ On -> B C_ On ) )
11	9 10	syl5com	\|- ( Lim A -> ( B C_ A -> B C_ On ) )
12		ssorduni	\|- ( B C_ On -> Ord U. B )
13	11 12	syl6	\|- ( Lim A -> ( B C_ A -> Ord U. B ) )
14	13 7	jctird	\|- ( Lim A -> ( B C_ A -> ( Ord U. B /\ Ord A ) ) )
15		ordsseleq	\|- ( ( Ord U. B /\ Ord A ) -> ( U. B C_ A <-> ( U. B e. A \/ U. B = A ) ) )
16	14 15	syl6	\|- ( Lim A -> ( B C_ A -> ( U. B C_ A <-> ( U. B e. A \/ U. B = A ) ) ) )
17	16	imp	\|- ( ( Lim A /\ B C_ A ) -> ( U. B C_ A <-> ( U. B e. A \/ U. B = A ) ) )
18	6 17	mpbid	\|- ( ( Lim A /\ B C_ A ) -> ( U. B e. A \/ U. B = A ) )
19	18	ord	\|- ( ( Lim A /\ B C_ A ) -> ( -. U. B e. A -> U. B = A ) )
20	1	cfslb	\|- ( ( Lim A /\ B C_ A /\ U. B = A ) -> ( cf ` A ) ~<_ B )
21		domnsym	\|- ( ( cf ` A ) ~<_ B -> -. B ~< ( cf ` A ) )
22	20 21	syl	\|- ( ( Lim A /\ B C_ A /\ U. B = A ) -> -. B ~< ( cf ` A ) )
23	22	3expia	\|- ( ( Lim A /\ B C_ A ) -> ( U. B = A -> -. B ~< ( cf ` A ) ) )
24	19 23	syld	\|- ( ( Lim A /\ B C_ A ) -> ( -. U. B e. A -> -. B ~< ( cf ` A ) ) )
25	24	con4d	\|- ( ( Lim A /\ B C_ A ) -> ( B ~< ( cf ` A ) -> U. B e. A ) )
26	25	3impia	\|- ( ( Lim A /\ B C_ A /\ B ~< ( cf ` A ) ) -> U. B e. A )

Metamath Proof Explorer

Theorem cfslbn

Proof