| Step | Hyp | Ref
| Expression |
| 1 | | pimdecfgtioc.y |
. . . . . . 7
⊢ 𝑌 = {𝑥 ∈ 𝐴 ∣ 𝑅 < (𝐹‘𝑥)} |
| 2 | | ssrab2 4080 |
. . . . . . 7
⊢ {𝑥 ∈ 𝐴 ∣ 𝑅 < (𝐹‘𝑥)} ⊆ 𝐴 |
| 3 | 1, 2 | eqsstri 4030 |
. . . . . 6
⊢ 𝑌 ⊆ 𝐴 |
| 4 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑌 ⊆ 𝐴) |
| 5 | | pimdecfgtioc.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
| 6 | 4, 5 | sstrd 3994 |
. . . 4
⊢ (𝜑 → 𝑌 ⊆ ℝ) |
| 7 | | pimdecfgtioc.c |
. . . 4
⊢ 𝑆 = sup(𝑌, ℝ*, <
) |
| 8 | | pimdecfgtioc.e |
. . . 4
⊢ (𝜑 → 𝑆 ∈ 𝑌) |
| 9 | | pimdecfgtioc.d |
. . . 4
⊢ 𝐼 = (-∞(,]𝑆) |
| 10 | 6, 7, 8, 9 | ressiocsup 45567 |
. . 3
⊢ (𝜑 → 𝑌 ⊆ 𝐼) |
| 11 | 10, 4 | ssind 4241 |
. 2
⊢ (𝜑 → 𝑌 ⊆ (𝐼 ∩ 𝐴)) |
| 12 | | pimdecfgtioc.x |
. . . 4
⊢
Ⅎ𝑥𝜑 |
| 13 | | elinel2 4202 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐼 ∩ 𝐴) → 𝑥 ∈ 𝐴) |
| 14 | 13 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ∈ 𝐴) |
| 15 | | pimdecfgtioc.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
| 16 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑅 ∈
ℝ*) |
| 17 | | pimdecfgtioc.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) |
| 18 | 3, 8 | sselid 3981 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ 𝐴) |
| 19 | 17, 18 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑆) ∈
ℝ*) |
| 20 | 19 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → (𝐹‘𝑆) ∈
ℝ*) |
| 21 | 17 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝐹:𝐴⟶ℝ*) |
| 22 | 21, 14 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → (𝐹‘𝑥) ∈
ℝ*) |
| 23 | 8, 1 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ {𝑥 ∈ 𝐴 ∣ 𝑅 < (𝐹‘𝑥)}) |
| 24 | | nfrab1 3457 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝑅 < (𝐹‘𝑥)} |
| 25 | 1, 24 | nfcxfr 2903 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑌 |
| 26 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥ℝ* |
| 27 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥
< |
| 28 | 25, 26, 27 | nfsup 9491 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥sup(𝑌, ℝ*, <
) |
| 29 | 7, 28 | nfcxfr 2903 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑆 |
| 30 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝐴 |
| 31 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝑅 |
| 32 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝐹 |
| 33 | 32, 29 | nffv 6916 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝐹‘𝑆) |
| 34 | 31, 27, 33 | nfbr 5190 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥 𝑅 < (𝐹‘𝑆) |
| 35 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑆 → (𝐹‘𝑥) = (𝐹‘𝑆)) |
| 36 | 35 | breq2d 5155 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑆 → (𝑅 < (𝐹‘𝑥) ↔ 𝑅 < (𝐹‘𝑆))) |
| 37 | 29, 30, 34, 36 | elrabf 3688 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ {𝑥 ∈ 𝐴 ∣ 𝑅 < (𝐹‘𝑥)} ↔ (𝑆 ∈ 𝐴 ∧ 𝑅 < (𝐹‘𝑆))) |
| 38 | 23, 37 | sylib 218 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 ∈ 𝐴 ∧ 𝑅 < (𝐹‘𝑆))) |
| 39 | 38 | simprd 495 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 < (𝐹‘𝑆)) |
| 40 | 39 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑅 < (𝐹‘𝑆)) |
| 41 | 18 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑆 ∈ 𝐴) |
| 42 | | pimdecfgtioc.i |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) |
| 43 | 42 | r19.21bi 3251 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) |
| 44 | 14, 43 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) |
| 45 | 41, 44 | jca 511 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → (𝑆 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥)))) |
| 46 | | mnfxr 11318 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
| 47 | 46 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → -∞ ∈
ℝ*) |
| 48 | | ressxr 11305 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℝ* |
| 49 | 6, 8 | sseldd 3984 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ ℝ) |
| 50 | 48, 49 | sselid 3981 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈
ℝ*) |
| 51 | 50 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑆 ∈
ℝ*) |
| 52 | | elinel1 4201 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐼 ∩ 𝐴) → 𝑥 ∈ 𝐼) |
| 53 | 52, 9 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐼 ∩ 𝐴) → 𝑥 ∈ (-∞(,]𝑆)) |
| 54 | 53 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ∈ (-∞(,]𝑆)) |
| 55 | | iocleub 45516 |
. . . . . . . . . 10
⊢
((-∞ ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ 𝑥 ∈ (-∞(,]𝑆)) → 𝑥 ≤ 𝑆) |
| 56 | 47, 51, 54, 55 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ≤ 𝑆) |
| 57 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑆 → (𝑥 ≤ 𝑦 ↔ 𝑥 ≤ 𝑆)) |
| 58 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑆 → (𝐹‘𝑦) = (𝐹‘𝑆)) |
| 59 | 58 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑆 → ((𝐹‘𝑦) ≤ (𝐹‘𝑥) ↔ (𝐹‘𝑆) ≤ (𝐹‘𝑥))) |
| 60 | 57, 59 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑆 → ((𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥)) ↔ (𝑥 ≤ 𝑆 → (𝐹‘𝑆) ≤ (𝐹‘𝑥)))) |
| 61 | 60 | rspcva 3620 |
. . . . . . . . 9
⊢ ((𝑆 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) → (𝑥 ≤ 𝑆 → (𝐹‘𝑆) ≤ (𝐹‘𝑥))) |
| 62 | 45, 56, 61 | sylc 65 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → (𝐹‘𝑆) ≤ (𝐹‘𝑥)) |
| 63 | 16, 20, 22, 40, 62 | xrltletrd 13203 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑅 < (𝐹‘𝑥)) |
| 64 | 14, 63 | jca 511 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → (𝑥 ∈ 𝐴 ∧ 𝑅 < (𝐹‘𝑥))) |
| 65 | 1 | reqabi 3460 |
. . . . . 6
⊢ (𝑥 ∈ 𝑌 ↔ (𝑥 ∈ 𝐴 ∧ 𝑅 < (𝐹‘𝑥))) |
| 66 | 64, 65 | sylibr 234 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ∈ 𝑌) |
| 67 | 66 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐼 ∩ 𝐴) → 𝑥 ∈ 𝑌)) |
| 68 | 12, 67 | ralrimi 3257 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (𝐼 ∩ 𝐴)𝑥 ∈ 𝑌) |
| 69 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑥 𝑧 ∈ (𝐼 ∩ 𝐴) |
| 70 | 69 | nfci 2893 |
. . . 4
⊢
Ⅎ𝑥(𝐼 ∩ 𝐴) |
| 71 | 70, 25 | dfss3f 3975 |
. . 3
⊢ ((𝐼 ∩ 𝐴) ⊆ 𝑌 ↔ ∀𝑥 ∈ (𝐼 ∩ 𝐴)𝑥 ∈ 𝑌) |
| 72 | 68, 71 | sylibr 234 |
. 2
⊢ (𝜑 → (𝐼 ∩ 𝐴) ⊆ 𝑌) |
| 73 | 11, 72 | eqssd 4001 |
1
⊢ (𝜑 → 𝑌 = (𝐼 ∩ 𝐴)) |