Theorem ind1

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

	Ref	Expression
Assertion	ind1	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝐴 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		simp2	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝐴 ) → 𝐴 ⊆ 𝑂 )
2		simp3	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
3	1 2	sseldd	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝑂 )
4		indfval	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = if ( 𝑋 ∈ 𝐴 , 1 , 0 ) )
5	3 4	syld3an3	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝐴 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = if ( 𝑋 ∈ 𝐴 , 1 , 0 ) )
6		iftrue	⊢ ( 𝑋 ∈ 𝐴 → if ( 𝑋 ∈ 𝐴 , 1 , 0 ) = 1 )
7	6	3ad2ant3	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝐴 ) → if ( 𝑋 ∈ 𝐴 , 1 , 0 ) = 1 )
8	5 7	eqtrd	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝐴 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = 1 )