volivth - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > volivth		Structured version Visualization version GIF version

Theorem volivth 25928

Description: The Intermediate Value Theorem for the Lebesgue volume function. For any positive 𝐵 ≤ (vol‘𝐴), there is a measurable subset of 𝐴 whose volume is 𝐵. (Contributed by Mario Carneiro, 30-Aug-2014.)

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

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵

Proof of Theorem volivth Dummy variables 𝑢 𝑛 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll 779	. . . 4 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐴 ∈ dom vol)
2		mnfxr 11366	. . . . . 6 ⊢ -∞ ∈ ℝ^*
3	2	a1i 11	. . . . 5 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → -∞ ∈ ℝ^*)
4		iccssxr 13561	. . . . . . 7 ⊢ (0[,](vol‘𝐴)) ⊆ ℝ^*
5		simpr 490	. . . . . . 7 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 𝐵 ∈ (0[,](vol‘𝐴)))
6	4, 5	sselid 3906	. . . . . 6 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 𝐵 ∈ ℝ^*)
7	6	adantr 486	. . . . 5 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐵 ∈ ℝ^*)
8		iccssxr 13561	. . . . . . . 8 ⊢ (0[,]+∞) ⊆ ℝ^*
9		volf 25850	. . . . . . . . 9 ⊢ vol:dom vol⟶(0[,]+∞)
10	9	ffvelcdmi 7083	. . . . . . . 8 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) ∈ (0[,]+∞))
11	8, 10	sselid 3906	. . . . . . 7 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) ∈ ℝ^*)
12	11	adantr 486	. . . . . 6 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (vol‘𝐴) ∈ ℝ^*)
13	12	adantr 486	. . . . 5 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → (vol‘𝐴) ∈ ℝ^*)
14		0xr 11356	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
15		elicc1 13520	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ (vol‘𝐴) ∈ ℝ^) → (𝐵 ∈ (0[,](vol‘𝐴)) ↔ (𝐵 ∈ ℝ^ ∧ 0 ≤ 𝐵 ∧ 𝐵 ≤ (vol‘𝐴))))
16	14, 12, 15	sylancr 599	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 ∈ (0[,](vol‘𝐴)) ↔ (𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ∧ 𝐵 ≤ (vol‘𝐴))))
17	5, 16	mpbid 235	. . . . . . . 8 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ∧ 𝐵 ≤ (vol‘𝐴)))
18	17	simp2d 1161	. . . . . . 7 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 0 ≤ 𝐵)
19	18	adantr 486	. . . . . 6 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 0 ≤ 𝐵)
20		mnflt0 13254	. . . . . . . 8 ⊢ -∞ < 0
21		xrltletr 13286	. . . . . . . 8 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((-∞ < 0 ∧ 0 ≤ 𝐵) → -∞ < 𝐵))
22	20, 21	mpani 709	. . . . . . 7 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (0 ≤ 𝐵 → -∞ < 𝐵))
23	2, 14, 22	mp3an12 1480	. . . . . 6 ⊢ (𝐵 ∈ ℝ^* → (0 ≤ 𝐵 → -∞ < 𝐵))
24	7, 19, 23	sylc 66	. . . . 5 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → -∞ < 𝐵)
25		simpr 490	. . . . 5 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐵 < (vol‘𝐴))
26		xrre2 13300	. . . . 5 ⊢ (((-∞ ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (vol‘𝐴) ∈ ℝ^*) ∧ (-∞ < 𝐵 ∧ 𝐵 < (vol‘𝐴))) → 𝐵 ∈ ℝ)
27	3, 7, 13, 24, 25, 26	syl32anc 1405	. . . 4 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐵 ∈ ℝ)
28		volsup2 25926	. . . 4 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))
29	1, 27, 25, 28	syl3anc 1398	. . 3 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))
30		nnre 12342	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
31	30	ad2antrl 741	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 𝑛 ∈ ℝ)
32	31	renegcld 11743	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → -𝑛 ∈ ℝ)
33	27	adantr 486	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 𝐵 ∈ ℝ)
34		0red 11311	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 0 ∈ ℝ)
35		nngt0 12369	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → 0 < 𝑛)
36	35	ad2antrl 741	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 0 < 𝑛)
37	31	lt0neg2d 11886	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (0 < 𝑛 ↔ -𝑛 < 0))
38	36, 37	mpbid 235	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → -𝑛 < 0)
39	32, 34, 31, 38, 36	lttrd 11471	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → -𝑛 < 𝑛)
40		iccssre 13560	. . . . . 6 ⊢ (( -𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ( -𝑛[,]𝑛) ⊆ ℝ)
41	32, 31, 40	syl2anc 596	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ( -𝑛[,]𝑛) ⊆ ℝ)
42		ax-resscn 11257	. . . . . . 7 ⊢ ℝ ⊆ ℂ
43		ssid 3930	. . . . . . 7 ⊢ ℂ ⊆ ℂ
44		cncfss 25220	. . . . . . 7 ⊢ ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
45	42, 43, 44	mp2an 705	. . . . . 6 ⊢ (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ)
46	1	adantr 486	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 𝐴 ∈ dom vol)
47		eqid 2760	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦)))) = (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))
48	47	volcn 25927	. . . . . . 7 ⊢ ((𝐴 ∈ dom vol ∧ -𝑛 ∈ ℝ) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦)))) ∈ (ℝ–cn→ℝ))
49	46, 32, 48	syl2anc 596	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦)))) ∈ (ℝ–cn→ℝ))
50	45, 49	sselid 3906	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦)))) ∈ (ℝ–cn→ℂ))
51	41	sselda 3908	. . . . . 6 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ 𝑢 ∈ ( -𝑛[,]𝑛)) → 𝑢 ∈ ℝ)
52		cncff 25214	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦)))) ∈ (ℝ–cn→ℝ) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦)))):ℝ⟶ℝ)
53	49, 52	syl 18	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦)))):ℝ⟶ℝ)
54	53	ffvelcdmda 7084	. . . . . 6 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ 𝑢 ∈ ℝ) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑢) ∈ ℝ)
55	51, 54	syldan 603	. . . . 5 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ 𝑢 ∈ ( -𝑛[,]𝑛)) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑢) ∈ ℝ)
56		oveq2 7428	. . . . . . . . . . . 12 ⊢ (𝑦 = -𝑛 → ( -𝑛[,]𝑦) = ( -𝑛[,] -𝑛))
57	56	ineq2d 4117	. . . . . . . . . . 11 ⊢ (𝑦 = -𝑛 → (𝐴 ∩ ( -𝑛[,]𝑦)) = (𝐴 ∩ ( -𝑛[,] -𝑛)))
58	57	fveq2d 6889	. . . . . . . . . 10 ⊢ (𝑦 = -𝑛 → (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))) = (vol‘(𝐴 ∩ ( -𝑛[,] -𝑛))))
59		fvex 6898	. . . . . . . . . 10 ⊢ (vol‘(𝐴 ∩ ( -𝑛[,] -𝑛))) ∈ V
60	58, 47, 59	fvmpt 6993	. . . . . . . . 9 ⊢ ( -𝑛 ∈ ℝ → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘ -𝑛) = (vol‘(𝐴 ∩ ( -𝑛[,] -𝑛))))
61	32, 60	syl 18	. . . . . . . 8 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘ -𝑛) = (vol‘(𝐴 ∩ ( -𝑛[,] -𝑛))))
62		inss2 4134	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ ( -𝑛[,] -𝑛)) ⊆ ( -𝑛[,] -𝑛)
63	32	rexrd 11359	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → -𝑛 ∈ ℝ^*)
64		iccid 13521	. . . . . . . . . . . . 13 ⊢ ( -𝑛 ∈ ℝ^* → ( -𝑛[,] -𝑛) = { -𝑛})
65	63, 64	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ( -𝑛[,] -𝑛) = { -𝑛})
66	62, 65	sseqtrid 3950	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (𝐴 ∩ ( -𝑛[,] -𝑛)) ⊆ { -𝑛})
67	32	snssd 4746	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → { -𝑛} ⊆ ℝ)
68	66, 67	sstrd 3918	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (𝐴 ∩ ( -𝑛[,] -𝑛)) ⊆ ℝ)
69		ovolsn 25816	. . . . . . . . . . . 12 ⊢ ( -𝑛 ∈ ℝ → (vol*‘{ -𝑛}) = 0)
70	32, 69	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (vol*‘{ -𝑛}) = 0)
71		ovolssnul 25808	. . . . . . . . . . 11 ⊢ (((𝐴 ∩ ( -𝑛[,] -𝑛)) ⊆ { -𝑛} ∧ { -𝑛} ⊆ ℝ ∧ (vol‘{ -𝑛}) = 0) → (vol‘(𝐴 ∩ ( -𝑛[,] -𝑛))) = 0)
72	66, 67, 70, 71	syl3anc 1398	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (vol*‘(𝐴 ∩ ( -𝑛[,] -𝑛))) = 0)
73		nulmbl 25856	. . . . . . . . . 10 ⊢ (((𝐴 ∩ ( -𝑛[,] -𝑛)) ⊆ ℝ ∧ (vol*‘(𝐴 ∩ ( -𝑛[,] -𝑛))) = 0) → (𝐴 ∩ ( -𝑛[,] -𝑛)) ∈ dom vol)
74	68, 72, 73	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (𝐴 ∩ ( -𝑛[,] -𝑛)) ∈ dom vol)
75		mblvol 25851	. . . . . . . . 9 ⊢ ((𝐴 ∩ ( -𝑛[,] -𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ ( -𝑛[,] -𝑛))) = (vol*‘(𝐴 ∩ ( -𝑛[,] -𝑛))))
76	74, 75	syl 18	. . . . . . . 8 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (vol‘(𝐴 ∩ ( -𝑛[,] -𝑛))) = (vol*‘(𝐴 ∩ ( -𝑛[,] -𝑛))))
77	61, 76, 72	3eqtrd 2799	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘ -𝑛) = 0)
78	19	adantr 486	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 0 ≤ 𝐵)
79	77, 78	eqbrtrd 5126	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘ -𝑛) ≤ 𝐵)
80	7	adantr 486	. . . . . . . 8 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 𝐵 ∈ ℝ^*)
81		iccmbl 25887	. . . . . . . . . . 11 ⊢ (( -𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ( -𝑛[,]𝑛) ∈ dom vol)
82	32, 31, 81	syl2anc 596	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ( -𝑛[,]𝑛) ∈ dom vol)
83		inmbl 25863	. . . . . . . . . 10 ⊢ ((𝐴 ∈ dom vol ∧ ( -𝑛[,]𝑛) ∈ dom vol) → (𝐴 ∩ ( -𝑛[,]𝑛)) ∈ dom vol)
84	46, 82, 83	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (𝐴 ∩ ( -𝑛[,]𝑛)) ∈ dom vol)
85	9	ffvelcdmi 7083	. . . . . . . . . 10 ⊢ ((𝐴 ∩ ( -𝑛[,]𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))) ∈ (0[,]+∞))
86	8, 85	sselid 3906	. . . . . . . . 9 ⊢ ((𝐴 ∩ ( -𝑛[,]𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))) ∈ ℝ^*)
87	84, 86	syl 18	. . . . . . . 8 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))) ∈ ℝ^*)
88		simprr 785	. . . . . . . 8 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))
89	80, 87, 88	xrltled 13279	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 𝐵 ≤ (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))
90		oveq2 7428	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 → ( -𝑛[,]𝑦) = ( -𝑛[,]𝑛))
91	90	ineq2d 4117	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (𝐴 ∩ ( -𝑛[,]𝑦)) = (𝐴 ∩ ( -𝑛[,]𝑛)))
92	91	fveq2d 6889	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))) = (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))
93		fvex 6898	. . . . . . . . 9 ⊢ (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))) ∈ V
94	92, 47, 93	fvmpt 6993	. . . . . . . 8 ⊢ (𝑛 ∈ ℝ → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑛) = (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))
95	31, 94	syl 18	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑛) = (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))
96	89, 95	breqtrrd 5132	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 𝐵 ≤ ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑛))
97	79, 96	jca 521	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘ -𝑛) ≤ 𝐵 ∧ 𝐵 ≤ ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑛)))
98	32, 31, 33, 39, 41, 50, 55, 97	ivthle 25777	. . . 4 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ∃𝑧 ∈ ( -𝑛[,]𝑛)((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑧) = 𝐵)
99	41	sselda 3908	. . . . . . . 8 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ 𝑧 ∈ ( -𝑛[,]𝑛)) → 𝑧 ∈ ℝ)
100		oveq2 7428	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ( -𝑛[,]𝑦) = ( -𝑛[,]𝑧))
101	100	ineq2d 4117	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝐴 ∩ ( -𝑛[,]𝑦)) = (𝐴 ∩ ( -𝑛[,]𝑧)))
102	101	fveq2d 6889	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))) = (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))))
103		fvex 6898	. . . . . . . . 9 ⊢ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) ∈ V
104	102, 47, 103	fvmpt 6993	. . . . . . . 8 ⊢ (𝑧 ∈ ℝ → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑧) = (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))))
105	99, 104	syl 18	. . . . . . 7 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ 𝑧 ∈ ( -𝑛[,]𝑛)) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑧) = (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))))
106	105	eqeq1d 2762	. . . . . 6 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ 𝑧 ∈ ( -𝑛[,]𝑛)) → (((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑧) = 𝐵 ↔ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵))
107	46	adantr 486	. . . . . . . . 9 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ (𝑧 ∈ ( -𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵)) → 𝐴 ∈ dom vol)
108	32	adantr 486	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ (𝑧 ∈ ( -𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵)) → -𝑛 ∈ ℝ)
109	99	adantrr 730	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ (𝑧 ∈ ( -𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵)) → 𝑧 ∈ ℝ)
110		iccmbl 25887	. . . . . . . . . 10 ⊢ (( -𝑛 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ( -𝑛[,]𝑧) ∈ dom vol)
111	108, 109, 110	syl2anc 596	. . . . . . . . 9 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ (𝑧 ∈ ( -𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵)) → ( -𝑛[,]𝑧) ∈ dom vol)
112		inmbl 25863	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom vol ∧ ( -𝑛[,]𝑧) ∈ dom vol) → (𝐴 ∩ ( -𝑛[,]𝑧)) ∈ dom vol)
113	107, 111, 112	syl2anc 596	. . . . . . . 8 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ (𝑧 ∈ ( -𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵)) → (𝐴 ∩ ( -𝑛[,]𝑧)) ∈ dom vol)
114		inss1 4133	. . . . . . . . 9 ⊢ (𝐴 ∩ ( -𝑛[,]𝑧)) ⊆ 𝐴
115	114	a1i 11	. . . . . . . 8 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ (𝑧 ∈ ( -𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵)) → (𝐴 ∩ ( -𝑛[,]𝑧)) ⊆ 𝐴)
116		simprr 785	. . . . . . . 8 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ (𝑧 ∈ ( -𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵)) → (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵)
117		sseq1 3933	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴 ∩ ( -𝑛[,]𝑧)) → (𝑥 ⊆ 𝐴 ↔ (𝐴 ∩ ( -𝑛[,]𝑧)) ⊆ 𝐴))
118		fveqeq2 6894	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴 ∩ ( -𝑛[,]𝑧)) → ((vol‘𝑥) = 𝐵 ↔ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵))
119	117, 118	anbi12d 644	. . . . . . . . 9 ⊢ (𝑥 = (𝐴 ∩ ( -𝑛[,]𝑧)) → ((𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵) ↔ ((𝐴 ∩ ( -𝑛[,]𝑧)) ⊆ 𝐴 ∧ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵)))
120	119	rspcev 3576	. . . . . . . 8 ⊢ (((𝐴 ∩ ( -𝑛[,]𝑧)) ∈ dom vol ∧ ((𝐴 ∩ ( -𝑛[,]𝑧)) ⊆ 𝐴 ∧ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))
121	113, 115, 116, 120	syl12anc 850	. . . . . . 7 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ (𝑧 ∈ ( -𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))
122	121	expr 462	. . . . . 6 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ 𝑧 ∈ ( -𝑛[,]𝑛)) → ((vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵 → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)))
123	106, 122	sylbid 243	. . . . 5 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ 𝑧 ∈ ( -𝑛[,]𝑛)) → (((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑧) = 𝐵 → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)))
124	123	rexlimdva 3163	. . . 4 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (∃𝑧 ∈ ( -𝑛[,]𝑛)((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑧) = 𝐵 → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)))
125	98, 124	mpd 16	. . 3 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))
126	29, 125	rexlimddv 3169	. 2 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))
127		simpll 779	. . 3 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → 𝐴 ∈ dom vol)
128		ssid 3930	. . . 4 ⊢ 𝐴 ⊆ 𝐴
129	128	a1i 11	. . 3 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → 𝐴 ⊆ 𝐴)
130		simpr 490	. . . 4 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → 𝐵 = (vol‘𝐴))
131	130	eqcomd 2766	. . 3 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → (vol‘𝐴) = 𝐵)
132		sseq1 3933	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
133		fveqeq2 6894	. . . . 5 ⊢ (𝑥 = 𝐴 → ((vol‘𝑥) = 𝐵 ↔ (vol‘𝐴) = 𝐵))
134	132, 133	anbi12d 644	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵) ↔ (𝐴 ⊆ 𝐴 ∧ (vol‘𝐴) = 𝐵)))
135	134	rspcev 3576	. . 3 ⊢ ((𝐴 ∈ dom vol ∧ (𝐴 ⊆ 𝐴 ∧ (vol‘𝐴) = 𝐵)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))
136	127, 129, 131, 135	syl12anc 850	. 2 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))
137	17	simp3d 1162	. . 3 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 𝐵 ≤ (vol‘𝐴))
138		xrleloe 13273	. . . 4 ⊢ ((𝐵 ∈ ℝ^* ∧ (vol‘𝐴) ∈ ℝ^*) → (𝐵 ≤ (vol‘𝐴) ↔ (𝐵 < (vol‘𝐴) ∨ 𝐵 = (vol‘𝐴))))
139	6, 12, 138	syl2anc 596	. . 3 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 ≤ (vol‘𝐴) ↔ (𝐵 < (vol‘𝐴) ∨ 𝐵 = (vol‘𝐴))))
140	137, 139	mpbid 235	. 2 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 < (vol‘𝐴) ∨ 𝐵 = (vol‘𝐴)))
141	126, 136, 140	mpjaodan 973	1 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∃wrex 3086 ⊆ wss 3895 ∩ cin 4089 {csn 4583 class class class wbr 5102 ↦ cmpt 5185 dom cdm 5650 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 ℂcc 11198 ℝcr 11199 0cc0 11200 +∞cpnf 11340 -∞cmnf 11341 ℝ^*cxr 11342 < clt 11343 ≤ cle 11344 -cneg 11542 ℕcn 12335 [,]cicc 13479 –cn→ccncf 25197 vol*covol 25783 volcvol 25784

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9642 ax-cc 10513 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-disj 5070 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-er 8717 df-map 8849 df-pm 8850 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9504 df-dju 9982 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-n0 12607 df-z 12694 df-uz 12966 df-q 13076 df-rp 13121 df-xneg 13241 df-xadd 13242 df-xmul 13243 df-ioo 13480 df-ico 13482 df-icc 13483 df-fz 13640 df-fzo 13789 df-fl 13932 df-seq 14145 df-exp 14205 df-hash 14475 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-clim 15655 df-rlim 15656 df-sum 15854 df-rest 17593 df-topgen 17614 df-psmet 21670 df-xmet 21671 df-met 21672 df-bl 21673 df-mopn 21674 df-top 23212 df-topon 23229 df-bases 23264 df-cmp 23705 df-cncf 25199 df-ovol 25785 df-vol 25786

This theorem is used by: itg2const2 26062

W3C validator