Metamath Proof Explorer

Theorem indval2

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

Ref Expression
Assertion indval2 
|- ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) = ( ( A X. { 1 } ) u. ( ( O \ A ) X. { 0 } ) ) )

Proof

Step Hyp Ref Expression
1 dfmpt3 
 |-  ( x e. O |-> if ( x e. A , 1 , 0 ) ) = U_ x e. O ( { x } X. { if ( x e. A , 1 , 0 ) } )
2 indval 
 |-  ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) = ( x e. O |-> if ( x e. A , 1 , 0 ) ) )
3 undif 
 |-  ( A C_ O <-> ( A u. ( O \ A ) ) = O )
4 3 biimpi 
 |-  ( A C_ O -> ( A u. ( O \ A ) ) = O )
5 4 adantl 
 |-  ( ( O e. V /\ A C_ O ) -> ( A u. ( O \ A ) ) = O )
6 5 iuneq1d 
 |-  ( ( O e. V /\ A C_ O ) -> U_ x e. ( A u. ( O \ A ) ) ( { x } X. { if ( x e. A , 1 , 0 ) } ) = U_ x e. O ( { x } X. { if ( x e. A , 1 , 0 ) } ) )
7 1 2 6 3eqtr4a 
 |-  ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) = U_ x e. ( A u. ( O \ A ) ) ( { x } X. { if ( x e. A , 1 , 0 ) } ) )
8 iunxun 
 |-  U_ x e. ( A u. ( O \ A ) ) ( { x } X. { if ( x e. A , 1 , 0 ) } ) = ( U_ x e. A ( { x } X. { if ( x e. A , 1 , 0 ) } ) u. U_ x e. ( O \ A ) ( { x } X. { if ( x e. A , 1 , 0 ) } ) )
9 7 8 eqtrdi 
 |-  ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) = ( U_ x e. A ( { x } X. { if ( x e. A , 1 , 0 ) } ) u. U_ x e. ( O \ A ) ( { x } X. { if ( x e. A , 1 , 0 ) } ) ) )
10 iftrue 
 |-  ( x e. A -> if ( x e. A , 1 , 0 ) = 1 )
11 10 sneqd 
 |-  ( x e. A -> { if ( x e. A , 1 , 0 ) } = { 1 } )
12 11 xpeq2d 
 |-  ( x e. A -> ( { x } X. { if ( x e. A , 1 , 0 ) } ) = ( { x } X. { 1 } ) )
13 12 iuneq2i 
 |-  U_ x e. A ( { x } X. { if ( x e. A , 1 , 0 ) } ) = U_ x e. A ( { x } X. { 1 } )
14 iunxpconst 
 |-  U_ x e. A ( { x } X. { 1 } ) = ( A X. { 1 } )
15 13 14 eqtri 
 |-  U_ x e. A ( { x } X. { if ( x e. A , 1 , 0 ) } ) = ( A X. { 1 } )
16 eldifn 
 |-  ( x e. ( O \ A ) -> -. x e. A )
17 iffalse 
 |-  ( -. x e. A -> if ( x e. A , 1 , 0 ) = 0 )
18 17 sneqd 
 |-  ( -. x e. A -> { if ( x e. A , 1 , 0 ) } = { 0 } )
19 16 18 syl 
 |-  ( x e. ( O \ A ) -> { if ( x e. A , 1 , 0 ) } = { 0 } )
20 19 xpeq2d 
 |-  ( x e. ( O \ A ) -> ( { x } X. { if ( x e. A , 1 , 0 ) } ) = ( { x } X. { 0 } ) )
21 20 iuneq2i 
 |-  U_ x e. ( O \ A ) ( { x } X. { if ( x e. A , 1 , 0 ) } ) = U_ x e. ( O \ A ) ( { x } X. { 0 } )
22 iunxpconst 
 |-  U_ x e. ( O \ A ) ( { x } X. { 0 } ) = ( ( O \ A ) X. { 0 } )
23 21 22 eqtri 
 |-  U_ x e. ( O \ A ) ( { x } X. { if ( x e. A , 1 , 0 ) } ) = ( ( O \ A ) X. { 0 } )
24 15 23 uneq12i 
 |-  ( U_ x e. A ( { x } X. { if ( x e. A , 1 , 0 ) } ) u. U_ x e. ( O \ A ) ( { x } X. { if ( x e. A , 1 , 0 ) } ) ) = ( ( A X. { 1 } ) u. ( ( O \ A ) X. { 0 } ) )
25 9 24 eqtrdi 
 |-  ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) = ( ( A X. { 1 } ) u. ( ( O \ A ) X. { 0 } ) ) )