Metamath Proof Explorer


Theorem indval

Description: Value of the indicator function generator for a set A and a domain O . (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 ) ) )