Metamath Proof Explorer

Theorem cnicciblnc

Description: Choice-free proof of cniccibl . (Contributed by Brendan Leahy, 2-Nov-2017)

Ref Expression
Assertion cnicciblnc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ F : A B ⟶cn ℂ → F ∈ 𝐿 1

Proof

Step Hyp Ref Expression
1 iccmbl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ∈ dom ⁡ vol
2 cnmbf ⊢ A B ∈ dom ⁡ vol ∧ F : A B ⟶cn ℂ → F ∈ MblFn
3 1 2 stoic3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ F : A B ⟶cn ℂ → F ∈ MblFn
4 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ F : A B ⟶cn ℂ → F : A B ⟶cn ℂ
5 cncff ⊢ F : A B ⟶cn ℂ → F : A B ⟶ ℂ
6 fdm ⊢ F : A B ⟶ ℂ → dom ⁡ F = A B
7 4 5 6 3syl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ F : A B ⟶cn ℂ → dom ⁡ F = A B
8 7 fveq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ F : A B ⟶cn ℂ → vol ⁡ dom ⁡ F = vol ⁡ A B
9 iccvolcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → vol ⁡ A B ∈ ℝ
10 9 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ F : A B ⟶cn ℂ → vol ⁡ A B ∈ ℝ
11 8 10 eqeltrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ F : A B ⟶cn ℂ → vol ⁡ dom ⁡ F ∈ ℝ
12 cniccbdd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ F : A B ⟶cn ℂ → ∃ x ∈ ℝ ∀ y ∈ A B F ⁡ y ≤ x
13 7 raleqdv ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ F : A B ⟶cn ℂ → ∀ y ∈ dom ⁡ F F ⁡ y ≤ x ↔ ∀ y ∈ A B F ⁡ y ≤ x
14 13 rexbidv ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ F : A B ⟶cn ℂ → ∃ x ∈ ℝ ∀ y ∈ dom ⁡ F F ⁡ y ≤ x ↔ ∃ x ∈ ℝ ∀ y ∈ A B F ⁡ y ≤ x
15 12 14 mpbird ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ F : A B ⟶cn ℂ → ∃ x ∈ ℝ ∀ y ∈ dom ⁡ F F ⁡ y ≤ x
16 bddiblnc ⊢ F ∈ MblFn ∧ vol ⁡ dom ⁡ F ∈ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ dom ⁡ F F ⁡ y ≤ x → F ∈ 𝐿 1
17 3 11 15 16 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ F : A B ⟶cn ℂ → F ∈ 𝐿 1