Step |
Hyp |
Ref |
Expression |
1 |
|
indval |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) |
2 |
1
|
3adant3 |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) |
3 |
|
simpr |
⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 ) |
4 |
3
|
eleq1d |
⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) ∧ 𝑥 = 𝑋 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴 ) ) |
5 |
4
|
ifbid |
⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) ∧ 𝑥 = 𝑋 ) → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) = if ( 𝑋 ∈ 𝐴 , 1 , 0 ) ) |
6 |
|
simp3 |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) → 𝑋 ∈ 𝑂 ) |
7 |
|
1re |
⊢ 1 ∈ ℝ |
8 |
|
0re |
⊢ 0 ∈ ℝ |
9 |
7 8
|
ifcli |
⊢ if ( 𝑋 ∈ 𝐴 , 1 , 0 ) ∈ ℝ |
10 |
9
|
a1i |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) → if ( 𝑋 ∈ 𝐴 , 1 , 0 ) ∈ ℝ ) |
11 |
2 5 6 10
|
fvmptd |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = if ( 𝑋 ∈ 𝐴 , 1 , 0 ) ) |