Metamath Proof Explorer

Theorem mbfposb

Description: A function is measurable iff its positive and negative parts are measurable. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypothesis mbfpos.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
Assertion mbfposb ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn ) ) )

Proof

Step Hyp Ref Expression
1 mbfpos.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
2 nfcv ⊢ Ⅎ 𝑥 0
3 nfcv ⊢ Ⅎ 𝑥 ≤
4 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
5 2 3 4 nfbr ⊢ Ⅎ 𝑥 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
6 5 4 2 nfif ⊢ Ⅎ 𝑥 if ( 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 )
7 nfcv ⊢ Ⅎ 𝑦 if ( 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , 0 )
8 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
9 8 breq2d ⊢ ( 𝑦 = 𝑥 → ( 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ↔ 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) )
10 9 8 ifbieq1d ⊢ ( 𝑦 = 𝑥 → if ( 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 ) = if ( 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , 0 ) )
11 6 7 10 cbvmpt ⊢ ( 𝑦 ∈ 𝐴 ↦ if ( 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , 0 ) )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
13 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
14 13 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
15 12 1 14 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
16 15 breq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ 0 ≤ 𝐵 ) )
17 16 15 ifbieq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , 0 ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
18 17 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) )
19 11 18 syl5eq ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ if ( 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) → ( 𝑦 ∈ 𝐴 ↦ if ( 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) )
21 1 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ )
22 21 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ )
23 22 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ∈ ℝ )
24 nfcv ⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 )
25 4 24 8 cbvmpt ⊢ ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
26 15 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
27 25 26 syl5eq ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
28 27 eleq1d ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ) ∈ MblFn ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) )
29 28 biimpar ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) → ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ) ∈ MblFn )
30 23 29 mbfpos ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) → ( 𝑦 ∈ 𝐴 ↦ if ( 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 ) ) ∈ MblFn )
31 20 30 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn )
32 4 nfneg ⊢ Ⅎ 𝑥 - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
33 2 3 32 nfbr ⊢ Ⅎ 𝑥 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
34 33 32 2 nfif ⊢ Ⅎ 𝑥 if ( 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 )
35 nfcv ⊢ Ⅎ 𝑦 if ( 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , 0 )
36 8 negeqd ⊢ ( 𝑦 = 𝑥 → - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) = - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
37 36 breq2d ⊢ ( 𝑦 = 𝑥 → ( 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ↔ 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) )
38 37 36 ifbieq1d ⊢ ( 𝑦 = 𝑥 → if ( 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 ) = if ( 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , 0 ) )
39 34 35 38 cbvmpt ⊢ ( 𝑦 ∈ 𝐴 ↦ if ( 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , 0 ) )
40 15 negeqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = - 𝐵 )
41 40 breq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ 0 ≤ - 𝐵 ) )
42 41 40 ifbieq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , 0 ) = if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
43 42 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) )
44 39 43 syl5eq ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ if ( 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) )
45 44 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) → ( 𝑦 ∈ 𝐴 ↦ if ( 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) )
46 23 renegcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) ∧ 𝑦 ∈ 𝐴 ) → - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ∈ ℝ )
47 23 29 mbfneg ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) → ( 𝑦 ∈ 𝐴 ↦ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ) ∈ MblFn )
48 46 47 mbfpos ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) → ( 𝑦 ∈ 𝐴 ↦ if ( 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 ) ) ∈ MblFn )
49 45 48 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn )
50 31 49 jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) → ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn ) )
51 27 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn ) ) → ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
52 21 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ∈ ℝ )
53 52 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn ) ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ∈ ℝ )
54 19 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn ) ) → ( 𝑦 ∈ 𝐴 ↦ if ( 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) )
55 simprl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn ) ) → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn )
56 54 55 eqeltrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn ) ) → ( 𝑦 ∈ 𝐴 ↦ if ( 0 ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 ) ) ∈ MblFn )
57 44 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn ) ) → ( 𝑦 ∈ 𝐴 ↦ if ( 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) )
58 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn ) ) → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn )
59 57 58 eqeltrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn ) ) → ( 𝑦 ∈ 𝐴 ↦ if ( 0 ≤ - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , - ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) , 0 ) ) ∈ MblFn )
60 53 56 59 mbfposr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn ) ) → ( 𝑦 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ) ∈ MblFn )
61 51 60 eqeltrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn ) ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
62 50 61 impbida ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn ) ) )