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 bilani ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( 𝐴 ∪ ( 𝑂 ∖ 𝐴 ) ) = 𝑂 )
5 4 iuneq1d ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ∪ 𝑥 ∈ ( 𝐴 ∪ ( 𝑂 ∖ 𝐴 ) ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ∪ 𝑥 ∈ 𝑂 ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) )
6 1 2 5 3eqtr4a ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ∪ 𝑥 ∈ ( 𝐴 ∪ ( 𝑂 ∖ 𝐴 ) ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) )
7 iunxun ⊢ ∪ 𝑥 ∈ ( 𝐴 ∪ ( 𝑂 ∖ 𝐴 ) ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) ∪ ∪ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) )
8 6 7 eqtrdi ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) ∪ ∪ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) ) )
9 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) = 1 )
10 9 sneqd ⊢ ( 𝑥 ∈ 𝐴 → { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } = { 1 } )
11 10 xpeq2d ⊢ ( 𝑥 ∈ 𝐴 → ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ( { 𝑥 } × { 1 } ) )
12 11 iuneq2i ⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 1 } )
13 iunxpconst ⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { 1 } ) = ( 𝐴 × { 1 } )
14 12 13 eqtri ⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ( 𝐴 × { 1 } )
15 eldifn ⊢ ( 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 )
16 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) = 0 )
17 16 sneqd ⊢ ( ¬ 𝑥 ∈ 𝐴 → { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } = { 0 } )
18 15 17 syl ⊢ ( 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) → { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } = { 0 } )
19 18 xpeq2d ⊢ ( 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) → ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ( { 𝑥 } × { 0 } ) )
20 19 iuneq2i ⊢ ∪ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ∪ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ( { 𝑥 } × { 0 } )
21 iunxpconst ⊢ ∪ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ( { 𝑥 } × { 0 } ) = ( ( 𝑂 ∖ 𝐴 ) × { 0 } )
22 20 21 eqtri ⊢ ∪ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) = ( ( 𝑂 ∖ 𝐴 ) × { 0 } )
23 14 22 uneq12i ⊢ ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) ∪ ∪ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ( { 𝑥 } × { if ( 𝑥 ∈ 𝐴 , 1 , 0 ) } ) ) = ( ( 𝐴 × { 1 } ) ∪ ( ( 𝑂 ∖ 𝐴 ) × { 0 } ) )
24 8 23 eqtrdi ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( ( 𝐴 × { 1 } ) ∪ ( ( 𝑂 ∖ 𝐴 ) × { 0 } ) ) )