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	$⊢ (A \in dom vol \land B \in [0, vol (A)]) \to \exists x \in dom vol (x \subseteq A \land vol (x) = B)$

Proof

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

Metamath Proof Explorer

Theorem volivth

Proof