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	syl5bb	⊢ ( 𝑦 ∈ ℝ → ( ( 𝐹 ‘ 𝑦 ) ∈ { 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 } ) = 𝐴 ) )