| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mbfresfi.1 | . 2
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) | 
| 2 |  | mbfresfi.3 | . 2
⊢ (𝜑 → ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) | 
| 3 |  | mbfresfi.4 | . . 3
⊢ (𝜑 → ∪ 𝑆 =
𝐴) | 
| 4 |  | mbfresfi.2 | . . . . . . 7
⊢ (𝜑 → 𝑆 ∈ Fin) | 
| 5 | 4 | uniexd 7762 | . . . . . 6
⊢ (𝜑 → ∪ 𝑆
∈ V) | 
| 6 | 3, 5 | eqeltrrd 2842 | . . . . 5
⊢ (𝜑 → 𝐴 ∈ V) | 
| 7 |  | fex 7246 | . . . . . . 7
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ∈ V) → 𝐹 ∈ V) | 
| 8 | 7 | ex 412 | . . . . . 6
⊢ (𝐹:𝐴⟶ℂ → (𝐴 ∈ V → 𝐹 ∈ V)) | 
| 9 | 1, 8 | syl 17 | . . . . 5
⊢ (𝜑 → (𝐴 ∈ V → 𝐹 ∈ V)) | 
| 10 | 6, 9 | jcai 516 | . . . 4
⊢ (𝜑 → (𝐴 ∈ V ∧ 𝐹 ∈ V)) | 
| 11 |  | feq2 6717 | . . . . . . . . 9
⊢ (𝑎 = 𝐴 → (𝑓:𝑎⟶ℂ ↔ 𝑓:𝐴⟶ℂ)) | 
| 12 | 11 | anbi1d 631 | . . . . . . . 8
⊢ (𝑎 = 𝐴 → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ↔ (𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn))) | 
| 13 |  | eqeq2 2749 | . . . . . . . 8
⊢ (𝑎 = 𝐴 → (∪ 𝑆 = 𝑎 ↔ ∪ 𝑆 = 𝐴)) | 
| 14 | 12, 13 | anbi12d 632 | . . . . . . 7
⊢ (𝑎 = 𝐴 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) ↔ ((𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴))) | 
| 15 | 14 | imbi1d 341 | . . . . . 6
⊢ (𝑎 = 𝐴 → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝑓 ∈
MblFn))) | 
| 16 | 15 | imbi2d 340 | . . . . 5
⊢ (𝑎 = 𝐴 → ((𝜑 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈ MblFn)) ↔ (𝜑 → (((𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝑓 ∈
MblFn)))) | 
| 17 |  | feq1 6716 | . . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑓:𝐴⟶ℂ ↔ 𝐹:𝐴⟶ℂ)) | 
| 18 |  | reseq1 5991 | . . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → (𝑓 ↾ 𝑠) = (𝐹 ↾ 𝑠)) | 
| 19 | 18 | eleq1d 2826 | . . . . . . . . . 10
⊢ (𝑓 = 𝐹 → ((𝑓 ↾ 𝑠) ∈ MblFn ↔ (𝐹 ↾ 𝑠) ∈ MblFn)) | 
| 20 | 19 | ralbidv 3178 | . . . . . . . . 9
⊢ (𝑓 = 𝐹 → (∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn ↔ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn)) | 
| 21 | 17, 20 | anbi12d 632 | . . . . . . . 8
⊢ (𝑓 = 𝐹 → ((𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn))) | 
| 22 | 21 | anbi1d 631 | . . . . . . 7
⊢ (𝑓 = 𝐹 → (((𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) ↔ ((𝐹:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴))) | 
| 23 |  | eleq1 2829 | . . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓 ∈ MblFn ↔ 𝐹 ∈ MblFn)) | 
| 24 | 22, 23 | imbi12d 344 | . . . . . 6
⊢ (𝑓 = 𝐹 → ((((𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝑓 ∈ MblFn) ↔ (((𝐹:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝐹 ∈ MblFn))) | 
| 25 | 24 | imbi2d 340 | . . . . 5
⊢ (𝑓 = 𝐹 → ((𝜑 → (((𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝑓 ∈ MblFn)) ↔ (𝜑 → (((𝐹:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝐹 ∈ MblFn)))) | 
| 26 |  | rzal 4509 | . . . . . . . . . . . 12
⊢ (𝑟 = ∅ → ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) | 
| 27 | 26 | biantrud 531 | . . . . . . . . . . 11
⊢ (𝑟 = ∅ → (𝑓:𝑎⟶ℂ ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn))) | 
| 28 | 27 | bicomd 223 | . . . . . . . . . 10
⊢ (𝑟 = ∅ → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ↔ 𝑓:𝑎⟶ℂ)) | 
| 29 |  | unieq 4918 | . . . . . . . . . . . 12
⊢ (𝑟 = ∅ → ∪ 𝑟 =
∪ ∅) | 
| 30 |  | uni0 4935 | . . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ | 
| 31 | 29, 30 | eqtrdi 2793 | . . . . . . . . . . 11
⊢ (𝑟 = ∅ → ∪ 𝑟 =
∅) | 
| 32 | 31 | eqeq1d 2739 | . . . . . . . . . 10
⊢ (𝑟 = ∅ → (∪ 𝑟 =
𝑎 ↔ ∅ = 𝑎)) | 
| 33 | 28, 32 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑟 = ∅ → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) ↔ (𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎))) | 
| 34 | 33 | imbi1d 341 | . . . . . . . 8
⊢ (𝑟 = ∅ → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔ ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn))) | 
| 35 | 34 | 2albidv 1923 | . . . . . . 7
⊢ (𝑟 = ∅ → (∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔
∀𝑓∀𝑎((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn))) | 
| 36 |  | raleq 3323 | . . . . . . . . . . . 12
⊢ (𝑟 = 𝑡 → (∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn ↔ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn)) | 
| 37 | 36 | anbi2d 630 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑡 → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn))) | 
| 38 |  | unieq 4918 | . . . . . . . . . . . 12
⊢ (𝑟 = 𝑡 → ∪ 𝑟 = ∪
𝑡) | 
| 39 | 38 | eqeq1d 2739 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑡 → (∪ 𝑟 = 𝑎 ↔ ∪ 𝑡 = 𝑎)) | 
| 40 | 37, 39 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑟 = 𝑡 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) ↔ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑎))) | 
| 41 | 40 | imbi1d 341 | . . . . . . . . 9
⊢ (𝑟 = 𝑡 → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑎) → 𝑓 ∈
MblFn))) | 
| 42 | 41 | 2albidv 1923 | . . . . . . . 8
⊢ (𝑟 = 𝑡 → (∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔
∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑎) → 𝑓 ∈
MblFn))) | 
| 43 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → 𝑓 = 𝑔) | 
| 44 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → 𝑎 = 𝑏) | 
| 45 | 43, 44 | feq12d 6724 | . . . . . . . . . . . 12
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → (𝑓:𝑎⟶ℂ ↔ 𝑔:𝑏⟶ℂ)) | 
| 46 |  | reseq1 5991 | . . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑔 → (𝑓 ↾ 𝑠) = (𝑔 ↾ 𝑠)) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → (𝑓 ↾ 𝑠) = (𝑔 ↾ 𝑠)) | 
| 48 | 47 | eleq1d 2826 | . . . . . . . . . . . . 13
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → ((𝑓 ↾ 𝑠) ∈ MblFn ↔ (𝑔 ↾ 𝑠) ∈ MblFn)) | 
| 49 | 48 | ralbidv 3178 | . . . . . . . . . . . 12
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → (∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn ↔ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn)) | 
| 50 | 45, 49 | anbi12d 632 | . . . . . . . . . . 11
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn) ↔ (𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn))) | 
| 51 |  | eqeq2 2749 | . . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → (∪ 𝑡 = 𝑎 ↔ ∪ 𝑡 = 𝑏)) | 
| 52 | 51 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → (∪ 𝑡 = 𝑎 ↔ ∪ 𝑡 = 𝑏)) | 
| 53 | 50, 52 | anbi12d 632 | . . . . . . . . . 10
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑎) ↔ ((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏))) | 
| 54 |  | eleq1 2829 | . . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → (𝑓 ∈ MblFn ↔ 𝑔 ∈ MblFn)) | 
| 55 | 54 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → (𝑓 ∈ MblFn ↔ 𝑔 ∈ MblFn)) | 
| 56 | 53, 55 | imbi12d 344 | . . . . . . . . 9
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈
MblFn))) | 
| 57 | 56 | cbval2vw 2039 | . . . . . . . 8
⊢
(∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑎) → 𝑓 ∈ MblFn) ↔
∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn)) | 
| 58 | 42, 57 | bitrdi 287 | . . . . . . 7
⊢ (𝑟 = 𝑡 → (∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔
∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈
MblFn))) | 
| 59 |  | raleq 3323 | . . . . . . . . . . 11
⊢ (𝑟 = (𝑡 ∪ {ℎ}) → (∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn ↔ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn)) | 
| 60 | 59 | anbi2d 630 | . . . . . . . . . 10
⊢ (𝑟 = (𝑡 ∪ {ℎ}) → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn))) | 
| 61 |  | unieq 4918 | . . . . . . . . . . 11
⊢ (𝑟 = (𝑡 ∪ {ℎ}) → ∪ 𝑟 = ∪
(𝑡 ∪ {ℎ})) | 
| 62 | 61 | eqeq1d 2739 | . . . . . . . . . 10
⊢ (𝑟 = (𝑡 ∪ {ℎ}) → (∪ 𝑟 = 𝑎 ↔ ∪ (𝑡 ∪ {ℎ}) = 𝑎)) | 
| 63 | 60, 62 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑟 = (𝑡 ∪ {ℎ}) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) ↔ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎))) | 
| 64 | 63 | imbi1d 341 | . . . . . . . 8
⊢ (𝑟 = (𝑡 ∪ {ℎ}) → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → 𝑓 ∈ MblFn))) | 
| 65 | 64 | 2albidv 1923 | . . . . . . 7
⊢ (𝑟 = (𝑡 ∪ {ℎ}) → (∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔
∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → 𝑓 ∈ MblFn))) | 
| 66 |  | raleq 3323 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑆 → (∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn ↔ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn)) | 
| 67 | 66 | anbi2d 630 | . . . . . . . . . 10
⊢ (𝑟 = 𝑆 → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn))) | 
| 68 |  | unieq 4918 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑆 → ∪ 𝑟 = ∪
𝑆) | 
| 69 | 68 | eqeq1d 2739 | . . . . . . . . . 10
⊢ (𝑟 = 𝑆 → (∪ 𝑟 = 𝑎 ↔ ∪ 𝑆 = 𝑎)) | 
| 70 | 67, 69 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑟 = 𝑆 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) ↔ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎))) | 
| 71 | 70 | imbi1d 341 | . . . . . . . 8
⊢ (𝑟 = 𝑆 → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈
MblFn))) | 
| 72 | 71 | 2albidv 1923 | . . . . . . 7
⊢ (𝑟 = 𝑆 → (∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔
∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈
MblFn))) | 
| 73 |  | frel 6741 | . . . . . . . . . 10
⊢ (𝑓:𝑎⟶ℂ → Rel 𝑓) | 
| 74 | 73 | adantr 480 | . . . . . . . . 9
⊢ ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → Rel 𝑓) | 
| 75 |  | fdm 6745 | . . . . . . . . . 10
⊢ (𝑓:𝑎⟶ℂ → dom 𝑓 = 𝑎) | 
| 76 |  | eqcom 2744 | . . . . . . . . . . 11
⊢ (∅
= 𝑎 ↔ 𝑎 = ∅) | 
| 77 | 76 | biimpi 216 | . . . . . . . . . 10
⊢ (∅
= 𝑎 → 𝑎 = ∅) | 
| 78 | 75, 77 | sylan9eq 2797 | . . . . . . . . 9
⊢ ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → dom 𝑓 = ∅) | 
| 79 |  | reldm0 5938 | . . . . . . . . . . 11
⊢ (Rel
𝑓 → (𝑓 = ∅ ↔ dom 𝑓 = ∅)) | 
| 80 | 79 | biimpar 477 | . . . . . . . . . 10
⊢ ((Rel
𝑓 ∧ dom 𝑓 = ∅) → 𝑓 = ∅) | 
| 81 |  | mbf0 25669 | . . . . . . . . . 10
⊢ ∅
∈ MblFn | 
| 82 | 80, 81 | eqeltrdi 2849 | . . . . . . . . 9
⊢ ((Rel
𝑓 ∧ dom 𝑓 = ∅) → 𝑓 ∈ MblFn) | 
| 83 | 74, 78, 82 | syl2anc 584 | . . . . . . . 8
⊢ ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn) | 
| 84 | 83 | gen2 1796 | . . . . . . 7
⊢
∀𝑓∀𝑎((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn) | 
| 85 |  | ref 15151 | . . . . . . . . . . . . . . 15
⊢
ℜ:ℂ⟶ℝ | 
| 86 |  | fco 6760 | . . . . . . . . . . . . . . 15
⊢
((ℜ:ℂ⟶ℝ ∧ 𝑓:𝑎⟶ℂ) → (ℜ ∘ 𝑓):𝑎⟶ℝ) | 
| 87 | 85, 86 | mpan 690 | . . . . . . . . . . . . . 14
⊢ (𝑓:𝑎⟶ℂ → (ℜ ∘ 𝑓):𝑎⟶ℝ) | 
| 88 | 87 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → (ℜ ∘ 𝑓):𝑎⟶ℝ) | 
| 89 | 88 | ad2antrl 728 | . . . . . . . . . . . 12
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → (ℜ ∘ 𝑓):𝑎⟶ℝ) | 
| 90 |  | recncf 24928 | . . . . . . . . . . . . . . . . 17
⊢ ℜ
∈ (ℂ–cn→ℝ) | 
| 91 | 90 | elexi 3503 | . . . . . . . . . . . . . . . 16
⊢ ℜ
∈ V | 
| 92 |  | vex 3484 | . . . . . . . . . . . . . . . 16
⊢ 𝑓 ∈ V | 
| 93 | 91, 92 | coex 7952 | . . . . . . . . . . . . . . 15
⊢ (ℜ
∘ 𝑓) ∈
V | 
| 94 | 93 | resex 6047 | . . . . . . . . . . . . . 14
⊢ ((ℜ
∘ 𝑓) ↾ ∪ 𝑡)
∈ V | 
| 95 |  | vuniex 7759 | . . . . . . . . . . . . . 14
⊢ ∪ 𝑡
∈ V | 
| 96 |  | eqcom 2744 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = ∪
𝑡 ↔ ∪ 𝑡 =
𝑏) | 
| 97 | 96 | biimpi 216 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = ∪
𝑡 → ∪ 𝑡 =
𝑏) | 
| 98 | 97 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ∪ 𝑡 = 𝑏) | 
| 99 | 98 | biantrud 531 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ↔ ((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏))) | 
| 100 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . 19
⊢ ℂ =
ℂ | 
| 101 |  | feq123 6726 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡
∧ ℂ = ℂ) → (𝑔:𝑏⟶ℂ ↔ ((ℜ ∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ)) | 
| 102 | 100, 101 | mp3an3 1452 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (𝑔:𝑏⟶ℂ ↔ ((ℜ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ)) | 
| 103 |  | reseq1 5991 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
→ (𝑔 ↾ 𝑠) = (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠)) | 
| 104 | 103 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
→ ((𝑔 ↾ 𝑠) ∈ MblFn ↔ (((ℜ
∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn)) | 
| 105 | 104 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((𝑔 ↾ 𝑠) ∈ MblFn ↔ (((ℜ
∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn)) | 
| 106 | 105 | ralbidv 3178 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (∀𝑠 ∈
𝑡 (𝑔 ↾ 𝑠) ∈ MblFn ↔ ∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠) ∈ MblFn)) | 
| 107 | 102, 106 | anbi12d 632 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ↔ (((ℜ ∘
𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn))) | 
| 108 | 99, 107 | bitr3d 281 | . . . . . . . . . . . . . . . 16
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) ↔ (((ℜ ∘
𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn))) | 
| 109 |  | eleq1 2829 | . . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
→ (𝑔 ∈ MblFn
↔ ((ℜ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn)) | 
| 110 | 109 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (𝑔 ∈ MblFn
↔ ((ℜ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn)) | 
| 111 | 108, 110 | imbi12d 344 | . . . . . . . . . . . . . . 15
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ↔ ((((ℜ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℜ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn))) | 
| 112 | 111 | spc2gv 3600 | . . . . . . . . . . . . . 14
⊢
((((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ∈ V ∧ ∪ 𝑡
∈ V) → (∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) → ((((ℜ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℜ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn))) | 
| 113 | 94, 95, 112 | mp2an 692 | . . . . . . . . . . . . 13
⊢
(∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) → ((((ℜ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℜ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn)) | 
| 114 |  | ax-resscn 11212 | . . . . . . . . . . . . . . . . . 18
⊢ ℝ
⊆ ℂ | 
| 115 |  | fss 6752 | . . . . . . . . . . . . . . . . . 18
⊢
((ℜ:ℂ⟶ℝ ∧ ℝ ⊆ ℂ) →
ℜ:ℂ⟶ℂ) | 
| 116 | 85, 114, 115 | mp2an 692 | . . . . . . . . . . . . . . . . 17
⊢
ℜ:ℂ⟶ℂ | 
| 117 |  | fco 6760 | . . . . . . . . . . . . . . . . 17
⊢
((ℜ:ℂ⟶ℂ ∧ 𝑓:𝑎⟶ℂ) → (ℜ ∘ 𝑓):𝑎⟶ℂ) | 
| 118 | 116, 117 | mpan 690 | . . . . . . . . . . . . . . . 16
⊢ (𝑓:𝑎⟶ℂ → (ℜ ∘ 𝑓):𝑎⟶ℂ) | 
| 119 |  | ssun1 4178 | . . . . . . . . . . . . . . . . . 18
⊢ 𝑡 ⊆ (𝑡 ∪ {ℎ}) | 
| 120 | 119 | unissi 4916 | . . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑡
⊆ ∪ (𝑡 ∪ {ℎ}) | 
| 121 |  | id 22 | . . . . . . . . . . . . . . . . 17
⊢ (∪ (𝑡
∪ {ℎ}) = 𝑎 → ∪ (𝑡
∪ {ℎ}) = 𝑎) | 
| 122 | 120, 121 | sseqtrid 4026 | . . . . . . . . . . . . . . . 16
⊢ (∪ (𝑡
∪ {ℎ}) = 𝑎 → ∪ 𝑡
⊆ 𝑎) | 
| 123 |  | fssres 6774 | . . . . . . . . . . . . . . . 16
⊢ (((ℜ
∘ 𝑓):𝑎⟶ℂ ∧ ∪ 𝑡
⊆ 𝑎) → ((ℜ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ) | 
| 124 | 118, 122,
123 | syl2an 596 | . . . . . . . . . . . . . . 15
⊢ ((𝑓:𝑎⟶ℂ ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → ((ℜ ∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ) | 
| 125 | 124 | adantlr 715 | . . . . . . . . . . . . . 14
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → ((ℜ ∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ) | 
| 126 |  | elssuni 4937 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 ∈ 𝑡 → 𝑟 ⊆ ∪ 𝑡) | 
| 127 | 126 | resabs1d 6026 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 ∈ 𝑡 → (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) = ((ℜ ∘ 𝑓) ↾ 𝑟)) | 
| 128 |  | resco 6270 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((ℜ
∘ 𝑓) ↾ 𝑟) = (ℜ ∘ (𝑓 ↾ 𝑟)) | 
| 129 | 127, 128 | eqtrdi 2793 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ 𝑡 → (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) = (ℜ ∘ (𝑓 ↾ 𝑟))) | 
| 130 | 129 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) = (ℜ ∘ (𝑓 ↾ 𝑟))) | 
| 131 |  | elun1 4182 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑟 ∈ 𝑡 → 𝑟 ∈ (𝑡 ∪ {ℎ})) | 
| 132 |  | reseq2 5992 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 = 𝑟 → (𝑓 ↾ 𝑠) = (𝑓 ↾ 𝑟)) | 
| 133 | 132 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠 = 𝑟 → ((𝑓 ↾ 𝑠) ∈ MblFn ↔ (𝑓 ↾ 𝑟) ∈ MblFn)) | 
| 134 | 133 | rspccva 3621 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑠 ∈
(𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn ∧ 𝑟 ∈ (𝑡 ∪ {ℎ})) → (𝑓 ↾ 𝑟) ∈ MblFn) | 
| 135 | 131, 134 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑠 ∈
(𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn ∧ 𝑟 ∈ 𝑡) → (𝑓 ↾ 𝑟) ∈ MblFn) | 
| 136 | 135 | adantll 714 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → (𝑓 ↾ 𝑟) ∈ MblFn) | 
| 137 |  | fresin 6777 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓:𝑎⟶ℂ → (𝑓 ↾ 𝑟):(𝑎 ∩ 𝑟)⟶ℂ) | 
| 138 |  | ismbfcn 25664 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓 ↾ 𝑟):(𝑎 ∩ 𝑟)⟶ℂ → ((𝑓 ↾ 𝑟) ∈ MblFn ↔ ((ℜ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn))) | 
| 139 | 137, 138 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓:𝑎⟶ℂ → ((𝑓 ↾ 𝑟) ∈ MblFn ↔ ((ℜ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn))) | 
| 140 | 139 | biimpd 229 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓:𝑎⟶ℂ → ((𝑓 ↾ 𝑟) ∈ MblFn → ((ℜ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn))) | 
| 141 | 140 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → ((𝑓 ↾ 𝑟) ∈ MblFn → ((ℜ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn))) | 
| 142 | 136, 141 | mpd 15 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → ((ℜ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn)) | 
| 143 | 142 | simpld 494 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → (ℜ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn) | 
| 144 | 130, 143 | eqeltrd 2841 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) ∈ MblFn) | 
| 145 | 144 | ralrimiva 3146 | . . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → ∀𝑟 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) ∈ MblFn) | 
| 146 |  | reseq2 5992 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = 𝑠 → (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) = (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠)) | 
| 147 | 146 | eleq1d 2826 | . . . . . . . . . . . . . . . . 17
⊢ (𝑟 = 𝑠 → ((((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) ∈ MblFn ↔ (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn)) | 
| 148 | 147 | cbvralvw 3237 | . . . . . . . . . . . . . . . 16
⊢
(∀𝑟 ∈
𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑟) ∈ MblFn
↔ ∀𝑠 ∈
𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn) | 
| 149 | 145, 148 | sylib 218 | . . . . . . . . . . . . . . 15
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → ∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠) ∈ MblFn) | 
| 150 | 149 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → ∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠) ∈ MblFn) | 
| 151 |  | pm2.27 42 | . . . . . . . . . . . . . 14
⊢
((((ℜ ∘ 𝑓) ↾ ∪ 𝑡):∪
𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ (((((ℜ ∘ 𝑓) ↾ ∪ 𝑡):∪
𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℜ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∈ MblFn)) | 
| 152 | 125, 150,
151 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → (((((ℜ ∘
𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℜ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∈ MblFn)) | 
| 153 | 113, 152 | mpan9 506 | . . . . . . . . . . . 12
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∈ MblFn) | 
| 154 |  | vsnid 4663 | . . . . . . . . . . . . . . 15
⊢ ℎ ∈ {ℎ} | 
| 155 |  | elun2 4183 | . . . . . . . . . . . . . . 15
⊢ (ℎ ∈ {ℎ} → ℎ ∈ (𝑡 ∪ {ℎ})) | 
| 156 |  | reseq2 5992 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠 = ℎ → (𝑓 ↾ 𝑠) = (𝑓 ↾ ℎ)) | 
| 157 | 156 | eleq1d 2826 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 = ℎ → ((𝑓 ↾ 𝑠) ∈ MblFn ↔ (𝑓 ↾ ℎ) ∈ MblFn)) | 
| 158 | 157 | rspcv 3618 | . . . . . . . . . . . . . . 15
⊢ (ℎ ∈ (𝑡 ∪ {ℎ}) → (∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn → (𝑓 ↾ ℎ) ∈ MblFn)) | 
| 159 | 154, 155,
158 | mp2b 10 | . . . . . . . . . . . . . 14
⊢
(∀𝑠 ∈
(𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn → (𝑓 ↾ ℎ) ∈ MblFn) | 
| 160 |  | resco 6270 | . . . . . . . . . . . . . . 15
⊢ ((ℜ
∘ 𝑓) ↾ ℎ) = (ℜ ∘ (𝑓 ↾ ℎ)) | 
| 161 |  | fresin 6777 | . . . . . . . . . . . . . . . . 17
⊢ (𝑓:𝑎⟶ℂ → (𝑓 ↾ ℎ):(𝑎 ∩ ℎ)⟶ℂ) | 
| 162 |  | ismbfcn 25664 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ↾ ℎ):(𝑎 ∩ ℎ)⟶ℂ → ((𝑓 ↾ ℎ) ∈ MblFn ↔ ((ℜ ∘ (𝑓 ↾ ℎ)) ∈ MblFn ∧ (ℑ ∘ (𝑓 ↾ ℎ)) ∈ MblFn))) | 
| 163 | 161, 162 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑓:𝑎⟶ℂ → ((𝑓 ↾ ℎ) ∈ MblFn ↔ ((ℜ ∘ (𝑓 ↾ ℎ)) ∈ MblFn ∧ (ℑ ∘ (𝑓 ↾ ℎ)) ∈ MblFn))) | 
| 164 | 163 | simprbda 498 | . . . . . . . . . . . . . . 15
⊢ ((𝑓:𝑎⟶ℂ ∧ (𝑓 ↾ ℎ) ∈ MblFn) → (ℜ ∘ (𝑓 ↾ ℎ)) ∈ MblFn) | 
| 165 | 160, 164 | eqeltrid 2845 | . . . . . . . . . . . . . 14
⊢ ((𝑓:𝑎⟶ℂ ∧ (𝑓 ↾ ℎ) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ ℎ) ∈ MblFn) | 
| 166 | 159, 165 | sylan2 593 | . . . . . . . . . . . . 13
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ ℎ) ∈ MblFn) | 
| 167 | 166 | ad2antrl 728 | . . . . . . . . . . . 12
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → ((ℜ ∘ 𝑓) ↾ ℎ) ∈ MblFn) | 
| 168 |  | uniun 4930 | . . . . . . . . . . . . . . 15
⊢ ∪ (𝑡
∪ {ℎ}) = (∪ 𝑡
∪ ∪ {ℎ}) | 
| 169 |  | unisnv 4927 | . . . . . . . . . . . . . . . 16
⊢ ∪ {ℎ} =
ℎ | 
| 170 | 169 | uneq2i 4165 | . . . . . . . . . . . . . . 15
⊢ (∪ 𝑡
∪ ∪ {ℎ}) = (∪ 𝑡 ∪ ℎ) | 
| 171 | 168, 170 | eqtri 2765 | . . . . . . . . . . . . . 14
⊢ ∪ (𝑡
∪ {ℎ}) = (∪ 𝑡
∪ ℎ) | 
| 172 | 171, 121 | eqtr3id 2791 | . . . . . . . . . . . . 13
⊢ (∪ (𝑡
∪ {ℎ}) = 𝑎 → (∪ 𝑡
∪ ℎ) = 𝑎) | 
| 173 | 172 | ad2antll 729 | . . . . . . . . . . . 12
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → (∪ 𝑡
∪ ℎ) = 𝑎) | 
| 174 | 89, 153, 167, 173 | mbfres2 25680 | . . . . . . . . . . 11
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → (ℜ ∘ 𝑓) ∈ MblFn) | 
| 175 |  | imf 15152 | . . . . . . . . . . . . . . 15
⊢
ℑ:ℂ⟶ℝ | 
| 176 |  | fco 6760 | . . . . . . . . . . . . . . 15
⊢
((ℑ:ℂ⟶ℝ ∧ 𝑓:𝑎⟶ℂ) → (ℑ ∘
𝑓):𝑎⟶ℝ) | 
| 177 | 175, 176 | mpan 690 | . . . . . . . . . . . . . 14
⊢ (𝑓:𝑎⟶ℂ → (ℑ ∘ 𝑓):𝑎⟶ℝ) | 
| 178 | 177 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → (ℑ ∘ 𝑓):𝑎⟶ℝ) | 
| 179 | 178 | ad2antrl 728 | . . . . . . . . . . . 12
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → (ℑ ∘ 𝑓):𝑎⟶ℝ) | 
| 180 |  | imcncf 24929 | . . . . . . . . . . . . . . . . 17
⊢ ℑ
∈ (ℂ–cn→ℝ) | 
| 181 | 180 | elexi 3503 | . . . . . . . . . . . . . . . 16
⊢ ℑ
∈ V | 
| 182 | 181, 92 | coex 7952 | . . . . . . . . . . . . . . 15
⊢ (ℑ
∘ 𝑓) ∈
V | 
| 183 | 182 | resex 6047 | . . . . . . . . . . . . . 14
⊢ ((ℑ
∘ 𝑓) ↾ ∪ 𝑡)
∈ V | 
| 184 | 97 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ∪ 𝑡 = 𝑏) | 
| 185 | 184 | biantrud 531 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ↔ ((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏))) | 
| 186 |  | feq123 6726 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡
∧ ℂ = ℂ) → (𝑔:𝑏⟶ℂ ↔ ((ℑ ∘
𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ)) | 
| 187 | 100, 186 | mp3an3 1452 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (𝑔:𝑏⟶ℂ ↔ ((ℑ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ)) | 
| 188 |  | reseq1 5991 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
→ (𝑔 ↾ 𝑠) = (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠)) | 
| 189 | 188 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
→ ((𝑔 ↾ 𝑠) ∈ MblFn ↔ (((ℑ
∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn)) | 
| 190 | 189 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((𝑔 ↾ 𝑠) ∈ MblFn ↔ (((ℑ
∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn)) | 
| 191 | 190 | ralbidv 3178 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (∀𝑠 ∈
𝑡 (𝑔 ↾ 𝑠) ∈ MblFn ↔ ∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠) ∈ MblFn)) | 
| 192 | 187, 191 | anbi12d 632 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ↔ (((ℑ ∘
𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn))) | 
| 193 | 185, 192 | bitr3d 281 | . . . . . . . . . . . . . . . 16
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) ↔ (((ℑ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn))) | 
| 194 |  | eleq1 2829 | . . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
→ (𝑔 ∈ MblFn
↔ ((ℑ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn)) | 
| 195 | 194 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (𝑔 ∈ MblFn
↔ ((ℑ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn)) | 
| 196 | 193, 195 | imbi12d 344 | . . . . . . . . . . . . . . 15
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ↔
((((ℑ ∘ 𝑓)
↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℑ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn))) | 
| 197 | 196 | spc2gv 3600 | . . . . . . . . . . . . . 14
⊢
((((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ∈ V ∧ ∪ 𝑡
∈ V) → (∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) →
((((ℑ ∘ 𝑓)
↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℑ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn))) | 
| 198 | 183, 95, 197 | mp2an 692 | . . . . . . . . . . . . 13
⊢
(∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) →
((((ℑ ∘ 𝑓)
↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℑ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn)) | 
| 199 |  | fss 6752 | . . . . . . . . . . . . . . . . . 18
⊢
((ℑ:ℂ⟶ℝ ∧ ℝ ⊆ ℂ) →
ℑ:ℂ⟶ℂ) | 
| 200 | 175, 114,
199 | mp2an 692 | . . . . . . . . . . . . . . . . 17
⊢
ℑ:ℂ⟶ℂ | 
| 201 |  | fco 6760 | . . . . . . . . . . . . . . . . 17
⊢
((ℑ:ℂ⟶ℂ ∧ 𝑓:𝑎⟶ℂ) → (ℑ ∘
𝑓):𝑎⟶ℂ) | 
| 202 | 200, 201 | mpan 690 | . . . . . . . . . . . . . . . 16
⊢ (𝑓:𝑎⟶ℂ → (ℑ ∘ 𝑓):𝑎⟶ℂ) | 
| 203 |  | fssres 6774 | . . . . . . . . . . . . . . . 16
⊢
(((ℑ ∘ 𝑓):𝑎⟶ℂ ∧ ∪ 𝑡
⊆ 𝑎) → ((ℑ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ) | 
| 204 | 202, 122,
203 | syl2an 596 | . . . . . . . . . . . . . . 15
⊢ ((𝑓:𝑎⟶ℂ ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → ((ℑ ∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ) | 
| 205 | 204 | adantlr 715 | . . . . . . . . . . . . . 14
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → ((ℑ ∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ) | 
| 206 | 126 | resabs1d 6026 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 ∈ 𝑡 → (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) = ((ℑ ∘ 𝑓) ↾ 𝑟)) | 
| 207 |  | resco 6270 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((ℑ
∘ 𝑓) ↾ 𝑟) = (ℑ ∘ (𝑓 ↾ 𝑟)) | 
| 208 | 206, 207 | eqtrdi 2793 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ 𝑡 → (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) = (ℑ ∘ (𝑓 ↾ 𝑟))) | 
| 209 | 208 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑟) = (ℑ
∘ (𝑓 ↾ 𝑟))) | 
| 210 | 142 | simprd 495 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → (ℑ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn) | 
| 211 | 209, 210 | eqeltrd 2841 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑟) ∈
MblFn) | 
| 212 | 211 | ralrimiva 3146 | . . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → ∀𝑟 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) ∈ MblFn) | 
| 213 |  | reseq2 5992 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = 𝑠 → (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) = (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠)) | 
| 214 | 213 | eleq1d 2826 | . . . . . . . . . . . . . . . . 17
⊢ (𝑟 = 𝑠 → ((((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑟) ∈ MblFn
↔ (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠) ∈ MblFn)) | 
| 215 | 214 | cbvralvw 3237 | . . . . . . . . . . . . . . . 16
⊢
(∀𝑟 ∈
𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑟) ∈ MblFn
↔ ∀𝑠 ∈
𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn) | 
| 216 | 212, 215 | sylib 218 | . . . . . . . . . . . . . . 15
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → ∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠) ∈ MblFn) | 
| 217 | 216 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → ∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠) ∈ MblFn) | 
| 218 |  | pm2.27 42 | . . . . . . . . . . . . . 14
⊢
((((ℑ ∘ 𝑓) ↾ ∪ 𝑡):∪
𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ (((((ℑ ∘ 𝑓) ↾ ∪ 𝑡):∪
𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℑ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn) → ((ℑ ∘
𝑓) ↾ ∪ 𝑡)
∈ MblFn)) | 
| 219 | 205, 217,
218 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → (((((ℑ ∘
𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℑ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn) → ((ℑ ∘
𝑓) ↾ ∪ 𝑡)
∈ MblFn)) | 
| 220 | 198, 219 | mpan9 506 | . . . . . . . . . . . 12
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → ((ℑ ∘
𝑓) ↾ ∪ 𝑡)
∈ MblFn) | 
| 221 |  | resco 6270 | . . . . . . . . . . . . . . 15
⊢ ((ℑ
∘ 𝑓) ↾ ℎ) = (ℑ ∘ (𝑓 ↾ ℎ)) | 
| 222 | 163 | simplbda 499 | . . . . . . . . . . . . . . 15
⊢ ((𝑓:𝑎⟶ℂ ∧ (𝑓 ↾ ℎ) ∈ MblFn) → (ℑ ∘ (𝑓 ↾ ℎ)) ∈ MblFn) | 
| 223 | 221, 222 | eqeltrid 2845 | . . . . . . . . . . . . . 14
⊢ ((𝑓:𝑎⟶ℂ ∧ (𝑓 ↾ ℎ) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ ℎ) ∈ MblFn) | 
| 224 | 159, 223 | sylan2 593 | . . . . . . . . . . . . 13
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → ((ℑ ∘
𝑓) ↾ ℎ) ∈ MblFn) | 
| 225 | 224 | ad2antrl 728 | . . . . . . . . . . . 12
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → ((ℑ ∘
𝑓) ↾ ℎ) ∈ MblFn) | 
| 226 | 179, 220,
225, 173 | mbfres2 25680 | . . . . . . . . . . 11
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → (ℑ ∘ 𝑓) ∈ MblFn) | 
| 227 |  | ismbfcn 25664 | . . . . . . . . . . . . 13
⊢ (𝑓:𝑎⟶ℂ → (𝑓 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ∈ MblFn ∧ (ℑ
∘ 𝑓) ∈
MblFn))) | 
| 228 | 227 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → (𝑓 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ∈ MblFn ∧ (ℑ
∘ 𝑓) ∈
MblFn))) | 
| 229 | 228 | ad2antrl 728 | . . . . . . . . . . 11
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → (𝑓 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ∈ MblFn ∧ (ℑ
∘ 𝑓) ∈
MblFn))) | 
| 230 | 174, 226,
229 | mpbir2and 713 | . . . . . . . . . 10
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → 𝑓 ∈ MblFn) | 
| 231 | 230 | ex 412 | . . . . . . . . 9
⊢
(∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → 𝑓 ∈ MblFn)) | 
| 232 | 231 | alrimivv 1928 | . . . . . . . 8
⊢
(∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) →
∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → 𝑓 ∈ MblFn)) | 
| 233 | 232 | a1i 11 | . . . . . . 7
⊢ (𝑡 ∈ Fin →
(∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) →
∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → 𝑓 ∈ MblFn))) | 
| 234 | 35, 58, 65, 72, 84, 233 | findcard2 9204 | . . . . . 6
⊢ (𝑆 ∈ Fin → ∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈ MblFn)) | 
| 235 |  | 2sp 2186 | . . . . . 6
⊢
(∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈ MblFn) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈ MblFn)) | 
| 236 | 4, 234, 235 | 3syl 18 | . . . . 5
⊢ (𝜑 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈ MblFn)) | 
| 237 | 16, 25, 236 | vtocl2g 3574 | . . . 4
⊢ ((𝐴 ∈ V ∧ 𝐹 ∈ V) → (𝜑 → (((𝐹:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝐹 ∈ MblFn))) | 
| 238 | 10, 237 | mpcom 38 | . . 3
⊢ (𝜑 → (((𝐹:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝐹 ∈ MblFn)) | 
| 239 | 3, 238 | mpan2d 694 | . 2
⊢ (𝜑 → ((𝐹:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) → 𝐹 ∈ MblFn)) | 
| 240 | 1, 2, 239 | mp2and 699 | 1
⊢ (𝜑 → 𝐹 ∈ MblFn) |