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