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 25596

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 773	. . . 4 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐴 ∈ dom vol)
2		mnfxr 11197	. . . . . 6 ⊢ -∞ ∈ ℝ^*
3	2	a1i 11	. . . . 5 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → -∞ ∈ ℝ^*)
4		iccssxr 13378	. . . . . . 7 ⊢ (0[,](vol‘𝐴)) ⊆ ℝ^*
5		simpr 486	. . . . . . 7 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 𝐵 ∈ (0[,](vol‘𝐴)))
6	4, 5	sselid 3915	. . . . . 6 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 𝐵 ∈ ℝ^*)
7	6	adantr 482	. . . . 5 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐵 ∈ ℝ^*)
8		iccssxr 13378	. . . . . . . 8 ⊢ (0[,]+∞) ⊆ ℝ^*
9		volf 25518	. . . . . . . . 9 ⊢ vol:dom vol⟶(0[,]+∞)
10	9	ffvelcdmi 7028	. . . . . . . 8 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) ∈ (0[,]+∞))
11	8, 10	sselid 3915	. . . . . . 7 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) ∈ ℝ^*)
12	11	adantr 482	. . . . . 6 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (vol‘𝐴) ∈ ℝ^*)
13	12	adantr 482	. . . . 5 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → (vol‘𝐴) ∈ ℝ^*)
14		0xr 11187	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
15		elicc1 13337	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ (vol‘𝐴) ∈ ℝ^) → (𝐵 ∈ (0[,](vol‘𝐴)) ↔ (𝐵 ∈ ℝ^ ∧ 0 ≤ 𝐵 ∧ 𝐵 ≤ (vol‘𝐴))))
16	14, 12, 15	sylancr 594	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 ∈ (0[,](vol‘𝐴)) ↔ (𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ∧ 𝐵 ≤ (vol‘𝐴))))
17	5, 16	mpbid 234	. . . . . . . 8 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ∧ 𝐵 ≤ (vol‘𝐴)))
18	17	simp2d 1150	. . . . . . 7 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 0 ≤ 𝐵)
19	18	adantr 482	. . . . . 6 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 0 ≤ 𝐵)
20		mnflt0 13071	. . . . . . . 8 ⊢ -∞ < 0
21		xrltletr 13103	. . . . . . . 8 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((-∞ < 0 ∧ 0 ≤ 𝐵) → -∞ < 𝐵))
22	20, 21	mpani 703	. . . . . . 7 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (0 ≤ 𝐵 → -∞ < 𝐵))
23	2, 14, 22	mp3an12 1460	. . . . . 6 ⊢ (𝐵 ∈ ℝ^* → (0 ≤ 𝐵 → -∞ < 𝐵))
24	7, 19, 23	sylc 65	. . . . 5 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → -∞ < 𝐵)
25		simpr 486	. . . . 5 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐵 < (vol‘𝐴))
26		xrre2 13117	. . . . 5 ⊢ (((-∞ ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (vol‘𝐴) ∈ ℝ^*) ∧ (-∞ < 𝐵 ∧ 𝐵 < (vol‘𝐴))) → 𝐵 ∈ ℝ)
27	3, 7, 13, 24, 25, 26	syl32anc 1387	. . . 4 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐵 ∈ ℝ)
28		volsup2 25594	. . . 4 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))
29	1, 27, 25, 28	syl3anc 1380	. . 3 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))
30		nnre 12176	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
31	30	ad2antrl 735	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝑛 ∈ ℝ)
32	31	renegcld 11572	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → -𝑛 ∈ ℝ)
33	27	adantr 482	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐵 ∈ ℝ)
34		0red 11142	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 0 ∈ ℝ)
35		nngt0 12203	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → 0 < 𝑛)
36	35	ad2antrl 735	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 0 < 𝑛)
37	31	lt0neg2d 11715	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (0 < 𝑛 ↔ -𝑛 < 0))
38	36, 37	mpbid 234	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → -𝑛 < 0)
39	32, 34, 31, 38, 36	lttrd 11302	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → -𝑛 < 𝑛)
40		iccssre 13377	. . . . . 6 ⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ⊆ ℝ)
41	32, 31, 40	syl2anc 591	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (-𝑛[,]𝑛) ⊆ ℝ)
42		ax-resscn 11090	. . . . . . 7 ⊢ ℝ ⊆ ℂ
43		ssid 3939	. . . . . . 7 ⊢ ℂ ⊆ ℂ
44		cncfss 24888	. . . . . . 7 ⊢ ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
45	42, 43, 44	mp2an 699	. . . . . 6 ⊢ (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ)
46	1	adantr 482	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐴 ∈ dom vol)
47		eqid 2741	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) = (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))
48	47	volcn 25595	. . . . . . 7 ⊢ ((𝐴 ∈ dom vol ∧ -𝑛 ∈ ℝ) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) ∈ (ℝ–cn→ℝ))
49	46, 32, 48	syl2anc 591	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) ∈ (ℝ–cn→ℝ))
50	45, 49	sselid 3915	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) ∈ (ℝ–cn→ℂ))
51	41	sselda 3917	. . . . . 6 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑢 ∈ (-𝑛[,]𝑛)) → 𝑢 ∈ ℝ)
52		cncff 24882	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))) ∈ (ℝ–cn→ℝ) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))):ℝ⟶ℝ)
53	49, 52	syl 17	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦)))):ℝ⟶ℝ)
54	53	ffvelcdmda 7029	. . . . . 6 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑢 ∈ ℝ) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑢) ∈ ℝ)
55	51, 54	syldan 598	. . . . 5 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑢 ∈ (-𝑛[,]𝑛)) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑢) ∈ ℝ)
56		oveq2 7368	. . . . . . . . . . . 12 ⊢ (𝑦 = -𝑛 → (-𝑛[,]𝑦) = (-𝑛[,]-𝑛))
57	56	ineq2d 4152	. . . . . . . . . . 11 ⊢ (𝑦 = -𝑛 → (𝐴 ∩ (-𝑛[,]𝑦)) = (𝐴 ∩ (-𝑛[,]-𝑛)))
58	57	fveq2d 6835	. . . . . . . . . 10 ⊢ (𝑦 = -𝑛 → (vol‘(𝐴 ∩ (-𝑛[,]𝑦))) = (vol‘(𝐴 ∩ (-𝑛[,]-𝑛))))
59		fvex 6844	. . . . . . . . . 10 ⊢ (vol‘(𝐴 ∩ (-𝑛[,]-𝑛))) ∈ V
60	58, 47, 59	fvmpt 6939	. . . . . . . . 9 ⊢ (-𝑛 ∈ ℝ → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘-𝑛) = (vol‘(𝐴 ∩ (-𝑛[,]-𝑛))))
61	32, 60	syl 17	. . . . . . . 8 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘-𝑛) = (vol‘(𝐴 ∩ (-𝑛[,]-𝑛))))
62		inss2 4169	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ (-𝑛[,]-𝑛)) ⊆ (-𝑛[,]-𝑛)
63	32	rexrd 11190	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → -𝑛 ∈ ℝ^*)
64		iccid 13338	. . . . . . . . . . . . 13 ⊢ (-𝑛 ∈ ℝ^* → (-𝑛[,]-𝑛) = {-𝑛})
65	63, 64	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (-𝑛[,]-𝑛) = {-𝑛})
66	62, 65	sseqtrid 3959	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝐴 ∩ (-𝑛[,]-𝑛)) ⊆ {-𝑛})
67	32	snssd 4721	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → {-𝑛} ⊆ ℝ)
68	66, 67	sstrd 3927	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝐴 ∩ (-𝑛[,]-𝑛)) ⊆ ℝ)
69		ovolsn 25484	. . . . . . . . . . . 12 ⊢ (-𝑛 ∈ ℝ → (vol*‘{-𝑛}) = 0)
70	32, 69	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (vol*‘{-𝑛}) = 0)
71		ovolssnul 25476	. . . . . . . . . . 11 ⊢ (((𝐴 ∩ (-𝑛[,]-𝑛)) ⊆ {-𝑛} ∧ {-𝑛} ⊆ ℝ ∧ (vol‘{-𝑛}) = 0) → (vol‘(𝐴 ∩ (-𝑛[,]-𝑛))) = 0)
72	66, 67, 70, 71	syl3anc 1380	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (vol*‘(𝐴 ∩ (-𝑛[,]-𝑛))) = 0)
73		nulmbl 25524	. . . . . . . . . 10 ⊢ (((𝐴 ∩ (-𝑛[,]-𝑛)) ⊆ ℝ ∧ (vol*‘(𝐴 ∩ (-𝑛[,]-𝑛))) = 0) → (𝐴 ∩ (-𝑛[,]-𝑛)) ∈ dom vol)
74	68, 72, 73	syl2anc 591	. . . . . . . . 9 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝐴 ∩ (-𝑛[,]-𝑛)) ∈ dom vol)
75		mblvol 25519	. . . . . . . . 9 ⊢ ((𝐴 ∩ (-𝑛[,]-𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ (-𝑛[,]-𝑛))) = (vol*‘(𝐴 ∩ (-𝑛[,]-𝑛))))
76	74, 75	syl 17	. . . . . . . 8 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (vol‘(𝐴 ∩ (-𝑛[,]-𝑛))) = (vol*‘(𝐴 ∩ (-𝑛[,]-𝑛))))
77	61, 76, 72	3eqtrd 2780	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘-𝑛) = 0)
78	19	adantr 482	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 0 ≤ 𝐵)
79	77, 78	eqbrtrd 5097	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘-𝑛) ≤ 𝐵)
80	7	adantr 482	. . . . . . . 8 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐵 ∈ ℝ^*)
81		iccmbl 25555	. . . . . . . . . . 11 ⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ∈ dom vol)
82	32, 31, 81	syl2anc 591	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (-𝑛[,]𝑛) ∈ dom vol)
83		inmbl 25531	. . . . . . . . . 10 ⊢ ((𝐴 ∈ dom vol ∧ (-𝑛[,]𝑛) ∈ dom vol) → (𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol)
84	46, 82, 83	syl2anc 591	. . . . . . . . 9 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol)
85	9	ffvelcdmi 7028	. . . . . . . . . 10 ⊢ ((𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈ (0[,]+∞))
86	8, 85	sselid 3915	. . . . . . . . 9 ⊢ ((𝐴 ∩ (-𝑛[,]𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈ ℝ^*)
87	84, 86	syl 17	. . . . . . . 8 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈ ℝ^*)
88		simprr 779	. . . . . . . 8 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))
89	80, 87, 88	xrltled 13096	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐵 ≤ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))
90		oveq2 7368	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 → (-𝑛[,]𝑦) = (-𝑛[,]𝑛))
91	90	ineq2d 4152	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (𝐴 ∩ (-𝑛[,]𝑦)) = (𝐴 ∩ (-𝑛[,]𝑛)))
92	91	fveq2d 6835	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (vol‘(𝐴 ∩ (-𝑛[,]𝑦))) = (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))
93		fvex 6844	. . . . . . . . 9 ⊢ (vol‘(𝐴 ∩ (-𝑛[,]𝑛))) ∈ V
94	92, 47, 93	fvmpt 6939	. . . . . . . 8 ⊢ (𝑛 ∈ ℝ → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑛) = (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))
95	31, 94	syl 17	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑛) = (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))
96	89, 95	breqtrrd 5103	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → 𝐵 ≤ ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑛))
97	79, 96	jca 517	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘-𝑛) ≤ 𝐵 ∧ 𝐵 ≤ ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑛)))
98	32, 31, 33, 39, 41, 50, 55, 97	ivthle 25445	. . . 4 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ∃𝑧 ∈ (-𝑛[,]𝑛)((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = 𝐵)
99	41	sselda 3917	. . . . . . . 8 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑧 ∈ (-𝑛[,]𝑛)) → 𝑧 ∈ ℝ)
100		oveq2 7368	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (-𝑛[,]𝑦) = (-𝑛[,]𝑧))
101	100	ineq2d 4152	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝐴 ∩ (-𝑛[,]𝑦)) = (𝐴 ∩ (-𝑛[,]𝑧)))
102	101	fveq2d 6835	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (vol‘(𝐴 ∩ (-𝑛[,]𝑦))) = (vol‘(𝐴 ∩ (-𝑛[,]𝑧))))
103		fvex 6844	. . . . . . . . 9 ⊢ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) ∈ V
104	102, 47, 103	fvmpt 6939	. . . . . . . 8 ⊢ (𝑧 ∈ ℝ → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = (vol‘(𝐴 ∩ (-𝑛[,]𝑧))))
105	99, 104	syl 17	. . . . . . 7 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑧 ∈ (-𝑛[,]𝑛)) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = (vol‘(𝐴 ∩ (-𝑛[,]𝑧))))
106	105	eqeq1d 2743	. . . . . 6 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑧 ∈ (-𝑛[,]𝑛)) → (((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = 𝐵 ↔ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵))
107	46	adantr 482	. . . . . . . . 9 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → 𝐴 ∈ dom vol)
108	32	adantr 482	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → -𝑛 ∈ ℝ)
109	99	adantrr 724	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → 𝑧 ∈ ℝ)
110		iccmbl 25555	. . . . . . . . . 10 ⊢ ((-𝑛 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (-𝑛[,]𝑧) ∈ dom vol)
111	108, 109, 110	syl2anc 591	. . . . . . . . 9 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → (-𝑛[,]𝑧) ∈ dom vol)
112		inmbl 25531	. . . . . . . . 9 ⊢ ((𝐴 ∈ dom vol ∧ (-𝑛[,]𝑧) ∈ dom vol) → (𝐴 ∩ (-𝑛[,]𝑧)) ∈ dom vol)
113	107, 111, 112	syl2anc 591	. . . . . . . 8 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → (𝐴 ∩ (-𝑛[,]𝑧)) ∈ dom vol)
114		inss1 4168	. . . . . . . . 9 ⊢ (𝐴 ∩ (-𝑛[,]𝑧)) ⊆ 𝐴
115	114	a1i 11	. . . . . . . 8 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → (𝐴 ∩ (-𝑛[,]𝑧)) ⊆ 𝐴)
116		simprr 779	. . . . . . . 8 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)
117		sseq1 3942	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴 ∩ (-𝑛[,]𝑧)) → (𝑥 ⊆ 𝐴 ↔ (𝐴 ∩ (-𝑛[,]𝑧)) ⊆ 𝐴))
118		fveqeq2 6840	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴 ∩ (-𝑛[,]𝑧)) → ((vol‘𝑥) = 𝐵 ↔ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵))
119	117, 118	anbi12d 639	. . . . . . . . 9 ⊢ (𝑥 = (𝐴 ∩ (-𝑛[,]𝑧)) → ((𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵) ↔ ((𝐴 ∩ (-𝑛[,]𝑧)) ⊆ 𝐴 ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)))
120	119	rspcev 3562	. . . . . . . 8 ⊢ (((𝐴 ∩ (-𝑛[,]𝑧)) ∈ dom vol ∧ ((𝐴 ∩ (-𝑛[,]𝑧)) ⊆ 𝐴 ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))
121	113, 115, 116, 120	syl12anc 843	. . . . . . 7 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ (𝑧 ∈ (-𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))
122	121	expr 458	. . . . . 6 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑧 ∈ (-𝑛[,]𝑛)) → ((vol‘(𝐴 ∩ (-𝑛[,]𝑧))) = 𝐵 → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)))
123	106, 122	sylbid 242	. . . . 5 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) ∧ 𝑧 ∈ (-𝑛[,]𝑛)) → (((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = 𝐵 → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)))
124	123	rexlimdva 3142	. . . 4 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → (∃𝑧 ∈ (-𝑛[,]𝑛)((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ (-𝑛[,]𝑦))))‘𝑧) = 𝐵 → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵)))
125	98, 124	mpd 15	. . 3 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ (-𝑛[,]𝑛))))) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))
126	29, 125	rexlimddv 3148	. 2 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))
127		simpll 773	. . 3 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → 𝐴 ∈ dom vol)
128		ssid 3939	. . . 4 ⊢ 𝐴 ⊆ 𝐴
129	128	a1i 11	. . 3 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → 𝐴 ⊆ 𝐴)
130		simpr 486	. . . 4 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → 𝐵 = (vol‘𝐴))
131	130	eqcomd 2747	. . 3 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → (vol‘𝐴) = 𝐵)
132		sseq1 3942	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
133		fveqeq2 6840	. . . . 5 ⊢ (𝑥 = 𝐴 → ((vol‘𝑥) = 𝐵 ↔ (vol‘𝐴) = 𝐵))
134	132, 133	anbi12d 639	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵) ↔ (𝐴 ⊆ 𝐴 ∧ (vol‘𝐴) = 𝐵)))
135	134	rspcev 3562	. . 3 ⊢ ((𝐴 ∈ dom vol ∧ (𝐴 ⊆ 𝐴 ∧ (vol‘𝐴) = 𝐵)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))
136	127, 129, 131, 135	syl12anc 843	. 2 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))
137	17	simp3d 1151	. . 3 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 𝐵 ≤ (vol‘𝐴))
138		xrleloe 13090	. . . 4 ⊢ ((𝐵 ∈ ℝ^* ∧ (vol‘𝐴) ∈ ℝ^*) → (𝐵 ≤ (vol‘𝐴) ↔ (𝐵 < (vol‘𝐴) ∨ 𝐵 = (vol‘𝐴))))
139	6, 12, 138	syl2anc 591	. . 3 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 ≤ (vol‘𝐴) ↔ (𝐵 < (vol‘𝐴) ∨ 𝐵 = (vol‘𝐴))))
140	137, 139	mpbid 234	. 2 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → (𝐵 < (vol‘𝐴) ∨ 𝐵 = (vol‘𝐴)))
141	126, 136, 140	mpjaodan 967	1 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 397 ∨ wo 854 ∧ w3a 1093 = wceq 1548 ∈ wcel 2121 ∃wrex 3065 ∩ cin 3884 ⊆ wss 3885 {csn 4558 class class class wbr 5075 ↦ cmpt 5156 dom cdm 5621 ⟶wf 6485 ‘cfv 6489 (class class class)co 7360 ℂcc 11031 ℝcr 11032 0cc0 11033 +∞cpnf 11171 -∞cmnf 11172 ℝ^*cxr 11173 < clt 11174 ≤ cle 11175 -cneg 11373 ℕcn 12169 [,]cicc 13296 –cn→ccncf 24865 vol*covol 25451 volcvol 25452

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-rep 5202 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7682 ax-inf2 9557 ax-cc 10352 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-pre-sup 11111

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-rmo 3346 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4842 df-int 4881 df-iun 4926 df-disj 5043 df-br 5076 df-opab 5138 df-mpt 5157 df-tr 5183 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-se 5575 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-isom 6498 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-of 7624 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-2o 8400 df-er 8637 df-map 8769 df-pm 8770 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-fi 9318 df-sup 9349 df-inf 9350 df-oi 9419 df-dju 9820 df-card 9858 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-div 11803 df-nn 12170 df-2 12239 df-3 12240 df-n0 12433 df-z 12520 df-uz 12784 df-q 12894 df-rp 12938 df-xneg 13058 df-xadd 13059 df-xmul 13060 df-ioo 13297 df-ico 13299 df-icc 13300 df-fz 13457 df-fzo 13604 df-fl 13746 df-seq 13959 df-exp 14019 df-hash 14288 df-cj 15056 df-re 15057 df-im 15058 df-sqrt 15192 df-abs 15193 df-clim 15445 df-rlim 15446 df-sum 15644 df-rest 17380 df-topgen 17401 df-psmet 21343 df-xmet 21344 df-met 21345 df-bl 21346 df-mopn 21347 df-top 22881 df-topon 22898 df-bases 22933 df-cmp 23374 df-cncf 24867 df-ovol 25453 df-vol 25454

This theorem is referenced by: itg2const2 25730

W3C validator