Step |
Hyp |
Ref |
Expression |
1 |
|
df-ind |
⊢ 𝟭 = ( 𝑜 ∈ V ↦ ( 𝑎 ∈ 𝒫 𝑜 ↦ ( 𝑥 ∈ 𝑜 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) ) |
2 |
|
pweq |
⊢ ( 𝑜 = 𝑂 → 𝒫 𝑜 = 𝒫 𝑂 ) |
3 |
|
mpteq1 |
⊢ ( 𝑜 = 𝑂 → ( 𝑥 ∈ 𝑜 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) |
4 |
2 3
|
mpteq12dv |
⊢ ( 𝑜 = 𝑂 → ( 𝑎 ∈ 𝒫 𝑜 ↦ ( 𝑥 ∈ 𝑜 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) ) |
5 |
|
elex |
⊢ ( 𝑂 ∈ 𝑉 → 𝑂 ∈ V ) |
6 |
|
pwexg |
⊢ ( 𝑂 ∈ V → 𝒫 𝑂 ∈ V ) |
7 |
|
mptexg |
⊢ ( 𝒫 𝑂 ∈ V → ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) ∈ V ) |
8 |
5 6 7
|
3syl |
⊢ ( 𝑂 ∈ 𝑉 → ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) ∈ V ) |
9 |
1 4 5 8
|
fvmptd3 |
⊢ ( 𝑂 ∈ 𝑉 → ( 𝟭 ‘ 𝑂 ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) ) |