Metamath Proof Explorer

Theorem infleinf2

Description: If any element in B is greater than or equal to an element in A , then the infimum of A is less than or equal to the infimum of B . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses infleinf2.x 
|- F/ x ph
infleinf2.p 
|- F/ y ph
infleinf2.a 
|- ( ph -> A C_ RR* )
infleinf2.b 
|- ( ph -> B C_ RR* )
infleinf2.y 
|- ( ( ph /\ x e. B ) -> E. y e. A y <_ x )
Assertion infleinf2 
|- ( ph -> inf ( A , RR* , < ) <_ inf ( B , RR* , < ) )

Proof

Step Hyp Ref Expression
1 infleinf2.x 
 |-  F/ x ph
2 infleinf2.p 
 |-  F/ y ph
3 infleinf2.a 
 |-  ( ph -> A C_ RR* )
4 infleinf2.b 
 |-  ( ph -> B C_ RR* )
5 infleinf2.y 
 |-  ( ( ph /\ x e. B ) -> E. y e. A y <_ x )
6 nfv 
 |-  F/ y x e. B
7 2 6 nfan 
 |-  F/ y ( ph /\ x e. B )
8 nfv 
 |-  F/ y inf ( A , RR* , < ) <_ x
9 3 infxrcld 
 |-  ( ph -> inf ( A , RR* , < ) e. RR* )
10 9 3ad2ant1 
 |-  ( ( ph /\ y e. A /\ y <_ x ) -> inf ( A , RR* , < ) e. RR* )
11 10 3adant1r 
 |-  ( ( ( ph /\ x e. B ) /\ y e. A /\ y <_ x ) -> inf ( A , RR* , < ) e. RR* )
12 3 sselda 
 |-  ( ( ph /\ y e. A ) -> y e. RR* )
13 12 3adant3 
 |-  ( ( ph /\ y e. A /\ y <_ x ) -> y e. RR* )
14 13 3adant1r 
 |-  ( ( ( ph /\ x e. B ) /\ y e. A /\ y <_ x ) -> y e. RR* )
15 4 sselda 
 |-  ( ( ph /\ x e. B ) -> x e. RR* )
16 15 3ad2ant1 
 |-  ( ( ( ph /\ x e. B ) /\ y e. A /\ y <_ x ) -> x e. RR* )
17 3 adantr 
 |-  ( ( ph /\ y e. A ) -> A C_ RR* )
18 simpr 
 |-  ( ( ph /\ y e. A ) -> y e. A )
19 infxrlb 
 |-  ( ( A C_ RR* /\ y e. A ) -> inf ( A , RR* , < ) <_ y )
20 17 18 19 syl2anc 
 |-  ( ( ph /\ y e. A ) -> inf ( A , RR* , < ) <_ y )
21 20 3adant3 
 |-  ( ( ph /\ y e. A /\ y <_ x ) -> inf ( A , RR* , < ) <_ y )
22 21 3adant1r 
 |-  ( ( ( ph /\ x e. B ) /\ y e. A /\ y <_ x ) -> inf ( A , RR* , < ) <_ y )
23 simp3 
 |-  ( ( ( ph /\ x e. B ) /\ y e. A /\ y <_ x ) -> y <_ x )
24 11 14 16 22 23 xrletrd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. A /\ y <_ x ) -> inf ( A , RR* , < ) <_ x )
25 24 3exp 
 |-  ( ( ph /\ x e. B ) -> ( y e. A -> ( y <_ x -> inf ( A , RR* , < ) <_ x ) ) )
26 7 8 25 rexlimd 
 |-  ( ( ph /\ x e. B ) -> ( E. y e. A y <_ x -> inf ( A , RR* , < ) <_ x ) )
27 5 26 mpd 
 |-  ( ( ph /\ x e. B ) -> inf ( A , RR* , < ) <_ x )
28 1 27 ralrimia 
 |-  ( ph -> A. x e. B inf ( A , RR* , < ) <_ x )
29 infxrgelb 
 |-  ( ( B C_ RR* /\ inf ( A , RR* , < ) e. RR* ) -> ( inf ( A , RR* , < ) <_ inf ( B , RR* , < ) <-> A. x e. B inf ( A , RR* , < ) <_ x ) )
30 4 9 29 syl2anc 
 |-  ( ph -> ( inf ( A , RR* , < ) <_ inf ( B , RR* , < ) <-> A. x e. B inf ( A , RR* , < ) <_ x ) )
31 28 30 mpbird 
 |-  ( ph -> inf ( A , RR* , < ) <_ inf ( B , RR* , < ) )