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