Step |
Hyp |
Ref |
Expression |
1 |
|
dfmpt3 |
⊢ ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) = ∪ 𝑥 ∈ 𝑂 ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) |
2 |
|
indval |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) ) |
3 |
|
undif |
⊢ ( 𝐴 ⊆ 𝑂 ↔ ( 𝐴 ∪ ( 𝑂 ∖ 𝐴 ) ) = 𝑂 ) |
4 |
3
|
biimpi |
⊢ ( 𝐴 ⊆ 𝑂 → ( 𝐴 ∪ ( 𝑂 ∖ 𝐴 ) ) = 𝑂 ) |
5 |
4
|
adantl |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝐴 ∪ ( 𝑂 ∖ 𝐴 ) ) = 𝑂 ) |
6 |
5
|
iuneq1d |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ∪ 𝑥 ∈ ( 𝐴 ∪ ( 𝑂 ∖ 𝐴 ) ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ∪ 𝑥 ∈ 𝑂 ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) ) |
7 |
1 2 6
|
3eqtr4a |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ∪ 𝑥 ∈ ( 𝐴 ∪ ( 𝑂 ∖ 𝐴 ) ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) ) |
8 |
|
iunxun |
⊢ ∪ 𝑥 ∈ ( 𝐴 ∪ ( 𝑂 ∖ 𝐴 ) ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) ∪ ∪ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) ) |
9 |
7 8
|
eqtrdi |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) ∪ ∪ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) ) ) |
10 |
|
iftrue |
⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) = 1 ) |
11 |
10
|
sneqd |
⊢ ( 𝑥 ∈ 𝐴 → { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } = { 1 } ) |
12 |
11
|
xpeq2d |
⊢ ( 𝑥 ∈ 𝐴 → ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ( { 𝑥 } × { 1 } ) ) |
13 |
12
|
iuneq2i |
⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 1 } ) |
14 |
|
iunxpconst |
⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 1 } ) = ( 𝐴 × { 1 } ) |
15 |
13 14
|
eqtri |
⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ( 𝐴 × { 1 } ) |
16 |
|
eldifn |
⊢ ( 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 ) |
17 |
|
iffalse |
⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) = 0 ) |
18 |
17
|
sneqd |
⊢ ( ¬ 𝑥 ∈ 𝐴 → { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } = { 0 } ) |
19 |
16 18
|
syl |
⊢ ( 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) → { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } = { 0 } ) |
20 |
19
|
xpeq2d |
⊢ ( 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) → ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ( { 𝑥 } × { 0 } ) ) |
21 |
20
|
iuneq2i |
⊢ ∪ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ∪ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ( { 𝑥 } × { 0 } ) |
22 |
|
iunxpconst |
⊢ ∪ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ( { 𝑥 } × { 0 } ) = ( ( 𝑂 ∖ 𝐴 ) × { 0 } ) |
23 |
21 22
|
eqtri |
⊢ ∪ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ( ( 𝑂 ∖ 𝐴 ) × { 0 } ) |
24 |
15 23
|
uneq12i |
⊢ ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) ∪ ∪ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) ) = ( ( 𝐴 × { 1 } ) ∪ ( ( 𝑂 ∖ 𝐴 ) × { 0 } ) ) |
25 |
9 24
|
eqtrdi |
⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( ( 𝐴 × { 1 } ) ∪ ( ( 𝑂 ∖ 𝐴 ) × { 0 } ) ) ) |