Metamath Proof Explorer

Theorem fisupcl

Description: A nonempty finite set contains its supremum. (Contributed by Jeff Madsen, 9-May-2011)

Ref Expression
Assertion fisupcl 
|- ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> sup ( B , A , R ) e. B )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> R Or A )
2 1 supval2 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> sup ( B , A , R ) = ( iota_ x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) )
3 simpr3 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> B C_ A )
4 breq2 
 |-  ( z = x -> ( y R z <-> y R x ) )
5 4 rspcev 
 |-  ( ( x e. B /\ y R x ) -> E. z e. B y R z )
6 5 ex 
 |-  ( x e. B -> ( y R x -> E. z e. B y R z ) )
7 6 ralrimivw 
 |-  ( x e. B -> A. y e. A ( y R x -> E. z e. B y R z ) )
8 7 a1d 
 |-  ( x e. B -> ( A. y e. B ( y R x -> E. z e. B y R z ) -> A. y e. A ( y R x -> E. z e. B y R z ) ) )
9 8 anim2d 
 |-  ( x e. B -> ( ( A. y e. B -. x R y /\ A. y e. B ( y R x -> E. z e. B y R z ) ) -> ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) )
10 9 rgen 
 |-  A. x e. B ( ( A. y e. B -. x R y /\ A. y e. B ( y R x -> E. z e. B y R z ) ) -> ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
11 10 a1i 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> A. x e. B ( ( A. y e. B -. x R y /\ A. y e. B ( y R x -> E. z e. B y R z ) ) -> ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) )
12 soss 
 |-  ( B C_ A -> ( R Or A -> R Or B ) )
13 3 1 12 sylc 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> R Or B )
14 simpr1 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> B e. Fin )
15 simpr2 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> B =/= (/) )
16 fisupg 
 |-  ( ( R Or B /\ B e. Fin /\ B =/= (/) ) -> E. x e. B ( A. y e. B -. x R y /\ A. y e. B ( y R x -> E. z e. B y R z ) ) )
17 13 14 15 16 syl3anc 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> E. x e. B ( A. y e. B -. x R y /\ A. y e. B ( y R x -> E. z e. B y R z ) ) )
18 fisup2g 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> E. x e. B ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
19 ssrexv 
 |-  ( B C_ A -> ( E. x e. B ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) )
20 3 18 19 sylc 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
21 1 20 supeu 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> E! x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
22 riotass2 
 |-  ( ( ( B C_ A /\ A. x e. B ( ( A. y e. B -. x R y /\ A. y e. B ( y R x -> E. z e. B y R z ) ) -> ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) ) /\ ( E. x e. B ( A. y e. B -. x R y /\ A. y e. B ( y R x -> E. z e. B y R z ) ) /\ E! x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) ) -> ( iota_ x e. B ( A. y e. B -. x R y /\ A. y e. B ( y R x -> E. z e. B y R z ) ) ) = ( iota_ x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) )
23 3 11 17 21 22 syl22anc 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> ( iota_ x e. B ( A. y e. B -. x R y /\ A. y e. B ( y R x -> E. z e. B y R z ) ) ) = ( iota_ x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) )
24 13 17 supeu 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> E! x e. B ( A. y e. B -. x R y /\ A. y e. B ( y R x -> E. z e. B y R z ) ) )
25 riotacl 
 |-  ( E! x e. B ( A. y e. B -. x R y /\ A. y e. B ( y R x -> E. z e. B y R z ) ) -> ( iota_ x e. B ( A. y e. B -. x R y /\ A. y e. B ( y R x -> E. z e. B y R z ) ) ) e. B )
26 24 25 syl 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> ( iota_ x e. B ( A. y e. B -. x R y /\ A. y e. B ( y R x -> E. z e. B y R z ) ) ) e. B )
27 23 26 eqeltrrd 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> ( iota_ x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) e. B )
28 2 27 eqeltrd 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> sup ( B , A , R ) e. B )