Metamath Proof Explorer

Definition 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 ∈ t ∈ 𝒫 ℝ 2 | ∀ x ∈ ℝ t x ∈ vol -1 ℝ ∧ x ∈ ℝ ⟼ vol ⁡ t x ∈ 𝐿 1 ⟼ ∫ ℝ vol ⁡ s x dx

Detailed syntax breakdown

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 ∈ vol -1 ℝ
15 14 6 3 wral wff ∀ x ∈ ℝ t x ∈ vol -1 ℝ
16 10 11 cfv class vol ⁡ t x
17 6 3 16 cmpt class x ∈ ℝ ⟼ vol ⁡ t x
18 cibl class 𝐿 1
19 17 18 wcel wff x ∈ ℝ ⟼ vol ⁡ t x ∈ 𝐿 1
20 15 19 wa wff ∀ x ∈ ℝ t x ∈ vol -1 ℝ ∧ x ∈ ℝ ⟼ vol ⁡ t x ∈ 𝐿 1
21 20 2 5 crab class t ∈ 𝒫 ℝ 2 | ∀ x ∈ ℝ t x ∈ vol -1 ℝ ∧ x ∈ ℝ ⟼ vol ⁡ t x ∈ 𝐿 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 ∫ ℝ vol ⁡ s x dx
26 1 21 25 cmpt class s ∈ t ∈ 𝒫 ℝ 2 | ∀ x ∈ ℝ t x ∈ vol -1 ℝ ∧ x ∈ ℝ ⟼ vol ⁡ t x ∈ 𝐿 1 ⟼ ∫ ℝ vol ⁡ s x dx
27 0 26 wceq wff area = s ∈ t ∈ 𝒫 ℝ 2 | ∀ x ∈ ℝ t x ∈ vol -1 ℝ ∧ x ∈ ℝ ⟼ vol ⁡ t x ∈ 𝐿 1 ⟼ ∫ ℝ vol ⁡ s x dx