Metamath Proof Explorer

Theorem fiinf2g

Description: A finite set satisfies the conditions to have an infimum. (Contributed by AV, 6-Oct-2020)

Ref Expression
Assertion fiinf2g 
|- ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> E. x e. B ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )

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 fiinfg 
 |-  ( ( R Or B /\ B e. Fin /\ B =/= (/) ) -> E. x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) )
4 2 3 infeu 
 |-  ( ( R Or B /\ B e. Fin /\ B =/= (/) ) -> E! x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) )
5 4 3exp 
 |-  ( R Or B -> ( B e. Fin -> ( B =/= (/) -> E! x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) ) ) )
6 1 5 syl6 
 |-  ( B C_ A -> ( R Or A -> ( B e. Fin -> ( B =/= (/) -> E! x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) ) ) ) )
7 6 com4l 
 |-  ( R Or A -> ( B e. Fin -> ( B =/= (/) -> ( B C_ A -> E! x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) ) ) ) )
8 7 3imp2 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> E! x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) )
9 reurex 
 |-  ( E! x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) -> E. x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) )
10 breq1 
 |-  ( z = x -> ( z R y <-> x R y ) )
11 10 rspcev 
 |-  ( ( x e. B /\ x R y ) -> E. z e. B z R y )
12 11 ex 
 |-  ( x e. B -> ( x R y -> E. z e. B z R y ) )
13 12 ralrimivw 
 |-  ( x e. B -> A. y e. A ( x R y -> E. z e. B z R y ) )
14 13 a1d 
 |-  ( x e. B -> ( A. y e. B ( x R y -> E. z e. B z R y ) -> A. y e. A ( x R y -> E. z e. B z R y ) ) )
15 14 anim2d 
 |-  ( x e. B -> ( ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) -> ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) )
16 15 reximia 
 |-  ( E. x e. B ( A. y e. B -. y R x /\ A. y e. B ( x R y -> E. z e. B z R y ) ) -> E. x e. B ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
17 8 9 16 3syl 
 |-  ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> E. x e. B ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )