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

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 ) ) ) )