Metamath Proof Explorer

Theorem coflim

Description: A simpler expression for the cofinality predicate, at a limit ordinal. (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion coflim 
|- ( ( Lim A /\ B C_ A ) -> ( U. B = A <-> A. x e. A E. y e. B x C_ y ) )

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( U. B = A -> ( x e. U. B <-> x e. A ) )
2 1 biimprd 
 |-  ( U. B = A -> ( x e. A -> x e. U. B ) )
3 eluni2 
 |-  ( x e. U. B <-> E. y e. B x e. y )
4 limord 
 |-  ( Lim A -> Ord A )
5 ssel2 
 |-  ( ( B C_ A /\ y e. B ) -> y e. A )
6 ordelon 
 |-  ( ( Ord A /\ y e. A ) -> y e. On )
7 4 5 6 syl2an 
 |-  ( ( Lim A /\ ( B C_ A /\ y e. B ) ) -> y e. On )
8 7 expr 
 |-  ( ( Lim A /\ B C_ A ) -> ( y e. B -> y e. On ) )
9 onelss 
 |-  ( y e. On -> ( x e. y -> x C_ y ) )
10 8 9 syl6 
 |-  ( ( Lim A /\ B C_ A ) -> ( y e. B -> ( x e. y -> x C_ y ) ) )
11 10 reximdvai 
 |-  ( ( Lim A /\ B C_ A ) -> ( E. y e. B x e. y -> E. y e. B x C_ y ) )
12 3 11 syl5bi 
 |-  ( ( Lim A /\ B C_ A ) -> ( x e. U. B -> E. y e. B x C_ y ) )
13 2 12 syl9r 
 |-  ( ( Lim A /\ B C_ A ) -> ( U. B = A -> ( x e. A -> E. y e. B x C_ y ) ) )
14 13 ralrimdv 
 |-  ( ( Lim A /\ B C_ A ) -> ( U. B = A -> A. x e. A E. y e. B x C_ y ) )
15 uniss 
 |-  ( B C_ A -> U. B C_ U. A )
16 15 3ad2ant2 
 |-  ( ( Lim A /\ B C_ A /\ A. x e. A E. y e. B x C_ y ) -> U. B C_ U. A )
17 uniss2 
 |-  ( A. x e. A E. y e. B x C_ y -> U. A C_ U. B )
18 17 3ad2ant3 
 |-  ( ( Lim A /\ B C_ A /\ A. x e. A E. y e. B x C_ y ) -> U. A C_ U. B )
19 16 18 eqssd 
 |-  ( ( Lim A /\ B C_ A /\ A. x e. A E. y e. B x C_ y ) -> U. B = U. A )
20 limuni 
 |-  ( Lim A -> A = U. A )
21 20 3ad2ant1 
 |-  ( ( Lim A /\ B C_ A /\ A. x e. A E. y e. B x C_ y ) -> A = U. A )
22 19 21 eqtr4d 
 |-  ( ( Lim A /\ B C_ A /\ A. x e. A E. y e. B x C_ y ) -> U. B = A )
23 22 3expia 
 |-  ( ( Lim A /\ B C_ A ) -> ( A. x e. A E. y e. B x C_ y -> U. B = A ) )
24 14 23 impbid 
 |-  ( ( Lim A /\ B C_ A ) -> ( U. B = A <-> A. x e. A E. y e. B x C_ y ) )