This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infxrrefi

Description: The real and extended real infima match when the set is finite. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Assertion infxrrefi 
|- ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> inf ( A , RR* , < ) = inf ( A , RR , < ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> A C_ RR )
2 simp3 
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> A =/= (/) )
3 fiminre2 
 |-  ( ( A C_ RR /\ A e. Fin ) -> E. x e. RR A. y e. A x <_ y )
4 3 3adant3 
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> E. x e. RR A. y e. A x <_ y )
5 infxrre 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> inf ( A , RR* , < ) = inf ( A , RR , < ) )
6 1 2 4 5 syl3anc 
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> inf ( A , RR* , < ) = inf ( A , RR , < ) )