Theorem taupilemrplb

Description: A set of positive reals has (in the reals) a lower bound. (Contributed by Jim Kingdon, 19-Feb-2019)

	Ref	Expression
Assertion	taupilemrplb	|- E. x e. RR A. y e. ( RR+ i^i A ) x <_ y

Proof

Step	Hyp	Ref	Expression
1		0re	|- 0 e. RR
2		inss1	|- ( RR+ i^i A ) C_ RR+
3	2	sseli	|- ( y e. ( RR+ i^i A ) -> y e. RR+ )
4	3	rpge0d	|- ( y e. ( RR+ i^i A ) -> 0 <_ y )
5	4	rgen	|- A. y e. ( RR+ i^i A ) 0 <_ y
6		breq1	|- ( x = 0 -> ( x <_ y <-> 0 <_ y ) )
7	6	ralbidv	|- ( x = 0 -> ( A. y e. ( RR+ i^i A ) x <_ y <-> A. y e. ( RR+ i^i A ) 0 <_ y ) )
8	7	rspcev	|- ( ( 0 e. RR /\ A. y e. ( RR+ i^i A ) 0 <_ y ) -> E. x e. RR A. y e. ( RR+ i^i A ) x <_ y )
9	1 5 8	mp2an	|- E. x e. RR A. y e. ( RR+ i^i A ) x <_ y