Theorem dmarea

Description: The domain of the area function is the set of finitely measurable subsets of RR X. RR . (Contributed by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Assertion	dmarea	⊢ ( 𝐴 ∈ dom area ↔ ( 𝐴 ⊆ ( ℝ × ℝ ) ∧ ∀ 𝑥 ∈ ℝ ( 𝐴 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝐴 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) )

Proof

Step	Hyp	Ref	Expression
1		itgex	⊢ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 ∈ V
2		df-area	⊢ area = ( 𝑠 ∈ { 𝑡 ∈ 𝒫 ( ℝ × ℝ ) ∣ ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) } ↦ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 )
3	1 2	dmmpti	⊢ dom area = { 𝑡 ∈ 𝒫 ( ℝ × ℝ ) ∣ ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) }
4	3	eleq2i	⊢ ( 𝐴 ∈ dom area ↔ 𝐴 ∈ { 𝑡 ∈ 𝒫 ( ℝ × ℝ ) ∣ ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) } )
5		imaeq1	⊢ ( 𝑡 = 𝐴 → ( 𝑡 “ { 𝑥 } ) = ( 𝐴 “ { 𝑥 } ) )
6	5	eleq1d	⊢ ( 𝑡 = 𝐴 → ( ( 𝑡 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ↔ ( 𝐴 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ) )
7	6	ralbidv	⊢ ( 𝑡 = 𝐴 → ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ↔ ∀ 𝑥 ∈ ℝ ( 𝐴 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ) )
8	5	fveq2d	⊢ ( 𝑡 = 𝐴 → ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) = ( vol ‘ ( 𝐴 “ { 𝑥 } ) ) )
9	8	mpteq2dv	⊢ ( 𝑡 = 𝐴 → ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) = ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝐴 “ { 𝑥 } ) ) ) )
10	9	eleq1d	⊢ ( 𝑡 = 𝐴 → ( ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 ↔ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝐴 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) )
11	7 10	anbi12d	⊢ ( 𝑡 = 𝐴 → ( ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) ↔ ( ∀ 𝑥 ∈ ℝ ( 𝐴 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝐴 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) ) )
12	11	elrab	⊢ ( 𝐴 ∈ { 𝑡 ∈ 𝒫 ( ℝ × ℝ ) ∣ ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) } ↔ ( 𝐴 ∈ 𝒫 ( ℝ × ℝ ) ∧ ( ∀ 𝑥 ∈ ℝ ( 𝐴 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝐴 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) ) )
13		reex	⊢ ℝ ∈ V
14	13 13	xpex	⊢ ( ℝ × ℝ ) ∈ V
15	14	elpw2	⊢ ( 𝐴 ∈ 𝒫 ( ℝ × ℝ ) ↔ 𝐴 ⊆ ( ℝ × ℝ ) )
16	15	anbi1i	⊢ ( ( 𝐴 ∈ 𝒫 ( ℝ × ℝ ) ∧ ( ∀ 𝑥 ∈ ℝ ( 𝐴 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝐴 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) ) ↔ ( 𝐴 ⊆ ( ℝ × ℝ ) ∧ ( ∀ 𝑥 ∈ ℝ ( 𝐴 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝐴 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) ) )
17		3anass	⊢ ( ( 𝐴 ⊆ ( ℝ × ℝ ) ∧ ∀ 𝑥 ∈ ℝ ( 𝐴 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝐴 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) ↔ ( 𝐴 ⊆ ( ℝ × ℝ ) ∧ ( ∀ 𝑥 ∈ ℝ ( 𝐴 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝐴 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) ) )
18	16 17	bitr4i	⊢ ( ( 𝐴 ∈ 𝒫 ( ℝ × ℝ ) ∧ ( ∀ 𝑥 ∈ ℝ ( 𝐴 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝐴 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) ) ↔ ( 𝐴 ⊆ ( ℝ × ℝ ) ∧ ∀ 𝑥 ∈ ℝ ( 𝐴 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝐴 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) )
19	4 12 18	3bitri	⊢ ( 𝐴 ∈ dom area ↔ ( 𝐴 ⊆ ( ℝ × ℝ ) ∧ ∀ 𝑥 ∈ ℝ ( 𝐴 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝐴 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) )