Step |
Hyp |
Ref |
Expression |
1 |
|
supminfxrrnmpt.x |
⊢ Ⅎ 𝑥 𝜑 |
2 |
|
supminfxrrnmpt.b |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* ) |
3 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
4 |
1 3 2
|
rnmptssd |
⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ* ) |
5 |
4
|
supminfxr2 |
⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) = -𝑒 inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ* , < ) ) |
6 |
|
xnegex |
⊢ -𝑒 𝑦 ∈ V |
7 |
3
|
elrnmpt |
⊢ ( -𝑒 𝑦 ∈ V → ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 -𝑒 𝑦 = 𝐵 ) ) |
8 |
6 7
|
ax-mp |
⊢ ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 -𝑒 𝑦 = 𝐵 ) |
9 |
8
|
biimpi |
⊢ ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 -𝑒 𝑦 = 𝐵 ) |
10 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) |
11 |
|
xnegneg |
⊢ ( 𝑦 ∈ ℝ* → -𝑒 -𝑒 𝑦 = 𝑦 ) |
12 |
11
|
eqcomd |
⊢ ( 𝑦 ∈ ℝ* → 𝑦 = -𝑒 -𝑒 𝑦 ) |
13 |
12
|
adantr |
⊢ ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 = 𝐵 ) → 𝑦 = -𝑒 -𝑒 𝑦 ) |
14 |
|
xnegeq |
⊢ ( -𝑒 𝑦 = 𝐵 → -𝑒 -𝑒 𝑦 = -𝑒 𝐵 ) |
15 |
14
|
adantl |
⊢ ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 = 𝐵 ) → -𝑒 -𝑒 𝑦 = -𝑒 𝐵 ) |
16 |
13 15
|
eqtrd |
⊢ ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 = 𝐵 ) → 𝑦 = -𝑒 𝐵 ) |
17 |
16
|
ex |
⊢ ( 𝑦 ∈ ℝ* → ( -𝑒 𝑦 = 𝐵 → 𝑦 = -𝑒 𝐵 ) ) |
18 |
17
|
reximdv |
⊢ ( 𝑦 ∈ ℝ* → ( ∃ 𝑥 ∈ 𝐴 -𝑒 𝑦 = 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = -𝑒 𝐵 ) ) |
19 |
18
|
imp |
⊢ ( ( 𝑦 ∈ ℝ* ∧ ∃ 𝑥 ∈ 𝐴 -𝑒 𝑦 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = -𝑒 𝐵 ) |
20 |
|
simpl |
⊢ ( ( 𝑦 ∈ ℝ* ∧ ∃ 𝑥 ∈ 𝐴 -𝑒 𝑦 = 𝐵 ) → 𝑦 ∈ ℝ* ) |
21 |
10 19 20
|
elrnmptd |
⊢ ( ( 𝑦 ∈ ℝ* ∧ ∃ 𝑥 ∈ 𝐴 -𝑒 𝑦 = 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) |
22 |
9 21
|
sylan2 |
⊢ ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) |
23 |
22
|
ex |
⊢ ( 𝑦 ∈ ℝ* → ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) ) |
24 |
23
|
rgen |
⊢ ∀ 𝑦 ∈ ℝ* ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) |
25 |
|
rabss |
⊢ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ⊆ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ↔ ∀ 𝑦 ∈ ℝ* ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) ) |
26 |
25
|
biimpri |
⊢ ( ∀ 𝑦 ∈ ℝ* ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) → { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ⊆ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) |
27 |
24 26
|
ax-mp |
⊢ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ⊆ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) |
28 |
27
|
a1i |
⊢ ( 𝜑 → { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ⊆ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) |
29 |
|
nfcv |
⊢ Ⅎ 𝑥 -𝑒 𝑦 |
30 |
|
nfmpt1 |
⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
31 |
30
|
nfrn |
⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
32 |
29 31
|
nfel |
⊢ Ⅎ 𝑥 -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
33 |
|
nfcv |
⊢ Ⅎ 𝑥 ℝ* |
34 |
32 33
|
nfrabw |
⊢ Ⅎ 𝑥 { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } |
35 |
|
xnegeq |
⊢ ( 𝑦 = -𝑒 𝐵 → -𝑒 𝑦 = -𝑒 -𝑒 𝐵 ) |
36 |
35
|
eleq1d |
⊢ ( 𝑦 = -𝑒 𝐵 → ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ -𝑒 -𝑒 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ) |
37 |
2
|
xnegcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -𝑒 𝐵 ∈ ℝ* ) |
38 |
|
xnegneg |
⊢ ( 𝐵 ∈ ℝ* → -𝑒 -𝑒 𝐵 = 𝐵 ) |
39 |
2 38
|
syl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -𝑒 -𝑒 𝐵 = 𝐵 ) |
40 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 ) |
41 |
3 40 2
|
elrnmpt1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) |
42 |
39 41
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -𝑒 -𝑒 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) |
43 |
36 37 42
|
elrabd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -𝑒 𝐵 ∈ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ) |
44 |
1 34 10 43
|
rnmptssdf |
⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ⊆ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ) |
45 |
28 44
|
eqssd |
⊢ ( 𝜑 → { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } = ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) |
46 |
45
|
infeq1d |
⊢ ( 𝜑 → inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ* , < ) = inf ( ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) , ℝ* , < ) ) |
47 |
46
|
xnegeqd |
⊢ ( 𝜑 → -𝑒 inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ* , < ) = -𝑒 inf ( ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) , ℝ* , < ) ) |
48 |
5 47
|
eqtrd |
⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) = -𝑒 inf ( ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) , ℝ* , < ) ) |