This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem i1f1lem

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

Ref Expression
Hypothesis i1f1.1 ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) )
Assertion i1f1lem ( 𝐹 : ℝ ⟶ { 0 , 1 } ∧ ( 𝐴 ∈ dom vol → ( ◡ 𝐹 “ { 1 } ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 i1f1.1 ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 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 ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ { 0 , 1 }
7 6 rgenw ⊢ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ { 0 , 1 }
8 1 fmpt ⊢ ( ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ { 0 , 1 } ↔ 𝐹 : ℝ ⟶ { 0 , 1 } )
9 7 8 mpbi ⊢ 𝐹 : ℝ ⟶ { 0 , 1 }
10 6 a1i ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ { 0 , 1 } )
11 10 1 fmptd ⊢ ( 𝐴 ∈ dom vol → 𝐹 : ℝ ⟶ { 0 , 1 } )
12 ffn ⊢ ( 𝐹 : ℝ ⟶ { 0 , 1 } → 𝐹 Fn ℝ )
13 elpreima ⊢ ( 𝐹 Fn ℝ → ( 𝑦 ∈ ( ◡ 𝐹 “ { 1 } ) ↔ ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑦 ) ∈ { 1 } ) ) )
14 11 12 13 3syl ⊢ ( 𝐴 ∈ dom vol → ( 𝑦 ∈ ( ◡ 𝐹 “ { 1 } ) ↔ ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑦 ) ∈ { 1 } ) ) )
15 fvex ⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
16 15 elsn ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ { 1 } ↔ ( 𝐹 ‘ 𝑦 ) = 1 )
17 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
18 17 ifbid ⊢ ( 𝑥 = 𝑦 → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) = if ( 𝑦 ∈ 𝐴 , 1 , 0 ) )
19 2 4 ifex ⊢ if ( 𝑦 ∈ 𝐴 , 1 , 0 ) ∈ V
20 18 1 19 fvmpt ⊢ ( 𝑦 ∈ ℝ → ( 𝐹 ‘ 𝑦 ) = if ( 𝑦 ∈ 𝐴 , 1 , 0 ) )
21 20 eqeq1d ⊢ ( 𝑦 ∈ ℝ → ( ( 𝐹 ‘ 𝑦 ) = 1 ↔ if ( 𝑦 ∈ 𝐴 , 1 , 0 ) = 1 ) )
22 0ne1 ⊢ 0 ≠ 1
23 iffalse ⊢ ( ¬ 𝑦 ∈ 𝐴 → if ( 𝑦 ∈ 𝐴 , 1 , 0 ) = 0 )
24 23 eqeq1d ⊢ ( ¬ 𝑦 ∈ 𝐴 → ( if ( 𝑦 ∈ 𝐴 , 1 , 0 ) = 1 ↔ 0 = 1 ) )
25 24 necon3bbid ⊢ ( ¬ 𝑦 ∈ 𝐴 → ( ¬ if ( 𝑦 ∈ 𝐴 , 1 , 0 ) = 1 ↔ 0 ≠ 1 ) )
26 22 25 mpbiri ⊢ ( ¬ 𝑦 ∈ 𝐴 → ¬ if ( 𝑦 ∈ 𝐴 , 1 , 0 ) = 1 )
27 26 con4i ⊢ ( if ( 𝑦 ∈ 𝐴 , 1 , 0 ) = 1 → 𝑦 ∈ 𝐴 )
28 iftrue ⊢ ( 𝑦 ∈ 𝐴 → if ( 𝑦 ∈ 𝐴 , 1 , 0 ) = 1 )
29 27 28 impbii ⊢ ( if ( 𝑦 ∈ 𝐴 , 1 , 0 ) = 1 ↔ 𝑦 ∈ 𝐴 )
30 21 29 bitrdi ⊢ ( 𝑦 ∈ ℝ → ( ( 𝐹 ‘ 𝑦 ) = 1 ↔ 𝑦 ∈ 𝐴 ) )
31 16 30 bitrid ⊢ ( 𝑦 ∈ ℝ → ( ( 𝐹 ‘ 𝑦 ) ∈ { 1 } ↔ 𝑦 ∈ 𝐴 ) )
32 31 pm5.32i ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑦 ) ∈ { 1 } ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) )
33 14 32 bitrdi ⊢ ( 𝐴 ∈ dom vol → ( 𝑦 ∈ ( ◡ 𝐹 “ { 1 } ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ) )
34 mblss ⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
35 34 sseld ⊢ ( 𝐴 ∈ dom vol → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℝ ) )
36 35 pm4.71rd ⊢ ( 𝐴 ∈ dom vol → ( 𝑦 ∈ 𝐴 ↔ ( 𝑦 ∈ ℝ ∧ 𝑦 ∈ 𝐴 ) ) )
37 33 36 bitr4d ⊢ ( 𝐴 ∈ dom vol → ( 𝑦 ∈ ( ◡ 𝐹 “ { 1 } ) ↔ 𝑦 ∈ 𝐴 ) )
38 37 eqrdv ⊢ ( 𝐴 ∈ dom vol → ( ◡ 𝐹 “ { 1 } ) = 𝐴 )
39 9 38 pm3.2i ⊢ ( 𝐹 : ℝ ⟶ { 0 , 1 } ∧ ( 𝐴 ∈ dom vol → ( ◡ 𝐹 “ { 1 } ) = 𝐴 ) )