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