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 = ( 𝑠 ∈ { 𝑡 ∈ 𝒫 ( ℝ × ℝ ) ∣ ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) } ↦ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 carea area
1 vs 𝑠
2 vt 𝑡
3 cr
4 3 3 cxp ( ℝ × ℝ )
5 4 cpw 𝒫 ( ℝ × ℝ )
6 vx 𝑥
7 2 cv 𝑡
8 6 cv 𝑥
9 8 csn { 𝑥 }
10 7 9 cima ( 𝑡 “ { 𝑥 } )
11 cvol vol
12 11 ccnv vol
13 12 3 cima ( vol “ ℝ )
14 10 13 wcel ( 𝑡 “ { 𝑥 } ) ∈ ( vol “ ℝ )
15 14 6 3 wral 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( vol “ ℝ )
16 10 11 cfv ( vol ‘ ( 𝑡 “ { 𝑥 } ) )
17 6 3 16 cmpt ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) )
18 cibl 𝐿1
19 17 18 wcel ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1
20 15 19 wa ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 )
21 20 2 5 crab { 𝑡 ∈ 𝒫 ( ℝ × ℝ ) ∣ ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) }
22 1 cv 𝑠
23 22 9 cima ( 𝑠 “ { 𝑥 } )
24 23 11 cfv ( vol ‘ ( 𝑠 “ { 𝑥 } ) )
25 6 3 24 citg ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥
26 1 21 25 cmpt ( 𝑠 ∈ { 𝑡 ∈ 𝒫 ( ℝ × ℝ ) ∣ ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) } ↦ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 )
27 0 26 wceq area = ( 𝑠 ∈ { 𝑡 ∈ 𝒫 ( ℝ × ℝ ) ∣ ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) } ↦ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 )