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

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 ( 𝐵 , ℝ* , < ) )