Proof of Theorem pimdecfgtioo
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pimdecfgtioo.y | . . . . . . 7
⊢ 𝑌 = {𝑥 ∈ 𝐴 ∣ 𝑅 < (𝐹‘𝑥)} | 
| 2 |  | ssrab2 4079 | . . . . . . 7
⊢ {𝑥 ∈ 𝐴 ∣ 𝑅 < (𝐹‘𝑥)} ⊆ 𝐴 | 
| 3 | 1, 2 | eqsstri 4029 | . . . . . 6
⊢ 𝑌 ⊆ 𝐴 | 
| 4 | 3 | a1i 11 | . . . . 5
⊢ (𝜑 → 𝑌 ⊆ 𝐴) | 
| 5 |  | pimdecfgtioo.a | . . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℝ) | 
| 6 | 4, 5 | sstrd 3993 | . . . 4
⊢ (𝜑 → 𝑌 ⊆ ℝ) | 
| 7 |  | pimdecfgtioo.c | . . . 4
⊢ 𝑆 = sup(𝑌, ℝ*, <
) | 
| 8 |  | pimdecfgtioo.e | . . . 4
⊢ (𝜑 → ¬ 𝑆 ∈ 𝑌) | 
| 9 |  | pimdecfgtioo.i | . . . 4
⊢ 𝐼 = (-∞(,)𝑆) | 
| 10 | 6, 7, 8, 9 | ressioosup 45573 | . . 3
⊢ (𝜑 → 𝑌 ⊆ 𝐼) | 
| 11 | 10, 4 | ssind 4240 | . 2
⊢ (𝜑 → 𝑌 ⊆ (𝐼 ∩ 𝐴)) | 
| 12 |  | pimdecfgtioo.x | . . . 4
⊢
Ⅎ𝑥𝜑 | 
| 13 |  | elinel2 4201 | . . . . . . . 8
⊢ (𝑥 ∈ (𝐼 ∩ 𝐴) → 𝑥 ∈ 𝐴) | 
| 14 | 13 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ∈ 𝐴) | 
| 15 |  | mnfxr 11319 | . . . . . . . . . . 11
⊢ -∞
∈ ℝ* | 
| 16 | 15 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → -∞ ∈
ℝ*) | 
| 17 |  | ressxr 11306 | . . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℝ* | 
| 18 | 6, 17 | sstrdi 3995 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ⊆
ℝ*) | 
| 19 | 18 | supxrcld 45117 | . . . . . . . . . . . 12
⊢ (𝜑 → sup(𝑌, ℝ*, < ) ∈
ℝ*) | 
| 20 | 7, 19 | eqeltrid 2844 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈
ℝ*) | 
| 21 | 20 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑆 ∈
ℝ*) | 
| 22 |  | elinel1 4200 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐼 ∩ 𝐴) → 𝑥 ∈ 𝐼) | 
| 23 | 22, 9 | eleqtrdi 2850 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐼 ∩ 𝐴) → 𝑥 ∈ (-∞(,)𝑆)) | 
| 24 | 23 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ∈ (-∞(,)𝑆)) | 
| 25 |  | iooltub 45528 | . . . . . . . . . 10
⊢
((-∞ ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ 𝑥 ∈ (-∞(,)𝑆)) → 𝑥 < 𝑆) | 
| 26 | 16, 21, 24, 25 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 < 𝑆) | 
| 27 | 26 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → 𝑥 < 𝑆) | 
| 28 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → ¬ 𝑅 < (𝐹‘𝑥)) | 
| 29 |  | pimdecfgtioo.f | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) | 
| 30 | 29 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝐹:𝐴⟶ℝ*) | 
| 31 | 30, 14 | ffvelcdmd 7104 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → (𝐹‘𝑥) ∈
ℝ*) | 
| 32 | 31 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → (𝐹‘𝑥) ∈
ℝ*) | 
| 33 |  | pimdecfgtioo.r | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑅 ∈
ℝ*) | 
| 34 | 33 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑅 ∈
ℝ*) | 
| 35 | 34 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → 𝑅 ∈
ℝ*) | 
| 36 | 32, 35 | xrlenltd 11328 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → ((𝐹‘𝑥) ≤ 𝑅 ↔ ¬ 𝑅 < (𝐹‘𝑥))) | 
| 37 | 28, 36 | mpbird 257 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → (𝐹‘𝑥) ≤ 𝑅) | 
| 38 |  | pimdecfgtioo.h | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦𝜑 | 
| 39 |  | nfv 1913 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦 𝑥 ∈ (𝐼 ∩ 𝐴) | 
| 40 | 38, 39 | nfan 1898 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) | 
| 41 |  | nfv 1913 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(𝐹‘𝑥) ≤ 𝑅 | 
| 42 | 40, 41 | nfan 1898 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑦((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) | 
| 43 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) | 
| 44 | 43 | breq2d 5154 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝑅 < (𝐹‘𝑥) ↔ 𝑅 < (𝐹‘𝑦))) | 
| 45 | 44, 1 | elrab2 3694 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝑌 ↔ (𝑦 ∈ 𝐴 ∧ 𝑅 < (𝐹‘𝑦))) | 
| 46 | 45 | biimpi 216 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑌 → (𝑦 ∈ 𝐴 ∧ 𝑅 < (𝐹‘𝑦))) | 
| 47 | 46 | simprd 495 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝑌 → 𝑅 < (𝐹‘𝑦)) | 
| 48 | 47 | ad2antlr 727 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑅 < (𝐹‘𝑦)) | 
| 49 | 5 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝐴 ⊆ ℝ) | 
| 50 | 49, 14 | sseldd 3983 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ∈ ℝ) | 
| 51 | 50 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑥 ∈ ℝ) | 
| 52 | 6 | sselda 3982 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ ℝ) | 
| 53 | 52 | ad4ant13 751 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑦 ∈ ℝ) | 
| 54 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → ¬ 𝑦 ≤ 𝑥) | 
| 55 | 51, 53 | ltnled 11409 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → (𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥)) | 
| 56 | 54, 55 | mpbird 257 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑥 < 𝑦) | 
| 57 | 51, 53, 56 | ltled 11410 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑥 ≤ 𝑦) | 
| 58 | 57 | adantllr 719 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑥 ≤ 𝑦) | 
| 59 | 29 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐹:𝐴⟶ℝ*) | 
| 60 | 4 | sselda 3982 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝐴) | 
| 61 | 59, 60 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐹‘𝑦) ∈
ℝ*) | 
| 62 | 61 | ad5ant14 757 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑦) ∈
ℝ*) | 
| 63 | 31 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑥) ∈
ℝ*) | 
| 64 | 34 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → 𝑅 ∈
ℝ*) | 
| 65 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → 𝑥 ≤ 𝑦) | 
| 66 |  | pimdecfgtioo.d | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) | 
| 67 |  | rspa 3247 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) | 
| 68 | 66, 13, 67 | syl2an 596 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) | 
| 69 | 68 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) | 
| 70 | 60 | ad4ant13 751 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → 𝑦 ∈ 𝐴) | 
| 71 |  | rspa 3247 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑦 ∈
𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) | 
| 72 | 69, 70, 71 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) | 
| 73 | 65, 72 | mpd 15 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑦) ≤ (𝐹‘𝑥)) | 
| 74 | 73 | adantllr 719 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑦) ≤ (𝐹‘𝑥)) | 
| 75 |  | simpllr 775 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑥) ≤ 𝑅) | 
| 76 | 62, 63, 64, 74, 75 | xrletrd 13205 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑦) ≤ 𝑅) | 
| 77 | 62, 64 | xrlenltd 11328 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → ((𝐹‘𝑦) ≤ 𝑅 ↔ ¬ 𝑅 < (𝐹‘𝑦))) | 
| 78 | 76, 77 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → ¬ 𝑅 < (𝐹‘𝑦)) | 
| 79 | 58, 78 | syldan 591 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → ¬ 𝑅 < (𝐹‘𝑦)) | 
| 80 | 48, 79 | condan 817 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) → 𝑦 ≤ 𝑥) | 
| 81 | 80 | ex 412 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) → (𝑦 ∈ 𝑌 → 𝑦 ≤ 𝑥)) | 
| 82 | 42, 81 | ralrimi 3256 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) → ∀𝑦 ∈ 𝑌 𝑦 ≤ 𝑥) | 
| 83 | 37, 82 | syldan 591 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → ∀𝑦 ∈ 𝑌 𝑦 ≤ 𝑥) | 
| 84 | 18 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑌 ⊆
ℝ*) | 
| 85 | 17, 50 | sselid 3980 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ∈ ℝ*) | 
| 86 |  | supxrleub 13369 | . . . . . . . . . . . . 13
⊢ ((𝑌 ⊆ ℝ*
∧ 𝑥 ∈
ℝ*) → (sup(𝑌, ℝ*, < ) ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑌 𝑦 ≤ 𝑥)) | 
| 87 | 84, 85, 86 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → (sup(𝑌, ℝ*, < ) ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑌 𝑦 ≤ 𝑥)) | 
| 88 | 87 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → (sup(𝑌, ℝ*, < ) ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑌 𝑦 ≤ 𝑥)) | 
| 89 | 83, 88 | mpbird 257 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → sup(𝑌, ℝ*, < ) ≤ 𝑥) | 
| 90 | 7, 89 | eqbrtrid 5177 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → 𝑆 ≤ 𝑥) | 
| 91 | 21 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → 𝑆 ∈
ℝ*) | 
| 92 | 85 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → 𝑥 ∈ ℝ*) | 
| 93 | 91, 92 | xrlenltd 11328 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → (𝑆 ≤ 𝑥 ↔ ¬ 𝑥 < 𝑆)) | 
| 94 | 90, 93 | mpbid 232 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → ¬ 𝑥 < 𝑆) | 
| 95 | 27, 94 | condan 817 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑅 < (𝐹‘𝑥)) | 
| 96 | 14, 95 | jca 511 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → (𝑥 ∈ 𝐴 ∧ 𝑅 < (𝐹‘𝑥))) | 
| 97 | 1 | reqabi 3459 | . . . . . 6
⊢ (𝑥 ∈ 𝑌 ↔ (𝑥 ∈ 𝐴 ∧ 𝑅 < (𝐹‘𝑥))) | 
| 98 | 96, 97 | sylibr 234 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ∈ 𝑌) | 
| 99 | 98 | ex 412 | . . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐼 ∩ 𝐴) → 𝑥 ∈ 𝑌)) | 
| 100 | 12, 99 | ralrimi 3256 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ (𝐼 ∩ 𝐴)𝑥 ∈ 𝑌) | 
| 101 |  | nfcv 2904 | . . . 4
⊢
Ⅎ𝑥(𝐼 ∩ 𝐴) | 
| 102 |  | nfrab1 3456 | . . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝑅 < (𝐹‘𝑥)} | 
| 103 | 1, 102 | nfcxfr 2902 | . . . 4
⊢
Ⅎ𝑥𝑌 | 
| 104 | 101, 103 | dfss3f 3974 | . . 3
⊢ ((𝐼 ∩ 𝐴) ⊆ 𝑌 ↔ ∀𝑥 ∈ (𝐼 ∩ 𝐴)𝑥 ∈ 𝑌) | 
| 105 | 100, 104 | sylibr 234 | . 2
⊢ (𝜑 → (𝐼 ∩ 𝐴) ⊆ 𝑌) | 
| 106 | 11, 105 | eqssd 4000 | 1
⊢ (𝜑 → 𝑌 = (𝐼 ∩ 𝐴)) |