Theorem ind0

Description: Value of the indicator function where it is 0 . (Contributed by Thierry Arnoux, 14-Aug-2017)

	Ref	Expression
Assertion	ind0	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ ( 𝑂 ∖ 𝐴 ) ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		eldifi	⊢ ( 𝑋 ∈ ( 𝑂 ∖ 𝐴 ) → 𝑋 ∈ 𝑂 )
2		indfval	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = if ( 𝑋 ∈ 𝐴 , 1 , 0 ) )
3	1 2	syl3an3	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ ( 𝑂 ∖ 𝐴 ) ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = if ( 𝑋 ∈ 𝐴 , 1 , 0 ) )
4		eldifn	⊢ ( 𝑋 ∈ ( 𝑂 ∖ 𝐴 ) → ¬ 𝑋 ∈ 𝐴 )
5	4	3ad2ant3	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ ( 𝑂 ∖ 𝐴 ) ) → ¬ 𝑋 ∈ 𝐴 )
6	5	iffalsed	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ ( 𝑂 ∖ 𝐴 ) ) → if ( 𝑋 ∈ 𝐴 , 1 , 0 ) = 0 )
7	3 6	eqtrd	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ ( 𝑂 ∖ 𝐴 ) ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = 0 )