Metamath Proof Explorer


Theorem indval2

Description: Alternate value of the indicator function generator. (Contributed by Thierry Arnoux, 2-Feb-2017)

Ref Expression
Assertion indval2 ( ( 𝑂𝑉𝐴𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( ( 𝐴 × { 1 } ) ∪ ( ( 𝑂𝐴 ) × { 0 } ) ) )

Proof

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