Metamath Proof Explorer

Theorem fimin2g

Description: A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020)

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

Proof

Step Hyp Ref Expression
1 3simpc 
 |-  ( ( R Or A /\ A e. Fin /\ A =/= (/) ) -> ( A e. Fin /\ A =/= (/) ) )
2 sopo 
 |-  ( R Or A -> R Po A )
3 2 3ad2ant1 
 |-  ( ( R Or A /\ A e. Fin /\ A =/= (/) ) -> R Po A )
4 simp2 
 |-  ( ( R Or A /\ A e. Fin /\ A =/= (/) ) -> A e. Fin )
5 frfi 
 |-  ( ( R Po A /\ A e. Fin ) -> R Fr A )
6 3 4 5 syl2anc 
 |-  ( ( R Or A /\ A e. Fin /\ A =/= (/) ) -> R Fr A )
7 ssid 
 |-  A C_ A
8 fri 
 |-  ( ( ( A e. Fin /\ R Fr A ) /\ ( A C_ A /\ A =/= (/) ) ) -> E. x e. A A. y e. A -. y R x )
9 7 8 mpanr1 
 |-  ( ( ( A e. Fin /\ R Fr A ) /\ A =/= (/) ) -> E. x e. A A. y e. A -. y R x )
10 9 an32s 
 |-  ( ( ( A e. Fin /\ A =/= (/) ) /\ R Fr A ) -> E. x e. A A. y e. A -. y R x )
11 1 6 10 syl2anc 
 |-  ( ( R Or A /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A -. y R x )