Metamath Proof Explorer

Theorem mbfresfi

Description: Measurability of a piecewise function across arbitrarily many subsets. (Contributed by Brendan Leahy, 31-Mar-2018)

Ref Expression
Hypotheses mbfresfi.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
mbfresfi.2 ⊢ ( 𝜑 → 𝑆 ∈ Fin )
mbfresfi.3 ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝑆 ( 𝐹 ↾ 𝑠 ) ∈ MblFn )
mbfresfi.4 ⊢ ( 𝜑 → ∪ 𝑆 = 𝐴 )
Assertion mbfresfi ( 𝜑 → 𝐹 ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfresfi.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2 mbfresfi.2 ⊢ ( 𝜑 → 𝑆 ∈ Fin )
3 mbfresfi.3 ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝑆 ( 𝐹 ↾ 𝑠 ) ∈ MblFn )
4 mbfresfi.4 ⊢ ( 𝜑 → ∪ 𝑆 = 𝐴 )
5 2 uniexd ⊢ ( 𝜑 → ∪ 𝑆 ∈ V )
6 4 5 eqeltrrd ⊢ ( 𝜑 → 𝐴 ∈ V )
7 fex ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ V ) → 𝐹 ∈ V )
8 7 ex ⊢ ( 𝐹 : 𝐴 ⟶ ℂ → ( 𝐴 ∈ V → 𝐹 ∈ V ) )
9 1 8 syl ⊢ ( 𝜑 → ( 𝐴 ∈ V → 𝐹 ∈ V ) )
10 6 9 jcai ⊢ ( 𝜑 → ( 𝐴 ∈ V ∧ 𝐹 ∈ V ) )
11 feq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑓 : 𝑎 ⟶ ℂ ↔ 𝑓 : 𝐴 ⟶ ℂ ) )
12 11 anbi1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ↔ ( 𝑓 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ) )
13 eqeq2 ⊢ ( 𝑎 = 𝐴 → ( ∪ 𝑆 = 𝑎 ↔ ∪ 𝑆 = 𝐴 ) )
14 12 13 anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝑎 ) ↔ ( ( 𝑓 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝐴 ) ) )
15 14 imbi1d ⊢ ( 𝑎 = 𝐴 → ( ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝑎 ) → 𝑓 ∈ MblFn ) ↔ ( ( ( 𝑓 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝐴 ) → 𝑓 ∈ MblFn ) ) )
16 15 imbi2d ⊢ ( 𝑎 = 𝐴 → ( ( 𝜑 → ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝑎 ) → 𝑓 ∈ MblFn ) ) ↔ ( 𝜑 → ( ( ( 𝑓 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝐴 ) → 𝑓 ∈ MblFn ) ) ) )
17 feq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝐴 ⟶ ℂ ↔ 𝐹 : 𝐴 ⟶ ℂ ) )
18 reseq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ↾ 𝑠 ) = ( 𝐹 ↾ 𝑠 ) )
19 18 eleq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ↾ 𝑠 ) ∈ MblFn ↔ ( 𝐹 ↾ 𝑠 ) ∈ MblFn ) )
20 19 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ↔ ∀ 𝑠 ∈ 𝑆 ( 𝐹 ↾ 𝑠 ) ∈ MblFn ) )
21 17 20 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝐹 ↾ 𝑠 ) ∈ MblFn ) ) )
22 21 anbi1d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝐴 ) ↔ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝐹 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝐴 ) ) )
23 eleq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ MblFn ↔ 𝐹 ∈ MblFn ) )
24 22 23 imbi12d ⊢ ( 𝑓 = 𝐹 → ( ( ( ( 𝑓 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝐴 ) → 𝑓 ∈ MblFn ) ↔ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝐹 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝐴 ) → 𝐹 ∈ MblFn ) ) )
25 24 imbi2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝜑 → ( ( ( 𝑓 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝐴 ) → 𝑓 ∈ MblFn ) ) ↔ ( 𝜑 → ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝐹 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝐴 ) → 𝐹 ∈ MblFn ) ) ) )
26 rzal ⊢ ( 𝑟 = ∅ → ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn )
27 26 biantrud ⊢ ( 𝑟 = ∅ → ( 𝑓 : 𝑎 ⟶ ℂ ↔ ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ) )
28 27 bicomd ⊢ ( 𝑟 = ∅ → ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ↔ 𝑓 : 𝑎 ⟶ ℂ ) )
29 unieq ⊢ ( 𝑟 = ∅ → ∪ 𝑟 = ∪ ∅ )
30 uni0 ⊢ ∪ ∅ = ∅
31 29 30 eqtrdi ⊢ ( 𝑟 = ∅ → ∪ 𝑟 = ∅ )
32 31 eqeq1d ⊢ ( 𝑟 = ∅ → ( ∪ 𝑟 = 𝑎 ↔ ∅ = 𝑎 ) )
33 28 32 anbi12d ⊢ ( 𝑟 = ∅ → ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑟 = 𝑎 ) ↔ ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∅ = 𝑎 ) ) )
34 33 imbi1d ⊢ ( 𝑟 = ∅ → ( ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑟 = 𝑎 ) → 𝑓 ∈ MblFn ) ↔ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∅ = 𝑎 ) → 𝑓 ∈ MblFn ) ) )
35 34 2albidv ⊢ ( 𝑟 = ∅ → ( ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑟 = 𝑎 ) → 𝑓 ∈ MblFn ) ↔ ∀ 𝑓 ∀ 𝑎 ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∅ = 𝑎 ) → 𝑓 ∈ MblFn ) ) )
36 raleq ⊢ ( 𝑟 = 𝑡 → ( ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ↔ ∀ 𝑠 ∈ 𝑡 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) )
37 36 anbi2d ⊢ ( 𝑟 = 𝑡 → ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ↔ ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ) )
38 unieq ⊢ ( 𝑟 = 𝑡 → ∪ 𝑟 = ∪ 𝑡 )
39 38 eqeq1d ⊢ ( 𝑟 = 𝑡 → ( ∪ 𝑟 = 𝑎 ↔ ∪ 𝑡 = 𝑎 ) )
40 37 39 anbi12d ⊢ ( 𝑟 = 𝑡 → ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑟 = 𝑎 ) ↔ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑎 ) ) )
41 40 imbi1d ⊢ ( 𝑟 = 𝑡 → ( ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑟 = 𝑎 ) → 𝑓 ∈ MblFn ) ↔ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑎 ) → 𝑓 ∈ MblFn ) ) )
42 41 2albidv ⊢ ( 𝑟 = 𝑡 → ( ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑟 = 𝑎 ) → 𝑓 ∈ MblFn ) ↔ ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑎 ) → 𝑓 ∈ MblFn ) ) )
43 simpl ⊢ ( ( 𝑓 = 𝑔 ∧ 𝑎 = 𝑏 ) → 𝑓 = 𝑔 )
44 simpr ⊢ ( ( 𝑓 = 𝑔 ∧ 𝑎 = 𝑏 ) → 𝑎 = 𝑏 )
45 43 44 feq12d ⊢ ( ( 𝑓 = 𝑔 ∧ 𝑎 = 𝑏 ) → ( 𝑓 : 𝑎 ⟶ ℂ ↔ 𝑔 : 𝑏 ⟶ ℂ ) )
46 reseq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ↾ 𝑠 ) = ( 𝑔 ↾ 𝑠 ) )
47 46 adantr ⊢ ( ( 𝑓 = 𝑔 ∧ 𝑎 = 𝑏 ) → ( 𝑓 ↾ 𝑠 ) = ( 𝑔 ↾ 𝑠 ) )
48 47 eleq1d ⊢ ( ( 𝑓 = 𝑔 ∧ 𝑎 = 𝑏 ) → ( ( 𝑓 ↾ 𝑠 ) ∈ MblFn ↔ ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) )
49 48 ralbidv ⊢ ( ( 𝑓 = 𝑔 ∧ 𝑎 = 𝑏 ) → ( ∀ 𝑠 ∈ 𝑡 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ↔ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) )
50 45 49 anbi12d ⊢ ( ( 𝑓 = 𝑔 ∧ 𝑎 = 𝑏 ) → ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ↔ ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ) )
51 eqeq2 ⊢ ( 𝑎 = 𝑏 → ( ∪ 𝑡 = 𝑎 ↔ ∪ 𝑡 = 𝑏 ) )
52 51 adantl ⊢ ( ( 𝑓 = 𝑔 ∧ 𝑎 = 𝑏 ) → ( ∪ 𝑡 = 𝑎 ↔ ∪ 𝑡 = 𝑏 ) )
53 50 52 anbi12d ⊢ ( ( 𝑓 = 𝑔 ∧ 𝑎 = 𝑏 ) → ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑎 ) ↔ ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) ) )
54 eleq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ∈ MblFn ↔ 𝑔 ∈ MblFn ) )
55 54 adantr ⊢ ( ( 𝑓 = 𝑔 ∧ 𝑎 = 𝑏 ) → ( 𝑓 ∈ MblFn ↔ 𝑔 ∈ MblFn ) )
56 53 55 imbi12d ⊢ ( ( 𝑓 = 𝑔 ∧ 𝑎 = 𝑏 ) → ( ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑎 ) → 𝑓 ∈ MblFn ) ↔ ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ) )
57 56 cbval2vw ⊢ ( ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑎 ) → 𝑓 ∈ MblFn ) ↔ ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) )
58 42 57 bitrdi ⊢ ( 𝑟 = 𝑡 → ( ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑟 = 𝑎 ) → 𝑓 ∈ MblFn ) ↔ ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ) )
59 raleq ⊢ ( 𝑟 = ( 𝑡 ∪ { ℎ } ) → ( ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ↔ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) )
60 59 anbi2d ⊢ ( 𝑟 = ( 𝑡 ∪ { ℎ } ) → ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ↔ ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ) )
61 unieq ⊢ ( 𝑟 = ( 𝑡 ∪ { ℎ } ) → ∪ 𝑟 = ∪ ( 𝑡 ∪ { ℎ } ) )
62 61 eqeq1d ⊢ ( 𝑟 = ( 𝑡 ∪ { ℎ } ) → ( ∪ 𝑟 = 𝑎 ↔ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) )
63 60 62 anbi12d ⊢ ( 𝑟 = ( 𝑡 ∪ { ℎ } ) → ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑟 = 𝑎 ) ↔ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) )
64 63 imbi1d ⊢ ( 𝑟 = ( 𝑡 ∪ { ℎ } ) → ( ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑟 = 𝑎 ) → 𝑓 ∈ MblFn ) ↔ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → 𝑓 ∈ MblFn ) ) )
65 64 2albidv ⊢ ( 𝑟 = ( 𝑡 ∪ { ℎ } ) → ( ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑟 = 𝑎 ) → 𝑓 ∈ MblFn ) ↔ ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → 𝑓 ∈ MblFn ) ) )
66 raleq ⊢ ( 𝑟 = 𝑆 → ( ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ↔ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) )
67 66 anbi2d ⊢ ( 𝑟 = 𝑆 → ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ↔ ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ) )
68 unieq ⊢ ( 𝑟 = 𝑆 → ∪ 𝑟 = ∪ 𝑆 )
69 68 eqeq1d ⊢ ( 𝑟 = 𝑆 → ( ∪ 𝑟 = 𝑎 ↔ ∪ 𝑆 = 𝑎 ) )
70 67 69 anbi12d ⊢ ( 𝑟 = 𝑆 → ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑟 = 𝑎 ) ↔ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝑎 ) ) )
71 70 imbi1d ⊢ ( 𝑟 = 𝑆 → ( ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑟 = 𝑎 ) → 𝑓 ∈ MblFn ) ↔ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝑎 ) → 𝑓 ∈ MblFn ) ) )
72 71 2albidv ⊢ ( 𝑟 = 𝑆 → ( ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑟 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑟 = 𝑎 ) → 𝑓 ∈ MblFn ) ↔ ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝑎 ) → 𝑓 ∈ MblFn ) ) )
73 frel ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → Rel 𝑓 )
74 73 adantr ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∅ = 𝑎 ) → Rel 𝑓 )
75 fdm ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → dom 𝑓 = 𝑎 )
76 eqcom ⊢ ( ∅ = 𝑎 ↔ 𝑎 = ∅ )
77 76 biimpi ⊢ ( ∅ = 𝑎 → 𝑎 = ∅ )
78 75 77 sylan9eq ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∅ = 𝑎 ) → dom 𝑓 = ∅ )
79 reldm0 ⊢ ( Rel 𝑓 → ( 𝑓 = ∅ ↔ dom 𝑓 = ∅ ) )
80 79 biimpar ⊢ ( ( Rel 𝑓 ∧ dom 𝑓 = ∅ ) → 𝑓 = ∅ )
81 mbf0 ⊢ ∅ ∈ MblFn
82 80 81 eqeltrdi ⊢ ( ( Rel 𝑓 ∧ dom 𝑓 = ∅ ) → 𝑓 ∈ MblFn )
83 74 78 82 syl2anc ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∅ = 𝑎 ) → 𝑓 ∈ MblFn )
84 83 gen2 ⊢ ∀ 𝑓 ∀ 𝑎 ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∅ = 𝑎 ) → 𝑓 ∈ MblFn )
85 ref ⊢ ℜ : ℂ ⟶ ℝ
86 fco ⊢ ( ( ℜ : ℂ ⟶ ℝ ∧ 𝑓 : 𝑎 ⟶ ℂ ) → ( ℜ ∘ 𝑓 ) : 𝑎 ⟶ ℝ )
87 85 86 mpan ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( ℜ ∘ 𝑓 ) : 𝑎 ⟶ ℝ )
88 87 adantr ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ( ℜ ∘ 𝑓 ) : 𝑎 ⟶ ℝ )
89 88 ad2antrl ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ℜ ∘ 𝑓 ) : 𝑎 ⟶ ℝ )
90 recncf ⊢ ℜ ∈ ( ℂ –cn→ ℝ )
91 90 elexi ⊢ ℜ ∈ V
92 vex ⊢ 𝑓 ∈ V
93 91 92 coex ⊢ ( ℜ ∘ 𝑓 ) ∈ V
94 93 resex ⊢ ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ V
95 vuniex ⊢ ∪ 𝑡 ∈ V
96 eqcom ⊢ ( 𝑏 = ∪ 𝑡 ↔ ∪ 𝑡 = 𝑏 )
97 96 biimpi ⊢ ( 𝑏 = ∪ 𝑡 → ∪ 𝑡 = 𝑏 )
98 97 adantl ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ∪ 𝑡 = 𝑏 )
99 98 biantrud ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ↔ ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) ) )
100 eqid ⊢ ℂ = ℂ
101 feq123 ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ∧ ℂ = ℂ ) → ( 𝑔 : 𝑏 ⟶ ℂ ↔ ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ) )
102 100 101 mp3an3 ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( 𝑔 : 𝑏 ⟶ ℂ ↔ ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ) )
103 reseq1 ⊢ ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) → ( 𝑔 ↾ 𝑠 ) = ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) )
104 103 eleq1d ⊢ ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) → ( ( 𝑔 ↾ 𝑠 ) ∈ MblFn ↔ ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
105 104 adantr ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( 𝑔 ↾ 𝑠 ) ∈ MblFn ↔ ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
106 105 ralbidv ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ↔ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
107 102 106 anbi12d ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ↔ ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) ) )
108 99 107 bitr3d ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) ↔ ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) ) )
109 eleq1 ⊢ ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) → ( 𝑔 ∈ MblFn ↔ ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
110 109 adantr ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( 𝑔 ∈ MblFn ↔ ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
111 108 110 imbi12d ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ↔ ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) ) )
112 111 spc2gv ⊢ ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ V ∧ ∪ 𝑡 ∈ V ) → ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) → ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) ) )
113 94 95 112 mp2an ⊢ ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) → ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
114 ax-resscn ⊢ ℝ ⊆ ℂ
115 fss ⊢ ( ( ℜ : ℂ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ℜ : ℂ ⟶ ℂ )
116 85 114 115 mp2an ⊢ ℜ : ℂ ⟶ ℂ
117 fco ⊢ ( ( ℜ : ℂ ⟶ ℂ ∧ 𝑓 : 𝑎 ⟶ ℂ ) → ( ℜ ∘ 𝑓 ) : 𝑎 ⟶ ℂ )
118 116 117 mpan ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( ℜ ∘ 𝑓 ) : 𝑎 ⟶ ℂ )
119 ssun1 ⊢ 𝑡 ⊆ ( 𝑡 ∪ { ℎ } )
120 119 unissi ⊢ ∪ 𝑡 ⊆ ∪ ( 𝑡 ∪ { ℎ } )
121 id ⊢ ( ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 → ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 )
122 120 121 sseqtrid ⊢ ( ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 → ∪ 𝑡 ⊆ 𝑎 )
123 fssres ⊢ ( ( ( ℜ ∘ 𝑓 ) : 𝑎 ⟶ ℂ ∧ ∪ 𝑡 ⊆ 𝑎 ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ )
124 118 122 123 syl2an ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ )
125 124 adantlr ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ )
126 elssuni ⊢ ( 𝑟 ∈ 𝑡 → 𝑟 ⊆ ∪ 𝑡 )
127 126 resabs1d ⊢ ( 𝑟 ∈ 𝑡 → ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ( ℜ ∘ 𝑓 ) ↾ 𝑟 ) )
128 resco ⊢ ( ( ℜ ∘ 𝑓 ) ↾ 𝑟 ) = ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) )
129 127 128 eqtrdi ⊢ ( 𝑟 ∈ 𝑡 → ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) )
130 129 adantl ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) )
131 elun1 ⊢ ( 𝑟 ∈ 𝑡 → 𝑟 ∈ ( 𝑡 ∪ { ℎ } ) )
132 reseq2 ⊢ ( 𝑠 = 𝑟 → ( 𝑓 ↾ 𝑠 ) = ( 𝑓 ↾ 𝑟 ) )
133 132 eleq1d ⊢ ( 𝑠 = 𝑟 → ( ( 𝑓 ↾ 𝑠 ) ∈ MblFn ↔ ( 𝑓 ↾ 𝑟 ) ∈ MblFn ) )
134 133 rspccva ⊢ ( ( ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ∧ 𝑟 ∈ ( 𝑡 ∪ { ℎ } ) ) → ( 𝑓 ↾ 𝑟 ) ∈ MblFn )
135 131 134 sylan2 ⊢ ( ( ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ∧ 𝑟 ∈ 𝑡 ) → ( 𝑓 ↾ 𝑟 ) ∈ MblFn )
136 135 adantll ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( 𝑓 ↾ 𝑟 ) ∈ MblFn )
137 fresin ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( 𝑓 ↾ 𝑟 ) : ( 𝑎 ∩ 𝑟 ) ⟶ ℂ )
138 ismbfcn ⊢ ( ( 𝑓 ↾ 𝑟 ) : ( 𝑎 ∩ 𝑟 ) ⟶ ℂ → ( ( 𝑓 ↾ 𝑟 ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ) ) )
139 137 138 syl ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( ( 𝑓 ↾ 𝑟 ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ) ) )
140 139 biimpd ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( ( 𝑓 ↾ 𝑟 ) ∈ MblFn → ( ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ) ) )
141 140 ad2antrr ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ( 𝑓 ↾ 𝑟 ) ∈ MblFn → ( ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ) ) )
142 136 141 mpd ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ) )
143 142 simpld ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn )
144 130 143 eqeltrd ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn )
145 144 ralrimiva ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ∀ 𝑟 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn )
146 reseq2 ⊢ ( 𝑟 = 𝑠 → ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) )
147 146 eleq1d ⊢ ( 𝑟 = 𝑠 → ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn ↔ ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
148 147 cbvralvw ⊢ ( ∀ 𝑟 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn ↔ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn )
149 145 148 sylib ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn )
150 149 adantr ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn )
151 pm2.27 ⊢ ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
152 125 150 151 syl2anc ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ( ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
153 113 152 mpan9 ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn )
154 vsnid ⊢ ℎ ∈ { ℎ }
155 elun2 ⊢ ( ℎ ∈ { ℎ } → ℎ ∈ ( 𝑡 ∪ { ℎ } ) )
156 reseq2 ⊢ ( 𝑠 = ℎ → ( 𝑓 ↾ 𝑠 ) = ( 𝑓 ↾ ℎ ) )
157 156 eleq1d ⊢ ( 𝑠 = ℎ → ( ( 𝑓 ↾ 𝑠 ) ∈ MblFn ↔ ( 𝑓 ↾ ℎ ) ∈ MblFn ) )
158 157 rspcv ⊢ ( ℎ ∈ ( 𝑡 ∪ { ℎ } ) → ( ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn → ( 𝑓 ↾ ℎ ) ∈ MblFn ) )
159 154 155 158 mp2b ⊢ ( ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn → ( 𝑓 ↾ ℎ ) ∈ MblFn )
160 resco ⊢ ( ( ℜ ∘ 𝑓 ) ↾ ℎ ) = ( ℜ ∘ ( 𝑓 ↾ ℎ ) )
161 fresin ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( 𝑓 ↾ ℎ ) : ( 𝑎 ∩ ℎ ) ⟶ ℂ )
162 ismbfcn ⊢ ( ( 𝑓 ↾ ℎ ) : ( 𝑎 ∩ ℎ ) ⟶ ℂ → ( ( 𝑓 ↾ ℎ ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑓 ↾ ℎ ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑓 ↾ ℎ ) ) ∈ MblFn ) ) )
163 161 162 syl ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( ( 𝑓 ↾ ℎ ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑓 ↾ ℎ ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑓 ↾ ℎ ) ) ∈ MblFn ) ) )
164 163 simprbda ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ( 𝑓 ↾ ℎ ) ∈ MblFn ) → ( ℜ ∘ ( 𝑓 ↾ ℎ ) ) ∈ MblFn )
165 160 164 eqeltrid ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ( 𝑓 ↾ ℎ ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ℎ ) ∈ MblFn )
166 159 165 sylan2 ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ℎ ) ∈ MblFn )
167 166 ad2antrl ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ( ℜ ∘ 𝑓 ) ↾ ℎ ) ∈ MblFn )
168 uniun ⊢ ∪ ( 𝑡 ∪ { ℎ } ) = ( ∪ 𝑡 ∪ ∪ { ℎ } )
169 vex ⊢ ℎ ∈ V
170 169 unisn ⊢ ∪ { ℎ } = ℎ
171 170 uneq2i ⊢ ( ∪ 𝑡 ∪ ∪ { ℎ } ) = ( ∪ 𝑡 ∪ ℎ )
172 168 171 eqtri ⊢ ∪ ( 𝑡 ∪ { ℎ } ) = ( ∪ 𝑡 ∪ ℎ )
173 172 121 eqtr3id ⊢ ( ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 → ( ∪ 𝑡 ∪ ℎ ) = 𝑎 )
174 173 ad2antll ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ∪ 𝑡 ∪ ℎ ) = 𝑎 )
175 89 153 167 174 mbfres2 ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ℜ ∘ 𝑓 ) ∈ MblFn )
176 imf ⊢ ℑ : ℂ ⟶ ℝ
177 fco ⊢ ( ( ℑ : ℂ ⟶ ℝ ∧ 𝑓 : 𝑎 ⟶ ℂ ) → ( ℑ ∘ 𝑓 ) : 𝑎 ⟶ ℝ )
178 176 177 mpan ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( ℑ ∘ 𝑓 ) : 𝑎 ⟶ ℝ )
179 178 adantr ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ( ℑ ∘ 𝑓 ) : 𝑎 ⟶ ℝ )
180 179 ad2antrl ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ℑ ∘ 𝑓 ) : 𝑎 ⟶ ℝ )
181 imcncf ⊢ ℑ ∈ ( ℂ –cn→ ℝ )
182 181 elexi ⊢ ℑ ∈ V
183 182 92 coex ⊢ ( ℑ ∘ 𝑓 ) ∈ V
184 183 resex ⊢ ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ V
185 97 adantl ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ∪ 𝑡 = 𝑏 )
186 185 biantrud ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ↔ ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) ) )
187 feq123 ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ∧ ℂ = ℂ ) → ( 𝑔 : 𝑏 ⟶ ℂ ↔ ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ) )
188 100 187 mp3an3 ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( 𝑔 : 𝑏 ⟶ ℂ ↔ ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ) )
189 reseq1 ⊢ ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) → ( 𝑔 ↾ 𝑠 ) = ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) )
190 189 eleq1d ⊢ ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) → ( ( 𝑔 ↾ 𝑠 ) ∈ MblFn ↔ ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
191 190 adantr ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( 𝑔 ↾ 𝑠 ) ∈ MblFn ↔ ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
192 191 ralbidv ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ↔ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
193 188 192 anbi12d ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ↔ ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) ) )
194 186 193 bitr3d ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) ↔ ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) ) )
195 eleq1 ⊢ ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) → ( 𝑔 ∈ MblFn ↔ ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
196 195 adantr ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( 𝑔 ∈ MblFn ↔ ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
197 194 196 imbi12d ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ↔ ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) ) )
198 197 spc2gv ⊢ ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ V ∧ ∪ 𝑡 ∈ V ) → ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) → ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) ) )
199 184 95 198 mp2an ⊢ ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) → ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
200 fss ⊢ ( ( ℑ : ℂ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ℑ : ℂ ⟶ ℂ )
201 176 114 200 mp2an ⊢ ℑ : ℂ ⟶ ℂ
202 fco ⊢ ( ( ℑ : ℂ ⟶ ℂ ∧ 𝑓 : 𝑎 ⟶ ℂ ) → ( ℑ ∘ 𝑓 ) : 𝑎 ⟶ ℂ )
203 201 202 mpan ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( ℑ ∘ 𝑓 ) : 𝑎 ⟶ ℂ )
204 fssres ⊢ ( ( ( ℑ ∘ 𝑓 ) : 𝑎 ⟶ ℂ ∧ ∪ 𝑡 ⊆ 𝑎 ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ )
205 203 122 204 syl2an ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ )
206 205 adantlr ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ )
207 126 resabs1d ⊢ ( 𝑟 ∈ 𝑡 → ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ( ℑ ∘ 𝑓 ) ↾ 𝑟 ) )
208 resco ⊢ ( ( ℑ ∘ 𝑓 ) ↾ 𝑟 ) = ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) )
209 207 208 eqtrdi ⊢ ( 𝑟 ∈ 𝑡 → ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) )
210 209 adantl ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) )
211 142 simprd ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn )
212 210 211 eqeltrd ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn )
213 212 ralrimiva ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ∀ 𝑟 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn )
214 reseq2 ⊢ ( 𝑟 = 𝑠 → ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) )
215 214 eleq1d ⊢ ( 𝑟 = 𝑠 → ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn ↔ ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
216 215 cbvralvw ⊢ ( ∀ 𝑟 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn ↔ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn )
217 213 216 sylib ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn )
218 217 adantr ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn )
219 pm2.27 ⊢ ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
220 206 218 219 syl2anc ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ( ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
221 199 220 mpan9 ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn )
222 resco ⊢ ( ( ℑ ∘ 𝑓 ) ↾ ℎ ) = ( ℑ ∘ ( 𝑓 ↾ ℎ ) )
223 163 simplbda ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ( 𝑓 ↾ ℎ ) ∈ MblFn ) → ( ℑ ∘ ( 𝑓 ↾ ℎ ) ) ∈ MblFn )
224 222 223 eqeltrid ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ( 𝑓 ↾ ℎ ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ℎ ) ∈ MblFn )
225 159 224 sylan2 ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ℎ ) ∈ MblFn )
226 225 ad2antrl ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ( ℑ ∘ 𝑓 ) ↾ ℎ ) ∈ MblFn )
227 180 221 226 174 mbfres2 ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ℑ ∘ 𝑓 ) ∈ MblFn )
228 ismbfcn ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( 𝑓 ∈ MblFn ↔ ( ( ℜ ∘ 𝑓 ) ∈ MblFn ∧ ( ℑ ∘ 𝑓 ) ∈ MblFn ) ) )
229 228 adantr ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ( 𝑓 ∈ MblFn ↔ ( ( ℜ ∘ 𝑓 ) ∈ MblFn ∧ ( ℑ ∘ 𝑓 ) ∈ MblFn ) ) )
230 229 ad2antrl ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( 𝑓 ∈ MblFn ↔ ( ( ℜ ∘ 𝑓 ) ∈ MblFn ∧ ( ℑ ∘ 𝑓 ) ∈ MblFn ) ) )
231 175 227 230 mpbir2and ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → 𝑓 ∈ MblFn )
232 231 ex ⊢ ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) → ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → 𝑓 ∈ MblFn ) )
233 232 alrimivv ⊢ ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) → ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → 𝑓 ∈ MblFn ) )
234 233 a1i ⊢ ( 𝑡 ∈ Fin → ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) → ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → 𝑓 ∈ MblFn ) ) )
235 35 58 65 72 84 234 findcard2 ⊢ ( 𝑆 ∈ Fin → ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝑎 ) → 𝑓 ∈ MblFn ) )
236 2sp ⊢ ( ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝑎 ) → 𝑓 ∈ MblFn ) → ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝑎 ) → 𝑓 ∈ MblFn ) )
237 2 235 236 3syl ⊢ ( 𝜑 → ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝑎 ) → 𝑓 ∈ MblFn ) )
238 16 25 237 vtocl2g ⊢ ( ( 𝐴 ∈ V ∧ 𝐹 ∈ V ) → ( 𝜑 → ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝐹 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝐴 ) → 𝐹 ∈ MblFn ) ) )
239 10 238 mpcom ⊢ ( 𝜑 → ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝐹 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝐴 ) → 𝐹 ∈ MblFn ) )
240 4 239 mpan2d ⊢ ( 𝜑 → ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝐹 ↾ 𝑠 ) ∈ MblFn ) → 𝐹 ∈ MblFn ) )
241 1 3 240 mp2and ⊢ ( 𝜑 → 𝐹 ∈ MblFn )