Step | Hyp | Ref
| Expression |
1 | | simpll 790 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐴 ∈ dom vol) |
2 | | mnfxr 10096 |
. . . . . 6
⊢ -∞
∈ ℝ* |
3 | 2 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → -∞ ∈
ℝ*) |
4 | | iccssxr 12256 |
. . . . . . 7
⊢
(0[,](vol‘𝐴))
⊆ ℝ* |
5 | | simpr 477 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 𝐵 ∈ (0[,](vol‘𝐴))) |
6 | 4, 5 | sseldi 3601 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 𝐵 ∈
ℝ*) |
7 | 6 | adantr 481 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐵 ∈
ℝ*) |
8 | | iccssxr 12256 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
9 | | volf 23297 |
. . . . . . . . 9
⊢ vol:dom
vol⟶(0[,]+∞) |
10 | 9 | ffvelrni 6358 |
. . . . . . . 8
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
(0[,]+∞)) |
11 | 8, 10 | sseldi 3601 |
. . . . . . 7
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) ∈
ℝ*) |
12 | 11 | adantr 481 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (vol‘𝐴) ∈
ℝ*) |
13 | 12 | adantr 481 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → (vol‘𝐴) ∈
ℝ*) |
14 | | 0xr 10086 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
15 | | elicc1 12219 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ (vol‘𝐴) ∈ ℝ*) → (𝐵 ∈ (0[,](vol‘𝐴)) ↔ (𝐵 ∈ ℝ* ∧ 0 ≤
𝐵 ∧ 𝐵 ≤ (vol‘𝐴)))) |
16 | 14, 12, 15 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 ∈ (0[,](vol‘𝐴)) ↔ (𝐵 ∈ ℝ* ∧ 0 ≤
𝐵 ∧ 𝐵 ≤ (vol‘𝐴)))) |
17 | 5, 16 | mpbid 222 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 ∈ ℝ* ∧ 0 ≤
𝐵 ∧ 𝐵 ≤ (vol‘𝐴))) |
18 | 17 | simp2d 1074 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 0 ≤ 𝐵) |
19 | 18 | adantr 481 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 0 ≤ 𝐵) |
20 | | mnflt0 11959 |
. . . . . . . 8
⊢ -∞
< 0 |
21 | | xrltletr 11988 |
. . . . . . . 8
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((-∞ < 0 ∧ 0 ≤ 𝐵) → -∞ < 𝐵)) |
22 | 20, 21 | mpani 712 |
. . . . . . 7
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (0 ≤ 𝐵 → -∞ < 𝐵)) |
23 | 2, 14, 22 | mp3an12 1414 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
→ (0 ≤ 𝐵 →
-∞ < 𝐵)) |
24 | 7, 19, 23 | sylc 65 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → -∞ < 𝐵) |
25 | | simpr 477 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐵 < (vol‘𝐴)) |
26 | | xrre2 12001 |
. . . . 5
⊢
(((-∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧
(vol‘𝐴) ∈
ℝ*) ∧ (-∞ < 𝐵 ∧ 𝐵 < (vol‘𝐴))) → 𝐵 ∈ ℝ) |
27 | 3, 7, 13, 24, 25, 26 | syl32anc 1334 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐵 ∈ ℝ) |
28 | | volsup2 23373 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
29 | 1, 27, 25, 28 | syl3anc 1326 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
30 | | nnre 11027 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
31 | 30 | ad2antrl 764 |
. . . . . 6
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝑛 ∈ ℝ) |
32 | 31 | renegcld 10457 |
. . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → -𝑛 ∈ ℝ) |
33 | 27 | adantr 481 |
. . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐵 ∈ ℝ) |
34 | | 0red 10041 |
. . . . . 6
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 0 ∈
ℝ) |
35 | | nngt0 11049 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 0 <
𝑛) |
36 | 35 | ad2antrl 764 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 0 < 𝑛) |
37 | 31 | lt0neg2d 10598 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (0 < 𝑛 ↔ -𝑛 < 0)) |
38 | 36, 37 | mpbid 222 |
. . . . . 6
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → -𝑛 < 0) |
39 | 32, 34, 31, 38, 36 | lttrd 10198 |
. . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → -𝑛 < 𝑛) |
40 | | iccssre 12255 |
. . . . . 6
⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ⊆ ℝ) |
41 | 32, 31, 40 | syl2anc 693 |
. . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (-𝑛[,]𝑛) ⊆ ℝ) |
42 | | ax-resscn 9993 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
43 | | ssid 3624 |
. . . . . . 7
⊢ ℂ
⊆ ℂ |
44 | | cncfss 22702 |
. . . . . . 7
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ)) |
45 | 42, 43, 44 | mp2an 708 |
. . . . . 6
⊢
(ℝ–cn→ℝ)
⊆ (ℝ–cn→ℂ) |
46 | 1 | adantr 481 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐴 ∈ dom vol) |
47 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ ↦
(vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) = (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) |
48 | 47 | volcn 23374 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ -𝑛 ∈ ℝ) → (𝑦 ∈ ℝ ↦
(vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) ∈ (ℝ–cn→ℝ)) |
49 | 46, 32, 48 | syl2anc 693 |
. . . . . 6
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) ∈ (ℝ–cn→ℝ)) |
50 | 45, 49 | sseldi 3601 |
. . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) ∈ (ℝ–cn→ℂ)) |
51 | 41 | sselda 3603 |
. . . . . 6
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑢 ∈ (-𝑛[,]𝑛)) → 𝑢 ∈ ℝ) |
52 | | cncff 22696 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ↦
(vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) ∈ (ℝ–cn→ℝ) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))):ℝ⟶ℝ) |
53 | 49, 52 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))):ℝ⟶ℝ) |
54 | 53 | ffvelrnda 6359 |
. . . . . 6
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑢 ∈ ℝ) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑢) ∈ ℝ) |
55 | 51, 54 | syldan 487 |
. . . . 5
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑢 ∈ (-𝑛[,]𝑛)) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑢) ∈ ℝ) |
56 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑦 = -𝑛 → (-𝑛[,]𝑦) = (-𝑛[,]-𝑛)) |
57 | 56 | ineq2d 3814 |
. . . . . . . . . . 11
⊢ (𝑦 = -𝑛 → (𝐴 ∩ (-𝑛[,]𝑦)) = (𝐴 ∩ (-𝑛[,]-𝑛))) |
58 | 57 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑦 = -𝑛 → (vol‘(𝐴 ∩ (-𝑛[,]𝑦))) = (vol‘(𝐴 ∩ (-𝑛[,]-𝑛)))) |
59 | | fvex 6201 |
. . . . . . . . . 10
⊢
(vol‘(𝐴 ∩
(-𝑛[,]-𝑛))) ∈ V |
60 | 58, 47, 59 | fvmpt 6282 |
. . . . . . . . 9
⊢ (-𝑛 ∈ ℝ → ((𝑦 ∈ ℝ ↦
(vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘-𝑛) = (vol‘(𝐴 ∩ (-𝑛[,]-𝑛)))) |
61 | 32, 60 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘-𝑛) = (vol‘(𝐴 ∩ (-𝑛[,]-𝑛)))) |
62 | | inss2 3834 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ (-𝑛[,]-𝑛)) ⊆ (-𝑛[,]-𝑛) |
63 | 32 | rexrd 10089 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → -𝑛 ∈ ℝ*) |
64 | | iccid 12220 |
. . . . . . . . . . . . 13
⊢ (-𝑛 ∈ ℝ*
→ (-𝑛[,]-𝑛) = {-𝑛}) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (-𝑛[,]-𝑛) = {-𝑛}) |
66 | 62, 65 | syl5sseq 3653 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝐴 ∩ (-𝑛[,]-𝑛)) ⊆ {-𝑛}) |
67 | 32 | snssd 4340 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → {-𝑛} ⊆ ℝ) |
68 | 66, 67 | sstrd 3613 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝐴 ∩ (-𝑛[,]-𝑛)) ⊆ ℝ) |
69 | | ovolsn 23263 |
. . . . . . . . . . . 12
⊢ (-𝑛 ∈ ℝ →
(vol*‘{-𝑛}) =
0) |
70 | 32, 69 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (vol*‘{-𝑛}) = 0) |
71 | | ovolssnul 23255 |
. . . . . . . . . . 11
⊢ (((𝐴 ∩ (-𝑛[,]-𝑛)) ⊆ {-𝑛} ∧ {-𝑛} ⊆ ℝ ∧ (vol*‘{-𝑛}) = 0) →
(vol*‘(𝐴 ∩
(-𝑛[,]-𝑛))) = 0) |
72 | 66, 67, 70, 71 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (vol*‘(𝐴 ∩ (-𝑛[,]-𝑛))) = 0) |
73 | | nulmbl 23303 |
. . . . . . . . . 10
⊢ (((𝐴 ∩ (-𝑛[,]-𝑛)) ⊆ ℝ ∧ (vol*‘(𝐴 ∩ (-𝑛[,]-𝑛))) = 0) → (𝐴 ∩ (-𝑛[,]-𝑛)) ∈ dom vol) |
74 | 68, 72, 73 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝐴 ∩ (-𝑛[,]-𝑛)) ∈ dom vol) |
75 | | mblvol 23298 |
. . . . . . . . 9
⊢ ((𝐴 ∩ (-𝑛[,]-𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ (-𝑛[,]-𝑛))) = (vol*‘(𝐴 ∩ (-𝑛[,]-𝑛)))) |
76 | 74, 75 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (vol‘(𝐴 ∩ (-𝑛[,]-𝑛))) = (vol*‘(𝐴 ∩ (-𝑛[,]-𝑛)))) |
77 | 61, 76, 72 | 3eqtrd 2660 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘-𝑛) = 0) |
78 | 19 | adantr 481 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 0 ≤ 𝐵) |
79 | 77, 78 | eqbrtrd 4675 |
. . . . . 6
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘-𝑛) ≤ 𝐵) |
80 | | simprr 796 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
81 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐵 ∈
ℝ*) |
82 | | iccmbl 23334 |
. . . . . . . . . . . 12
⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ∈ dom vol) |
83 | 32, 31, 82 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (-𝑛[,]𝑛) ∈ dom vol) |
84 | | inmbl 23310 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom vol ∧ (-𝑛[,]𝑛) ∈ dom vol) → (𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol) |
85 | 46, 83, 84 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol) |
86 | 9 | ffvelrni 6358 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈ (0[,]+∞)) |
87 | 8, 86 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈
ℝ*) |
88 | 85, 87 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈
ℝ*) |
89 | | xrltle 11982 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ (vol‘(𝐴 ∩
(-𝑛[,]𝑛))) ∈ ℝ*) → (𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) → 𝐵 ≤ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) |
90 | 81, 88, 89 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) → 𝐵 ≤ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) |
91 | 80, 90 | mpd 15 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐵 ≤ (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
92 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑛 → (-𝑛[,]𝑦) = (-𝑛[,]𝑛)) |
93 | 92 | ineq2d 3814 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑛 → (𝐴 ∩ (-𝑛[,]𝑦)) = (𝐴 ∩ (-𝑛[,]𝑛))) |
94 | 93 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑦 = 𝑛 → (vol‘(𝐴 ∩ (-𝑛[,]𝑦))) = (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
95 | | fvex 6201 |
. . . . . . . . 9
⊢
(vol‘(𝐴 ∩
(-𝑛[,]𝑛))) ∈ V |
96 | 94, 47, 95 | fvmpt 6282 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ → ((𝑦 ∈ ℝ ↦
(vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑛) = (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
97 | 31, 96 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑛) = (vol‘(𝐴 ∩ (-𝑛[,]𝑛)))) |
98 | 91, 97 | breqtrrd 4681 |
. . . . . 6
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐵 ≤ ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑛)) |
99 | 79, 98 | jca 554 |
. . . . 5
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘-𝑛) ≤ 𝐵 ∧ 𝐵 ≤ ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑛))) |
100 | 32, 31, 33, 39, 41, 50, 55, 99 | ivthle 23225 |
. . . 4
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ∃𝑧 ∈ (-𝑛[,]𝑛)((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = 𝐵) |
101 | 41 | sselda 3603 |
. . . . . . . 8
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑧 ∈ (-𝑛[,]𝑛)) → 𝑧 ∈ ℝ) |
102 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (-𝑛[,]𝑦) = (-𝑛[,]𝑧)) |
103 | 102 | ineq2d 3814 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (𝐴 ∩ (-𝑛[,]𝑦)) = (𝐴 ∩ (-𝑛[,]𝑧))) |
104 | 103 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (vol‘(𝐴 ∩ (-𝑛[,]𝑦))) = (vol‘(𝐴 ∩ (-𝑛[,]𝑧)))) |
105 | | fvex 6201 |
. . . . . . . . 9
⊢
(vol‘(𝐴 ∩
(-𝑛[,]𝑧))) ∈ V |
106 | 104, 47, 105 | fvmpt 6282 |
. . . . . . . 8
⊢ (𝑧 ∈ ℝ → ((𝑦 ∈ ℝ ↦
(vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = (vol‘(𝐴 ∩ (-𝑛[,]𝑧)))) |
107 | 101, 106 | syl 17 |
. . . . . . 7
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑧 ∈ (-𝑛[,]𝑛)) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = (vol‘(𝐴 ∩ (-𝑛[,]𝑧)))) |
108 | 107 | eqeq1d 2624 |
. . . . . 6
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑧 ∈ (-𝑛[,]𝑛)) → (((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = 𝐵 ↔ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) |
109 | 46 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → 𝐴 ∈ dom vol) |
110 | 32 | adantr 481 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → -𝑛 ∈ ℝ) |
111 | 101 | adantrr 753 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → 𝑧 ∈ ℝ) |
112 | | iccmbl 23334 |
. . . . . . . . . 10
⊢ ((-𝑛 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-𝑛[,]𝑧) ∈ dom vol) |
113 | 110, 111,
112 | syl2anc 693 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → (-𝑛[,]𝑧) ∈ dom vol) |
114 | | inmbl 23310 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom vol ∧ (-𝑛[,]𝑧) ∈ dom vol) → (𝐴 ∩ (-𝑛[,]𝑧)) ∈ dom vol) |
115 | 109, 113,
114 | syl2anc 693 |
. . . . . . . 8
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → (𝐴 ∩ (-𝑛[,]𝑧)) ∈ dom vol) |
116 | | inss1 3833 |
. . . . . . . . 9
⊢ (𝐴 ∩ (-𝑛[,]𝑧)) ⊆ 𝐴 |
117 | 116 | a1i 11 |
. . . . . . . 8
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → (𝐴 ∩ (-𝑛[,]𝑧)) ⊆ 𝐴) |
118 | | simprr 796 |
. . . . . . . 8
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵) |
119 | | sseq1 3626 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐴 ∩ (-𝑛[,]𝑧)) → (𝑥 ⊆ 𝐴 ↔ (𝐴 ∩ (-𝑛[,]𝑧)) ⊆ 𝐴)) |
120 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐴 ∩ (-𝑛[,]𝑧)) → (vol‘𝑥) = (vol‘(𝐴 ∩ (-𝑛[,]𝑧)))) |
121 | 120 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐴 ∩ (-𝑛[,]𝑧)) → ((vol‘𝑥) = 𝐵 ↔ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) |
122 | 119, 121 | anbi12d 747 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴 ∩ (-𝑛[,]𝑧)) → ((𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵) ↔ ((𝐴 ∩ (-𝑛[,]𝑧)) ⊆ 𝐴 ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵))) |
123 | 122 | rspcev 3309 |
. . . . . . . 8
⊢ (((𝐴 ∩ (-𝑛[,]𝑧)) ∈ dom vol ∧ ((𝐴 ∩ (-𝑛[,]𝑧)) ⊆ 𝐴 ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)) |
124 | 115, 117,
118, 123 | syl12anc 1324 |
. . . . . . 7
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)) |
125 | 124 | expr 643 |
. . . . . 6
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑧 ∈ (-𝑛[,]𝑛)) → ((vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵 → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))) |
126 | 108, 125 | sylbid 230 |
. . . . 5
⊢
(((((𝐴 ∈ dom
vol ∧ 𝐵 ∈
(0[,](vol‘𝐴))) ∧
𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑧 ∈ (-𝑛[,]𝑛)) → (((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = 𝐵 → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))) |
127 | 126 | rexlimdva 3031 |
. . . 4
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (∃𝑧 ∈ (-𝑛[,]𝑛)((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = 𝐵 → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))) |
128 | 100, 127 | mpd 15 |
. . 3
⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)) |
129 | 29, 128 | rexlimddv 3035 |
. 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)) |
130 | | simpll 790 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → 𝐴 ∈ dom vol) |
131 | | ssid 3624 |
. . . 4
⊢ 𝐴 ⊆ 𝐴 |
132 | 131 | a1i 11 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → 𝐴 ⊆ 𝐴) |
133 | | simpr 477 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → 𝐵 = (vol‘𝐴)) |
134 | 133 | eqcomd 2628 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → (vol‘𝐴) = 𝐵) |
135 | | sseq1 3626 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
136 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (vol‘𝑥) = (vol‘𝐴)) |
137 | 136 | eqeq1d 2624 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((vol‘𝑥) = 𝐵 ↔ (vol‘𝐴) = 𝐵)) |
138 | 135, 137 | anbi12d 747 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵) ↔ (𝐴 ⊆ 𝐴 ∧ (vol‘𝐴) = 𝐵))) |
139 | 138 | rspcev 3309 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧ (𝐴 ⊆ 𝐴 ∧ (vol‘𝐴) = 𝐵)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)) |
140 | 130, 132,
134, 139 | syl12anc 1324 |
. 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)) |
141 | 17 | simp3d 1075 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 𝐵 ≤ (vol‘𝐴)) |
142 | | xrleloe 11977 |
. . . 4
⊢ ((𝐵 ∈ ℝ*
∧ (vol‘𝐴) ∈
ℝ*) → (𝐵 ≤ (vol‘𝐴) ↔ (𝐵 < (vol‘𝐴) ∨ 𝐵 = (vol‘𝐴)))) |
143 | 6, 12, 142 | syl2anc 693 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 ≤ (vol‘𝐴) ↔ (𝐵 < (vol‘𝐴) ∨ 𝐵 = (vol‘𝐴)))) |
144 | 141, 143 | mpbid 222 |
. 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 < (vol‘𝐴) ∨ 𝐵 = (vol‘𝐴))) |
145 | 129, 140,
144 | mpjaodan 827 |
1
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)) |