Step | Hyp | Ref
| Expression |
1 | | mbfresfi.1 |
. 2
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
2 | | mbfresfi.3 |
. 2
⊢ (𝜑 → ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) |
3 | | mbfresfi.4 |
. . 3
⊢ (𝜑 → ∪ 𝑆 =
𝐴) |
4 | | mbfresfi.2 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ Fin) |
5 | | uniexg 7234 |
. . . . . . 7
⊢ (𝑆 ∈ Fin → ∪ 𝑆
∈ V) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑆
∈ V) |
7 | 3, 6 | eqeltrrd 2860 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ V) |
8 | | fex 6763 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ∈ V) → 𝐹 ∈ V) |
9 | 8 | ex 403 |
. . . . . 6
⊢ (𝐹:𝐴⟶ℂ → (𝐴 ∈ V → 𝐹 ∈ V)) |
10 | 1, 9 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴 ∈ V → 𝐹 ∈ V)) |
11 | 7, 10 | jcai 512 |
. . . 4
⊢ (𝜑 → (𝐴 ∈ V ∧ 𝐹 ∈ V)) |
12 | | feq2 6275 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (𝑓:𝑎⟶ℂ ↔ 𝑓:𝐴⟶ℂ)) |
13 | 12 | anbi1d 623 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ↔ (𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn))) |
14 | | eqeq2 2789 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (∪ 𝑆 = 𝑎 ↔ ∪ 𝑆 = 𝐴)) |
15 | 13, 14 | anbi12d 624 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) ↔ ((𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴))) |
16 | 15 | imbi1d 333 |
. . . . . 6
⊢ (𝑎 = 𝐴 → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝑓 ∈
MblFn))) |
17 | 16 | imbi2d 332 |
. . . . 5
⊢ (𝑎 = 𝐴 → ((𝜑 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈ MblFn)) ↔ (𝜑 → (((𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝑓 ∈
MblFn)))) |
18 | | feq1 6274 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑓:𝐴⟶ℂ ↔ 𝐹:𝐴⟶ℂ)) |
19 | | reseq1 5638 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → (𝑓 ↾ 𝑠) = (𝐹 ↾ 𝑠)) |
20 | 19 | eleq1d 2844 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐹 → ((𝑓 ↾ 𝑠) ∈ MblFn ↔ (𝐹 ↾ 𝑠) ∈ MblFn)) |
21 | 20 | ralbidv 3168 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn ↔ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn)) |
22 | 18, 21 | anbi12d 624 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → ((𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn))) |
23 | 22 | anbi1d 623 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (((𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) ↔ ((𝐹:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴))) |
24 | | eleq1 2847 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝑓 ∈ MblFn ↔ 𝐹 ∈ MblFn)) |
25 | 23, 24 | imbi12d 336 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((((𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝑓 ∈ MblFn) ↔ (((𝐹:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝐹 ∈ MblFn))) |
26 | 25 | imbi2d 332 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((𝜑 → (((𝑓:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝑓 ∈ MblFn)) ↔ (𝜑 → (((𝐹:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝐹 ∈ MblFn)))) |
27 | | rzal 4296 |
. . . . . . . . . . . 12
⊢ (𝑟 = ∅ → ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) |
28 | 27 | biantrud 527 |
. . . . . . . . . . 11
⊢ (𝑟 = ∅ → (𝑓:𝑎⟶ℂ ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn))) |
29 | 28 | bicomd 215 |
. . . . . . . . . 10
⊢ (𝑟 = ∅ → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ↔ 𝑓:𝑎⟶ℂ)) |
30 | | unieq 4681 |
. . . . . . . . . . . 12
⊢ (𝑟 = ∅ → ∪ 𝑟 =
∪ ∅) |
31 | | uni0 4702 |
. . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ |
32 | 30, 31 | syl6eq 2830 |
. . . . . . . . . . 11
⊢ (𝑟 = ∅ → ∪ 𝑟 =
∅) |
33 | 32 | eqeq1d 2780 |
. . . . . . . . . 10
⊢ (𝑟 = ∅ → (∪ 𝑟 =
𝑎 ↔ ∅ = 𝑎)) |
34 | 29, 33 | anbi12d 624 |
. . . . . . . . 9
⊢ (𝑟 = ∅ → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) ↔ (𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎))) |
35 | 34 | imbi1d 333 |
. . . . . . . 8
⊢ (𝑟 = ∅ → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔ ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn))) |
36 | 35 | 2albidv 1966 |
. . . . . . 7
⊢ (𝑟 = ∅ → (∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔
∀𝑓∀𝑎((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn))) |
37 | | raleq 3330 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑡 → (∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn ↔ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn)) |
38 | 37 | anbi2d 622 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑡 → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn))) |
39 | | unieq 4681 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑡 → ∪ 𝑟 = ∪
𝑡) |
40 | 39 | eqeq1d 2780 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑡 → (∪ 𝑟 = 𝑎 ↔ ∪ 𝑡 = 𝑎)) |
41 | 38, 40 | anbi12d 624 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑡 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) ↔ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑎))) |
42 | 41 | imbi1d 333 |
. . . . . . . . 9
⊢ (𝑟 = 𝑡 → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑎) → 𝑓 ∈
MblFn))) |
43 | 42 | 2albidv 1966 |
. . . . . . . 8
⊢ (𝑟 = 𝑡 → (∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔
∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑎) → 𝑓 ∈
MblFn))) |
44 | | simpl 476 |
. . . . . . . . . . . . 13
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → 𝑓 = 𝑔) |
45 | | simpr 479 |
. . . . . . . . . . . . 13
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → 𝑎 = 𝑏) |
46 | 44, 45 | feq12d 6281 |
. . . . . . . . . . . 12
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → (𝑓:𝑎⟶ℂ ↔ 𝑔:𝑏⟶ℂ)) |
47 | | reseq1 5638 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑔 → (𝑓 ↾ 𝑠) = (𝑔 ↾ 𝑠)) |
48 | 47 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → (𝑓 ↾ 𝑠) = (𝑔 ↾ 𝑠)) |
49 | 48 | eleq1d 2844 |
. . . . . . . . . . . . 13
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → ((𝑓 ↾ 𝑠) ∈ MblFn ↔ (𝑔 ↾ 𝑠) ∈ MblFn)) |
50 | 49 | ralbidv 3168 |
. . . . . . . . . . . 12
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → (∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn ↔ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn)) |
51 | 46, 50 | anbi12d 624 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn) ↔ (𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn))) |
52 | | eqeq2 2789 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → (∪ 𝑡 = 𝑎 ↔ ∪ 𝑡 = 𝑏)) |
53 | 52 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → (∪ 𝑡 = 𝑎 ↔ ∪ 𝑡 = 𝑏)) |
54 | 51, 53 | anbi12d 624 |
. . . . . . . . . 10
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑎) ↔ ((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏))) |
55 | | eleq1 2847 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → (𝑓 ∈ MblFn ↔ 𝑔 ∈ MblFn)) |
56 | 55 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → (𝑓 ∈ MblFn ↔ 𝑔 ∈ MblFn)) |
57 | 54, 56 | imbi12d 336 |
. . . . . . . . 9
⊢ ((𝑓 = 𝑔 ∧ 𝑎 = 𝑏) → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈
MblFn))) |
58 | 57 | cbval2v 2378 |
. . . . . . . 8
⊢
(∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑎) → 𝑓 ∈ MblFn) ↔
∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn)) |
59 | 43, 58 | syl6bb 279 |
. . . . . . 7
⊢ (𝑟 = 𝑡 → (∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔
∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈
MblFn))) |
60 | | raleq 3330 |
. . . . . . . . . . 11
⊢ (𝑟 = (𝑡 ∪ {ℎ}) → (∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn ↔ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn)) |
61 | 60 | anbi2d 622 |
. . . . . . . . . 10
⊢ (𝑟 = (𝑡 ∪ {ℎ}) → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn))) |
62 | | unieq 4681 |
. . . . . . . . . . 11
⊢ (𝑟 = (𝑡 ∪ {ℎ}) → ∪ 𝑟 = ∪
(𝑡 ∪ {ℎ})) |
63 | 62 | eqeq1d 2780 |
. . . . . . . . . 10
⊢ (𝑟 = (𝑡 ∪ {ℎ}) → (∪ 𝑟 = 𝑎 ↔ ∪ (𝑡 ∪ {ℎ}) = 𝑎)) |
64 | 61, 63 | anbi12d 624 |
. . . . . . . . 9
⊢ (𝑟 = (𝑡 ∪ {ℎ}) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) ↔ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎))) |
65 | 64 | imbi1d 333 |
. . . . . . . 8
⊢ (𝑟 = (𝑡 ∪ {ℎ}) → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → 𝑓 ∈ MblFn))) |
66 | 65 | 2albidv 1966 |
. . . . . . 7
⊢ (𝑟 = (𝑡 ∪ {ℎ}) → (∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔
∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → 𝑓 ∈ MblFn))) |
67 | | raleq 3330 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑆 → (∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn ↔ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn)) |
68 | 67 | anbi2d 622 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑆 → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn))) |
69 | | unieq 4681 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑆 → ∪ 𝑟 = ∪
𝑆) |
70 | 69 | eqeq1d 2780 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑆 → (∪ 𝑟 = 𝑎 ↔ ∪ 𝑆 = 𝑎)) |
71 | 68, 70 | anbi12d 624 |
. . . . . . . . 9
⊢ (𝑟 = 𝑆 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) ↔ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎))) |
72 | 71 | imbi1d 333 |
. . . . . . . 8
⊢ (𝑟 = 𝑆 → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈
MblFn))) |
73 | 72 | 2albidv 1966 |
. . . . . . 7
⊢ (𝑟 = 𝑆 → (∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑟 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑟 =
𝑎) → 𝑓 ∈ MblFn) ↔
∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈
MblFn))) |
74 | | frel 6298 |
. . . . . . . . . 10
⊢ (𝑓:𝑎⟶ℂ → Rel 𝑓) |
75 | 74 | adantr 474 |
. . . . . . . . 9
⊢ ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → Rel 𝑓) |
76 | | fdm 6301 |
. . . . . . . . . 10
⊢ (𝑓:𝑎⟶ℂ → dom 𝑓 = 𝑎) |
77 | | eqcom 2785 |
. . . . . . . . . . 11
⊢ (∅
= 𝑎 ↔ 𝑎 = ∅) |
78 | 77 | biimpi 208 |
. . . . . . . . . 10
⊢ (∅
= 𝑎 → 𝑎 = ∅) |
79 | 76, 78 | sylan9eq 2834 |
. . . . . . . . 9
⊢ ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → dom 𝑓 = ∅) |
80 | | reldm0 5590 |
. . . . . . . . . . 11
⊢ (Rel
𝑓 → (𝑓 = ∅ ↔ dom 𝑓 = ∅)) |
81 | 80 | biimpar 471 |
. . . . . . . . . 10
⊢ ((Rel
𝑓 ∧ dom 𝑓 = ∅) → 𝑓 = ∅) |
82 | | mbf0 23849 |
. . . . . . . . . 10
⊢ ∅
∈ MblFn |
83 | 81, 82 | syl6eqel 2867 |
. . . . . . . . 9
⊢ ((Rel
𝑓 ∧ dom 𝑓 = ∅) → 𝑓 ∈ MblFn) |
84 | 75, 79, 83 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn) |
85 | 84 | gen2 1840 |
. . . . . . 7
⊢
∀𝑓∀𝑎((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn) |
86 | | ref 14265 |
. . . . . . . . . . . . . . 15
⊢
ℜ:ℂ⟶ℝ |
87 | | fco 6310 |
. . . . . . . . . . . . . . 15
⊢
((ℜ:ℂ⟶ℝ ∧ 𝑓:𝑎⟶ℂ) → (ℜ ∘ 𝑓):𝑎⟶ℝ) |
88 | 86, 87 | mpan 680 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝑎⟶ℂ → (ℜ ∘ 𝑓):𝑎⟶ℝ) |
89 | 88 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → (ℜ ∘ 𝑓):𝑎⟶ℝ) |
90 | 89 | ad2antrl 718 |
. . . . . . . . . . . 12
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → (ℜ ∘ 𝑓):𝑎⟶ℝ) |
91 | | recncf 23124 |
. . . . . . . . . . . . . . . . 17
⊢ ℜ
∈ (ℂ–cn→ℝ) |
92 | 91 | elexi 3415 |
. . . . . . . . . . . . . . . 16
⊢ ℜ
∈ V |
93 | | vex 3401 |
. . . . . . . . . . . . . . . 16
⊢ 𝑓 ∈ V |
94 | 92, 93 | coex 7399 |
. . . . . . . . . . . . . . 15
⊢ (ℜ
∘ 𝑓) ∈
V |
95 | 94 | resex 5695 |
. . . . . . . . . . . . . 14
⊢ ((ℜ
∘ 𝑓) ↾ ∪ 𝑡)
∈ V |
96 | | vuniex 7233 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑡
∈ V |
97 | | eqcom 2785 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = ∪
𝑡 ↔ ∪ 𝑡 =
𝑏) |
98 | 97 | biimpi 208 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = ∪
𝑡 → ∪ 𝑡 =
𝑏) |
99 | 98 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ∪ 𝑡 = 𝑏) |
100 | 99 | biantrud 527 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ↔ ((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏))) |
101 | | eqid 2778 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℂ =
ℂ |
102 | | feq123 6283 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡
∧ ℂ = ℂ) → (𝑔:𝑏⟶ℂ ↔ ((ℜ ∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ)) |
103 | 101, 102 | mp3an3 1523 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (𝑔:𝑏⟶ℂ ↔ ((ℜ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ)) |
104 | | reseq1 5638 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
→ (𝑔 ↾ 𝑠) = (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠)) |
105 | 104 | eleq1d 2844 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
→ ((𝑔 ↾ 𝑠) ∈ MblFn ↔ (((ℜ
∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn)) |
106 | 105 | adantr 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((𝑔 ↾ 𝑠) ∈ MblFn ↔ (((ℜ
∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn)) |
107 | 106 | ralbidv 3168 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (∀𝑠 ∈
𝑡 (𝑔 ↾ 𝑠) ∈ MblFn ↔ ∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠) ∈ MblFn)) |
108 | 103, 107 | anbi12d 624 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ↔ (((ℜ ∘
𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn))) |
109 | 100, 108 | bitr3d 273 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) ↔ (((ℜ ∘
𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn))) |
110 | | eleq1 2847 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
→ (𝑔 ∈ MblFn
↔ ((ℜ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn)) |
111 | 110 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (𝑔 ∈ MblFn
↔ ((ℜ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn)) |
112 | 109, 111 | imbi12d 336 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 = ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ↔ ((((ℜ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℜ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn))) |
113 | 112 | spc2gv 3498 |
. . . . . . . . . . . . . 14
⊢
((((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ∈ V ∧ ∪ 𝑡
∈ V) → (∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) → ((((ℜ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℜ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn))) |
114 | 95, 96, 113 | mp2an 682 |
. . . . . . . . . . . . 13
⊢
(∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) → ((((ℜ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℜ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn)) |
115 | | ax-resscn 10331 |
. . . . . . . . . . . . . . . . . 18
⊢ ℝ
⊆ ℂ |
116 | | fss 6306 |
. . . . . . . . . . . . . . . . . 18
⊢
((ℜ:ℂ⟶ℝ ∧ ℝ ⊆ ℂ) →
ℜ:ℂ⟶ℂ) |
117 | 86, 115, 116 | mp2an 682 |
. . . . . . . . . . . . . . . . 17
⊢
ℜ:ℂ⟶ℂ |
118 | | fco 6310 |
. . . . . . . . . . . . . . . . 17
⊢
((ℜ:ℂ⟶ℂ ∧ 𝑓:𝑎⟶ℂ) → (ℜ ∘ 𝑓):𝑎⟶ℂ) |
119 | 117, 118 | mpan 680 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝑎⟶ℂ → (ℜ ∘ 𝑓):𝑎⟶ℂ) |
120 | | ssun1 3999 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑡 ⊆ (𝑡 ∪ {ℎ}) |
121 | 120 | unissi 4698 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑡
⊆ ∪ (𝑡 ∪ {ℎ}) |
122 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ (𝑡
∪ {ℎ}) = 𝑎 → ∪ (𝑡
∪ {ℎ}) = 𝑎) |
123 | 121, 122 | syl5sseq 3872 |
. . . . . . . . . . . . . . . 16
⊢ (∪ (𝑡
∪ {ℎ}) = 𝑎 → ∪ 𝑡
⊆ 𝑎) |
124 | | fssres 6322 |
. . . . . . . . . . . . . . . 16
⊢ (((ℜ
∘ 𝑓):𝑎⟶ℂ ∧ ∪ 𝑡
⊆ 𝑎) → ((ℜ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ) |
125 | 119, 123,
124 | syl2an 589 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝑎⟶ℂ ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → ((ℜ ∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ) |
126 | 125 | adantlr 705 |
. . . . . . . . . . . . . 14
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → ((ℜ ∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ) |
127 | | elssuni 4704 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 ∈ 𝑡 → 𝑟 ⊆ ∪ 𝑡) |
128 | 127 | resabs1d 5679 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 ∈ 𝑡 → (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) = ((ℜ ∘ 𝑓) ↾ 𝑟)) |
129 | | resco 5895 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℜ
∘ 𝑓) ↾ 𝑟) = (ℜ ∘ (𝑓 ↾ 𝑟)) |
130 | 128, 129 | syl6eq 2830 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ 𝑡 → (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) = (ℜ ∘ (𝑓 ↾ 𝑟))) |
131 | 130 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) = (ℜ ∘ (𝑓 ↾ 𝑟))) |
132 | | elun1 4003 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑟 ∈ 𝑡 → 𝑟 ∈ (𝑡 ∪ {ℎ})) |
133 | | reseq2 5639 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑠 = 𝑟 → (𝑓 ↾ 𝑠) = (𝑓 ↾ 𝑟)) |
134 | 133 | eleq1d 2844 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠 = 𝑟 → ((𝑓 ↾ 𝑠) ∈ MblFn ↔ (𝑓 ↾ 𝑟) ∈ MblFn)) |
135 | 134 | rspccva 3510 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑠 ∈
(𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn ∧ 𝑟 ∈ (𝑡 ∪ {ℎ})) → (𝑓 ↾ 𝑟) ∈ MblFn) |
136 | 132, 135 | sylan2 586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑠 ∈
(𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn ∧ 𝑟 ∈ 𝑡) → (𝑓 ↾ 𝑟) ∈ MblFn) |
137 | 136 | adantll 704 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → (𝑓 ↾ 𝑟) ∈ MblFn) |
138 | | fresin 6325 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓:𝑎⟶ℂ → (𝑓 ↾ 𝑟):(𝑎 ∩ 𝑟)⟶ℂ) |
139 | | ismbfcn 23844 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓 ↾ 𝑟):(𝑎 ∩ 𝑟)⟶ℂ → ((𝑓 ↾ 𝑟) ∈ MblFn ↔ ((ℜ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn))) |
140 | 138, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓:𝑎⟶ℂ → ((𝑓 ↾ 𝑟) ∈ MblFn ↔ ((ℜ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn))) |
141 | 140 | biimpd 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓:𝑎⟶ℂ → ((𝑓 ↾ 𝑟) ∈ MblFn → ((ℜ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn))) |
142 | 141 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → ((𝑓 ↾ 𝑟) ∈ MblFn → ((ℜ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn))) |
143 | 137, 142 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → ((ℜ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn)) |
144 | 143 | simpld 490 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → (ℜ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn) |
145 | 131, 144 | eqeltrd 2859 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) ∈ MblFn) |
146 | 145 | ralrimiva 3148 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → ∀𝑟 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) ∈ MblFn) |
147 | | reseq2 5639 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = 𝑠 → (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) = (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠)) |
148 | 147 | eleq1d 2844 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = 𝑠 → ((((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) ∈ MblFn ↔ (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn)) |
149 | 148 | cbvralv 3367 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑟 ∈
𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑟) ∈ MblFn
↔ ∀𝑠 ∈
𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn) |
150 | 146, 149 | sylib 210 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → ∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠) ∈ MblFn) |
151 | 150 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → ∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠) ∈ MblFn) |
152 | | pm2.27 42 |
. . . . . . . . . . . . . 14
⊢
((((ℜ ∘ 𝑓) ↾ ∪ 𝑡):∪
𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ (((((ℜ ∘ 𝑓) ↾ ∪ 𝑡):∪
𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℜ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∈ MblFn)) |
153 | 126, 151,
152 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → (((((ℜ ∘
𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℜ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∈ MblFn)) |
154 | 114, 153 | mpan9 502 |
. . . . . . . . . . . 12
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → ((ℜ ∘ 𝑓) ↾ ∪ 𝑡)
∈ MblFn) |
155 | | vsnid 4431 |
. . . . . . . . . . . . . . 15
⊢ ℎ ∈ {ℎ} |
156 | | elun2 4004 |
. . . . . . . . . . . . . . 15
⊢ (ℎ ∈ {ℎ} → ℎ ∈ (𝑡 ∪ {ℎ})) |
157 | | reseq2 5639 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = ℎ → (𝑓 ↾ 𝑠) = (𝑓 ↾ ℎ)) |
158 | 157 | eleq1d 2844 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = ℎ → ((𝑓 ↾ 𝑠) ∈ MblFn ↔ (𝑓 ↾ ℎ) ∈ MblFn)) |
159 | 158 | rspcv 3507 |
. . . . . . . . . . . . . . 15
⊢ (ℎ ∈ (𝑡 ∪ {ℎ}) → (∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn → (𝑓 ↾ ℎ) ∈ MblFn)) |
160 | 155, 156,
159 | mp2b 10 |
. . . . . . . . . . . . . 14
⊢
(∀𝑠 ∈
(𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn → (𝑓 ↾ ℎ) ∈ MblFn) |
161 | | resco 5895 |
. . . . . . . . . . . . . . 15
⊢ ((ℜ
∘ 𝑓) ↾ ℎ) = (ℜ ∘ (𝑓 ↾ ℎ)) |
162 | | fresin 6325 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:𝑎⟶ℂ → (𝑓 ↾ ℎ):(𝑎 ∩ ℎ)⟶ℂ) |
163 | | ismbfcn 23844 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ↾ ℎ):(𝑎 ∩ ℎ)⟶ℂ → ((𝑓 ↾ ℎ) ∈ MblFn ↔ ((ℜ ∘ (𝑓 ↾ ℎ)) ∈ MblFn ∧ (ℑ ∘ (𝑓 ↾ ℎ)) ∈ MblFn))) |
164 | 162, 163 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝑎⟶ℂ → ((𝑓 ↾ ℎ) ∈ MblFn ↔ ((ℜ ∘ (𝑓 ↾ ℎ)) ∈ MblFn ∧ (ℑ ∘ (𝑓 ↾ ℎ)) ∈ MblFn))) |
165 | 164 | simprbda 494 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝑎⟶ℂ ∧ (𝑓 ↾ ℎ) ∈ MblFn) → (ℜ ∘ (𝑓 ↾ ℎ)) ∈ MblFn) |
166 | 161, 165 | syl5eqel 2863 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝑎⟶ℂ ∧ (𝑓 ↾ ℎ) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ ℎ) ∈ MblFn) |
167 | 160, 166 | sylan2 586 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ ℎ) ∈ MblFn) |
168 | 167 | ad2antrl 718 |
. . . . . . . . . . . 12
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → ((ℜ ∘ 𝑓) ↾ ℎ) ∈ MblFn) |
169 | | uniun 4694 |
. . . . . . . . . . . . . . 15
⊢ ∪ (𝑡
∪ {ℎ}) = (∪ 𝑡
∪ ∪ {ℎ}) |
170 | | vex 3401 |
. . . . . . . . . . . . . . . . 17
⊢ ℎ ∈ V |
171 | 170 | unisn 4689 |
. . . . . . . . . . . . . . . 16
⊢ ∪ {ℎ} =
ℎ |
172 | 171 | uneq2i 3987 |
. . . . . . . . . . . . . . 15
⊢ (∪ 𝑡
∪ ∪ {ℎ}) = (∪ 𝑡 ∪ ℎ) |
173 | 169, 172 | eqtri 2802 |
. . . . . . . . . . . . . 14
⊢ ∪ (𝑡
∪ {ℎ}) = (∪ 𝑡
∪ ℎ) |
174 | 173, 122 | syl5eqr 2828 |
. . . . . . . . . . . . 13
⊢ (∪ (𝑡
∪ {ℎ}) = 𝑎 → (∪ 𝑡
∪ ℎ) = 𝑎) |
175 | 174 | ad2antll 719 |
. . . . . . . . . . . 12
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → (∪ 𝑡
∪ ℎ) = 𝑎) |
176 | 90, 154, 168, 175 | mbfres2 23860 |
. . . . . . . . . . 11
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → (ℜ ∘ 𝑓) ∈ MblFn) |
177 | | imf 14266 |
. . . . . . . . . . . . . . 15
⊢
ℑ:ℂ⟶ℝ |
178 | | fco 6310 |
. . . . . . . . . . . . . . 15
⊢
((ℑ:ℂ⟶ℝ ∧ 𝑓:𝑎⟶ℂ) → (ℑ ∘
𝑓):𝑎⟶ℝ) |
179 | 177, 178 | mpan 680 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝑎⟶ℂ → (ℑ ∘ 𝑓):𝑎⟶ℝ) |
180 | 179 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → (ℑ ∘ 𝑓):𝑎⟶ℝ) |
181 | 180 | ad2antrl 718 |
. . . . . . . . . . . 12
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → (ℑ ∘ 𝑓):𝑎⟶ℝ) |
182 | | imcncf 23125 |
. . . . . . . . . . . . . . . . 17
⊢ ℑ
∈ (ℂ–cn→ℝ) |
183 | 182 | elexi 3415 |
. . . . . . . . . . . . . . . 16
⊢ ℑ
∈ V |
184 | 183, 93 | coex 7399 |
. . . . . . . . . . . . . . 15
⊢ (ℑ
∘ 𝑓) ∈
V |
185 | 184 | resex 5695 |
. . . . . . . . . . . . . 14
⊢ ((ℑ
∘ 𝑓) ↾ ∪ 𝑡)
∈ V |
186 | 98 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ∪ 𝑡 = 𝑏) |
187 | 186 | biantrud 527 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ↔ ((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏))) |
188 | | feq123 6283 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡
∧ ℂ = ℂ) → (𝑔:𝑏⟶ℂ ↔ ((ℑ ∘
𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ)) |
189 | 101, 188 | mp3an3 1523 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (𝑔:𝑏⟶ℂ ↔ ((ℑ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ)) |
190 | | reseq1 5638 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
→ (𝑔 ↾ 𝑠) = (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠)) |
191 | 190 | eleq1d 2844 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
→ ((𝑔 ↾ 𝑠) ∈ MblFn ↔ (((ℑ
∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn)) |
192 | 191 | adantr 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((𝑔 ↾ 𝑠) ∈ MblFn ↔ (((ℑ
∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn)) |
193 | 192 | ralbidv 3168 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (∀𝑠 ∈
𝑡 (𝑔 ↾ 𝑠) ∈ MblFn ↔ ∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠) ∈ MblFn)) |
194 | 189, 193 | anbi12d 624 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ↔ (((ℑ ∘
𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn))) |
195 | 187, 194 | bitr3d 273 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) ↔ (((ℑ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn))) |
196 | | eleq1 2847 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
→ (𝑔 ∈ MblFn
↔ ((ℑ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn)) |
197 | 196 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ (𝑔 ∈ MblFn
↔ ((ℑ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn)) |
198 | 195, 197 | imbi12d 336 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 = ((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
∧ 𝑏 = ∪ 𝑡)
→ ((((𝑔:𝑏⟶ℂ ∧
∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ↔
((((ℑ ∘ 𝑓)
↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℑ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn))) |
199 | 198 | spc2gv 3498 |
. . . . . . . . . . . . . 14
⊢
((((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ∈ V ∧ ∪ 𝑡
∈ V) → (∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) →
((((ℑ ∘ 𝑓)
↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℑ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn))) |
200 | 185, 96, 199 | mp2an 682 |
. . . . . . . . . . . . 13
⊢
(∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) →
((((ℑ ∘ 𝑓)
↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℑ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn)) |
201 | | fss 6306 |
. . . . . . . . . . . . . . . . . 18
⊢
((ℑ:ℂ⟶ℝ ∧ ℝ ⊆ ℂ) →
ℑ:ℂ⟶ℂ) |
202 | 177, 115,
201 | mp2an 682 |
. . . . . . . . . . . . . . . . 17
⊢
ℑ:ℂ⟶ℂ |
203 | | fco 6310 |
. . . . . . . . . . . . . . . . 17
⊢
((ℑ:ℂ⟶ℂ ∧ 𝑓:𝑎⟶ℂ) → (ℑ ∘
𝑓):𝑎⟶ℂ) |
204 | 202, 203 | mpan 680 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝑎⟶ℂ → (ℑ ∘ 𝑓):𝑎⟶ℂ) |
205 | | fssres 6322 |
. . . . . . . . . . . . . . . 16
⊢
(((ℑ ∘ 𝑓):𝑎⟶ℂ ∧ ∪ 𝑡
⊆ 𝑎) → ((ℑ
∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ) |
206 | 204, 123,
205 | syl2an 589 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝑎⟶ℂ ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → ((ℑ ∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ) |
207 | 206 | adantlr 705 |
. . . . . . . . . . . . . 14
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → ((ℑ ∘ 𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ) |
208 | 127 | resabs1d 5679 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 ∈ 𝑡 → (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) = ((ℑ ∘ 𝑓) ↾ 𝑟)) |
209 | | resco 5895 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℑ
∘ 𝑓) ↾ 𝑟) = (ℑ ∘ (𝑓 ↾ 𝑟)) |
210 | 208, 209 | syl6eq 2830 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ 𝑡 → (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) = (ℑ ∘ (𝑓 ↾ 𝑟))) |
211 | 210 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑟) = (ℑ
∘ (𝑓 ↾ 𝑟))) |
212 | 143 | simprd 491 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → (ℑ ∘ (𝑓 ↾ 𝑟)) ∈ MblFn) |
213 | 211, 212 | eqeltrd 2859 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ 𝑟 ∈ 𝑡) → (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑟) ∈
MblFn) |
214 | 213 | ralrimiva 3148 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → ∀𝑟 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) ∈ MblFn) |
215 | | reseq2 5639 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = 𝑠 → (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑟) = (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠)) |
216 | 215 | eleq1d 2844 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = 𝑠 → ((((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑟) ∈ MblFn
↔ (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠) ∈ MblFn)) |
217 | 216 | cbvralv 3367 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑟 ∈
𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑟) ∈ MblFn
↔ ∀𝑠 ∈
𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈
MblFn) |
218 | 214, 217 | sylib 210 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → ∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠) ∈ MblFn) |
219 | 218 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → ∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡) ↾ 𝑠) ∈ MblFn) |
220 | | pm2.27 42 |
. . . . . . . . . . . . . 14
⊢
((((ℑ ∘ 𝑓) ↾ ∪ 𝑡):∪
𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ (((((ℑ ∘ 𝑓) ↾ ∪ 𝑡):∪
𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℑ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn) → ((ℑ ∘
𝑓) ↾ ∪ 𝑡)
∈ MblFn)) |
221 | 207, 219,
220 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → (((((ℑ ∘
𝑓) ↾ ∪ 𝑡):∪ 𝑡⟶ℂ ∧
∀𝑠 ∈ 𝑡 (((ℑ ∘ 𝑓) ↾ ∪ 𝑡)
↾ 𝑠) ∈ MblFn)
→ ((ℑ ∘ 𝑓)
↾ ∪ 𝑡) ∈ MblFn) → ((ℑ ∘
𝑓) ↾ ∪ 𝑡)
∈ MblFn)) |
222 | 200, 221 | mpan9 502 |
. . . . . . . . . . . 12
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → ((ℑ ∘
𝑓) ↾ ∪ 𝑡)
∈ MblFn) |
223 | | resco 5895 |
. . . . . . . . . . . . . . 15
⊢ ((ℑ
∘ 𝑓) ↾ ℎ) = (ℑ ∘ (𝑓 ↾ ℎ)) |
224 | 164 | simplbda 495 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝑎⟶ℂ ∧ (𝑓 ↾ ℎ) ∈ MblFn) → (ℑ ∘ (𝑓 ↾ ℎ)) ∈ MblFn) |
225 | 223, 224 | syl5eqel 2863 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝑎⟶ℂ ∧ (𝑓 ↾ ℎ) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ ℎ) ∈ MblFn) |
226 | 160, 225 | sylan2 586 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → ((ℑ ∘
𝑓) ↾ ℎ) ∈ MblFn) |
227 | 226 | ad2antrl 718 |
. . . . . . . . . . . 12
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → ((ℑ ∘
𝑓) ↾ ℎ) ∈ MblFn) |
228 | 181, 222,
227, 175 | mbfres2 23860 |
. . . . . . . . . . 11
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → (ℑ ∘ 𝑓) ∈ MblFn) |
229 | | ismbfcn 23844 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝑎⟶ℂ → (𝑓 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ∈ MblFn ∧ (ℑ
∘ 𝑓) ∈
MblFn))) |
230 | 229 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) → (𝑓 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ∈ MblFn ∧ (ℑ
∘ 𝑓) ∈
MblFn))) |
231 | 230 | ad2antrl 718 |
. . . . . . . . . . 11
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → (𝑓 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ∈ MblFn ∧ (ℑ
∘ 𝑓) ∈
MblFn))) |
232 | 176, 228,
231 | mpbir2and 703 |
. . . . . . . . . 10
⊢
((∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎)) → 𝑓 ∈ MblFn) |
233 | 232 | ex 403 |
. . . . . . . . 9
⊢
(∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → 𝑓 ∈ MblFn)) |
234 | 233 | alrimivv 1971 |
. . . . . . . 8
⊢
(∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) →
∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → 𝑓 ∈ MblFn)) |
235 | 234 | a1i 11 |
. . . . . . 7
⊢ (𝑡 ∈ Fin →
(∀𝑔∀𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠 ∈ 𝑡 (𝑔 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑡 =
𝑏) → 𝑔 ∈ MblFn) →
∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {ℎ})(𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ (𝑡
∪ {ℎ}) = 𝑎) → 𝑓 ∈ MblFn))) |
236 | 36, 59, 66, 73, 85, 235 | findcard2 8490 |
. . . . . 6
⊢ (𝑆 ∈ Fin → ∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈ MblFn)) |
237 | | 2sp 2170 |
. . . . . 6
⊢
(∀𝑓∀𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈ MblFn) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈ MblFn)) |
238 | 4, 236, 237 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝑓 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝑎) → 𝑓 ∈ MblFn)) |
239 | 17, 26, 238 | vtocl2g 3471 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐹 ∈ V) → (𝜑 → (((𝐹:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝐹 ∈ MblFn))) |
240 | 11, 239 | mpcom 38 |
. . 3
⊢ (𝜑 → (((𝐹:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) ∧ ∪ 𝑆 =
𝐴) → 𝐹 ∈ MblFn)) |
241 | 3, 240 | mpan2d 684 |
. 2
⊢ (𝜑 → ((𝐹:𝐴⟶ℂ ∧ ∀𝑠 ∈ 𝑆 (𝐹 ↾ 𝑠) ∈ MblFn) → 𝐹 ∈ MblFn)) |
242 | 1, 2, 241 | mp2and 689 |
1
⊢ (𝜑 → 𝐹 ∈ MblFn) |