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 34090
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)
5 uniexg 7234 . . . . . . 7 (𝑆 ∈ Fin → 𝑆 ∈ V)
64, 5syl 17 . . . . . 6 (𝜑 𝑆 ∈ V)
73, 6eqeltrrd 2860 . . . . 5 (𝜑𝐴 ∈ V)
8 fex 6763 . . . . . . 7 ((𝐹:𝐴⟶ℂ ∧ 𝐴 ∈ V) → 𝐹 ∈ V)
98ex 403 . . . . . 6 (𝐹:𝐴⟶ℂ → (𝐴 ∈ V → 𝐹 ∈ V))
101, 9syl 17 . . . . 5 (𝜑 → (𝐴 ∈ V → 𝐹 ∈ V))
117, 10jcai 512 . . . 4 (𝜑 → (𝐴 ∈ V ∧ 𝐹 ∈ V))
12 feq2 6275 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑓:𝑎⟶ℂ ↔ 𝑓:𝐴⟶ℂ))
1312anbi1d 623 . . . . . . . 8 (𝑎 = 𝐴 → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ↔ (𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn)))
14 eqeq2 2789 . . . . . . . 8 (𝑎 = 𝐴 → ( 𝑆 = 𝑎 𝑆 = 𝐴))
1513, 14anbi12d 624 . . . . . . 7 (𝑎 = 𝐴 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) ↔ ((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴)))
1615imbi1d 333 . . . . . 6 (𝑎 = 𝐴 → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝑓 ∈ MblFn)))
1716imbi2d 332 . . . . 5 (𝑎 = 𝐴 → ((𝜑 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn)) ↔ (𝜑 → (((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝑓 ∈ MblFn))))
18 feq1 6274 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓:𝐴⟶ℂ ↔ 𝐹:𝐴⟶ℂ))
19 reseq1 5638 . . . . . . . . . . 11 (𝑓 = 𝐹 → (𝑓𝑠) = (𝐹𝑠))
2019eleq1d 2844 . . . . . . . . . 10 (𝑓 = 𝐹 → ((𝑓𝑠) ∈ MblFn ↔ (𝐹𝑠) ∈ MblFn))
2120ralbidv 3168 . . . . . . . . 9 (𝑓 = 𝐹 → (∀𝑠𝑆 (𝑓𝑠) ∈ MblFn ↔ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn))
2218, 21anbi12d 624 . . . . . . . 8 (𝑓 = 𝐹 → ((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn)))
2322anbi1d 623 . . . . . . 7 (𝑓 = 𝐹 → (((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) ↔ ((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴)))
24 eleq1 2847 . . . . . . 7 (𝑓 = 𝐹 → (𝑓 ∈ MblFn ↔ 𝐹 ∈ MblFn))
2523, 24imbi12d 336 . . . . . 6 (𝑓 = 𝐹 → ((((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝑓 ∈ MblFn) ↔ (((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝐹 ∈ MblFn)))
2625imbi2d 332 . . . . 5 (𝑓 = 𝐹 → ((𝜑 → (((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝑓 ∈ MblFn)) ↔ (𝜑 → (((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝐹 ∈ MblFn))))
27 rzal 4296 . . . . . . . . . . . 12 (𝑟 = ∅ → ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn)
2827biantrud 527 . . . . . . . . . . 11 (𝑟 = ∅ → (𝑓:𝑎⟶ℂ ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn)))
2928bicomd 215 . . . . . . . . . 10 (𝑟 = ∅ → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ↔ 𝑓:𝑎⟶ℂ))
30 unieq 4681 . . . . . . . . . . . 12 (𝑟 = ∅ → 𝑟 = ∅)
31 uni0 4702 . . . . . . . . . . . 12 ∅ = ∅
3230, 31syl6eq 2830 . . . . . . . . . . 11 (𝑟 = ∅ → 𝑟 = ∅)
3332eqeq1d 2780 . . . . . . . . . 10 (𝑟 = ∅ → ( 𝑟 = 𝑎 ↔ ∅ = 𝑎))
3429, 33anbi12d 624 . . . . . . . . 9 (𝑟 = ∅ → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) ↔ (𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎)))
3534imbi1d 333 . . . . . . . 8 (𝑟 = ∅ → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn)))
36352albidv 1966 . . . . . . 7 (𝑟 = ∅ → (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑓𝑎((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn)))
37 raleq 3330 . . . . . . . . . . . 12 (𝑟 = 𝑡 → (∀𝑠𝑟 (𝑓𝑠) ∈ MblFn ↔ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn))
3837anbi2d 622 . . . . . . . . . . 11 (𝑟 = 𝑡 → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn)))
39 unieq 4681 . . . . . . . . . . . 12 (𝑟 = 𝑡 𝑟 = 𝑡)
4039eqeq1d 2780 . . . . . . . . . . 11 (𝑟 = 𝑡 → ( 𝑟 = 𝑎 𝑡 = 𝑎))
4138, 40anbi12d 624 . . . . . . . . . 10 (𝑟 = 𝑡 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) ↔ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎)))
4241imbi1d 333 . . . . . . . . 9 (𝑟 = 𝑡 → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎) → 𝑓 ∈ MblFn)))
43422albidv 1966 . . . . . . . 8 (𝑟 = 𝑡 → (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎) → 𝑓 ∈ MblFn)))
44 simpl 476 . . . . . . . . . . . . 13 ((𝑓 = 𝑔𝑎 = 𝑏) → 𝑓 = 𝑔)
45 simpr 479 . . . . . . . . . . . . 13 ((𝑓 = 𝑔𝑎 = 𝑏) → 𝑎 = 𝑏)
4644, 45feq12d 6281 . . . . . . . . . . . 12 ((𝑓 = 𝑔𝑎 = 𝑏) → (𝑓:𝑎⟶ℂ ↔ 𝑔:𝑏⟶ℂ))
47 reseq1 5638 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝑓𝑠) = (𝑔𝑠))
4847adantr 474 . . . . . . . . . . . . . 14 ((𝑓 = 𝑔𝑎 = 𝑏) → (𝑓𝑠) = (𝑔𝑠))
4948eleq1d 2844 . . . . . . . . . . . . 13 ((𝑓 = 𝑔𝑎 = 𝑏) → ((𝑓𝑠) ∈ MblFn ↔ (𝑔𝑠) ∈ MblFn))
5049ralbidv 3168 . . . . . . . . . . . 12 ((𝑓 = 𝑔𝑎 = 𝑏) → (∀𝑠𝑡 (𝑓𝑠) ∈ MblFn ↔ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn))
5146, 50anbi12d 624 . . . . . . . . . . 11 ((𝑓 = 𝑔𝑎 = 𝑏) → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ↔ (𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn)))
52 eqeq2 2789 . . . . . . . . . . . 12 (𝑎 = 𝑏 → ( 𝑡 = 𝑎 𝑡 = 𝑏))
5352adantl 475 . . . . . . . . . . 11 ((𝑓 = 𝑔𝑎 = 𝑏) → ( 𝑡 = 𝑎 𝑡 = 𝑏))
5451, 53anbi12d 624 . . . . . . . . . 10 ((𝑓 = 𝑔𝑎 = 𝑏) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎) ↔ ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏)))
55 eleq1 2847 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑓 ∈ MblFn ↔ 𝑔 ∈ MblFn))
5655adantr 474 . . . . . . . . . 10 ((𝑓 = 𝑔𝑎 = 𝑏) → (𝑓 ∈ MblFn ↔ 𝑔 ∈ MblFn))
5754, 56imbi12d 336 . . . . . . . . 9 ((𝑓 = 𝑔𝑎 = 𝑏) → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn)))
5857cbval2v 2378 . . . . . . . 8 (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn))
5943, 58syl6bb 279 . . . . . . 7 (𝑟 = 𝑡 → (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn)))
60 raleq 3330 . . . . . . . . . . 11 (𝑟 = (𝑡 ∪ {}) → (∀𝑠𝑟 (𝑓𝑠) ∈ MblFn ↔ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn))
6160anbi2d 622 . . . . . . . . . 10 (𝑟 = (𝑡 ∪ {}) → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn)))
62 unieq 4681 . . . . . . . . . . 11 (𝑟 = (𝑡 ∪ {}) → 𝑟 = (𝑡 ∪ {}))
6362eqeq1d 2780 . . . . . . . . . 10 (𝑟 = (𝑡 ∪ {}) → ( 𝑟 = 𝑎 (𝑡 ∪ {}) = 𝑎))
6461, 63anbi12d 624 . . . . . . . . 9 (𝑟 = (𝑡 ∪ {}) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) ↔ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)))
6564imbi1d 333 . . . . . . . 8 (𝑟 = (𝑡 ∪ {}) → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → 𝑓 ∈ MblFn)))
66652albidv 1966 . . . . . . 7 (𝑟 = (𝑡 ∪ {}) → (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → 𝑓 ∈ MblFn)))
67 raleq 3330 . . . . . . . . . . 11 (𝑟 = 𝑆 → (∀𝑠𝑟 (𝑓𝑠) ∈ MblFn ↔ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn))
6867anbi2d 622 . . . . . . . . . 10 (𝑟 = 𝑆 → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn)))
69 unieq 4681 . . . . . . . . . . 11 (𝑟 = 𝑆 𝑟 = 𝑆)
7069eqeq1d 2780 . . . . . . . . . 10 (𝑟 = 𝑆 → ( 𝑟 = 𝑎 𝑆 = 𝑎))
7168, 70anbi12d 624 . . . . . . . . 9 (𝑟 = 𝑆 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) ↔ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎)))
7271imbi1d 333 . . . . . . . 8 (𝑟 = 𝑆 → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn)))
73722albidv 1966 . . . . . . 7 (𝑟 = 𝑆 → (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn)))
74 frel 6298 . . . . . . . . . 10 (𝑓:𝑎⟶ℂ → Rel 𝑓)
7574adantr 474 . . . . . . . . 9 ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → Rel 𝑓)
76 fdm 6301 . . . . . . . . . 10 (𝑓:𝑎⟶ℂ → dom 𝑓 = 𝑎)
77 eqcom 2785 . . . . . . . . . . 11 (∅ = 𝑎𝑎 = ∅)
7877biimpi 208 . . . . . . . . . 10 (∅ = 𝑎𝑎 = ∅)
7976, 78sylan9eq 2834 . . . . . . . . 9 ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → dom 𝑓 = ∅)
80 reldm0 5590 . . . . . . . . . . 11 (Rel 𝑓 → (𝑓 = ∅ ↔ dom 𝑓 = ∅))
8180biimpar 471 . . . . . . . . . 10 ((Rel 𝑓 ∧ dom 𝑓 = ∅) → 𝑓 = ∅)
82 mbf0 23849 . . . . . . . . . 10 ∅ ∈ MblFn
8381, 82syl6eqel 2867 . . . . . . . . 9 ((Rel 𝑓 ∧ dom 𝑓 = ∅) → 𝑓 ∈ MblFn)
8475, 79, 83syl2anc 579 . . . . . . . 8 ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn)
8584gen2 1840 . . . . . . 7 𝑓𝑎((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn)
86 ref 14265 . . . . . . . . . . . . . . 15 ℜ:ℂ⟶ℝ
87 fco 6310 . . . . . . . . . . . . . . 15 ((ℜ:ℂ⟶ℝ ∧ 𝑓:𝑎⟶ℂ) → (ℜ ∘ 𝑓):𝑎⟶ℝ)
8886, 87mpan 680 . . . . . . . . . . . . . 14 (𝑓:𝑎⟶ℂ → (ℜ ∘ 𝑓):𝑎⟶ℝ)
8988adantr 474 . . . . . . . . . . . . 13 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → (ℜ ∘ 𝑓):𝑎⟶ℝ)
9089ad2antrl 718 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → (ℜ ∘ 𝑓):𝑎⟶ℝ)
91 recncf 23124 . . . . . . . . . . . . . . . . 17 ℜ ∈ (ℂ–cn→ℝ)
9291elexi 3415 . . . . . . . . . . . . . . . 16 ℜ ∈ V
93 vex 3401 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
9492, 93coex 7399 . . . . . . . . . . . . . . 15 (ℜ ∘ 𝑓) ∈ V
9594resex 5695 . . . . . . . . . . . . . 14 ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ V
96 vuniex 7233 . . . . . . . . . . . . . 14 𝑡 ∈ V
97 eqcom 2785 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑡 𝑡 = 𝑏)
9897biimpi 208 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑡 𝑡 = 𝑏)
9998adantl 475 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → 𝑡 = 𝑏)
10099biantrud 527 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ↔ ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏)))
101 eqid 2778 . . . . . . . . . . . . . . . . . . 19 ℂ = ℂ
102 feq123 6283 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡 ∧ ℂ = ℂ) → (𝑔:𝑏⟶ℂ ↔ ((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ))
103101, 102mp3an3 1523 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (𝑔:𝑏⟶ℂ ↔ ((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ))
104 reseq1 5638 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) → (𝑔𝑠) = (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠))
105104eleq1d 2844 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) → ((𝑔𝑠) ∈ MblFn ↔ (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
106105adantr 474 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔𝑠) ∈ MblFn ↔ (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
107106ralbidv 3168 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (∀𝑠𝑡 (𝑔𝑠) ∈ MblFn ↔ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
108103, 107anbi12d 624 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ↔ (((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)))
109100, 108bitr3d 273 . . . . . . . . . . . . . . . 16 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) ↔ (((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)))
110 eleq1 2847 . . . . . . . . . . . . . . . . 17 (𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) → (𝑔 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
111110adantr 474 . . . . . . . . . . . . . . . 16 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (𝑔 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
112109, 111imbi12d 336 . . . . . . . . . . . . . . 15 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ↔ ((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)))
113112spc2gv 3498 . . . . . . . . . . . . . 14 ((((ℜ ∘ 𝑓) ↾ 𝑡) ∈ V ∧ 𝑡 ∈ V) → (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)))
11495, 96, 113mp2an 682 . . . . . . . . . . . . 13 (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
115 ax-resscn 10331 . . . . . . . . . . . . . . . . . 18 ℝ ⊆ ℂ
116 fss 6306 . . . . . . . . . . . . . . . . . 18 ((ℜ:ℂ⟶ℝ ∧ ℝ ⊆ ℂ) → ℜ:ℂ⟶ℂ)
11786, 115, 116mp2an 682 . . . . . . . . . . . . . . . . 17 ℜ:ℂ⟶ℂ
118 fco 6310 . . . . . . . . . . . . . . . . 17 ((ℜ:ℂ⟶ℂ ∧ 𝑓:𝑎⟶ℂ) → (ℜ ∘ 𝑓):𝑎⟶ℂ)
119117, 118mpan 680 . . . . . . . . . . . . . . . 16 (𝑓:𝑎⟶ℂ → (ℜ ∘ 𝑓):𝑎⟶ℂ)
120 ssun1 3999 . . . . . . . . . . . . . . . . . 18 𝑡 ⊆ (𝑡 ∪ {})
121120unissi 4698 . . . . . . . . . . . . . . . . 17 𝑡 (𝑡 ∪ {})
122 id 22 . . . . . . . . . . . . . . . . 17 ( (𝑡 ∪ {}) = 𝑎 (𝑡 ∪ {}) = 𝑎)
123121, 122syl5sseq 3872 . . . . . . . . . . . . . . . 16 ( (𝑡 ∪ {}) = 𝑎 𝑡𝑎)
124 fssres 6322 . . . . . . . . . . . . . . . 16 (((ℜ ∘ 𝑓):𝑎⟶ℂ ∧ 𝑡𝑎) → ((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
125119, 123, 124syl2an 589 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ (𝑡 ∪ {}) = 𝑎) → ((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
126125adantlr 705 . . . . . . . . . . . . . 14 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → ((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
127 elssuni 4704 . . . . . . . . . . . . . . . . . . . . 21 (𝑟𝑡𝑟 𝑡)
128127resabs1d 5679 . . . . . . . . . . . . . . . . . . . 20 (𝑟𝑡 → (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = ((ℜ ∘ 𝑓) ↾ 𝑟))
129 resco 5895 . . . . . . . . . . . . . . . . . . . 20 ((ℜ ∘ 𝑓) ↾ 𝑟) = (ℜ ∘ (𝑓𝑟))
130128, 129syl6eq 2830 . . . . . . . . . . . . . . . . . . 19 (𝑟𝑡 → (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (ℜ ∘ (𝑓𝑟)))
131130adantl 475 . . . . . . . . . . . . . . . . . 18 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (ℜ ∘ (𝑓𝑟)))
132 elun1 4003 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟𝑡𝑟 ∈ (𝑡 ∪ {}))
133 reseq2 5639 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = 𝑟 → (𝑓𝑠) = (𝑓𝑟))
134133eleq1d 2844 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = 𝑟 → ((𝑓𝑠) ∈ MblFn ↔ (𝑓𝑟) ∈ MblFn))
135134rspccva 3510 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn ∧ 𝑟 ∈ (𝑡 ∪ {})) → (𝑓𝑟) ∈ MblFn)
136132, 135sylan2 586 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn ∧ 𝑟𝑡) → (𝑓𝑟) ∈ MblFn)
137136adantll 704 . . . . . . . . . . . . . . . . . . . 20 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (𝑓𝑟) ∈ MblFn)
138 fresin 6325 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:𝑎⟶ℂ → (𝑓𝑟):(𝑎𝑟)⟶ℂ)
139 ismbfcn 23844 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑟):(𝑎𝑟)⟶ℂ → ((𝑓𝑟) ∈ MblFn ↔ ((ℜ ∘ (𝑓𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓𝑟)) ∈ MblFn)))
140138, 139syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:𝑎⟶ℂ → ((𝑓𝑟) ∈ MblFn ↔ ((ℜ ∘ (𝑓𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓𝑟)) ∈ MblFn)))
141140biimpd 221 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:𝑎⟶ℂ → ((𝑓𝑟) ∈ MblFn → ((ℜ ∘ (𝑓𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓𝑟)) ∈ MblFn)))
142141ad2antrr 716 . . . . . . . . . . . . . . . . . . . 20 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → ((𝑓𝑟) ∈ MblFn → ((ℜ ∘ (𝑓𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓𝑟)) ∈ MblFn)))
143137, 142mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → ((ℜ ∘ (𝑓𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓𝑟)) ∈ MblFn))
144143simpld 490 . . . . . . . . . . . . . . . . . 18 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (ℜ ∘ (𝑓𝑟)) ∈ MblFn)
145131, 144eqeltrd 2859 . . . . . . . . . . . . . . . . 17 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn)
146145ralrimiva 3148 . . . . . . . . . . . . . . . 16 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ∀𝑟𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn)
147 reseq2 5639 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑠 → (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠))
148147eleq1d 2844 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑠 → ((((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn ↔ (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
149148cbvralv 3367 . . . . . . . . . . . . . . . 16 (∀𝑟𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn ↔ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
150146, 149sylib 210 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
151150adantr 474 . . . . . . . . . . . . . 14 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
152 pm2.27 42 . . . . . . . . . . . . . 14 ((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → (((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
153126, 151, 152syl2anc 579 . . . . . . . . . . . . 13 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → (((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
154114, 153mpan9 502 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)
155 vsnid 4431 . . . . . . . . . . . . . . 15 ∈ {}
156 elun2 4004 . . . . . . . . . . . . . . 15 ( ∈ {} → ∈ (𝑡 ∪ {}))
157 reseq2 5639 . . . . . . . . . . . . . . . . 17 (𝑠 = → (𝑓𝑠) = (𝑓))
158157eleq1d 2844 . . . . . . . . . . . . . . . 16 (𝑠 = → ((𝑓𝑠) ∈ MblFn ↔ (𝑓) ∈ MblFn))
159158rspcv 3507 . . . . . . . . . . . . . . 15 ( ∈ (𝑡 ∪ {}) → (∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn → (𝑓) ∈ MblFn))
160155, 156, 159mp2b 10 . . . . . . . . . . . . . 14 (∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn → (𝑓) ∈ MblFn)
161 resco 5895 . . . . . . . . . . . . . . 15 ((ℜ ∘ 𝑓) ↾ ) = (ℜ ∘ (𝑓))
162 fresin 6325 . . . . . . . . . . . . . . . . 17 (𝑓:𝑎⟶ℂ → (𝑓):(𝑎)⟶ℂ)
163 ismbfcn 23844 . . . . . . . . . . . . . . . . 17 ((𝑓):(𝑎)⟶ℂ → ((𝑓) ∈ MblFn ↔ ((ℜ ∘ (𝑓)) ∈ MblFn ∧ (ℑ ∘ (𝑓)) ∈ MblFn)))
164162, 163syl 17 . . . . . . . . . . . . . . . 16 (𝑓:𝑎⟶ℂ → ((𝑓) ∈ MblFn ↔ ((ℜ ∘ (𝑓)) ∈ MblFn ∧ (ℑ ∘ (𝑓)) ∈ MblFn)))
165164simprbda 494 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ (𝑓) ∈ MblFn) → (ℜ ∘ (𝑓)) ∈ MblFn)
166161, 165syl5eqel 2863 . . . . . . . . . . . . . 14 ((𝑓:𝑎⟶ℂ ∧ (𝑓) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ ) ∈ MblFn)
167160, 166sylan2 586 . . . . . . . . . . . . 13 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ ) ∈ MblFn)
168167ad2antrl 718 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → ((ℜ ∘ 𝑓) ↾ ) ∈ MblFn)
169 uniun 4694 . . . . . . . . . . . . . . 15 (𝑡 ∪ {}) = ( 𝑡 {})
170 vex 3401 . . . . . . . . . . . . . . . . 17 ∈ V
171170unisn 4689 . . . . . . . . . . . . . . . 16 {} =
172171uneq2i 3987 . . . . . . . . . . . . . . 15 ( 𝑡 {}) = ( 𝑡)
173169, 172eqtri 2802 . . . . . . . . . . . . . 14 (𝑡 ∪ {}) = ( 𝑡)
174173, 122syl5eqr 2828 . . . . . . . . . . . . 13 ( (𝑡 ∪ {}) = 𝑎 → ( 𝑡) = 𝑎)
175174ad2antll 719 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → ( 𝑡) = 𝑎)
17690, 154, 168, 175mbfres2 23860 . . . . . . . . . . 11 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → (ℜ ∘ 𝑓) ∈ MblFn)
177 imf 14266 . . . . . . . . . . . . . . 15 ℑ:ℂ⟶ℝ
178 fco 6310 . . . . . . . . . . . . . . 15 ((ℑ:ℂ⟶ℝ ∧ 𝑓:𝑎⟶ℂ) → (ℑ ∘ 𝑓):𝑎⟶ℝ)
179177, 178mpan 680 . . . . . . . . . . . . . 14 (𝑓:𝑎⟶ℂ → (ℑ ∘ 𝑓):𝑎⟶ℝ)
180179adantr 474 . . . . . . . . . . . . 13 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → (ℑ ∘ 𝑓):𝑎⟶ℝ)
181180ad2antrl 718 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → (ℑ ∘ 𝑓):𝑎⟶ℝ)
182 imcncf 23125 . . . . . . . . . . . . . . . . 17 ℑ ∈ (ℂ–cn→ℝ)
183182elexi 3415 . . . . . . . . . . . . . . . 16 ℑ ∈ V
184183, 93coex 7399 . . . . . . . . . . . . . . 15 (ℑ ∘ 𝑓) ∈ V
185184resex 5695 . . . . . . . . . . . . . 14 ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ V
18698adantl 475 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → 𝑡 = 𝑏)
187186biantrud 527 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ↔ ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏)))
188 feq123 6283 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡 ∧ ℂ = ℂ) → (𝑔:𝑏⟶ℂ ↔ ((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ))
189101, 188mp3an3 1523 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (𝑔:𝑏⟶ℂ ↔ ((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ))
190 reseq1 5638 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) → (𝑔𝑠) = (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠))
191190eleq1d 2844 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) → ((𝑔𝑠) ∈ MblFn ↔ (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
192191adantr 474 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔𝑠) ∈ MblFn ↔ (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
193192ralbidv 3168 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (∀𝑠𝑡 (𝑔𝑠) ∈ MblFn ↔ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
194189, 193anbi12d 624 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ↔ (((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)))
195187, 194bitr3d 273 . . . . . . . . . . . . . . . 16 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) ↔ (((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)))
196 eleq1 2847 . . . . . . . . . . . . . . . . 17 (𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) → (𝑔 ∈ MblFn ↔ ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
197196adantr 474 . . . . . . . . . . . . . . . 16 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (𝑔 ∈ MblFn ↔ ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
198195, 197imbi12d 336 . . . . . . . . . . . . . . 15 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ↔ ((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)))
199198spc2gv 3498 . . . . . . . . . . . . . 14 ((((ℑ ∘ 𝑓) ↾ 𝑡) ∈ V ∧ 𝑡 ∈ V) → (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)))
200185, 96, 199mp2an 682 . . . . . . . . . . . . 13 (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
201 fss 6306 . . . . . . . . . . . . . . . . . 18 ((ℑ:ℂ⟶ℝ ∧ ℝ ⊆ ℂ) → ℑ:ℂ⟶ℂ)
202177, 115, 201mp2an 682 . . . . . . . . . . . . . . . . 17 ℑ:ℂ⟶ℂ
203 fco 6310 . . . . . . . . . . . . . . . . 17 ((ℑ:ℂ⟶ℂ ∧ 𝑓:𝑎⟶ℂ) → (ℑ ∘ 𝑓):𝑎⟶ℂ)
204202, 203mpan 680 . . . . . . . . . . . . . . . 16 (𝑓:𝑎⟶ℂ → (ℑ ∘ 𝑓):𝑎⟶ℂ)
205 fssres 6322 . . . . . . . . . . . . . . . 16 (((ℑ ∘ 𝑓):𝑎⟶ℂ ∧ 𝑡𝑎) → ((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
206204, 123, 205syl2an 589 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ (𝑡 ∪ {}) = 𝑎) → ((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
207206adantlr 705 . . . . . . . . . . . . . 14 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → ((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
208127resabs1d 5679 . . . . . . . . . . . . . . . . . . . 20 (𝑟𝑡 → (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = ((ℑ ∘ 𝑓) ↾ 𝑟))
209 resco 5895 . . . . . . . . . . . . . . . . . . . 20 ((ℑ ∘ 𝑓) ↾ 𝑟) = (ℑ ∘ (𝑓𝑟))
210208, 209syl6eq 2830 . . . . . . . . . . . . . . . . . . 19 (𝑟𝑡 → (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (ℑ ∘ (𝑓𝑟)))
211210adantl 475 . . . . . . . . . . . . . . . . . 18 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (ℑ ∘ (𝑓𝑟)))
212143simprd 491 . . . . . . . . . . . . . . . . . 18 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (ℑ ∘ (𝑓𝑟)) ∈ MblFn)
213211, 212eqeltrd 2859 . . . . . . . . . . . . . . . . 17 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn)
214213ralrimiva 3148 . . . . . . . . . . . . . . . 16 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ∀𝑟𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn)
215 reseq2 5639 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑠 → (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠))
216215eleq1d 2844 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑠 → ((((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn ↔ (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
217216cbvralv 3367 . . . . . . . . . . . . . . . 16 (∀𝑟𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn ↔ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
218214, 217sylib 210 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
219218adantr 474 . . . . . . . . . . . . . 14 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
220 pm2.27 42 . . . . . . . . . . . . . 14 ((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → (((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
221207, 219, 220syl2anc 579 . . . . . . . . . . . . 13 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → (((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
222200, 221mpan9 502 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)
223 resco 5895 . . . . . . . . . . . . . . 15 ((ℑ ∘ 𝑓) ↾ ) = (ℑ ∘ (𝑓))
224164simplbda 495 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ (𝑓) ∈ MblFn) → (ℑ ∘ (𝑓)) ∈ MblFn)
225223, 224syl5eqel 2863 . . . . . . . . . . . . . 14 ((𝑓:𝑎⟶ℂ ∧ (𝑓) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ ) ∈ MblFn)
226160, 225sylan2 586 . . . . . . . . . . . . 13 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ ) ∈ MblFn)
227226ad2antrl 718 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → ((ℑ ∘ 𝑓) ↾ ) ∈ MblFn)
228181, 222, 227, 175mbfres2 23860 . . . . . . . . . . 11 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → (ℑ ∘ 𝑓) ∈ MblFn)
229 ismbfcn 23844 . . . . . . . . . . . . 13 (𝑓:𝑎⟶ℂ → (𝑓 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ∈ MblFn ∧ (ℑ ∘ 𝑓) ∈ MblFn)))
230229adantr 474 . . . . . . . . . . . 12 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → (𝑓 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ∈ MblFn ∧ (ℑ ∘ 𝑓) ∈ MblFn)))
231230ad2antrl 718 . . . . . . . . . . 11 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → (𝑓 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ∈ MblFn ∧ (ℑ ∘ 𝑓) ∈ MblFn)))
232176, 228, 231mpbir2and 703 . . . . . . . . . 10 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → 𝑓 ∈ MblFn)
233232ex 403 . . . . . . . . 9 (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → 𝑓 ∈ MblFn))
234233alrimivv 1971 . . . . . . . 8 (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → 𝑓 ∈ MblFn))
235234a1i 11 . . . . . . 7 (𝑡 ∈ Fin → (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → 𝑓 ∈ MblFn)))
23636, 59, 66, 73, 85, 235findcard2 8490 . . . . . 6 (𝑆 ∈ Fin → ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn))
237 2sp 2170 . . . . . 6 (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn))
2384, 236, 2373syl 18 . . . . 5 (𝜑 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn))
23917, 26, 238vtocl2g 3471 . . . 4 ((𝐴 ∈ V ∧ 𝐹 ∈ V) → (𝜑 → (((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝐹 ∈ MblFn)))
24011, 239mpcom 38 . . 3 (𝜑 → (((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝐹 ∈ MblFn))
2413, 240mpan2d 684 . 2 (𝜑 → ((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) → 𝐹 ∈ MblFn))
2421, 2, 241mp2and 689 1 (𝜑𝐹 ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  wal 1599   = wceq 1601  wcel 2107  wral 3090  Vcvv 3398  cun 3790  cin 3791  wss 3792  c0 4141  {csn 4398   cuni 4673  dom cdm 5357  cres 5359  ccom 5361  Rel wrel 5362  wf 6133  (class class class)co 6924  Fincfn 8243  cc 10272  cr 10273  cre 14250  cim 14251  cnccncf 23098  MblFncmbf 23829
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-inf2 8837  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351  ax-pre-sup 10352
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-se 5317  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-isom 6146  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-of 7176  df-om 7346  df-1st 7447  df-2nd 7448  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-2o 7846  df-oadd 7849  df-er 8028  df-map 8144  df-pm 8145  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-sup 8638  df-inf 8639  df-oi 8706  df-card 9100  df-cda 9327  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11036  df-nn 11380  df-2 11443  df-3 11444  df-n0 11648  df-z 11734  df-uz 11998  df-q 12101  df-rp 12143  df-xadd 12263  df-ioo 12496  df-ico 12498  df-icc 12499  df-fz 12649  df-fzo 12790  df-fl 12917  df-seq 13125  df-exp 13184  df-hash 13442  df-cj 14252  df-re 14253  df-im 14254  df-sqrt 14388  df-abs 14389  df-clim 14636  df-sum 14834  df-xmet 20146  df-met 20147  df-cncf 23100  df-ovol 23679  df-vol 23680  df-mbf 23834
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator