Metamath Proof Explorer

Theorem fiminre

Description: A nonempty finite set of real numbers has a minimum. Analogous to fimaxre . (Contributed by AV, 9-Aug-2020) (Proof shortened by Steven Nguyen, 3-Jun-2023)

Ref Expression
Assertion fiminre 
|- ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A x <_ y )

Proof

Step Hyp Ref Expression
1 ltso 
 |-  < Or RR
2 soss 
 |-  ( A C_ RR -> ( < Or RR -> < Or A ) )
3 1 2 mpi 
 |-  ( A C_ RR -> < Or A )
4 fiming 
 |-  ( ( < Or A /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A ( x =/= y -> x < y ) )
5 3 4 syl3an1 
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A ( x =/= y -> x < y ) )
6 ssel2 
 |-  ( ( A C_ RR /\ x e. A ) -> x e. RR )
7 6 adantr 
 |-  ( ( ( A C_ RR /\ x e. A ) /\ y e. A ) -> x e. RR )
8 ssel2 
 |-  ( ( A C_ RR /\ y e. A ) -> y e. RR )
9 8 adantlr 
 |-  ( ( ( A C_ RR /\ x e. A ) /\ y e. A ) -> y e. RR )
10 7 9 leloed 
 |-  ( ( ( A C_ RR /\ x e. A ) /\ y e. A ) -> ( x <_ y <-> ( x < y \/ x = y ) ) )
11 orcom 
 |-  ( ( x = y \/ x < y ) <-> ( x < y \/ x = y ) )
12 11 a1i 
 |-  ( ( ( A C_ RR /\ x e. A ) /\ y e. A ) -> ( ( x = y \/ x < y ) <-> ( x < y \/ x = y ) ) )
13 neor 
 |-  ( ( x = y \/ x < y ) <-> ( x =/= y -> x < y ) )
14 13 a1i 
 |-  ( ( ( A C_ RR /\ x e. A ) /\ y e. A ) -> ( ( x = y \/ x < y ) <-> ( x =/= y -> x < y ) ) )
15 10 12 14 3bitr2d 
 |-  ( ( ( A C_ RR /\ x e. A ) /\ y e. A ) -> ( x <_ y <-> ( x =/= y -> x < y ) ) )
16 15 biimprd 
 |-  ( ( ( A C_ RR /\ x e. A ) /\ y e. A ) -> ( ( x =/= y -> x < y ) -> x <_ y ) )
17 16 ralimdva 
 |-  ( ( A C_ RR /\ x e. A ) -> ( A. y e. A ( x =/= y -> x < y ) -> A. y e. A x <_ y ) )
18 17 reximdva 
 |-  ( A C_ RR -> ( E. x e. A A. y e. A ( x =/= y -> x < y ) -> E. x e. A A. y e. A x <_ y ) )
19 18 3ad2ant1 
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> ( E. x e. A A. y e. A ( x =/= y -> x < y ) -> E. x e. A A. y e. A x <_ y ) )
20 5 19 mpd 
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A x <_ y )