Metamath Proof Explorer


Theorem indv

Description: Value of the indicator function generator with domain O . (Contributed by Thierry Arnoux, 23-Aug-2017)

Ref Expression
Assertion indv ( 𝑂𝑉 → ( 𝟭 ‘ 𝑂 ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥𝑂 ↦ if ( 𝑥𝑎 , 1 , 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 df-ind 𝟭 = ( 𝑜 ∈ V ↦ ( 𝑎 ∈ 𝒫 𝑜 ↦ ( 𝑥𝑜 ↦ if ( 𝑥𝑎 , 1 , 0 ) ) ) )
2 pweq ( 𝑜 = 𝑂 → 𝒫 𝑜 = 𝒫 𝑂 )
3 mpteq1 ( 𝑜 = 𝑂 → ( 𝑥𝑜 ↦ if ( 𝑥𝑎 , 1 , 0 ) ) = ( 𝑥𝑂 ↦ if ( 𝑥𝑎 , 1 , 0 ) ) )
4 2 3 mpteq12dv ( 𝑜 = 𝑂 → ( 𝑎 ∈ 𝒫 𝑜 ↦ ( 𝑥𝑜 ↦ if ( 𝑥𝑎 , 1 , 0 ) ) ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥𝑂 ↦ if ( 𝑥𝑎 , 1 , 0 ) ) ) )
5 elex ( 𝑂𝑉𝑂 ∈ V )
6 pwexg ( 𝑂 ∈ V → 𝒫 𝑂 ∈ V )
7 mptexg ( 𝒫 𝑂 ∈ V → ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥𝑂 ↦ if ( 𝑥𝑎 , 1 , 0 ) ) ) ∈ V )
8 5 6 7 3syl ( 𝑂𝑉 → ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥𝑂 ↦ if ( 𝑥𝑎 , 1 , 0 ) ) ) ∈ V )
9 1 4 5 8 fvmptd3 ( 𝑂𝑉 → ( 𝟭 ‘ 𝑂 ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥𝑂 ↦ if ( 𝑥𝑎 , 1 , 0 ) ) ) )