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