Metamath Proof Explorer

Theorem volivth

Description: The Intermediate Value Theorem for the Lebesgue volume function. For any positive B <_ ( volA ) , there is a measurable subset of A whose volume is B . (Contributed by Mario Carneiro, 30-Aug-2014)

Ref Expression
Assertion volivth ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) → ∃ 𝑥 ∈ dom vol ( 𝑥 ⊆ 𝐴 ∧ ( vol ‘ 𝑥 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) → 𝐴 ∈ dom vol )
2 mnfxr ⊢ -∞ ∈ ℝ*
3 2 a1i ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) → -∞ ∈ ℝ* )
4 iccssxr ⊢ ( 0 [,] ( vol ‘ 𝐴 ) ) ⊆ ℝ*
5 simpr ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) → 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) )
6 4 5 sseldi ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) → 𝐵 ∈ ℝ* )
7 6 adantr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) → 𝐵 ∈ ℝ* )
8 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
9 volf ⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
10 9 ffvelrni ⊢ ( 𝐴 ∈ dom vol → ( vol ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
11 8 10 sseldi ⊢ ( 𝐴 ∈ dom vol → ( vol ‘ 𝐴 ) ∈ ℝ* )
12 11 adantr ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) → ( vol ‘ 𝐴 ) ∈ ℝ* )
13 12 adantr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) → ( vol ‘ 𝐴 ) ∈ ℝ* )
14 0xr ⊢ 0 ∈ ℝ*
15 elicc1 ⊢ ( ( 0 ∈ ℝ* ∧ ( vol ‘ 𝐴 ) ∈ ℝ* ) → ( 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ↔ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ∧ 𝐵 ≤ ( vol ‘ 𝐴 ) ) ) )
16 14 12 15 sylancr ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) → ( 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ↔ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ∧ 𝐵 ≤ ( vol ‘ 𝐴 ) ) ) )
17 5 16 mpbid ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) → ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ∧ 𝐵 ≤ ( vol ‘ 𝐴 ) ) )
18 17 simp2d ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) → 0 ≤ 𝐵 )
19 18 adantr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) → 0 ≤ 𝐵 )
20 mnflt0 ⊢ -∞ < 0
21 xrltletr ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( -∞ < 0 ∧ 0 ≤ 𝐵 ) → -∞ < 𝐵 ) )
22 20 21 mpani ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 ≤ 𝐵 → -∞ < 𝐵 ) )
23 2 14 22 mp3an12 ⊢ ( 𝐵 ∈ ℝ* → ( 0 ≤ 𝐵 → -∞ < 𝐵 ) )
24 7 19 23 sylc ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) → -∞ < 𝐵 )
25 simpr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) → 𝐵 < ( vol ‘ 𝐴 ) )
26 xrre2 ⊢ ( ( ( -∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( vol ‘ 𝐴 ) ∈ ℝ* ) ∧ ( -∞ < 𝐵 ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ) → 𝐵 ∈ ℝ )
27 3 7 13 24 25 26 syl32anc ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) → 𝐵 ∈ ℝ )
28 volsup2 ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < ( vol ‘ 𝐴 ) ) → ∃ 𝑛 ∈ ℕ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) )
29 1 27 25 28 syl3anc ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) → ∃ 𝑛 ∈ ℕ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) )
30 nnre ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
31 30 ad2antrl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → 𝑛 ∈ ℝ )
32 31 renegcld ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → - 𝑛 ∈ ℝ )
33 27 adantr ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → 𝐵 ∈ ℝ )
34 0red ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → 0 ∈ ℝ )
35 nngt0 ⊢ ( 𝑛 ∈ ℕ → 0 < 𝑛 )
36 35 ad2antrl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → 0 < 𝑛 )
37 31 lt0neg2d ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( 0 < 𝑛 ↔ - 𝑛 < 0 ) )
38 36 37 mpbid ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → - 𝑛 < 0 )
39 32 34 31 38 36 lttrd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → - 𝑛 < 𝑛 )
40 iccssre ⊢ ( ( - 𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( - 𝑛 [,] 𝑛 ) ⊆ ℝ )
41 32 31 40 syl2anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( - 𝑛 [,] 𝑛 ) ⊆ ℝ )
42 ax-resscn ⊢ ℝ ⊆ ℂ
43 ssid ⊢ ℂ ⊆ ℂ
44 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℝ –cn→ ℝ ) ⊆ ( ℝ –cn→ ℂ ) )
45 42 43 44 mp2an ⊢ ( ℝ –cn→ ℝ ) ⊆ ( ℝ –cn→ ℂ )
46 1 adantr ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → 𝐴 ∈ dom vol )
47 eqid ⊢ ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) )
48 47 volcn ⊢ ( ( 𝐴 ∈ dom vol ∧ - 𝑛 ∈ ℝ ) → ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ∈ ( ℝ –cn→ ℝ ) )
49 46 32 48 syl2anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ∈ ( ℝ –cn→ ℝ ) )
50 45 49 sseldi ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ∈ ( ℝ –cn→ ℂ ) )
51 41 sselda ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ 𝑢 ∈ ( - 𝑛 [,] 𝑛 ) ) → 𝑢 ∈ ℝ )
52 cncff ⊢ ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ∈ ( ℝ –cn→ ℝ ) → ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) : ℝ ⟶ ℝ )
53 49 52 syl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) : ℝ ⟶ ℝ )
54 53 ffvelrnda ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ 𝑢 ∈ ℝ ) → ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ 𝑢 ) ∈ ℝ )
55 51 54 syldan ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ 𝑢 ∈ ( - 𝑛 [,] 𝑛 ) ) → ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ 𝑢 ) ∈ ℝ )
56 oveq2 ⊢ ( 𝑦 = - 𝑛 → ( - 𝑛 [,] 𝑦 ) = ( - 𝑛 [,] - 𝑛 ) )
57 56 ineq2d ⊢ ( 𝑦 = - 𝑛 → ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) = ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) )
58 57 fveq2d ⊢ ( 𝑦 = - 𝑛 → ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) = ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ) )
59 fvex ⊢ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ) ∈ V
60 58 47 59 fvmpt ⊢ ( - 𝑛 ∈ ℝ → ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ - 𝑛 ) = ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ) )
61 32 60 syl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ - 𝑛 ) = ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ) )
62 inss2 ⊢ ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ⊆ ( - 𝑛 [,] - 𝑛 )
63 32 rexrd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → - 𝑛 ∈ ℝ* )
64 iccid ⊢ ( - 𝑛 ∈ ℝ* → ( - 𝑛 [,] - 𝑛 ) = { - 𝑛 } )
65 63 64 syl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( - 𝑛 [,] - 𝑛 ) = { - 𝑛 } )
66 62 65 sseqtrid ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ⊆ { - 𝑛 } )
67 32 snssd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → { - 𝑛 } ⊆ ℝ )
68 66 67 sstrd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ⊆ ℝ )
69 ovolsn ⊢ ( - 𝑛 ∈ ℝ → ( vol* ‘ { - 𝑛 } ) = 0 )
70 32 69 syl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( vol* ‘ { - 𝑛 } ) = 0 )
71 ovolssnul ⊢ ( ( ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ⊆ { - 𝑛 } ∧ { - 𝑛 } ⊆ ℝ ∧ ( vol* ‘ { - 𝑛 } ) = 0 ) → ( vol* ‘ ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ) = 0 )
72 66 67 70 71 syl3anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( vol* ‘ ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ) = 0 )
73 nulmbl ⊢ ( ( ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ) = 0 ) → ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ∈ dom vol )
74 68 72 73 syl2anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ∈ dom vol )
75 mblvol ⊢ ( ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ∈ dom vol → ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ) = ( vol* ‘ ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ) )
76 74 75 syl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ) = ( vol* ‘ ( 𝐴 ∩ ( - 𝑛 [,] - 𝑛 ) ) ) )
77 61 76 72 3eqtrd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ - 𝑛 ) = 0 )
78 19 adantr ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → 0 ≤ 𝐵 )
79 77 78 eqbrtrd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ - 𝑛 ) ≤ 𝐵 )
80 7 adantr ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → 𝐵 ∈ ℝ* )
81 iccmbl ⊢ ( ( - 𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( - 𝑛 [,] 𝑛 ) ∈ dom vol )
82 32 31 81 syl2anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( - 𝑛 [,] 𝑛 ) ∈ dom vol )
83 inmbl ⊢ ( ( 𝐴 ∈ dom vol ∧ ( - 𝑛 [,] 𝑛 ) ∈ dom vol ) → ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ∈ dom vol )
84 46 82 83 syl2anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ∈ dom vol )
85 9 ffvelrni ⊢ ( ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ∈ dom vol → ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ∈ ( 0 [,] +∞ ) )
86 8 85 sseldi ⊢ ( ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ∈ dom vol → ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ∈ ℝ* )
87 84 86 syl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ∈ ℝ* )
88 simprr ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) )
89 80 87 88 xrltled ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → 𝐵 ≤ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) )
90 oveq2 ⊢ ( 𝑦 = 𝑛 → ( - 𝑛 [,] 𝑦 ) = ( - 𝑛 [,] 𝑛 ) )
91 90 ineq2d ⊢ ( 𝑦 = 𝑛 → ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) = ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) )
92 91 fveq2d ⊢ ( 𝑦 = 𝑛 → ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) = ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) )
93 fvex ⊢ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ∈ V
94 92 47 93 fvmpt ⊢ ( 𝑛 ∈ ℝ → ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ 𝑛 ) = ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) )
95 31 94 syl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ 𝑛 ) = ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) )
96 89 95 breqtrrd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → 𝐵 ≤ ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ 𝑛 ) )
97 79 96 jca ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ - 𝑛 ) ≤ 𝐵 ∧ 𝐵 ≤ ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ 𝑛 ) ) )
98 32 31 33 39 41 50 55 97 ivthle ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ∃ 𝑧 ∈ ( - 𝑛 [,] 𝑛 ) ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ 𝑧 ) = 𝐵 )
99 41 sselda ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ 𝑧 ∈ ( - 𝑛 [,] 𝑛 ) ) → 𝑧 ∈ ℝ )
100 oveq2 ⊢ ( 𝑦 = 𝑧 → ( - 𝑛 [,] 𝑦 ) = ( - 𝑛 [,] 𝑧 ) )
101 100 ineq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) = ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) )
102 101 fveq2d ⊢ ( 𝑦 = 𝑧 → ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) = ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) )
103 fvex ⊢ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) ∈ V
104 102 47 103 fvmpt ⊢ ( 𝑧 ∈ ℝ → ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ 𝑧 ) = ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) )
105 99 104 syl ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ 𝑧 ∈ ( - 𝑛 [,] 𝑛 ) ) → ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ 𝑧 ) = ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) )
106 105 eqeq1d ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ 𝑧 ∈ ( - 𝑛 [,] 𝑛 ) ) → ( ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ 𝑧 ) = 𝐵 ↔ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) = 𝐵 ) )
107 46 adantr ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ ( 𝑧 ∈ ( - 𝑛 [,] 𝑛 ) ∧ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) = 𝐵 ) ) → 𝐴 ∈ dom vol )
108 32 adantr ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ ( 𝑧 ∈ ( - 𝑛 [,] 𝑛 ) ∧ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) = 𝐵 ) ) → - 𝑛 ∈ ℝ )
109 99 adantrr ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ ( 𝑧 ∈ ( - 𝑛 [,] 𝑛 ) ∧ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) = 𝐵 ) ) → 𝑧 ∈ ℝ )
110 iccmbl ⊢ ( ( - 𝑛 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( - 𝑛 [,] 𝑧 ) ∈ dom vol )
111 108 109 110 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ ( 𝑧 ∈ ( - 𝑛 [,] 𝑛 ) ∧ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) = 𝐵 ) ) → ( - 𝑛 [,] 𝑧 ) ∈ dom vol )
112 inmbl ⊢ ( ( 𝐴 ∈ dom vol ∧ ( - 𝑛 [,] 𝑧 ) ∈ dom vol ) → ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ∈ dom vol )
113 107 111 112 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ ( 𝑧 ∈ ( - 𝑛 [,] 𝑛 ) ∧ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) = 𝐵 ) ) → ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ∈ dom vol )
114 inss1 ⊢ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ⊆ 𝐴
115 114 a1i ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ ( 𝑧 ∈ ( - 𝑛 [,] 𝑛 ) ∧ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) = 𝐵 ) ) → ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ⊆ 𝐴 )
116 simprr ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ ( 𝑧 ∈ ( - 𝑛 [,] 𝑛 ) ∧ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) = 𝐵 ) ) → ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) = 𝐵 )
117 sseq1 ⊢ ( 𝑥 = ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) → ( 𝑥 ⊆ 𝐴 ↔ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ⊆ 𝐴 ) )
118 fveqeq2 ⊢ ( 𝑥 = ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) → ( ( vol ‘ 𝑥 ) = 𝐵 ↔ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) = 𝐵 ) )
119 117 118 anbi12d ⊢ ( 𝑥 = ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) → ( ( 𝑥 ⊆ 𝐴 ∧ ( vol ‘ 𝑥 ) = 𝐵 ) ↔ ( ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ⊆ 𝐴 ∧ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) = 𝐵 ) ) )
120 119 rspcev ⊢ ( ( ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ∈ dom vol ∧ ( ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ⊆ 𝐴 ∧ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) = 𝐵 ) ) → ∃ 𝑥 ∈ dom vol ( 𝑥 ⊆ 𝐴 ∧ ( vol ‘ 𝑥 ) = 𝐵 ) )
121 113 115 116 120 syl12anc ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ ( 𝑧 ∈ ( - 𝑛 [,] 𝑛 ) ∧ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) = 𝐵 ) ) → ∃ 𝑥 ∈ dom vol ( 𝑥 ⊆ 𝐴 ∧ ( vol ‘ 𝑥 ) = 𝐵 ) )
122 121 expr ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ 𝑧 ∈ ( - 𝑛 [,] 𝑛 ) ) → ( ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑧 ) ) ) = 𝐵 → ∃ 𝑥 ∈ dom vol ( 𝑥 ⊆ 𝐴 ∧ ( vol ‘ 𝑥 ) = 𝐵 ) ) )
123 106 122 sylbid ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) ∧ 𝑧 ∈ ( - 𝑛 [,] 𝑛 ) ) → ( ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ 𝑧 ) = 𝐵 → ∃ 𝑥 ∈ dom vol ( 𝑥 ⊆ 𝐴 ∧ ( vol ‘ 𝑥 ) = 𝐵 ) ) )
124 123 rexlimdva ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ( ∃ 𝑧 ∈ ( - 𝑛 [,] 𝑛 ) ( ( 𝑦 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑦 ) ) ) ) ‘ 𝑧 ) = 𝐵 → ∃ 𝑥 ∈ dom vol ( 𝑥 ⊆ 𝐴 ∧ ( vol ‘ 𝑥 ) = 𝐵 ) ) )
125 98 124 mpd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 < ( vol ‘ ( 𝐴 ∩ ( - 𝑛 [,] 𝑛 ) ) ) ) ) → ∃ 𝑥 ∈ dom vol ( 𝑥 ⊆ 𝐴 ∧ ( vol ‘ 𝑥 ) = 𝐵 ) )
126 29 125 rexlimddv ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 < ( vol ‘ 𝐴 ) ) → ∃ 𝑥 ∈ dom vol ( 𝑥 ⊆ 𝐴 ∧ ( vol ‘ 𝑥 ) = 𝐵 ) )
127 simpll ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 = ( vol ‘ 𝐴 ) ) → 𝐴 ∈ dom vol )
128 ssid ⊢ 𝐴 ⊆ 𝐴
129 128 a1i ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 = ( vol ‘ 𝐴 ) ) → 𝐴 ⊆ 𝐴 )
130 simpr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 = ( vol ‘ 𝐴 ) ) → 𝐵 = ( vol ‘ 𝐴 ) )
131 130 eqcomd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 = ( vol ‘ 𝐴 ) ) → ( vol ‘ 𝐴 ) = 𝐵 )
132 sseq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
133 fveqeq2 ⊢ ( 𝑥 = 𝐴 → ( ( vol ‘ 𝑥 ) = 𝐵 ↔ ( vol ‘ 𝐴 ) = 𝐵 ) )
134 132 133 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ⊆ 𝐴 ∧ ( vol ‘ 𝑥 ) = 𝐵 ) ↔ ( 𝐴 ⊆ 𝐴 ∧ ( vol ‘ 𝐴 ) = 𝐵 ) ) )
135 134 rspcev ⊢ ( ( 𝐴 ∈ dom vol ∧ ( 𝐴 ⊆ 𝐴 ∧ ( vol ‘ 𝐴 ) = 𝐵 ) ) → ∃ 𝑥 ∈ dom vol ( 𝑥 ⊆ 𝐴 ∧ ( vol ‘ 𝑥 ) = 𝐵 ) )
136 127 129 131 135 syl12anc ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) ∧ 𝐵 = ( vol ‘ 𝐴 ) ) → ∃ 𝑥 ∈ dom vol ( 𝑥 ⊆ 𝐴 ∧ ( vol ‘ 𝑥 ) = 𝐵 ) )
137 17 simp3d ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) → 𝐵 ≤ ( vol ‘ 𝐴 ) )
138 xrleloe ⊢ ( ( 𝐵 ∈ ℝ* ∧ ( vol ‘ 𝐴 ) ∈ ℝ* ) → ( 𝐵 ≤ ( vol ‘ 𝐴 ) ↔ ( 𝐵 < ( vol ‘ 𝐴 ) ∨ 𝐵 = ( vol ‘ 𝐴 ) ) ) )
139 6 12 138 syl2anc ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) → ( 𝐵 ≤ ( vol ‘ 𝐴 ) ↔ ( 𝐵 < ( vol ‘ 𝐴 ) ∨ 𝐵 = ( vol ‘ 𝐴 ) ) ) )
140 137 139 mpbid ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) → ( 𝐵 < ( vol ‘ 𝐴 ) ∨ 𝐵 = ( vol ‘ 𝐴 ) ) )
141 126 136 140 mpjaodan ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ( 0 [,] ( vol ‘ 𝐴 ) ) ) → ∃ 𝑥 ∈ dom vol ( 𝑥 ⊆ 𝐴 ∧ ( vol ‘ 𝑥 ) = 𝐵 ) )