Step |
Hyp |
Ref |
Expression |
1 |
|
indv |
⊢ ( 𝑂 ∈ 𝑉 → ( 𝟭 ‘ 𝑂 ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) ) |
2 |
1
|
adantr |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝟭 ‘ 𝑂 ) = ( 𝑎 ∈ 𝒫 𝑂 ↦ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) ) ) |
3 |
|
eleq2 |
⊢ ( 𝑎 = 𝐴 → ( 𝑥 ∈ 𝑎 ↔ 𝑥 ∈ 𝐴 ) ) |
4 |
3
|
ifbid |
⊢ ( 𝑎 = 𝐴 → if ( 𝑥 ∈ 𝑎 , 1 , 0 ) = if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) |
5 |
4
|
mpteq2dv |
⊢ ( 𝑎 = 𝐴 → ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) |
6 |
5
|
adantl |
⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) ∧ 𝑎 = 𝐴 ) → ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝑎 , 1 , 0 ) ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) |
7 |
|
ssexg |
⊢ ( ( 𝐴 ⊆ 𝑂 ∧ 𝑂 ∈ 𝑉 ) → 𝐴 ∈ V ) |
8 |
7
|
ancoms |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → 𝐴 ∈ V ) |
9 |
|
simpr |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → 𝐴 ⊆ 𝑂 ) |
10 |
8 9
|
elpwd |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → 𝐴 ∈ 𝒫 𝑂 ) |
11 |
|
mptexg |
⊢ ( 𝑂 ∈ 𝑉 → ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ∈ V ) |
12 |
11
|
adantr |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ∈ V ) |
13 |
2 6 10 12
|
fvmptd |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) |