Proof of Theorem pimiooltgt
| Step | Hyp | Ref
| Expression |
| 1 | | pimiooltgt.1 |
. . . . 5
⊢
Ⅎ𝑥𝜑 |
| 2 | | pimiooltgt.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈
ℝ*) |
| 3 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐿 ∈
ℝ*) |
| 4 | 3 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ (𝐿(,)𝑅)) → 𝐿 ∈
ℝ*) |
| 5 | | pimiooltgt.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
| 6 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈
ℝ*) |
| 7 | 6 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ (𝐿(,)𝑅)) → 𝑅 ∈
ℝ*) |
| 8 | | simp3 1139 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ (𝐿(,)𝑅)) → 𝐵 ∈ (𝐿(,)𝑅)) |
| 9 | | iooltub 45523 |
. . . . . . 7
⊢ ((𝐿 ∈ ℝ*
∧ 𝑅 ∈
ℝ* ∧ 𝐵
∈ (𝐿(,)𝑅)) → 𝐵 < 𝑅) |
| 10 | 4, 7, 8, 9 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ (𝐿(,)𝑅)) → 𝐵 < 𝑅) |
| 11 | 10 | 3exp 1120 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝐵 ∈ (𝐿(,)𝑅) → 𝐵 < 𝑅))) |
| 12 | 1, 11 | ralrimi 3257 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐵 ∈ (𝐿(,)𝑅) → 𝐵 < 𝑅)) |
| 13 | | ss2rab 4071 |
. . . 4
⊢ ({𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)} ⊆ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∈ (𝐿(,)𝑅) → 𝐵 < 𝑅)) |
| 14 | 12, 13 | sylibr 234 |
. . 3
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)} ⊆ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅}) |
| 15 | | ioogtlb 45508 |
. . . . . . 7
⊢ ((𝐿 ∈ ℝ*
∧ 𝑅 ∈
ℝ* ∧ 𝐵
∈ (𝐿(,)𝑅)) → 𝐿 < 𝐵) |
| 16 | 4, 7, 8, 15 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ (𝐿(,)𝑅)) → 𝐿 < 𝐵) |
| 17 | 16 | 3exp 1120 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝐵 ∈ (𝐿(,)𝑅) → 𝐿 < 𝐵))) |
| 18 | 1, 17 | ralrimi 3257 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐵 ∈ (𝐿(,)𝑅) → 𝐿 < 𝐵)) |
| 19 | | ss2rab 4071 |
. . . 4
⊢ ({𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)} ⊆ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵} ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∈ (𝐿(,)𝑅) → 𝐿 < 𝐵)) |
| 20 | 18, 19 | sylibr 234 |
. . 3
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)} ⊆ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵}) |
| 21 | 14, 20 | ssind 4241 |
. 2
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)} ⊆ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) |
| 22 | | elinel1 4201 |
. . . . . . . . 9
⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵}) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅}) |
| 23 | | ssrab2 4080 |
. . . . . . . . . 10
⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ⊆ 𝐴 |
| 24 | 23 | sseli 3979 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} → 𝑥 ∈ 𝐴) |
| 25 | 22, 24 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵}) → 𝑥 ∈ 𝐴) |
| 26 | 25 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → 𝑥 ∈ 𝐴) |
| 27 | 26, 3 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → 𝐿 ∈
ℝ*) |
| 28 | 26, 6 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → 𝑅 ∈
ℝ*) |
| 29 | | pimiooltgt.4 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈
ℝ*) |
| 30 | 26, 29 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → 𝐵 ∈
ℝ*) |
| 31 | | mnfxr 11318 |
. . . . . . . . . . . 12
⊢ -∞
∈ ℝ* |
| 32 | 31 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → -∞ ∈
ℝ*) |
| 33 | 27 | mnfled 13178 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → -∞ ≤ 𝐿) |
| 34 | | elinel2 4202 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵}) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵}) |
| 35 | | rabidim2 45107 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵} → 𝐿 < 𝐵) |
| 36 | 34, 35 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵}) → 𝐿 < 𝐵) |
| 37 | 36 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → 𝐿 < 𝐵) |
| 38 | 32, 27, 30, 33, 37 | xrlelttrd 13202 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → -∞ < 𝐵) |
| 39 | 32, 30, 38 | xrltned 45368 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → -∞ ≠ 𝐵) |
| 40 | 39 | necomd 2996 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → 𝐵 ≠ -∞) |
| 41 | | pnfxr 11315 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
| 42 | 41 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → +∞ ∈
ℝ*) |
| 43 | | rabidim2 45107 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} → 𝐵 < 𝑅) |
| 44 | 22, 43 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵}) → 𝐵 < 𝑅) |
| 45 | 44 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → 𝐵 < 𝑅) |
| 46 | | pnfge 13172 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ*
→ 𝑅 ≤
+∞) |
| 47 | 28, 46 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → 𝑅 ≤ +∞) |
| 48 | 30, 28, 42, 45, 47 | xrltletrd 13203 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → 𝐵 < +∞) |
| 49 | 30, 42, 48 | xrltned 45368 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → 𝐵 ≠ +∞) |
| 50 | 30, 40, 49 | xrred 45376 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → 𝐵 ∈ ℝ) |
| 51 | 27, 28, 50, 37, 45 | eliood 45511 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → 𝐵 ∈ (𝐿(,)𝑅)) |
| 52 | 26, 51 | jca 511 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ (𝐿(,)𝑅))) |
| 53 | | rabid 3458 |
. . . . . 6
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)} ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ (𝐿(,)𝑅))) |
| 54 | 52, 53 | sylibr 234 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)}) |
| 55 | 54 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵}) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)})) |
| 56 | 1, 55 | ralrimi 3257 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)}) |
| 57 | | nfrab1 3457 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} |
| 58 | | nfrab1 3457 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵} |
| 59 | 57, 58 | nfin 4224 |
. . . 4
⊢
Ⅎ𝑥({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵}) |
| 60 | | nfrab1 3457 |
. . . 4
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)} |
| 61 | 59, 60 | dfss3f 3975 |
. . 3
⊢ (({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵}) ⊆ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)} ↔ ∀𝑥 ∈ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)}) |
| 62 | 56, 61 | sylibr 234 |
. 2
⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵}) ⊆ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)}) |
| 63 | 21, 62 | eqssd 4001 |
1
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (𝐿(,)𝑅)} = ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅} ∩ {𝑥 ∈ 𝐴 ∣ 𝐿 < 𝐵})) |