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 bilani ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ∪ 𝑡 = 𝑏 )
98 97 biantrud ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ↔ ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) ) )
99 eqid ⊢ ℂ = ℂ
100 feq123 ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ∧ ℂ = ℂ ) → ( 𝑔 : 𝑏 ⟶ ℂ ↔ ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ) )
101 99 100 mp3an3 ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( 𝑔 : 𝑏 ⟶ ℂ ↔ ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ) )
102 reseq1 ⊢ ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) → ( 𝑔 ↾ 𝑠 ) = ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) )
103 102 eleq1d ⊢ ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) → ( ( 𝑔 ↾ 𝑠 ) ∈ MblFn ↔ ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
104 103 adantr ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( 𝑔 ↾ 𝑠 ) ∈ MblFn ↔ ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
105 104 ralbidv ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ↔ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
106 101 105 anbi12d ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ↔ ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) ) )
107 98 106 bitr3d ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) ↔ ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) ) )
108 eleq1 ⊢ ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) → ( 𝑔 ∈ MblFn ↔ ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
109 108 adantr ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( 𝑔 ∈ MblFn ↔ ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
110 107 109 imbi12d ⊢ ( ( 𝑔 = ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ↔ ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) ) )
111 110 spc2gv ⊢ ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ V ∧ ∪ 𝑡 ∈ V ) → ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) → ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) ) )
112 94 95 111 mp2an ⊢ ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) → ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
113 ax-resscn ⊢ ℝ ⊆ ℂ
114 fss ⊢ ( ( ℜ : ℂ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ℜ : ℂ ⟶ ℂ )
115 85 113 114 mp2an ⊢ ℜ : ℂ ⟶ ℂ
116 fco ⊢ ( ( ℜ : ℂ ⟶ ℂ ∧ 𝑓 : 𝑎 ⟶ ℂ ) → ( ℜ ∘ 𝑓 ) : 𝑎 ⟶ ℂ )
117 115 116 mpan ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( ℜ ∘ 𝑓 ) : 𝑎 ⟶ ℂ )
118 ssun1 ⊢ 𝑡 ⊆ ( 𝑡 ∪ { ℎ } )
119 118 unissi ⊢ ∪ 𝑡 ⊆ ∪ ( 𝑡 ∪ { ℎ } )
120 id ⊢ ( ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 → ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 )
121 119 120 sseqtrid ⊢ ( ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 → ∪ 𝑡 ⊆ 𝑎 )
122 fssres ⊢ ( ( ( ℜ ∘ 𝑓 ) : 𝑎 ⟶ ℂ ∧ ∪ 𝑡 ⊆ 𝑎 ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ )
123 117 121 122 syl2an ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ )
124 123 adantlr ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ )
125 elssuni ⊢ ( 𝑟 ∈ 𝑡 → 𝑟 ⊆ ∪ 𝑡 )
126 125 resabs1d ⊢ ( 𝑟 ∈ 𝑡 → ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ( ℜ ∘ 𝑓 ) ↾ 𝑟 ) )
127 resco ⊢ ( ( ℜ ∘ 𝑓 ) ↾ 𝑟 ) = ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) )
128 126 127 eqtrdi ⊢ ( 𝑟 ∈ 𝑡 → ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) )
129 128 adantl ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) )
130 elun1 ⊢ ( 𝑟 ∈ 𝑡 → 𝑟 ∈ ( 𝑡 ∪ { ℎ } ) )
131 reseq2 ⊢ ( 𝑠 = 𝑟 → ( 𝑓 ↾ 𝑠 ) = ( 𝑓 ↾ 𝑟 ) )
132 131 eleq1d ⊢ ( 𝑠 = 𝑟 → ( ( 𝑓 ↾ 𝑠 ) ∈ MblFn ↔ ( 𝑓 ↾ 𝑟 ) ∈ MblFn ) )
133 132 rspccva ⊢ ( ( ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ∧ 𝑟 ∈ ( 𝑡 ∪ { ℎ } ) ) → ( 𝑓 ↾ 𝑟 ) ∈ MblFn )
134 130 133 sylan2 ⊢ ( ( ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ∧ 𝑟 ∈ 𝑡 ) → ( 𝑓 ↾ 𝑟 ) ∈ MblFn )
135 134 adantll ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( 𝑓 ↾ 𝑟 ) ∈ MblFn )
136 fresin ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( 𝑓 ↾ 𝑟 ) : ( 𝑎 ∩ 𝑟 ) ⟶ ℂ )
137 ismbfcn ⊢ ( ( 𝑓 ↾ 𝑟 ) : ( 𝑎 ∩ 𝑟 ) ⟶ ℂ → ( ( 𝑓 ↾ 𝑟 ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ) ) )
138 136 137 syl ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( ( 𝑓 ↾ 𝑟 ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ) ) )
139 138 biimpd ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( ( 𝑓 ↾ 𝑟 ) ∈ MblFn → ( ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ) ) )
140 139 ad2antrr ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ( 𝑓 ↾ 𝑟 ) ∈ MblFn → ( ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ) ) )
141 135 140 mpd ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn ) )
142 141 simpld ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ℜ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn )
143 129 142 eqeltrd ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn )
144 143 ralrimiva ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ∀ 𝑟 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn )
145 reseq2 ⊢ ( 𝑟 = 𝑠 → ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) )
146 145 eleq1d ⊢ ( 𝑟 = 𝑠 → ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn ↔ ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
147 146 cbvralvw ⊢ ( ∀ 𝑟 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn ↔ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn )
148 144 147 sylib ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn )
149 148 adantr ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn )
150 pm2.27 ⊢ ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
151 124 149 150 syl2anc ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ( ( ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
152 112 151 mpan9 ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ( ℜ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn )
153 vsnid ⊢ ℎ ∈ { ℎ }
154 elun2 ⊢ ( ℎ ∈ { ℎ } → ℎ ∈ ( 𝑡 ∪ { ℎ } ) )
155 reseq2 ⊢ ( 𝑠 = ℎ → ( 𝑓 ↾ 𝑠 ) = ( 𝑓 ↾ ℎ ) )
156 155 eleq1d ⊢ ( 𝑠 = ℎ → ( ( 𝑓 ↾ 𝑠 ) ∈ MblFn ↔ ( 𝑓 ↾ ℎ ) ∈ MblFn ) )
157 156 rspcv ⊢ ( ℎ ∈ ( 𝑡 ∪ { ℎ } ) → ( ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn → ( 𝑓 ↾ ℎ ) ∈ MblFn ) )
158 153 154 157 mp2b ⊢ ( ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn → ( 𝑓 ↾ ℎ ) ∈ MblFn )
159 resco ⊢ ( ( ℜ ∘ 𝑓 ) ↾ ℎ ) = ( ℜ ∘ ( 𝑓 ↾ ℎ ) )
160 fresin ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( 𝑓 ↾ ℎ ) : ( 𝑎 ∩ ℎ ) ⟶ ℂ )
161 ismbfcn ⊢ ( ( 𝑓 ↾ ℎ ) : ( 𝑎 ∩ ℎ ) ⟶ ℂ → ( ( 𝑓 ↾ ℎ ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑓 ↾ ℎ ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑓 ↾ ℎ ) ) ∈ MblFn ) ) )
162 160 161 syl ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( ( 𝑓 ↾ ℎ ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑓 ↾ ℎ ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑓 ↾ ℎ ) ) ∈ MblFn ) ) )
163 162 simprbda ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ( 𝑓 ↾ ℎ ) ∈ MblFn ) → ( ℜ ∘ ( 𝑓 ↾ ℎ ) ) ∈ MblFn )
164 159 163 eqeltrid ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ( 𝑓 ↾ ℎ ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ℎ ) ∈ MblFn )
165 158 164 sylan2 ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ( ( ℜ ∘ 𝑓 ) ↾ ℎ ) ∈ MblFn )
166 165 ad2antrl ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ( ℜ ∘ 𝑓 ) ↾ ℎ ) ∈ MblFn )
167 uniun ⊢ ∪ ( 𝑡 ∪ { ℎ } ) = ( ∪ 𝑡 ∪ ∪ { ℎ } )
168 unisnv ⊢ ∪ { ℎ } = ℎ
169 168 uneq2i ⊢ ( ∪ 𝑡 ∪ ∪ { ℎ } ) = ( ∪ 𝑡 ∪ ℎ )
170 167 169 eqtri ⊢ ∪ ( 𝑡 ∪ { ℎ } ) = ( ∪ 𝑡 ∪ ℎ )
171 170 120 eqtr3id ⊢ ( ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 → ( ∪ 𝑡 ∪ ℎ ) = 𝑎 )
172 171 ad2antll ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ∪ 𝑡 ∪ ℎ ) = 𝑎 )
173 89 152 166 172 mbfres2 ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ℜ ∘ 𝑓 ) ∈ MblFn )
174 imf ⊢ ℑ : ℂ ⟶ ℝ
175 fco ⊢ ( ( ℑ : ℂ ⟶ ℝ ∧ 𝑓 : 𝑎 ⟶ ℂ ) → ( ℑ ∘ 𝑓 ) : 𝑎 ⟶ ℝ )
176 174 175 mpan ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( ℑ ∘ 𝑓 ) : 𝑎 ⟶ ℝ )
177 176 adantr ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ( ℑ ∘ 𝑓 ) : 𝑎 ⟶ ℝ )
178 177 ad2antrl ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ℑ ∘ 𝑓 ) : 𝑎 ⟶ ℝ )
179 imcncf ⊢ ℑ ∈ ( ℂ –cn→ ℝ )
180 179 elexi ⊢ ℑ ∈ V
181 180 92 coex ⊢ ( ℑ ∘ 𝑓 ) ∈ V
182 181 resex ⊢ ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ V
183 96 bilani ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ∪ 𝑡 = 𝑏 )
184 183 biantrud ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ↔ ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) ) )
185 feq123 ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ∧ ℂ = ℂ ) → ( 𝑔 : 𝑏 ⟶ ℂ ↔ ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ) )
186 99 185 mp3an3 ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( 𝑔 : 𝑏 ⟶ ℂ ↔ ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ) )
187 reseq1 ⊢ ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) → ( 𝑔 ↾ 𝑠 ) = ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) )
188 187 eleq1d ⊢ ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) → ( ( 𝑔 ↾ 𝑠 ) ∈ MblFn ↔ ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
189 188 adantr ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( 𝑔 ↾ 𝑠 ) ∈ MblFn ↔ ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
190 189 ralbidv ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ↔ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
191 186 190 anbi12d ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ↔ ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) ) )
192 184 191 bitr3d ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) ↔ ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) ) )
193 eleq1 ⊢ ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) → ( 𝑔 ∈ MblFn ↔ ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
194 193 adantr ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( 𝑔 ∈ MblFn ↔ ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
195 192 194 imbi12d ⊢ ( ( 𝑔 = ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∧ 𝑏 = ∪ 𝑡 ) → ( ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ↔ ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) ) )
196 195 spc2gv ⊢ ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ V ∧ ∪ 𝑡 ∈ V ) → ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) → ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) ) )
197 182 95 196 mp2an ⊢ ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) → ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
198 fss ⊢ ( ( ℑ : ℂ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ℑ : ℂ ⟶ ℂ )
199 174 113 198 mp2an ⊢ ℑ : ℂ ⟶ ℂ
200 fco ⊢ ( ( ℑ : ℂ ⟶ ℂ ∧ 𝑓 : 𝑎 ⟶ ℂ ) → ( ℑ ∘ 𝑓 ) : 𝑎 ⟶ ℂ )
201 199 200 mpan ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( ℑ ∘ 𝑓 ) : 𝑎 ⟶ ℂ )
202 fssres ⊢ ( ( ( ℑ ∘ 𝑓 ) : 𝑎 ⟶ ℂ ∧ ∪ 𝑡 ⊆ 𝑎 ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ )
203 201 121 202 syl2an ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ )
204 203 adantlr ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ )
205 125 resabs1d ⊢ ( 𝑟 ∈ 𝑡 → ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ( ℑ ∘ 𝑓 ) ↾ 𝑟 ) )
206 resco ⊢ ( ( ℑ ∘ 𝑓 ) ↾ 𝑟 ) = ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) )
207 205 206 eqtrdi ⊢ ( 𝑟 ∈ 𝑡 → ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) )
208 207 adantl ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) )
209 141 simprd ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ℑ ∘ ( 𝑓 ↾ 𝑟 ) ) ∈ MblFn )
210 208 209 eqeltrd ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ 𝑟 ∈ 𝑡 ) → ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn )
211 210 ralrimiva ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ∀ 𝑟 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn )
212 reseq2 ⊢ ( 𝑟 = 𝑠 → ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) = ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) )
213 212 eleq1d ⊢ ( 𝑟 = 𝑠 → ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn ↔ ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) )
214 213 cbvralvw ⊢ ( ∀ 𝑟 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑟 ) ∈ MblFn ↔ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn )
215 211 214 sylib ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn )
216 215 adantr ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn )
217 pm2.27 ⊢ ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
218 204 216 217 syl2anc ⊢ ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → ( ( ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) : ∪ 𝑡 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ↾ 𝑠 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn ) )
219 197 218 mpan9 ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ( ℑ ∘ 𝑓 ) ↾ ∪ 𝑡 ) ∈ MblFn )
220 resco ⊢ ( ( ℑ ∘ 𝑓 ) ↾ ℎ ) = ( ℑ ∘ ( 𝑓 ↾ ℎ ) )
221 162 simplbda ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ( 𝑓 ↾ ℎ ) ∈ MblFn ) → ( ℑ ∘ ( 𝑓 ↾ ℎ ) ) ∈ MblFn )
222 220 221 eqeltrid ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ( 𝑓 ↾ ℎ ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ℎ ) ∈ MblFn )
223 158 222 sylan2 ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ( ( ℑ ∘ 𝑓 ) ↾ ℎ ) ∈ MblFn )
224 223 ad2antrl ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ( ℑ ∘ 𝑓 ) ↾ ℎ ) ∈ MblFn )
225 178 219 224 172 mbfres2 ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( ℑ ∘ 𝑓 ) ∈ MblFn )
226 ismbfcn ⊢ ( 𝑓 : 𝑎 ⟶ ℂ → ( 𝑓 ∈ MblFn ↔ ( ( ℜ ∘ 𝑓 ) ∈ MblFn ∧ ( ℑ ∘ 𝑓 ) ∈ MblFn ) ) )
227 226 adantr ⊢ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) → ( 𝑓 ∈ MblFn ↔ ( ( ℜ ∘ 𝑓 ) ∈ MblFn ∧ ( ℑ ∘ 𝑓 ) ∈ MblFn ) ) )
228 227 ad2antrl ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → ( 𝑓 ∈ MblFn ↔ ( ( ℜ ∘ 𝑓 ) ∈ MblFn ∧ ( ℑ ∘ 𝑓 ) ∈ MblFn ) ) )
229 173 225 228 mpbir2and ⊢ ( ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) ∧ ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) ) → 𝑓 ∈ MblFn )
230 229 ex ⊢ ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) → ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → 𝑓 ∈ MblFn ) )
231 230 alrimivv ⊢ ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) → ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → 𝑓 ∈ MblFn ) )
232 231 a1i ⊢ ( 𝑡 ∈ Fin → ( ∀ 𝑔 ∀ 𝑏 ( ( ( 𝑔 : 𝑏 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑔 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑡 = 𝑏 ) → 𝑔 ∈ MblFn ) → ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ ( 𝑡 ∪ { ℎ } ) ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ ( 𝑡 ∪ { ℎ } ) = 𝑎 ) → 𝑓 ∈ MblFn ) ) )
233 35 58 65 72 84 232 findcard2 ⊢ ( 𝑆 ∈ Fin → ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝑎 ) → 𝑓 ∈ MblFn ) )
234 2sp ⊢ ( ∀ 𝑓 ∀ 𝑎 ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝑎 ) → 𝑓 ∈ MblFn ) → ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝑎 ) → 𝑓 ∈ MblFn ) )
235 2 233 234 3syl ⊢ ( 𝜑 → ( ( ( 𝑓 : 𝑎 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝑓 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝑎 ) → 𝑓 ∈ MblFn ) )
236 16 25 235 vtocl2g ⊢ ( ( 𝐴 ∈ V ∧ 𝐹 ∈ V ) → ( 𝜑 → ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝐹 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝐴 ) → 𝐹 ∈ MblFn ) ) )
237 10 236 mpcom ⊢ ( 𝜑 → ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝐹 ↾ 𝑠 ) ∈ MblFn ) ∧ ∪ 𝑆 = 𝐴 ) → 𝐹 ∈ MblFn ) )
238 4 237 mpan2d ⊢ ( 𝜑 → ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑠 ∈ 𝑆 ( 𝐹 ↾ 𝑠 ) ∈ MblFn ) → 𝐹 ∈ MblFn ) )
239 1 3 238 mp2and ⊢ ( 𝜑 → 𝐹 ∈ MblFn )