df-area

Description: Define the area of a subset of RR X. RR . (Contributed by Mario Carneiro, 21-Jun-2015)

		Ref	Expression
	Assertion	df-area	$⊢ area = (s \in \{t \in 𝒫 ℝ^{2} \| (\forall x \in ℝ t [\{x\}] \in {vol}^{-1} [ℝ] \land (x \in ℝ ⟼ vol (t [\{x\}])) \in 𝐿^{1})\} ⟼ \int_{ℝ} vol (s [\{x\}]) d x)$

Step	Hyp	Ref	Expression
0		carea	$class area$
1		vs	$setvar s$
2		vt	$setvar t$
3		cr	$class ℝ$
4	3 3	cxp	$class ℝ^{2}$
5	4	cpw	$class 𝒫 ℝ^{2}$
6		vx	$setvar x$
7	2	cv	$setvar t$
8	6	cv	$setvar x$
9	8	csn	$class \{x\}$
10	7 9	cima	$class t [\{x\}]$
11		cvol	$class vol$
12	11	ccnv	$class {vol}^{-1}$
13	12 3	cima	$class {vol}^{-1} [ℝ]$
14	10 13	wcel	$wff t [\{x\}] \in {vol}^{-1} [ℝ]$
15	14 6 3	wral	$wff \forall x \in ℝ t [\{x\}] \in {vol}^{-1} [ℝ]$
16	10 11	cfv	$class vol (t [\{x\}])$
17	6 3 16	cmpt	$class (x \in ℝ ⟼ vol (t [\{x\}]))$
18		cibl	$class 𝐿^{1}$
19	17 18	wcel	$wff (x \in ℝ ⟼ vol (t [\{x\}])) \in 𝐿^{1}$
20	15 19	wa	$wff (\forall x \in ℝ t [\{x\}] \in {vol}^{-1} [ℝ] \land (x \in ℝ ⟼ vol (t [\{x\}])) \in 𝐿^{1})$
21	20 2 5	crab	$class \{t \in 𝒫 ℝ^{2} \| (\forall x \in ℝ t [\{x\}] \in {vol}^{-1} [ℝ] \land (x \in ℝ ⟼ vol (t [\{x\}])) \in 𝐿^{1})\}$
22	1	cv	$setvar s$
23	22 9	cima	$class s [\{x\}]$
24	23 11	cfv	$class vol (s [\{x\}])$
25	6 3 24	citg	$class \int_{ℝ} vol (s [\{x\}]) d x$
26	1 21 25	cmpt	$class (s \in \{t \in 𝒫 ℝ^{2} \| (\forall x \in ℝ t [\{x\}] \in {vol}^{-1} [ℝ] \land (x \in ℝ ⟼ vol (t [\{x\}])) \in 𝐿^{1})\} ⟼ \int_{ℝ} vol (s [\{x\}]) d x)$
27	0 26	wceq	$wff area = (s \in \{t \in 𝒫 ℝ^{2} \| (\forall x \in ℝ t [\{x\}] \in {vol}^{-1} [ℝ] \land (x \in ℝ ⟼ vol (t [\{x\}])) \in 𝐿^{1})\} ⟼ \int_{ℝ} vol (s [\{x\}]) d x)$

Metamath Proof Explorer