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 ) ) )