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 𝑥 𝜑
infleinf2.p 𝑦 𝜑
infleinf2.a ( 𝜑𝐴 ⊆ ℝ* )
infleinf2.b ( 𝜑𝐵 ⊆ ℝ* )
infleinf2.y ( ( 𝜑𝑥𝐵 ) → ∃ 𝑦𝐴 𝑦𝑥 )
Assertion infleinf2 ( 𝜑 → inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐵 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 infleinf2.x 𝑥 𝜑
2 infleinf2.p 𝑦 𝜑
3 infleinf2.a ( 𝜑𝐴 ⊆ ℝ* )
4 infleinf2.b ( 𝜑𝐵 ⊆ ℝ* )
5 infleinf2.y ( ( 𝜑𝑥𝐵 ) → ∃ 𝑦𝐴 𝑦𝑥 )
6 nfv 𝑦 𝑥𝐵
7 2 6 nfan 𝑦 ( 𝜑𝑥𝐵 )
8 nfv 𝑦 inf ( 𝐴 , ℝ* , < ) ≤ 𝑥
9 3 infxrcld ( 𝜑 → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
10 9 3ad2ant1 ( ( 𝜑𝑦𝐴𝑦𝑥 ) → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
11 10 3adant1r ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑦𝐴𝑦𝑥 ) → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
12 3 sselda ( ( 𝜑𝑦𝐴 ) → 𝑦 ∈ ℝ* )
13 12 3adant3 ( ( 𝜑𝑦𝐴𝑦𝑥 ) → 𝑦 ∈ ℝ* )
14 13 3adant1r ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑦𝐴𝑦𝑥 ) → 𝑦 ∈ ℝ* )
15 4 sselda ( ( 𝜑𝑥𝐵 ) → 𝑥 ∈ ℝ* )
16 15 3ad2ant1 ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑦𝐴𝑦𝑥 ) → 𝑥 ∈ ℝ* )
17 3 adantr ( ( 𝜑𝑦𝐴 ) → 𝐴 ⊆ ℝ* )
18 simpr ( ( 𝜑𝑦𝐴 ) → 𝑦𝐴 )
19 infxrlb ( ( 𝐴 ⊆ ℝ*𝑦𝐴 ) → inf ( 𝐴 , ℝ* , < ) ≤ 𝑦 )
20 17 18 19 syl2anc ( ( 𝜑𝑦𝐴 ) → inf ( 𝐴 , ℝ* , < ) ≤ 𝑦 )
21 20 3adant3 ( ( 𝜑𝑦𝐴𝑦𝑥 ) → inf ( 𝐴 , ℝ* , < ) ≤ 𝑦 )
22 21 3adant1r ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑦𝐴𝑦𝑥 ) → inf ( 𝐴 , ℝ* , < ) ≤ 𝑦 )
23 simp3 ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑦𝐴𝑦𝑥 ) → 𝑦𝑥 )
24 11 14 16 22 23 xrletrd ( ( ( 𝜑𝑥𝐵 ) ∧ 𝑦𝐴𝑦𝑥 ) → inf ( 𝐴 , ℝ* , < ) ≤ 𝑥 )
25 24 3exp ( ( 𝜑𝑥𝐵 ) → ( 𝑦𝐴 → ( 𝑦𝑥 → inf ( 𝐴 , ℝ* , < ) ≤ 𝑥 ) ) )
26 7 8 25 rexlimd ( ( 𝜑𝑥𝐵 ) → ( ∃ 𝑦𝐴 𝑦𝑥 → inf ( 𝐴 , ℝ* , < ) ≤ 𝑥 ) )
27 5 26 mpd ( ( 𝜑𝑥𝐵 ) → inf ( 𝐴 , ℝ* , < ) ≤ 𝑥 )
28 1 27 ralrimia ( 𝜑 → ∀ 𝑥𝐵 inf ( 𝐴 , ℝ* , < ) ≤ 𝑥 )
29 infxrgelb ( ( 𝐵 ⊆ ℝ* ∧ inf ( 𝐴 , ℝ* , < ) ∈ ℝ* ) → ( inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐵 , ℝ* , < ) ↔ ∀ 𝑥𝐵 inf ( 𝐴 , ℝ* , < ) ≤ 𝑥 ) )
30 4 9 29 syl2anc ( 𝜑 → ( inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐵 , ℝ* , < ) ↔ ∀ 𝑥𝐵 inf ( 𝐴 , ℝ* , < ) ≤ 𝑥 ) )
31 28 30 mpbird ( 𝜑 → inf ( 𝐴 , ℝ* , < ) ≤ inf ( 𝐵 , ℝ* , < ) )