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 25955

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 11390	. . . . . 6 ⊢ -∞ ∈ ℝ^*
3	2	a1i 11	. . . . 5 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → -∞ ∈ ℝ^*)
4		iccssxr 13585	. . . . . . 7 ⊢ (0[,](vol‘𝐴)) ⊆ ℝ^*
5		simpr 490	. . . . . . 7 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 𝐵 ∈ (0[,](vol‘𝐴)))
6	4, 5	sselid 3911	. . . . . 6 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → 𝐵 ∈ ℝ^*)
7	6	adantr 486	. . . . 5 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐵 ∈ ℝ^*)
8		iccssxr 13585	. . . . . . . 8 ⊢ (0[,]+∞) ⊆ ℝ^*
9		volf 25877	. . . . . . . . 9 ⊢ vol:dom vol⟶(0[,]+∞)
10	9	ffvelcdmi 7104	. . . . . . . 8 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) ∈ (0[,]+∞))
11	8, 10	sselid 3911	. . . . . . 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 11380	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
15		elicc1 13544	. . . . . . . . . 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 13278	. . . . . . . 8 ⊢ -∞ < 0
21		xrltletr 13310	. . . . . . . 8 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((-∞ < 0 ∧ 0 ≤ 𝐵) → -∞ < 𝐵))
22	20, 21	mpani 709	. . . . . . 7 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (0 ≤ 𝐵 → -∞ < 𝐵))
23	2, 14, 22	mp3an12 1481	. . . . . 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 13324	. . . . 5 ⊢ (((-∞ ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (vol‘𝐴) ∈ ℝ^*) ∧ (-∞ < 𝐵 ∧ 𝐵 < (vol‘𝐴))) → 𝐵 ∈ ℝ)
27	3, 7, 13, 24, 25, 26	syl32anc 1406	. . . 4 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → 𝐵 ∈ ℝ)
28		volsup2 25953	. . . 4 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))
29	1, 27, 25, 28	syl3anc 1399	. . 3 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))
30		nnre 12366	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
31	30	ad2antrl 741	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 𝑛 ∈ ℝ)
32	31	renegcld 11767	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → -𝑛 ∈ ℝ)
33	27	adantr 486	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 𝐵 ∈ ℝ)
34		0red 11335	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 0 ∈ ℝ)
35		nngt0 12393	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → 0 < 𝑛)
36	35	ad2antrl 741	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 0 < 𝑛)
37	31	lt0neg2d 11910	. . . . . . 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 11495	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → -𝑛 < 𝑛)
40		iccssre 13584	. . . . . 6 ⊢ (( -𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ( -𝑛[,]𝑛) ⊆ ℝ)
41	32, 31, 40	syl2anc 596	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ( -𝑛[,]𝑛) ⊆ ℝ)
42		ax-resscn 11281	. . . . . . 7 ⊢ ℝ ⊆ ℂ
43		ssid 3935	. . . . . . 7 ⊢ ℂ ⊆ ℂ
44		cncfss 25247	. . . . . . 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 2763	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦)))) = (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))
48	47	volcn 25954	. . . . . . 7 ⊢ ((𝐴 ∈ dom vol ∧ -𝑛 ∈ ℝ) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦)))) ∈ (ℝ–cn→ℝ))
49	46, 32, 48	syl2anc 596	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦)))) ∈ (ℝ–cn→ℝ))
50	45, 49	sselid 3911	. . . . 5 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦)))) ∈ (ℝ–cn→ℂ))
51	41	sselda 3913	. . . . . 6 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ 𝑢 ∈ ( -𝑛[,]𝑛)) → 𝑢 ∈ ℝ)
52		cncff 25241	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦)))) ∈ (ℝ–cn→ℝ) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦)))):ℝ⟶ℝ)
53	49, 52	syl 18	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦)))):ℝ⟶ℝ)
54	53	ffvelcdmda 7105	. . . . . 6 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ 𝑢 ∈ ℝ) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑢) ∈ ℝ)
55	51, 54	syldan 603	. . . . 5 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ 𝑢 ∈ ( -𝑛[,]𝑛)) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑢) ∈ ℝ)
56		oveq2 7448	. . . . . . . . . . . 12 ⊢ (𝑦 = -𝑛 → ( -𝑛[,]𝑦) = ( -𝑛[,] -𝑛))
57	56	ineq2d 4120	. . . . . . . . . . 11 ⊢ (𝑦 = -𝑛 → (𝐴 ∩ ( -𝑛[,]𝑦)) = (𝐴 ∩ ( -𝑛[,] -𝑛)))
58	57	fveq2d 6909	. . . . . . . . . 10 ⊢ (𝑦 = -𝑛 → (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))) = (vol‘(𝐴 ∩ ( -𝑛[,] -𝑛))))
59		fvex 6918	. . . . . . . . . 10 ⊢ (vol‘(𝐴 ∩ ( -𝑛[,] -𝑛))) ∈ V
60	58, 47, 59	fvmpt 7013	. . . . . . . . 9 ⊢ ( -𝑛 ∈ ℝ → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘ -𝑛) = (vol‘(𝐴 ∩ ( -𝑛[,] -𝑛))))
61	32, 60	syl 18	. . . . . . . 8 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘ -𝑛) = (vol‘(𝐴 ∩ ( -𝑛[,] -𝑛))))
62		inss2 4137	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ ( -𝑛[,] -𝑛)) ⊆ ( -𝑛[,] -𝑛)
63	32	rexrd 11383	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → -𝑛 ∈ ℝ^*)
64		iccid 13545	. . . . . . . . . . . . 13 ⊢ ( -𝑛 ∈ ℝ^* → ( -𝑛[,] -𝑛) = { -𝑛})
65	63, 64	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ( -𝑛[,] -𝑛) = { -𝑛})
66	62, 65	sseqtrid 3955	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (𝐴 ∩ ( -𝑛[,] -𝑛)) ⊆ { -𝑛})
67	32	snssd 4747	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → { -𝑛} ⊆ ℝ)
68	66, 67	sstrd 3923	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (𝐴 ∩ ( -𝑛[,] -𝑛)) ⊆ ℝ)
69		ovolsn 25843	. . . . . . . . . . . 12 ⊢ ( -𝑛 ∈ ℝ → (vol*‘{ -𝑛}) = 0)
70	32, 69	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (vol*‘{ -𝑛}) = 0)
71		ovolssnul 25835	. . . . . . . . . . 11 ⊢ (((𝐴 ∩ ( -𝑛[,] -𝑛)) ⊆ { -𝑛} ∧ { -𝑛} ⊆ ℝ ∧ (vol‘{ -𝑛}) = 0) → (vol‘(𝐴 ∩ ( -𝑛[,] -𝑛))) = 0)
72	66, 67, 70, 71	syl3anc 1399	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (vol*‘(𝐴 ∩ ( -𝑛[,] -𝑛))) = 0)
73		nulmbl 25883	. . . . . . . . . 10 ⊢ (((𝐴 ∩ ( -𝑛[,] -𝑛)) ⊆ ℝ ∧ (vol*‘(𝐴 ∩ ( -𝑛[,] -𝑛))) = 0) → (𝐴 ∩ ( -𝑛[,] -𝑛)) ∈ dom vol)
74	68, 72, 73	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (𝐴 ∩ ( -𝑛[,] -𝑛)) ∈ dom vol)
75		mblvol 25878	. . . . . . . . 9 ⊢ ((𝐴 ∩ ( -𝑛[,] -𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ ( -𝑛[,] -𝑛))) = (vol*‘(𝐴 ∩ ( -𝑛[,] -𝑛))))
76	74, 75	syl 18	. . . . . . . 8 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → (vol‘(𝐴 ∩ ( -𝑛[,] -𝑛))) = (vol*‘(𝐴 ∩ ( -𝑛[,] -𝑛))))
77	61, 76, 72	3eqtrd 2802	. . . . . . 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 5130	. . . . . 6 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘ -𝑛) ≤ 𝐵)
80	7	adantr 486	. . . . . . . 8 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 𝐵 ∈ ℝ^*)
81		iccmbl 25914	. . . . . . . . . . 11 ⊢ (( -𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ( -𝑛[,]𝑛) ∈ dom vol)
82	32, 31, 81	syl2anc 596	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ( -𝑛[,]𝑛) ∈ dom vol)
83		inmbl 25890	. . . . . . . . . 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 7104	. . . . . . . . . 10 ⊢ ((𝐴 ∩ ( -𝑛[,]𝑛)) ∈ dom vol → (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))) ∈ (0[,]+∞))
86	8, 85	sselid 3911	. . . . . . . . 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 13303	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → 𝐵 ≤ (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))
90		oveq2 7448	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 → ( -𝑛[,]𝑦) = ( -𝑛[,]𝑛))
91	90	ineq2d 4120	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (𝐴 ∩ ( -𝑛[,]𝑦)) = (𝐴 ∩ ( -𝑛[,]𝑛)))
92	91	fveq2d 6909	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))) = (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))
93		fvex 6918	. . . . . . . . 9 ⊢ (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))) ∈ V
94	92, 47, 93	fvmpt 7013	. . . . . . . 8 ⊢ (𝑛 ∈ ℝ → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑛) = (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))
95	31, 94	syl 18	. . . . . . 7 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑛) = (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))
96	89, 95	breqtrrd 5136	. . . . . 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 25804	. . . 4 ⊢ ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) → ∃𝑧 ∈ ( -𝑛[,]𝑛)((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑧) = 𝐵)
99	41	sselda 3913	. . . . . . . 8 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ 𝑧 ∈ ( -𝑛[,]𝑛)) → 𝑧 ∈ ℝ)
100		oveq2 7448	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ( -𝑛[,]𝑦) = ( -𝑛[,]𝑧))
101	100	ineq2d 4120	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝐴 ∩ ( -𝑛[,]𝑦)) = (𝐴 ∩ ( -𝑛[,]𝑧)))
102	101	fveq2d 6909	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))) = (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))))
103		fvex 6918	. . . . . . . . 9 ⊢ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) ∈ V
104	102, 47, 103	fvmpt 7013	. . . . . . . 8 ⊢ (𝑧 ∈ ℝ → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑧) = (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))))
105	99, 104	syl 18	. . . . . . 7 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ 𝑧 ∈ ( -𝑛[,]𝑛)) → ((𝑦 ∈ ℝ ↦ (vol‘(𝐴 ∩ ( -𝑛[,]𝑦))))‘𝑧) = (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))))
106	105	eqeq1d 2765	. . . . . 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 25914	. . . . . . . . . 10 ⊢ (( -𝑛 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ( -𝑛[,]𝑧) ∈ dom vol)
111	108, 109, 110	syl2anc 596	. . . . . . . . 9 ⊢ (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) ∧ (𝑛 ∈ ℕ ∧ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))) ∧ (𝑧 ∈ ( -𝑛[,]𝑛) ∧ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵)) → ( -𝑛[,]𝑧) ∈ dom vol)
112		inmbl 25890	. . . . . . . . 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 4136	. . . . . . . . 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 3938	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴 ∩ ( -𝑛[,]𝑧)) → (𝑥 ⊆ 𝐴 ↔ (𝐴 ∩ ( -𝑛[,]𝑧)) ⊆ 𝐴))
118		fveqeq2 6914	. . . . . . . . . 10 ⊢ (𝑥 = (𝐴 ∩ ( -𝑛[,]𝑧)) → ((vol‘𝑥) = 𝐵 ↔ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵))
119	117, 118	anbi12d 644	. . . . . . . . 9 ⊢ (𝑥 = (𝐴 ∩ ( -𝑛[,]𝑧)) → ((𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵) ↔ ((𝐴 ∩ ( -𝑛[,]𝑧)) ⊆ 𝐴 ∧ (vol‘(𝐴 ∩ ( -𝑛[,]𝑧))) = 𝐵)))
120	119	rspcev 3580	. . . . . . . 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 3167	. . . 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 3173	. 2 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 < (vol‘𝐴)) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))
127		simpll 779	. . 3 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → 𝐴 ∈ dom vol)
128		ssid 3935	. . . 4 ⊢ 𝐴 ⊆ 𝐴
129	128	a1i 11	. . 3 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → 𝐴 ⊆ 𝐴)
130		simpr 490	. . . 4 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → 𝐵 = (vol‘𝐴))
131	130	eqcomd 2769	. . 3 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) ∧ 𝐵 = (vol‘𝐴)) → (vol‘𝐴) = 𝐵)
132		sseq1 3938	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
133		fveqeq2 6914	. . . . 5 ⊢ (𝑥 = 𝐴 → ((vol‘𝑥) = 𝐵 ↔ (vol‘𝐴) = 𝐵))
134	132, 133	anbi12d 644	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵) ↔ (𝐴 ⊆ 𝐴 ∧ (vol‘𝐴) = 𝐵)))
135	134	rspcev 3580	. . 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 13297	. . . 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 1570 ∈ wcel 2147 ∃wrex 3090 ⊆ wss 3900 ∩ cin 4092 {csn 4588 class class class wbr 5106 ↦ cmpt 5189 dom cdm 5655 ⟶wf 6551 ‘cfv 6555 (class class class)co 7440 ℂcc 11222 ℝcr 11223 0cc0 11224 +∞cpnf 11364 -∞cmnf 11365 ℝ^*cxr 11366 < clt 11367 ≤ cle 11368 -cneg 11566 ℕcn 12359 [,]cicc 13503 –cn→ccncf 25224 vol*covol 25810 volcvol 25811

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-inf2 9666 ax-cc 10537 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301 ax-pre-sup 11302

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-disj 5074 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-isom 6564 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-of 7714 df-om 7899 df-1st 8022 df-2nd 8023 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-1o 8501 df-2o 8502 df-er 8742 df-map 8874 df-pm 8875 df-en 8999 df-dom 9000 df-sdom 9001 df-fin 9002 df-fi 9427 df-sup 9458 df-inf 9459 df-oi 9528 df-dju 10006 df-card 10044 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-div 11998 df-nn 12360 df-2 12429 df-3 12430 df-n0 12631 df-z 12718 df-uz 12990 df-q 13100 df-rp 13145 df-xneg 13265 df-xadd 13266 df-xmul 13267 df-ioo 13504 df-ico 13506 df-icc 13507 df-fz 13664 df-fzo 13813 df-fl 13956 df-seq 14169 df-exp 14229 df-hash 14499 df-cj 15292 df-re 15293 df-im 15294 df-sqrt 15428 df-abs 15429 df-clim 15681 df-rlim 15682 df-sum 15880 df-rest 17619 df-topgen 17640 df-psmet 21697 df-xmet 21698 df-met 21699 df-bl 21700 df-mopn 21701 df-top 23239 df-topon 23256 df-bases 23291 df-cmp 23732 df-cncf 25226 df-ovol 25812 df-vol 25813

This theorem is used by: itg2const2 26089

W3C validator