Theorem indval

Description: Value of the indicator function generator for a set A and a domain O , i.e., an indicator function for a given domain O and a given subset A of the domain. (Contributed by Thierry Arnoux, 2-Feb-2017)

	Ref	Expression
Assertion	indval	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		indv	⊢ ( 𝑂 ∈ 𝑉 → ( 𝟭 ‘ 𝑂 ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) )
2	1	adantr	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝟭 ‘ 𝑂 ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) )
3		eleq2	⊢ ( 𝑎 = 𝐴 → ( 𝑥 ∈ 𝑎 ↔ 𝑥 ∈ 𝐴 ) )
4	3	ifbid	⊢ ( 𝑎 = 𝐴 → if ( 𝑥 ∈ 𝑎 , 1 , 0 ) = if ( 𝑥 ∈ 𝐴 , 1 , 0 ) )
5	4	mpteq2dv	⊢ ( 𝑎 = 𝐴 → ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) )
6	5	adantl	⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) ∧ 𝑎 = 𝐴 ) → ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) )
7		ssexg	⊢ ( ( 𝐴 ⊆ 𝑂 ∧ 𝑂 ∈ 𝑉 ) → 𝐴 ∈ V )
8	7	ancoms	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → 𝐴 ∈ V )
9		simpr	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → 𝐴 ⊆ 𝑂 )
10	8 9	elpwd	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → 𝐴 ∈ 𝒫 𝑂 )
11		mptexg	⊢ ( 𝑂 ∈ 𝑉 → ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ∈ V )
12	11	adantr	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ∈ V )
13	2 6 10 12	fvmptd	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) )