Metamath Proof Explorer

Theorem fisup2g

Description: A finite set satisfies the conditions to have a supremum. (Contributed by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 soss 
 |-  ( B C_ A -> ( R Or A -> R Or B ) )
2 simp1 
 |-  ( ( R Or B /\ B e. Fin /\ B =/= (/) ) -> R Or B )
3 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 ) ) )
4 2 3 supeu 
 |-  ( ( 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 ) ) )
5 4 3exp 
 |-  ( 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 ) ) ) ) )
6 1 5 syl6 
 |-  ( B C_ A -> ( R Or A -> ( 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 ) ) ) ) ) )
7 6 com4l 
 |-  ( 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 ) ) ) ) ) )
8 7 3imp2 
 |-  ( ( 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 ) ) )
9 reurex 
 |-  ( 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. B ( A. y e. B -. x R y /\ A. y e. B ( y R x -> E. z e. B y R z ) ) )
10 breq2 
 |-  ( z = x -> ( y R z <-> y R x ) )
11 10 rspcev 
 |-  ( ( x e. B /\ y R x ) -> E. z e. B y R z )
12 11 ex 
 |-  ( x e. B -> ( y R x -> E. z e. B y R z ) )
13 12 ralrimivw 
 |-  ( x e. B -> A. y e. A ( y R x -> E. z e. B y R z ) )
14 13 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 ) ) )
15 14 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 ) ) ) )
16 15 reximia 
 |-  ( 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. B ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
17 8 9 16 3syl 
 |-  ( ( 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 ) ) )