Metamath Proof Explorer

Theorem i1f1lem

Description: Lemma for i1f1 and itg11 . (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypothesis i1f1.1 ⊢ F = x ∈ ℝ ⟼ if x ∈ A 1 0
Assertion i1f1lem ⊢ F : ℝ ⟶ 0 1 ∧ A ∈ dom ⁡ vol → F -1 1 = A

Proof

Step Hyp Ref Expression
1 i1f1.1 ⊢ F = x ∈ ℝ ⟼ if x ∈ A 1 0
2 1ex ⊢ 1 ∈ V
3 2 prid2 ⊢ 1 ∈ 0 1
4 c0ex ⊢ 0 ∈ V
5 4 prid1 ⊢ 0 ∈ 0 1
6 3 5 ifcli ⊢ if x ∈ A 1 0 ∈ 0 1
7 6 rgenw ⊢ ∀ x ∈ ℝ if x ∈ A 1 0 ∈ 0 1
8 1 fmpt ⊢ ∀ x ∈ ℝ if x ∈ A 1 0 ∈ 0 1 ↔ F : ℝ ⟶ 0 1
9 7 8 mpbi ⊢ F : ℝ ⟶ 0 1
10 6 a1i ⊢ A ∈ dom ⁡ vol ∧ x ∈ ℝ → if x ∈ A 1 0 ∈ 0 1
11 10 1 fmptd ⊢ A ∈ dom ⁡ vol → F : ℝ ⟶ 0 1
12 ffn ⊢ F : ℝ ⟶ 0 1 → F Fn ℝ
13 elpreima ⊢ F Fn ℝ → y ∈ F -1 1 ↔ y ∈ ℝ ∧ F ⁡ y ∈ 1
14 11 12 13 3syl ⊢ A ∈ dom ⁡ vol → y ∈ F -1 1 ↔ y ∈ ℝ ∧ F ⁡ y ∈ 1
15 fvex ⊢ F ⁡ y ∈ V
16 15 elsn ⊢ F ⁡ y ∈ 1 ↔ F ⁡ y = 1
17 eleq1w ⊢ x = y → x ∈ A ↔ y ∈ A
18 17 ifbid ⊢ x = y → if x ∈ A 1 0 = if y ∈ A 1 0
19 2 4 ifex ⊢ if y ∈ A 1 0 ∈ V
20 18 1 19 fvmpt ⊢ y ∈ ℝ → F ⁡ y = if y ∈ A 1 0
21 20 eqeq1d ⊢ y ∈ ℝ → F ⁡ y = 1 ↔ if y ∈ A 1 0 = 1
22 0ne1 ⊢ 0 ≠ 1
23 iffalse ⊢ ¬ y ∈ A → if y ∈ A 1 0 = 0
24 23 eqeq1d ⊢ ¬ y ∈ A → if y ∈ A 1 0 = 1 ↔ 0 = 1
25 24 necon3bbid ⊢ ¬ y ∈ A → ¬ if y ∈ A 1 0 = 1 ↔ 0 ≠ 1
26 22 25 mpbiri ⊢ ¬ y ∈ A → ¬ if y ∈ A 1 0 = 1
27 26 con4i ⊢ if y ∈ A 1 0 = 1 → y ∈ A
28 iftrue ⊢ y ∈ A → if y ∈ A 1 0 = 1
29 27 28 impbii ⊢ if y ∈ A 1 0 = 1 ↔ y ∈ A
30 21 29 bitrdi ⊢ y ∈ ℝ → F ⁡ y = 1 ↔ y ∈ A
31 16 30 syl5bb ⊢ y ∈ ℝ → F ⁡ y ∈ 1 ↔ y ∈ A
32 31 pm5.32i ⊢ y ∈ ℝ ∧ F ⁡ y ∈ 1 ↔ y ∈ ℝ ∧ y ∈ A
33 14 32 bitrdi ⊢ A ∈ dom ⁡ vol → y ∈ F -1 1 ↔ y ∈ ℝ ∧ y ∈ A
34 mblss ⊢ A ∈ dom ⁡ vol → A ⊆ ℝ
35 34 sseld ⊢ A ∈ dom ⁡ vol → y ∈ A → y ∈ ℝ
36 35 pm4.71rd ⊢ A ∈ dom ⁡ vol → y ∈ A ↔ y ∈ ℝ ∧ y ∈ A
37 33 36 bitr4d ⊢ A ∈ dom ⁡ vol → y ∈ F -1 1 ↔ y ∈ A
38 37 eqrdv ⊢ A ∈ dom ⁡ vol → F -1 1 = A
39 9 38 pm3.2i ⊢ F : ℝ ⟶ 0 1 ∧ A ∈ dom ⁡ vol → F -1 1 = A