Theorem ind1a

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

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

Proof

Step	Hyp	Ref	Expression
1		indfval	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = if ( 𝑋 ∈ 𝐴 , 1 , 0 ) )
2	1	eqeq1d	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = 1 ↔ if ( 𝑋 ∈ 𝐴 , 1 , 0 ) = 1 ) )
3		eqid	⊢ 1 = 1
4	3	biantru	⊢ ( 𝑋 ∈ 𝐴 ↔ ( 𝑋 ∈ 𝐴 ∧ 1 = 1 ) )
5		ax-1ne0	⊢ 1 ≠ 0
6	5	neii	⊢ ¬ 1 = 0
7	6	biorfri	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 1 = 1 ) ↔ ( ( 𝑋 ∈ 𝐴 ∧ 1 = 1 ) ∨ 1 = 0 ) )
8	6	bianfi	⊢ ( 1 = 0 ↔ ( ¬ 𝑋 ∈ 𝐴 ∧ 1 = 0 ) )
9	8	orbi2i	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 1 = 1 ) ∨ 1 = 0 ) ↔ ( ( 𝑋 ∈ 𝐴 ∧ 1 = 1 ) ∨ ( ¬ 𝑋 ∈ 𝐴 ∧ 1 = 0 ) ) )
10	4 7 9	3bitri	⊢ ( 𝑋 ∈ 𝐴 ↔ ( ( 𝑋 ∈ 𝐴 ∧ 1 = 1 ) ∨ ( ¬ 𝑋 ∈ 𝐴 ∧ 1 = 0 ) ) )
11		eqif	⊢ ( 1 = if ( 𝑋 ∈ 𝐴 , 1 , 0 ) ↔ ( ( 𝑋 ∈ 𝐴 ∧ 1 = 1 ) ∨ ( ¬ 𝑋 ∈ 𝐴 ∧ 1 = 0 ) ) )
12		eqcom	⊢ ( 1 = if ( 𝑋 ∈ 𝐴 , 1 , 0 ) ↔ if ( 𝑋 ∈ 𝐴 , 1 , 0 ) = 1 )
13	10 11 12	3bitr2ri	⊢ ( if ( 𝑋 ∈ 𝐴 , 1 , 0 ) = 1 ↔ 𝑋 ∈ 𝐴 )
14	2 13	bitrdi	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = 1 ↔ 𝑋 ∈ 𝐴 ) )