Proof of Theorem pimdecfgtioo
Step | Hyp | Ref
| Expression |
1 | | pimdecfgtioo.y |
. . . . . . 7
⊢ 𝑌 = {𝑥 ∈ 𝐴 ∣ 𝑅 < (𝐹‘𝑥)} |
2 | | ssrab2 3650 |
. . . . . . 7
⊢ {𝑥 ∈ 𝐴 ∣ 𝑅 < (𝐹‘𝑥)} ⊆ 𝐴 |
3 | 1, 2 | eqsstri 3598 |
. . . . . 6
⊢ 𝑌 ⊆ 𝐴 |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑌 ⊆ 𝐴) |
5 | | pimdecfgtioo.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
6 | 4, 5 | sstrd 3578 |
. . . 4
⊢ (𝜑 → 𝑌 ⊆ ℝ) |
7 | | pimdecfgtioo.c |
. . . 4
⊢ 𝑆 = sup(𝑌, ℝ*, <
) |
8 | | pimdecfgtioo.e |
. . . 4
⊢ (𝜑 → ¬ 𝑆 ∈ 𝑌) |
9 | | pimdecfgtioo.i |
. . . 4
⊢ 𝐼 = (-∞(,)𝑆) |
10 | 6, 7, 8, 9 | ressioosup 38629 |
. . 3
⊢ (𝜑 → 𝑌 ⊆ 𝐼) |
11 | 10, 4 | ssind 3799 |
. 2
⊢ (𝜑 → 𝑌 ⊆ (𝐼 ∩ 𝐴)) |
12 | | pimdecfgtioo.x |
. . . 4
⊢
Ⅎ𝑥𝜑 |
13 | | elinel2 3762 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐼 ∩ 𝐴) → 𝑥 ∈ 𝐴) |
14 | 13 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ∈ 𝐴) |
15 | | mnfxr 9975 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
16 | 15 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → -∞ ∈
ℝ*) |
17 | | ressxr 9962 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℝ* |
18 | 6, 17 | syl6ss 3580 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ⊆
ℝ*) |
19 | 18 | supxrcld 38321 |
. . . . . . . . . . . 12
⊢ (𝜑 → sup(𝑌, ℝ*, < ) ∈
ℝ*) |
20 | 7, 19 | syl5eqel 2692 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈
ℝ*) |
21 | 20 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑆 ∈
ℝ*) |
22 | | elinel1 3761 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐼 ∩ 𝐴) → 𝑥 ∈ 𝐼) |
23 | 22, 9 | syl6eleq 2698 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐼 ∩ 𝐴) → 𝑥 ∈ (-∞(,)𝑆)) |
24 | 23 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ∈ (-∞(,)𝑆)) |
25 | | iooltub 38582 |
. . . . . . . . . 10
⊢
((-∞ ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ 𝑥 ∈ (-∞(,)𝑆)) → 𝑥 < 𝑆) |
26 | 16, 21, 24, 25 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 < 𝑆) |
27 | 26 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → 𝑥 < 𝑆) |
28 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → ¬ 𝑅 < (𝐹‘𝑥)) |
29 | | pimdecfgtioo.f |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝐹:𝐴⟶ℝ*) |
31 | 30, 14 | ffvelrnd 6268 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → (𝐹‘𝑥) ∈
ℝ*) |
32 | 31 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → (𝐹‘𝑥) ∈
ℝ*) |
33 | | pimdecfgtioo.r |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑅 ∈
ℝ*) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → 𝑅 ∈
ℝ*) |
36 | 32, 35 | xrlenltd 9983 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → ((𝐹‘𝑥) ≤ 𝑅 ↔ ¬ 𝑅 < (𝐹‘𝑥))) |
37 | 28, 36 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → (𝐹‘𝑥) ≤ 𝑅) |
38 | | pimdecfgtioo.h |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦𝜑 |
39 | | nfv 1830 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦 𝑥 ∈ (𝐼 ∩ 𝐴) |
40 | 38, 39 | nfan 1816 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) |
41 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(𝐹‘𝑥) ≤ 𝑅 |
42 | 40, 41 | nfan 1816 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) |
43 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
44 | 43 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝑅 < (𝐹‘𝑥) ↔ 𝑅 < (𝐹‘𝑦))) |
45 | 44, 1 | elrab2 3333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝑌 ↔ (𝑦 ∈ 𝐴 ∧ 𝑅 < (𝐹‘𝑦))) |
46 | 45 | biimpi 205 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑌 → (𝑦 ∈ 𝐴 ∧ 𝑅 < (𝐹‘𝑦))) |
47 | 46 | simprd 478 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝑌 → 𝑅 < (𝐹‘𝑦)) |
48 | 47 | ad2antlr 759 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑅 < (𝐹‘𝑦)) |
49 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝐴 ⊆ ℝ) |
50 | 49, 14 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ∈ ℝ) |
51 | 50 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑥 ∈ ℝ) |
52 | 6 | sselda 3568 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ ℝ) |
53 | 52 | ad4ant13 1284 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑦 ∈ ℝ) |
54 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → ¬ 𝑦 ≤ 𝑥) |
55 | 51, 53 | ltnled 10063 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → (𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥)) |
56 | 54, 55 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑥 < 𝑦) |
57 | 51, 53, 56 | ltled 10064 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑥 ≤ 𝑦) |
58 | 57 | adantllr 751 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑥 ≤ 𝑦) |
59 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝐹:𝐴⟶ℝ*) |
60 | 4 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝐴) |
61 | 59, 60 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → (𝐹‘𝑦) ∈
ℝ*) |
62 | 61 | ad5ant14 1294 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑦) ∈
ℝ*) |
63 | 31 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑥) ∈
ℝ*) |
64 | 34 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → 𝑅 ∈
ℝ*) |
65 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → 𝑥 ≤ 𝑦) |
66 | | pimdecfgtioo.d |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) |
67 | | rspa 2914 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥)) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) |
68 | 66, 13, 67 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) |
69 | 68 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) |
70 | 60 | ad4ant13 1284 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → 𝑦 ∈ 𝐴) |
71 | | rspa 2914 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑦 ∈
𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) |
72 | 69, 70, 71 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥))) |
73 | 65, 72 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑦) ≤ (𝐹‘𝑥)) |
74 | 73 | adantllr 751 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑦) ≤ (𝐹‘𝑥)) |
75 | | simpllr 795 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑥) ≤ 𝑅) |
76 | 62, 63, 64, 74, 75 | xrletrd 11869 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → (𝐹‘𝑦) ≤ 𝑅) |
77 | 62, 64 | xrlenltd 9983 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → ((𝐹‘𝑦) ≤ 𝑅 ↔ ¬ 𝑅 < (𝐹‘𝑦))) |
78 | 76, 77 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ 𝑥 ≤ 𝑦) → ¬ 𝑅 < (𝐹‘𝑦)) |
79 | 58, 78 | syldan 486 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) ∧ ¬ 𝑦 ≤ 𝑥) → ¬ 𝑅 < (𝐹‘𝑦)) |
80 | 48, 79 | condan 831 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) ∧ 𝑦 ∈ 𝑌) → 𝑦 ≤ 𝑥) |
81 | 80 | ex 449 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) → (𝑦 ∈ 𝑌 → 𝑦 ≤ 𝑥)) |
82 | 42, 81 | ralrimi 2940 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ (𝐹‘𝑥) ≤ 𝑅) → ∀𝑦 ∈ 𝑌 𝑦 ≤ 𝑥) |
83 | 37, 82 | syldan 486 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → ∀𝑦 ∈ 𝑌 𝑦 ≤ 𝑥) |
84 | 18 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑌 ⊆
ℝ*) |
85 | 17, 50 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ∈ ℝ*) |
86 | | supxrleub 12028 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ⊆ ℝ*
∧ 𝑥 ∈
ℝ*) → (sup(𝑌, ℝ*, < ) ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑌 𝑦 ≤ 𝑥)) |
87 | 84, 85, 86 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → (sup(𝑌, ℝ*, < ) ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑌 𝑦 ≤ 𝑥)) |
88 | 87 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → (sup(𝑌, ℝ*, < ) ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑌 𝑦 ≤ 𝑥)) |
89 | 83, 88 | mpbird 246 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → sup(𝑌, ℝ*, < ) ≤ 𝑥) |
90 | 7, 89 | syl5eqbr 4618 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → 𝑆 ≤ 𝑥) |
91 | 21 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → 𝑆 ∈
ℝ*) |
92 | 85 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → 𝑥 ∈ ℝ*) |
93 | 91, 92 | xrlenltd 9983 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → (𝑆 ≤ 𝑥 ↔ ¬ 𝑥 < 𝑆)) |
94 | 90, 93 | mpbid 221 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) ∧ ¬ 𝑅 < (𝐹‘𝑥)) → ¬ 𝑥 < 𝑆) |
95 | 27, 94 | condan 831 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑅 < (𝐹‘𝑥)) |
96 | 14, 95 | jca 553 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → (𝑥 ∈ 𝐴 ∧ 𝑅 < (𝐹‘𝑥))) |
97 | 1 | rabid3 38285 |
. . . . . 6
⊢ (𝑥 ∈ 𝑌 ↔ (𝑥 ∈ 𝐴 ∧ 𝑅 < (𝐹‘𝑥))) |
98 | 96, 97 | sylibr 223 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ∈ 𝑌) |
99 | 98 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐼 ∩ 𝐴) → 𝑥 ∈ 𝑌)) |
100 | 12, 99 | ralrimi 2940 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (𝐼 ∩ 𝐴)𝑥 ∈ 𝑌) |
101 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑥(𝐼 ∩ 𝐴) |
102 | | nfrab1 3099 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝑅 < (𝐹‘𝑥)} |
103 | 1, 102 | nfcxfr 2749 |
. . . 4
⊢
Ⅎ𝑥𝑌 |
104 | 101, 103 | dfss3f 3560 |
. . 3
⊢ ((𝐼 ∩ 𝐴) ⊆ 𝑌 ↔ ∀𝑥 ∈ (𝐼 ∩ 𝐴)𝑥 ∈ 𝑌) |
105 | 100, 104 | sylibr 223 |
. 2
⊢ (𝜑 → (𝐼 ∩ 𝐴) ⊆ 𝑌) |
106 | 11, 105 | eqssd 3585 |
1
⊢ (𝜑 → 𝑌 = (𝐼 ∩ 𝐴)) |