Metamath Proof Explorer

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 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 )