Step |
Hyp |
Ref |
Expression |
1 |
|
reex |
⊢ ℝ ∈ V |
2 |
1
|
ssex |
⊢ ( 𝐴 ⊆ ℝ → 𝐴 ∈ V ) |
3 |
|
elpwg |
⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 ℝ ↔ 𝐴 ⊆ ℝ ) ) |
4 |
3
|
biimpar |
⊢ ( ( 𝐴 ∈ V ∧ 𝐴 ⊆ ℝ ) → 𝐴 ∈ 𝒫 ℝ ) |
5 |
2 4
|
mpancom |
⊢ ( 𝐴 ⊆ ℝ → 𝐴 ∈ 𝒫 ℝ ) |
6 |
|
eleq2 |
⊢ ( 𝑎 = 𝐴 → ( 0 ∈ 𝑎 ↔ 0 ∈ 𝐴 ) ) |
7 |
6
|
ifbid |
⊢ ( 𝑎 = 𝐴 → if ( 0 ∈ 𝑎 , 1 , 0 ) = if ( 0 ∈ 𝐴 , 1 , 0 ) ) |
8 |
|
df-dde |
⊢ δ = ( 𝑎 ∈ 𝒫 ℝ ↦ if ( 0 ∈ 𝑎 , 1 , 0 ) ) |
9 |
|
1ex |
⊢ 1 ∈ V |
10 |
|
c0ex |
⊢ 0 ∈ V |
11 |
9 10
|
ifex |
⊢ if ( 0 ∈ 𝐴 , 1 , 0 ) ∈ V |
12 |
7 8 11
|
fvmpt |
⊢ ( 𝐴 ∈ 𝒫 ℝ → ( δ ‘ 𝐴 ) = if ( 0 ∈ 𝐴 , 1 , 0 ) ) |
13 |
5 12
|
syl |
⊢ ( 𝐴 ⊆ ℝ → ( δ ‘ 𝐴 ) = if ( 0 ∈ 𝐴 , 1 , 0 ) ) |
14 |
|
iffalse |
⊢ ( ¬ 0 ∈ 𝐴 → if ( 0 ∈ 𝐴 , 1 , 0 ) = 0 ) |
15 |
13 14
|
sylan9eq |
⊢ ( ( 𝐴 ⊆ ℝ ∧ ¬ 0 ∈ 𝐴 ) → ( δ ‘ 𝐴 ) = 0 ) |