Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mbfresfi Structured version   Visualization version   GIF version

Theorem mbfresfi 34979
Description: Measurability of a piecewise function across arbitrarily many subsets. (Contributed by Brendan Leahy, 31-Mar-2018.)
Hypotheses
Ref Expression
mbfresfi.1 (𝜑𝐹:𝐴⟶ℂ)
mbfresfi.2 (𝜑𝑆 ∈ Fin)
mbfresfi.3 (𝜑 → ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn)
mbfresfi.4 (𝜑 𝑆 = 𝐴)
Assertion
Ref Expression
mbfresfi (𝜑𝐹 ∈ MblFn)
Distinct variable groups:   𝜑,𝑠   𝐴,𝑠   𝐹,𝑠   𝑆,𝑠

Proof of Theorem mbfresfi
Dummy variables 𝑎 𝑏 𝑓 𝑔 𝑟 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mbfresfi.1 . 2 (𝜑𝐹:𝐴⟶ℂ)
2 mbfresfi.3 . 2 (𝜑 → ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn)
3 mbfresfi.4 . . 3 (𝜑 𝑆 = 𝐴)
4 mbfresfi.2 . . . . . . 7 (𝜑𝑆 ∈ Fin)
54uniexd 7446 . . . . . 6 (𝜑 𝑆 ∈ V)
63, 5eqeltrrd 2912 . . . . 5 (𝜑𝐴 ∈ V)
7 fex 6965 . . . . . . 7 ((𝐹:𝐴⟶ℂ ∧ 𝐴 ∈ V) → 𝐹 ∈ V)
87ex 415 . . . . . 6 (𝐹:𝐴⟶ℂ → (𝐴 ∈ V → 𝐹 ∈ V))
91, 8syl 17 . . . . 5 (𝜑 → (𝐴 ∈ V → 𝐹 ∈ V))
106, 9jcai 519 . . . 4 (𝜑 → (𝐴 ∈ V ∧ 𝐹 ∈ V))
11 feq2 6472 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑓:𝑎⟶ℂ ↔ 𝑓:𝐴⟶ℂ))
1211anbi1d 631 . . . . . . . 8 (𝑎 = 𝐴 → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ↔ (𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn)))
13 eqeq2 2832 . . . . . . . 8 (𝑎 = 𝐴 → ( 𝑆 = 𝑎 𝑆 = 𝐴))
1412, 13anbi12d 632 . . . . . . 7 (𝑎 = 𝐴 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) ↔ ((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴)))
1514imbi1d 344 . . . . . 6 (𝑎 = 𝐴 → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝑓 ∈ MblFn)))
1615imbi2d 343 . . . . 5 (𝑎 = 𝐴 → ((𝜑 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn)) ↔ (𝜑 → (((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝑓 ∈ MblFn))))
17 feq1 6471 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓:𝐴⟶ℂ ↔ 𝐹:𝐴⟶ℂ))
18 reseq1 5823 . . . . . . . . . . 11 (𝑓 = 𝐹 → (𝑓𝑠) = (𝐹𝑠))
1918eleq1d 2895 . . . . . . . . . 10 (𝑓 = 𝐹 → ((𝑓𝑠) ∈ MblFn ↔ (𝐹𝑠) ∈ MblFn))
2019ralbidv 3184 . . . . . . . . 9 (𝑓 = 𝐹 → (∀𝑠𝑆 (𝑓𝑠) ∈ MblFn ↔ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn))
2117, 20anbi12d 632 . . . . . . . 8 (𝑓 = 𝐹 → ((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn)))
2221anbi1d 631 . . . . . . 7 (𝑓 = 𝐹 → (((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) ↔ ((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴)))
23 eleq1 2898 . . . . . . 7 (𝑓 = 𝐹 → (𝑓 ∈ MblFn ↔ 𝐹 ∈ MblFn))
2422, 23imbi12d 347 . . . . . 6 (𝑓 = 𝐹 → ((((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝑓 ∈ MblFn) ↔ (((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝐹 ∈ MblFn)))
2524imbi2d 343 . . . . 5 (𝑓 = 𝐹 → ((𝜑 → (((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝑓 ∈ MblFn)) ↔ (𝜑 → (((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝐹 ∈ MblFn))))
26 rzal 4429 . . . . . . . . . . . 12 (𝑟 = ∅ → ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn)
2726biantrud 534 . . . . . . . . . . 11 (𝑟 = ∅ → (𝑓:𝑎⟶ℂ ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn)))
2827bicomd 225 . . . . . . . . . 10 (𝑟 = ∅ → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ↔ 𝑓:𝑎⟶ℂ))
29 unieq 4825 . . . . . . . . . . . 12 (𝑟 = ∅ → 𝑟 = ∅)
30 uni0 4842 . . . . . . . . . . . 12 ∅ = ∅
3129, 30syl6eq 2871 . . . . . . . . . . 11 (𝑟 = ∅ → 𝑟 = ∅)
3231eqeq1d 2822 . . . . . . . . . 10 (𝑟 = ∅ → ( 𝑟 = 𝑎 ↔ ∅ = 𝑎))
3328, 32anbi12d 632 . . . . . . . . 9 (𝑟 = ∅ → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) ↔ (𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎)))
3433imbi1d 344 . . . . . . . 8 (𝑟 = ∅ → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn)))
35342albidv 1924 . . . . . . 7 (𝑟 = ∅ → (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑓𝑎((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn)))
36 raleq 3392 . . . . . . . . . . . 12 (𝑟 = 𝑡 → (∀𝑠𝑟 (𝑓𝑠) ∈ MblFn ↔ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn))
3736anbi2d 630 . . . . . . . . . . 11 (𝑟 = 𝑡 → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn)))
38 unieq 4825 . . . . . . . . . . . 12 (𝑟 = 𝑡 𝑟 = 𝑡)
3938eqeq1d 2822 . . . . . . . . . . 11 (𝑟 = 𝑡 → ( 𝑟 = 𝑎 𝑡 = 𝑎))
4037, 39anbi12d 632 . . . . . . . . . 10 (𝑟 = 𝑡 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) ↔ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎)))
4140imbi1d 344 . . . . . . . . 9 (𝑟 = 𝑡 → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎) → 𝑓 ∈ MblFn)))
42412albidv 1924 . . . . . . . 8 (𝑟 = 𝑡 → (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎) → 𝑓 ∈ MblFn)))
43 simpl 485 . . . . . . . . . . . . 13 ((𝑓 = 𝑔𝑎 = 𝑏) → 𝑓 = 𝑔)
44 simpr 487 . . . . . . . . . . . . 13 ((𝑓 = 𝑔𝑎 = 𝑏) → 𝑎 = 𝑏)
4543, 44feq12d 6478 . . . . . . . . . . . 12 ((𝑓 = 𝑔𝑎 = 𝑏) → (𝑓:𝑎⟶ℂ ↔ 𝑔:𝑏⟶ℂ))
46 reseq1 5823 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝑓𝑠) = (𝑔𝑠))
4746adantr 483 . . . . . . . . . . . . . 14 ((𝑓 = 𝑔𝑎 = 𝑏) → (𝑓𝑠) = (𝑔𝑠))
4847eleq1d 2895 . . . . . . . . . . . . 13 ((𝑓 = 𝑔𝑎 = 𝑏) → ((𝑓𝑠) ∈ MblFn ↔ (𝑔𝑠) ∈ MblFn))
4948ralbidv 3184 . . . . . . . . . . . 12 ((𝑓 = 𝑔𝑎 = 𝑏) → (∀𝑠𝑡 (𝑓𝑠) ∈ MblFn ↔ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn))
5045, 49anbi12d 632 . . . . . . . . . . 11 ((𝑓 = 𝑔𝑎 = 𝑏) → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ↔ (𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn)))
51 eqeq2 2832 . . . . . . . . . . . 12 (𝑎 = 𝑏 → ( 𝑡 = 𝑎 𝑡 = 𝑏))
5251adantl 484 . . . . . . . . . . 11 ((𝑓 = 𝑔𝑎 = 𝑏) → ( 𝑡 = 𝑎 𝑡 = 𝑏))
5350, 52anbi12d 632 . . . . . . . . . 10 ((𝑓 = 𝑔𝑎 = 𝑏) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎) ↔ ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏)))
54 eleq1 2898 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑓 ∈ MblFn ↔ 𝑔 ∈ MblFn))
5554adantr 483 . . . . . . . . . 10 ((𝑓 = 𝑔𝑎 = 𝑏) → (𝑓 ∈ MblFn ↔ 𝑔 ∈ MblFn))
5653, 55imbi12d 347 . . . . . . . . 9 ((𝑓 = 𝑔𝑎 = 𝑏) → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn)))
5756cbval2vw 2047 . . . . . . . 8 (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn))
5842, 57syl6bb 289 . . . . . . 7 (𝑟 = 𝑡 → (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn)))
59 raleq 3392 . . . . . . . . . . 11 (𝑟 = (𝑡 ∪ {}) → (∀𝑠𝑟 (𝑓𝑠) ∈ MblFn ↔ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn))
6059anbi2d 630 . . . . . . . . . 10 (𝑟 = (𝑡 ∪ {}) → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn)))
61 unieq 4825 . . . . . . . . . . 11 (𝑟 = (𝑡 ∪ {}) → 𝑟 = (𝑡 ∪ {}))
6261eqeq1d 2822 . . . . . . . . . 10 (𝑟 = (𝑡 ∪ {}) → ( 𝑟 = 𝑎 (𝑡 ∪ {}) = 𝑎))
6360, 62anbi12d 632 . . . . . . . . 9 (𝑟 = (𝑡 ∪ {}) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) ↔ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)))
6463imbi1d 344 . . . . . . . 8 (𝑟 = (𝑡 ∪ {}) → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → 𝑓 ∈ MblFn)))
65642albidv 1924 . . . . . . 7 (𝑟 = (𝑡 ∪ {}) → (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → 𝑓 ∈ MblFn)))
66 raleq 3392 . . . . . . . . . . 11 (𝑟 = 𝑆 → (∀𝑠𝑟 (𝑓𝑠) ∈ MblFn ↔ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn))
6766anbi2d 630 . . . . . . . . . 10 (𝑟 = 𝑆 → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn)))
68 unieq 4825 . . . . . . . . . . 11 (𝑟 = 𝑆 𝑟 = 𝑆)
6968eqeq1d 2822 . . . . . . . . . 10 (𝑟 = 𝑆 → ( 𝑟 = 𝑎 𝑆 = 𝑎))
7067, 69anbi12d 632 . . . . . . . . 9 (𝑟 = 𝑆 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) ↔ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎)))
7170imbi1d 344 . . . . . . . 8 (𝑟 = 𝑆 → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn)))
72712albidv 1924 . . . . . . 7 (𝑟 = 𝑆 → (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn)))
73 frel 6495 . . . . . . . . . 10 (𝑓:𝑎⟶ℂ → Rel 𝑓)
7473adantr 483 . . . . . . . . 9 ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → Rel 𝑓)
75 fdm 6498 . . . . . . . . . 10 (𝑓:𝑎⟶ℂ → dom 𝑓 = 𝑎)
76 eqcom 2827 . . . . . . . . . . 11 (∅ = 𝑎𝑎 = ∅)
7776biimpi 218 . . . . . . . . . 10 (∅ = 𝑎𝑎 = ∅)
7875, 77sylan9eq 2875 . . . . . . . . 9 ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → dom 𝑓 = ∅)
79 reldm0 5774 . . . . . . . . . . 11 (Rel 𝑓 → (𝑓 = ∅ ↔ dom 𝑓 = ∅))
8079biimpar 480 . . . . . . . . . 10 ((Rel 𝑓 ∧ dom 𝑓 = ∅) → 𝑓 = ∅)
81 mbf0 24217 . . . . . . . . . 10 ∅ ∈ MblFn
8280, 81eqeltrdi 2919 . . . . . . . . 9 ((Rel 𝑓 ∧ dom 𝑓 = ∅) → 𝑓 ∈ MblFn)
8374, 78, 82syl2anc 586 . . . . . . . 8 ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn)
8483gen2 1797 . . . . . . 7 𝑓𝑎((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn)
85 ref 14451 . . . . . . . . . . . . . . 15 ℜ:ℂ⟶ℝ
86 fco 6507 . . . . . . . . . . . . . . 15 ((ℜ:ℂ⟶ℝ ∧ 𝑓:𝑎⟶ℂ) → (ℜ ∘ 𝑓):𝑎⟶ℝ)
8785, 86mpan 688 . . . . . . . . . . . . . 14 (𝑓:𝑎⟶ℂ → (ℜ ∘ 𝑓):𝑎⟶ℝ)
8887adantr 483 . . . . . . . . . . . . 13 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → (ℜ ∘ 𝑓):𝑎⟶ℝ)
8988ad2antrl 726 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → (ℜ ∘ 𝑓):𝑎⟶ℝ)
90 recncf 23486 . . . . . . . . . . . . . . . . 17 ℜ ∈ (ℂ–cn→ℝ)
9190elexi 3492 . . . . . . . . . . . . . . . 16 ℜ ∈ V
92 vex 3476 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
9391, 92coex 7613 . . . . . . . . . . . . . . 15 (ℜ ∘ 𝑓) ∈ V
9493resex 5875 . . . . . . . . . . . . . 14 ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ V
95 vuniex 7443 . . . . . . . . . . . . . 14 𝑡 ∈ V
96 eqcom 2827 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑡 𝑡 = 𝑏)
9796biimpi 218 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑡 𝑡 = 𝑏)
9897adantl 484 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → 𝑡 = 𝑏)
9998biantrud 534 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ↔ ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏)))
100 eqid 2820 . . . . . . . . . . . . . . . . . . 19 ℂ = ℂ
101 feq123 6480 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡 ∧ ℂ = ℂ) → (𝑔:𝑏⟶ℂ ↔ ((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ))
102100, 101mp3an3 1446 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (𝑔:𝑏⟶ℂ ↔ ((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ))
103 reseq1 5823 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) → (𝑔𝑠) = (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠))
104103eleq1d 2895 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) → ((𝑔𝑠) ∈ MblFn ↔ (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
105104adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔𝑠) ∈ MblFn ↔ (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
106105ralbidv 3184 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (∀𝑠𝑡 (𝑔𝑠) ∈ MblFn ↔ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
107102, 106anbi12d 632 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ↔ (((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)))
10899, 107bitr3d 283 . . . . . . . . . . . . . . . 16 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) ↔ (((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)))
109 eleq1 2898 . . . . . . . . . . . . . . . . 17 (𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) → (𝑔 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
110109adantr 483 . . . . . . . . . . . . . . . 16 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (𝑔 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
111108, 110imbi12d 347 . . . . . . . . . . . . . . 15 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ↔ ((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)))
112111spc2gv 3580 . . . . . . . . . . . . . 14 ((((ℜ ∘ 𝑓) ↾ 𝑡) ∈ V ∧ 𝑡 ∈ V) → (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)))
11394, 95, 112mp2an 690 . . . . . . . . . . . . 13 (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
114 ax-resscn 10572 . . . . . . . . . . . . . . . . . 18 ℝ ⊆ ℂ
115 fss 6503 . . . . . . . . . . . . . . . . . 18 ((ℜ:ℂ⟶ℝ ∧ ℝ ⊆ ℂ) → ℜ:ℂ⟶ℂ)
11685, 114, 115mp2an 690 . . . . . . . . . . . . . . . . 17 ℜ:ℂ⟶ℂ
117 fco 6507 . . . . . . . . . . . . . . . . 17 ((ℜ:ℂ⟶ℂ ∧ 𝑓:𝑎⟶ℂ) → (ℜ ∘ 𝑓):𝑎⟶ℂ)
118116, 117mpan 688 . . . . . . . . . . . . . . . 16 (𝑓:𝑎⟶ℂ → (ℜ ∘ 𝑓):𝑎⟶ℂ)
119 ssun1 4127 . . . . . . . . . . . . . . . . . 18 𝑡 ⊆ (𝑡 ∪ {})
120119unissi 4823 . . . . . . . . . . . . . . . . 17 𝑡 (𝑡 ∪ {})
121 id 22 . . . . . . . . . . . . . . . . 17 ( (𝑡 ∪ {}) = 𝑎 (𝑡 ∪ {}) = 𝑎)
122120, 121sseqtrid 3998 . . . . . . . . . . . . . . . 16 ( (𝑡 ∪ {}) = 𝑎 𝑡𝑎)
123 fssres 6520 . . . . . . . . . . . . . . . 16 (((ℜ ∘ 𝑓):𝑎⟶ℂ ∧ 𝑡𝑎) → ((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
124118, 122, 123syl2an 597 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ (𝑡 ∪ {}) = 𝑎) → ((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
125124adantlr 713 . . . . . . . . . . . . . 14 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → ((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
126 elssuni 4844 . . . . . . . . . . . . . . . . . . . . 21 (𝑟𝑡𝑟 𝑡)
127126resabs1d 5860 . . . . . . . . . . . . . . . . . . . 20 (𝑟𝑡 → (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = ((ℜ ∘ 𝑓) ↾ 𝑟))
128 resco 6079 . . . . . . . . . . . . . . . . . . . 20 ((ℜ ∘ 𝑓) ↾ 𝑟) = (ℜ ∘ (𝑓𝑟))
129127, 128syl6eq 2871 . . . . . . . . . . . . . . . . . . 19 (𝑟𝑡 → (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (ℜ ∘ (𝑓𝑟)))
130129adantl 484 . . . . . . . . . . . . . . . . . 18 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (ℜ ∘ (𝑓𝑟)))
131 elun1 4131 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟𝑡𝑟 ∈ (𝑡 ∪ {}))
132 reseq2 5824 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = 𝑟 → (𝑓𝑠) = (𝑓𝑟))
133132eleq1d 2895 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = 𝑟 → ((𝑓𝑠) ∈ MblFn ↔ (𝑓𝑟) ∈ MblFn))
134133rspccva 3601 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn ∧ 𝑟 ∈ (𝑡 ∪ {})) → (𝑓𝑟) ∈ MblFn)
135131, 134sylan2 594 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn ∧ 𝑟𝑡) → (𝑓𝑟) ∈ MblFn)
136135adantll 712 . . . . . . . . . . . . . . . . . . . 20 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (𝑓𝑟) ∈ MblFn)
137 fresin 6523 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:𝑎⟶ℂ → (𝑓𝑟):(𝑎𝑟)⟶ℂ)
138 ismbfcn 24212 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑟):(𝑎𝑟)⟶ℂ → ((𝑓𝑟) ∈ MblFn ↔ ((ℜ ∘ (𝑓𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓𝑟)) ∈ MblFn)))
139137, 138syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:𝑎⟶ℂ → ((𝑓𝑟) ∈ MblFn ↔ ((ℜ ∘ (𝑓𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓𝑟)) ∈ MblFn)))
140139biimpd 231 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:𝑎⟶ℂ → ((𝑓𝑟) ∈ MblFn → ((ℜ ∘ (𝑓𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓𝑟)) ∈ MblFn)))
141140ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → ((𝑓𝑟) ∈ MblFn → ((ℜ ∘ (𝑓𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓𝑟)) ∈ MblFn)))
142136, 141mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → ((ℜ ∘ (𝑓𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓𝑟)) ∈ MblFn))
143142simpld 497 . . . . . . . . . . . . . . . . . 18 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (ℜ ∘ (𝑓𝑟)) ∈ MblFn)
144130, 143eqeltrd 2911 . . . . . . . . . . . . . . . . 17 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn)
145144ralrimiva 3169 . . . . . . . . . . . . . . . 16 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ∀𝑟𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn)
146 reseq2 5824 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑠 → (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠))
147146eleq1d 2895 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑠 → ((((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn ↔ (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
148147cbvralvw 3428 . . . . . . . . . . . . . . . 16 (∀𝑟𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn ↔ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
149145, 148sylib 220 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
150149adantr 483 . . . . . . . . . . . . . 14 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
151 pm2.27 42 . . . . . . . . . . . . . 14 ((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → (((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
152125, 150, 151syl2anc 586 . . . . . . . . . . . . 13 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → (((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
153113, 152mpan9 509 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)
154 vsnid 4578 . . . . . . . . . . . . . . 15 ∈ {}
155 elun2 4132 . . . . . . . . . . . . . . 15 ( ∈ {} → ∈ (𝑡 ∪ {}))
156 reseq2 5824 . . . . . . . . . . . . . . . . 17 (𝑠 = → (𝑓𝑠) = (𝑓))
157156eleq1d 2895 . . . . . . . . . . . . . . . 16 (𝑠 = → ((𝑓𝑠) ∈ MblFn ↔ (𝑓) ∈ MblFn))
158157rspcv 3597 . . . . . . . . . . . . . . 15 ( ∈ (𝑡 ∪ {}) → (∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn → (𝑓) ∈ MblFn))
159154, 155, 158mp2b 10 . . . . . . . . . . . . . 14 (∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn → (𝑓) ∈ MblFn)
160 resco 6079 . . . . . . . . . . . . . . 15 ((ℜ ∘ 𝑓) ↾ ) = (ℜ ∘ (𝑓))
161 fresin 6523 . . . . . . . . . . . . . . . . 17 (𝑓:𝑎⟶ℂ → (𝑓):(𝑎)⟶ℂ)
162 ismbfcn 24212 . . . . . . . . . . . . . . . . 17 ((𝑓):(𝑎)⟶ℂ → ((𝑓) ∈ MblFn ↔ ((ℜ ∘ (𝑓)) ∈ MblFn ∧ (ℑ ∘ (𝑓)) ∈ MblFn)))
163161, 162syl 17 . . . . . . . . . . . . . . . 16 (𝑓:𝑎⟶ℂ → ((𝑓) ∈ MblFn ↔ ((ℜ ∘ (𝑓)) ∈ MblFn ∧ (ℑ ∘ (𝑓)) ∈ MblFn)))
164163simprbda 501 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ (𝑓) ∈ MblFn) → (ℜ ∘ (𝑓)) ∈ MblFn)
165160, 164eqeltrid 2915 . . . . . . . . . . . . . 14 ((𝑓:𝑎⟶ℂ ∧ (𝑓) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ ) ∈ MblFn)
166159, 165sylan2 594 . . . . . . . . . . . . 13 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ ) ∈ MblFn)
167166ad2antrl 726 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → ((ℜ ∘ 𝑓) ↾ ) ∈ MblFn)
168 uniun 4837 . . . . . . . . . . . . . . 15 (𝑡 ∪ {}) = ( 𝑡 {})
169 vex 3476 . . . . . . . . . . . . . . . . 17 ∈ V
170169unisn 4834 . . . . . . . . . . . . . . . 16 {} =
171170uneq2i 4115 . . . . . . . . . . . . . . 15 ( 𝑡 {}) = ( 𝑡)
172168, 171eqtri 2843 . . . . . . . . . . . . . 14 (𝑡 ∪ {}) = ( 𝑡)
173172, 121syl5eqr 2869 . . . . . . . . . . . . 13 ( (𝑡 ∪ {}) = 𝑎 → ( 𝑡) = 𝑎)
174173ad2antll 727 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → ( 𝑡) = 𝑎)
17589, 153, 167, 174mbfres2 24228 . . . . . . . . . . 11 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → (ℜ ∘ 𝑓) ∈ MblFn)
176 imf 14452 . . . . . . . . . . . . . . 15 ℑ:ℂ⟶ℝ
177 fco 6507 . . . . . . . . . . . . . . 15 ((ℑ:ℂ⟶ℝ ∧ 𝑓:𝑎⟶ℂ) → (ℑ ∘ 𝑓):𝑎⟶ℝ)
178176, 177mpan 688 . . . . . . . . . . . . . 14 (𝑓:𝑎⟶ℂ → (ℑ ∘ 𝑓):𝑎⟶ℝ)
179178adantr 483 . . . . . . . . . . . . 13 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → (ℑ ∘ 𝑓):𝑎⟶ℝ)
180179ad2antrl 726 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → (ℑ ∘ 𝑓):𝑎⟶ℝ)
181 imcncf 23487 . . . . . . . . . . . . . . . . 17 ℑ ∈ (ℂ–cn→ℝ)
182181elexi 3492 . . . . . . . . . . . . . . . 16 ℑ ∈ V
183182, 92coex 7613 . . . . . . . . . . . . . . 15 (ℑ ∘ 𝑓) ∈ V
184183resex 5875 . . . . . . . . . . . . . 14 ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ V
18597adantl 484 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → 𝑡 = 𝑏)
186185biantrud 534 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ↔ ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏)))
187 feq123 6480 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡 ∧ ℂ = ℂ) → (𝑔:𝑏⟶ℂ ↔ ((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ))
188100, 187mp3an3 1446 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (𝑔:𝑏⟶ℂ ↔ ((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ))
189 reseq1 5823 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) → (𝑔𝑠) = (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠))
190189eleq1d 2895 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) → ((𝑔𝑠) ∈ MblFn ↔ (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
191190adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔𝑠) ∈ MblFn ↔ (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
192191ralbidv 3184 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (∀𝑠𝑡 (𝑔𝑠) ∈ MblFn ↔ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
193188, 192anbi12d 632 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ↔ (((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)))
194186, 193bitr3d 283 . . . . . . . . . . . . . . . 16 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) ↔ (((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)))
195 eleq1 2898 . . . . . . . . . . . . . . . . 17 (𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) → (𝑔 ∈ MblFn ↔ ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
196195adantr 483 . . . . . . . . . . . . . . . 16 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (𝑔 ∈ MblFn ↔ ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
197194, 196imbi12d 347 . . . . . . . . . . . . . . 15 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ↔ ((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)))
198197spc2gv 3580 . . . . . . . . . . . . . 14 ((((ℑ ∘ 𝑓) ↾ 𝑡) ∈ V ∧ 𝑡 ∈ V) → (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)))
199184, 95, 198mp2an 690 . . . . . . . . . . . . 13 (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
200 fss 6503 . . . . . . . . . . . . . . . . . 18 ((ℑ:ℂ⟶ℝ ∧ ℝ ⊆ ℂ) → ℑ:ℂ⟶ℂ)
201176, 114, 200mp2an 690 . . . . . . . . . . . . . . . . 17 ℑ:ℂ⟶ℂ
202 fco 6507 . . . . . . . . . . . . . . . . 17 ((ℑ:ℂ⟶ℂ ∧ 𝑓:𝑎⟶ℂ) → (ℑ ∘ 𝑓):𝑎⟶ℂ)
203201, 202mpan 688 . . . . . . . . . . . . . . . 16 (𝑓:𝑎⟶ℂ → (ℑ ∘ 𝑓):𝑎⟶ℂ)
204 fssres 6520 . . . . . . . . . . . . . . . 16 (((ℑ ∘ 𝑓):𝑎⟶ℂ ∧ 𝑡𝑎) → ((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
205203, 122, 204syl2an 597 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ (𝑡 ∪ {}) = 𝑎) → ((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
206205adantlr 713 . . . . . . . . . . . . . 14 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → ((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
207126resabs1d 5860 . . . . . . . . . . . . . . . . . . . 20 (𝑟𝑡 → (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = ((ℑ ∘ 𝑓) ↾ 𝑟))
208 resco 6079 . . . . . . . . . . . . . . . . . . . 20 ((ℑ ∘ 𝑓) ↾ 𝑟) = (ℑ ∘ (𝑓𝑟))
209207, 208syl6eq 2871 . . . . . . . . . . . . . . . . . . 19 (𝑟𝑡 → (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (ℑ ∘ (𝑓𝑟)))
210209adantl 484 . . . . . . . . . . . . . . . . . 18 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (ℑ ∘ (𝑓𝑟)))
211142simprd 498 . . . . . . . . . . . . . . . . . 18 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (ℑ ∘ (𝑓𝑟)) ∈ MblFn)
212210, 211eqeltrd 2911 . . . . . . . . . . . . . . . . 17 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn)
213212ralrimiva 3169 . . . . . . . . . . . . . . . 16 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ∀𝑟𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn)
214 reseq2 5824 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑠 → (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠))
215214eleq1d 2895 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑠 → ((((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn ↔ (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
216215cbvralvw 3428 . . . . . . . . . . . . . . . 16 (∀𝑟𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn ↔ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
217213, 216sylib 220 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
218217adantr 483 . . . . . . . . . . . . . 14 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
219 pm2.27 42 . . . . . . . . . . . . . 14 ((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → (((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
220206, 218, 219syl2anc 586 . . . . . . . . . . . . 13 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → (((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
221199, 220mpan9 509 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)
222 resco 6079 . . . . . . . . . . . . . . 15 ((ℑ ∘ 𝑓) ↾ ) = (ℑ ∘ (𝑓))
223163simplbda 502 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ (𝑓) ∈ MblFn) → (ℑ ∘ (𝑓)) ∈ MblFn)
224222, 223eqeltrid 2915 . . . . . . . . . . . . . 14 ((𝑓:𝑎⟶ℂ ∧ (𝑓) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ ) ∈ MblFn)
225159, 224sylan2 594 . . . . . . . . . . . . 13 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ ) ∈ MblFn)
226225ad2antrl 726 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → ((ℑ ∘ 𝑓) ↾ ) ∈ MblFn)
227180, 221, 226, 174mbfres2 24228 . . . . . . . . . . 11 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → (ℑ ∘ 𝑓) ∈ MblFn)
228 ismbfcn 24212 . . . . . . . . . . . . 13 (𝑓:𝑎⟶ℂ → (𝑓 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ∈ MblFn ∧ (ℑ ∘ 𝑓) ∈ MblFn)))
229228adantr 483 . . . . . . . . . . . 12 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → (𝑓 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ∈ MblFn ∧ (ℑ ∘ 𝑓) ∈ MblFn)))
230229ad2antrl 726 . . . . . . . . . . 11 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → (𝑓 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ∈ MblFn ∧ (ℑ ∘ 𝑓) ∈ MblFn)))
231175, 227, 230mpbir2and 711 . . . . . . . . . 10 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → 𝑓 ∈ MblFn)
232231ex 415 . . . . . . . . 9 (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → 𝑓 ∈ MblFn))
233232alrimivv 1929 . . . . . . . 8 (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → 𝑓 ∈ MblFn))
234233a1i 11 . . . . . . 7 (𝑡 ∈ Fin → (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → 𝑓 ∈ MblFn)))
23535, 58, 65, 72, 84, 234findcard2 8736 . . . . . 6 (𝑆 ∈ Fin → ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn))
236 2sp 2185 . . . . . 6 (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn))
2374, 235, 2363syl 18 . . . . 5 (𝜑 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn))
23816, 25, 237vtocl2g 3551 . . . 4 ((𝐴 ∈ V ∧ 𝐹 ∈ V) → (𝜑 → (((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝐹 ∈ MblFn)))
23910, 238mpcom 38 . . 3 (𝜑 → (((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝐹 ∈ MblFn))
2403, 239mpan2d 692 . 2 (𝜑 → ((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) → 𝐹 ∈ MblFn))
2411, 2, 240mp2and 697 1 (𝜑𝐹 ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  wal 1535   = wceq 1537  wcel 2114  wral 3125  Vcvv 3473  cun 3911  cin 3912  wss 3913  c0 4269  {csn 4543   cuni 4814  dom cdm 5531  cres 5533  ccom 5535  Rel wrel 5536  wf 6327  (class class class)co 7133  Fincfn 8487  cc 10513  cr 10514  cre 14436  cim 14437  cnccncf 23460  MblFncmbf 24197
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-inf2 9082  ax-cnex 10571  ax-resscn 10572  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-addrcl 10576  ax-mulcl 10577  ax-mulrcl 10578  ax-mulcom 10579  ax-addass 10580  ax-mulass 10581  ax-distr 10582  ax-i2m1 10583  ax-1ne0 10584  ax-1rid 10585  ax-rnegex 10586  ax-rrecex 10587  ax-cnre 10588  ax-pre-lttri 10589  ax-pre-lttrn 10590  ax-pre-ltadd 10591  ax-pre-mulgt0 10592  ax-pre-sup 10593
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-int 4853  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-se 5491  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-isom 6340  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-of 7387  df-om 7559  df-1st 7667  df-2nd 7668  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-1o 8080  df-2o 8081  df-oadd 8084  df-er 8267  df-map 8386  df-pm 8387  df-en 8488  df-dom 8489  df-sdom 8490  df-fin 8491  df-sup 8884  df-inf 8885  df-oi 8952  df-dju 9308  df-card 9346  df-pnf 10655  df-mnf 10656  df-xr 10657  df-ltxr 10658  df-le 10659  df-sub 10850  df-neg 10851  df-div 11276  df-nn 11617  df-2 11679  df-3 11680  df-n0 11877  df-z 11961  df-uz 12223  df-q 12328  df-rp 12369  df-xadd 12487  df-ioo 12721  df-ico 12723  df-icc 12724  df-fz 12877  df-fzo 13018  df-fl 13146  df-seq 13354  df-exp 13415  df-hash 13676  df-cj 14438  df-re 14439  df-im 14440  df-sqrt 14574  df-abs 14575  df-clim 14825  df-sum 15023  df-xmet 20514  df-met 20515  df-cncf 23462  df-ovol 24047  df-vol 24048  df-mbf 24202
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator