Metamath Proof Explorer

Theorem ordunifi

Description: The maximum of a finite collection of ordinals is in the set. (Contributed by Mario Carneiro, 28-May-2013) (Revised by Mario Carneiro, 29-Jan-2014)

Ref Expression
Assertion ordunifi 
|- ( ( A C_ On /\ A e. Fin /\ A =/= (/) ) -> U. A e. A )

Proof

Step Hyp Ref Expression
1 epweon 
 |-  _E We On
2 weso 
 |-  ( _E We On -> _E Or On )
3 1 2 ax-mp 
 |-  _E Or On
4 soss 
 |-  ( A C_ On -> ( _E Or On -> _E Or A ) )
5 3 4 mpi 
 |-  ( A C_ On -> _E Or A )
6 fimax2g 
 |-  ( ( _E Or A /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A -. x _E y )
7 5 6 syl3an1 
 |-  ( ( A C_ On /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A -. x _E y )
8 ssel2 
 |-  ( ( A C_ On /\ y e. A ) -> y e. On )
9 8 adantlr 
 |-  ( ( ( A C_ On /\ x e. A ) /\ y e. A ) -> y e. On )
10 ssel2 
 |-  ( ( A C_ On /\ x e. A ) -> x e. On )
11 10 adantr 
 |-  ( ( ( A C_ On /\ x e. A ) /\ y e. A ) -> x e. On )
12 epel 
 |-  ( x _E y <-> x e. y )
13 12 notbii 
 |-  ( -. x _E y <-> -. x e. y )
14 ontri1 
 |-  ( ( y e. On /\ x e. On ) -> ( y C_ x <-> -. x e. y ) )
15 13 14 bitr4id 
 |-  ( ( y e. On /\ x e. On ) -> ( -. x _E y <-> y C_ x ) )
16 9 11 15 syl2anc 
 |-  ( ( ( A C_ On /\ x e. A ) /\ y e. A ) -> ( -. x _E y <-> y C_ x ) )
17 16 ralbidva 
 |-  ( ( A C_ On /\ x e. A ) -> ( A. y e. A -. x _E y <-> A. y e. A y C_ x ) )
18 unissb 
 |-  ( U. A C_ x <-> A. y e. A y C_ x )
19 17 18 bitr4di 
 |-  ( ( A C_ On /\ x e. A ) -> ( A. y e. A -. x _E y <-> U. A C_ x ) )
20 19 rexbidva 
 |-  ( A C_ On -> ( E. x e. A A. y e. A -. x _E y <-> E. x e. A U. A C_ x ) )
21 20 3ad2ant1 
 |-  ( ( A C_ On /\ A e. Fin /\ A =/= (/) ) -> ( E. x e. A A. y e. A -. x _E y <-> E. x e. A U. A C_ x ) )
22 7 21 mpbid 
 |-  ( ( A C_ On /\ A e. Fin /\ A =/= (/) ) -> E. x e. A U. A C_ x )
23 elssuni 
 |-  ( x e. A -> x C_ U. A )
24 eqss 
 |-  ( x = U. A <-> ( x C_ U. A /\ U. A C_ x ) )
25 eleq1 
 |-  ( x = U. A -> ( x e. A <-> U. A e. A ) )
26 25 biimpcd 
 |-  ( x e. A -> ( x = U. A -> U. A e. A ) )
27 24 26 syl5bir 
 |-  ( x e. A -> ( ( x C_ U. A /\ U. A C_ x ) -> U. A e. A ) )
28 23 27 mpand 
 |-  ( x e. A -> ( U. A C_ x -> U. A e. A ) )
29 28 rexlimiv 
 |-  ( E. x e. A U. A C_ x -> U. A e. A )
30 22 29 syl 
 |-  ( ( A C_ On /\ A e. Fin /\ A =/= (/) ) -> U. A e. A )