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 37047
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 7729 . . . . . 6 (πœ‘ β†’ βˆͺ 𝑆 ∈ V)
63, 5eqeltrrd 2828 . . . . 5 (πœ‘ β†’ 𝐴 ∈ V)
7 fex 7223 . . . . . . 7 ((𝐹:π΄βŸΆβ„‚ ∧ 𝐴 ∈ V) β†’ 𝐹 ∈ V)
87ex 412 . . . . . 6 (𝐹:π΄βŸΆβ„‚ β†’ (𝐴 ∈ V β†’ 𝐹 ∈ V))
91, 8syl 17 . . . . 5 (πœ‘ β†’ (𝐴 ∈ V β†’ 𝐹 ∈ V))
106, 9jcai 516 . . . 4 (πœ‘ β†’ (𝐴 ∈ V ∧ 𝐹 ∈ V))
11 feq2 6693 . . . . . . . . 9 (π‘Ž = 𝐴 β†’ (𝑓:π‘ŽβŸΆβ„‚ ↔ 𝑓:π΄βŸΆβ„‚))
1211anbi1d 629 . . . . . . . 8 (π‘Ž = 𝐴 β†’ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ↔ (𝑓:π΄βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn)))
13 eqeq2 2738 . . . . . . . 8 (π‘Ž = 𝐴 β†’ (βˆͺ 𝑆 = π‘Ž ↔ βˆͺ 𝑆 = 𝐴))
1412, 13anbi12d 630 . . . . . . 7 (π‘Ž = 𝐴 β†’ (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = π‘Ž) ↔ ((𝑓:π΄βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = 𝐴)))
1514imbi1d 341 . . . . . 6 (π‘Ž = 𝐴 β†’ ((((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = π‘Ž) β†’ 𝑓 ∈ MblFn) ↔ (((𝑓:π΄βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = 𝐴) β†’ 𝑓 ∈ MblFn)))
1615imbi2d 340 . . . . 5 (π‘Ž = 𝐴 β†’ ((πœ‘ β†’ (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = π‘Ž) β†’ 𝑓 ∈ MblFn)) ↔ (πœ‘ β†’ (((𝑓:π΄βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = 𝐴) β†’ 𝑓 ∈ MblFn))))
17 feq1 6692 . . . . . . . . 9 (𝑓 = 𝐹 β†’ (𝑓:π΄βŸΆβ„‚ ↔ 𝐹:π΄βŸΆβ„‚))
18 reseq1 5969 . . . . . . . . . . 11 (𝑓 = 𝐹 β†’ (𝑓 β†Ύ 𝑠) = (𝐹 β†Ύ 𝑠))
1918eleq1d 2812 . . . . . . . . . 10 (𝑓 = 𝐹 β†’ ((𝑓 β†Ύ 𝑠) ∈ MblFn ↔ (𝐹 β†Ύ 𝑠) ∈ MblFn))
2019ralbidv 3171 . . . . . . . . 9 (𝑓 = 𝐹 β†’ (βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn ↔ βˆ€π‘  ∈ 𝑆 (𝐹 β†Ύ 𝑠) ∈ MblFn))
2117, 20anbi12d 630 . . . . . . . 8 (𝑓 = 𝐹 β†’ ((𝑓:π΄βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ↔ (𝐹:π΄βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝐹 β†Ύ 𝑠) ∈ MblFn)))
2221anbi1d 629 . . . . . . 7 (𝑓 = 𝐹 β†’ (((𝑓:π΄βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = 𝐴) ↔ ((𝐹:π΄βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝐹 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = 𝐴)))
23 eleq1 2815 . . . . . . 7 (𝑓 = 𝐹 β†’ (𝑓 ∈ MblFn ↔ 𝐹 ∈ MblFn))
2422, 23imbi12d 344 . . . . . 6 (𝑓 = 𝐹 β†’ ((((𝑓:π΄βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = 𝐴) β†’ 𝑓 ∈ MblFn) ↔ (((𝐹:π΄βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝐹 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = 𝐴) β†’ 𝐹 ∈ MblFn)))
2524imbi2d 340 . . . . 5 (𝑓 = 𝐹 β†’ ((πœ‘ β†’ (((𝑓:π΄βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = 𝐴) β†’ 𝑓 ∈ MblFn)) ↔ (πœ‘ β†’ (((𝐹:π΄βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝐹 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = 𝐴) β†’ 𝐹 ∈ MblFn))))
26 rzal 4503 . . . . . . . . . . . 12 (π‘Ÿ = βˆ… β†’ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn)
2726biantrud 531 . . . . . . . . . . 11 (π‘Ÿ = βˆ… β†’ (𝑓:π‘ŽβŸΆβ„‚ ↔ (𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn)))
2827bicomd 222 . . . . . . . . . 10 (π‘Ÿ = βˆ… β†’ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ↔ 𝑓:π‘ŽβŸΆβ„‚))
29 unieq 4913 . . . . . . . . . . . 12 (π‘Ÿ = βˆ… β†’ βˆͺ π‘Ÿ = βˆͺ βˆ…)
30 uni0 4932 . . . . . . . . . . . 12 βˆͺ βˆ… = βˆ…
3129, 30eqtrdi 2782 . . . . . . . . . . 11 (π‘Ÿ = βˆ… β†’ βˆͺ π‘Ÿ = βˆ…)
3231eqeq1d 2728 . . . . . . . . . 10 (π‘Ÿ = βˆ… β†’ (βˆͺ π‘Ÿ = π‘Ž ↔ βˆ… = π‘Ž))
3328, 32anbi12d 630 . . . . . . . . 9 (π‘Ÿ = βˆ… β†’ (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ π‘Ÿ = π‘Ž) ↔ (𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ… = π‘Ž)))
3433imbi1d 341 . . . . . . . 8 (π‘Ÿ = βˆ… β†’ ((((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ π‘Ÿ = π‘Ž) β†’ 𝑓 ∈ MblFn) ↔ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ… = π‘Ž) β†’ 𝑓 ∈ MblFn)))
35342albidv 1918 . . . . . . 7 (π‘Ÿ = βˆ… β†’ (βˆ€π‘“βˆ€π‘Ž(((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ π‘Ÿ = π‘Ž) β†’ 𝑓 ∈ MblFn) ↔ βˆ€π‘“βˆ€π‘Ž((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ… = π‘Ž) β†’ 𝑓 ∈ MblFn)))
36 raleq 3316 . . . . . . . . . . . 12 (π‘Ÿ = 𝑑 β†’ (βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn ↔ βˆ€π‘  ∈ 𝑑 (𝑓 β†Ύ 𝑠) ∈ MblFn))
3736anbi2d 628 . . . . . . . . . . 11 (π‘Ÿ = 𝑑 β†’ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ↔ (𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑓 β†Ύ 𝑠) ∈ MblFn)))
38 unieq 4913 . . . . . . . . . . . 12 (π‘Ÿ = 𝑑 β†’ βˆͺ π‘Ÿ = βˆͺ 𝑑)
3938eqeq1d 2728 . . . . . . . . . . 11 (π‘Ÿ = 𝑑 β†’ (βˆͺ π‘Ÿ = π‘Ž ↔ βˆͺ 𝑑 = π‘Ž))
4037, 39anbi12d 630 . . . . . . . . . 10 (π‘Ÿ = 𝑑 β†’ (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ π‘Ÿ = π‘Ž) ↔ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = π‘Ž)))
4140imbi1d 341 . . . . . . . . 9 (π‘Ÿ = 𝑑 β†’ ((((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ π‘Ÿ = π‘Ž) β†’ 𝑓 ∈ MblFn) ↔ (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = π‘Ž) β†’ 𝑓 ∈ MblFn)))
42412albidv 1918 . . . . . . . 8 (π‘Ÿ = 𝑑 β†’ (βˆ€π‘“βˆ€π‘Ž(((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ π‘Ÿ = π‘Ž) β†’ 𝑓 ∈ MblFn) ↔ βˆ€π‘“βˆ€π‘Ž(((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = π‘Ž) β†’ 𝑓 ∈ MblFn)))
43 simpl 482 . . . . . . . . . . . . 13 ((𝑓 = 𝑔 ∧ π‘Ž = 𝑏) β†’ 𝑓 = 𝑔)
44 simpr 484 . . . . . . . . . . . . 13 ((𝑓 = 𝑔 ∧ π‘Ž = 𝑏) β†’ π‘Ž = 𝑏)
4543, 44feq12d 6699 . . . . . . . . . . . 12 ((𝑓 = 𝑔 ∧ π‘Ž = 𝑏) β†’ (𝑓:π‘ŽβŸΆβ„‚ ↔ 𝑔:π‘βŸΆβ„‚))
46 reseq1 5969 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 β†’ (𝑓 β†Ύ 𝑠) = (𝑔 β†Ύ 𝑠))
4746adantr 480 . . . . . . . . . . . . . 14 ((𝑓 = 𝑔 ∧ π‘Ž = 𝑏) β†’ (𝑓 β†Ύ 𝑠) = (𝑔 β†Ύ 𝑠))
4847eleq1d 2812 . . . . . . . . . . . . 13 ((𝑓 = 𝑔 ∧ π‘Ž = 𝑏) β†’ ((𝑓 β†Ύ 𝑠) ∈ MblFn ↔ (𝑔 β†Ύ 𝑠) ∈ MblFn))
4948ralbidv 3171 . . . . . . . . . . . 12 ((𝑓 = 𝑔 ∧ π‘Ž = 𝑏) β†’ (βˆ€π‘  ∈ 𝑑 (𝑓 β†Ύ 𝑠) ∈ MblFn ↔ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn))
5045, 49anbi12d 630 . . . . . . . . . . 11 ((𝑓 = 𝑔 ∧ π‘Ž = 𝑏) β†’ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑓 β†Ύ 𝑠) ∈ MblFn) ↔ (𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn)))
51 eqeq2 2738 . . . . . . . . . . . 12 (π‘Ž = 𝑏 β†’ (βˆͺ 𝑑 = π‘Ž ↔ βˆͺ 𝑑 = 𝑏))
5251adantl 481 . . . . . . . . . . 11 ((𝑓 = 𝑔 ∧ π‘Ž = 𝑏) β†’ (βˆͺ 𝑑 = π‘Ž ↔ βˆͺ 𝑑 = 𝑏))
5350, 52anbi12d 630 . . . . . . . . . 10 ((𝑓 = 𝑔 ∧ π‘Ž = 𝑏) β†’ (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = π‘Ž) ↔ ((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏)))
54 eleq1 2815 . . . . . . . . . . 11 (𝑓 = 𝑔 β†’ (𝑓 ∈ MblFn ↔ 𝑔 ∈ MblFn))
5554adantr 480 . . . . . . . . . 10 ((𝑓 = 𝑔 ∧ π‘Ž = 𝑏) β†’ (𝑓 ∈ MblFn ↔ 𝑔 ∈ MblFn))
5653, 55imbi12d 344 . . . . . . . . 9 ((𝑓 = 𝑔 ∧ π‘Ž = 𝑏) β†’ ((((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = π‘Ž) β†’ 𝑓 ∈ MblFn) ↔ (((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn)))
5756cbval2vw 2035 . . . . . . . 8 (βˆ€π‘“βˆ€π‘Ž(((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = π‘Ž) β†’ 𝑓 ∈ MblFn) ↔ βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn))
5842, 57bitrdi 287 . . . . . . 7 (π‘Ÿ = 𝑑 β†’ (βˆ€π‘“βˆ€π‘Ž(((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ π‘Ÿ = π‘Ž) β†’ 𝑓 ∈ MblFn) ↔ βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn)))
59 raleq 3316 . . . . . . . . . . 11 (π‘Ÿ = (𝑑 βˆͺ {β„Ž}) β†’ (βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn ↔ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn))
6059anbi2d 628 . . . . . . . . . 10 (π‘Ÿ = (𝑑 βˆͺ {β„Ž}) β†’ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ↔ (𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn)))
61 unieq 4913 . . . . . . . . . . 11 (π‘Ÿ = (𝑑 βˆͺ {β„Ž}) β†’ βˆͺ π‘Ÿ = βˆͺ (𝑑 βˆͺ {β„Ž}))
6261eqeq1d 2728 . . . . . . . . . 10 (π‘Ÿ = (𝑑 βˆͺ {β„Ž}) β†’ (βˆͺ π‘Ÿ = π‘Ž ↔ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž))
6360, 62anbi12d 630 . . . . . . . . 9 (π‘Ÿ = (𝑑 βˆͺ {β„Ž}) β†’ (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ π‘Ÿ = π‘Ž) ↔ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž)))
6463imbi1d 341 . . . . . . . 8 (π‘Ÿ = (𝑑 βˆͺ {β„Ž}) β†’ ((((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ π‘Ÿ = π‘Ž) β†’ 𝑓 ∈ MblFn) ↔ (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž) β†’ 𝑓 ∈ MblFn)))
65642albidv 1918 . . . . . . 7 (π‘Ÿ = (𝑑 βˆͺ {β„Ž}) β†’ (βˆ€π‘“βˆ€π‘Ž(((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ π‘Ÿ = π‘Ž) β†’ 𝑓 ∈ MblFn) ↔ βˆ€π‘“βˆ€π‘Ž(((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž) β†’ 𝑓 ∈ MblFn)))
66 raleq 3316 . . . . . . . . . . 11 (π‘Ÿ = 𝑆 β†’ (βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn ↔ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn))
6766anbi2d 628 . . . . . . . . . 10 (π‘Ÿ = 𝑆 β†’ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ↔ (𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn)))
68 unieq 4913 . . . . . . . . . . 11 (π‘Ÿ = 𝑆 β†’ βˆͺ π‘Ÿ = βˆͺ 𝑆)
6968eqeq1d 2728 . . . . . . . . . 10 (π‘Ÿ = 𝑆 β†’ (βˆͺ π‘Ÿ = π‘Ž ↔ βˆͺ 𝑆 = π‘Ž))
7067, 69anbi12d 630 . . . . . . . . 9 (π‘Ÿ = 𝑆 β†’ (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ π‘Ÿ = π‘Ž) ↔ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = π‘Ž)))
7170imbi1d 341 . . . . . . . 8 (π‘Ÿ = 𝑆 β†’ ((((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ π‘Ÿ = π‘Ž) β†’ 𝑓 ∈ MblFn) ↔ (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = π‘Ž) β†’ 𝑓 ∈ MblFn)))
72712albidv 1918 . . . . . . 7 (π‘Ÿ = 𝑆 β†’ (βˆ€π‘“βˆ€π‘Ž(((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ π‘Ÿ (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ π‘Ÿ = π‘Ž) β†’ 𝑓 ∈ MblFn) ↔ βˆ€π‘“βˆ€π‘Ž(((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = π‘Ž) β†’ 𝑓 ∈ MblFn)))
73 frel 6716 . . . . . . . . . 10 (𝑓:π‘ŽβŸΆβ„‚ β†’ Rel 𝑓)
7473adantr 480 . . . . . . . . 9 ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ… = π‘Ž) β†’ Rel 𝑓)
75 fdm 6720 . . . . . . . . . 10 (𝑓:π‘ŽβŸΆβ„‚ β†’ dom 𝑓 = π‘Ž)
76 eqcom 2733 . . . . . . . . . . 11 (βˆ… = π‘Ž ↔ π‘Ž = βˆ…)
7776biimpi 215 . . . . . . . . . 10 (βˆ… = π‘Ž β†’ π‘Ž = βˆ…)
7875, 77sylan9eq 2786 . . . . . . . . 9 ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ… = π‘Ž) β†’ dom 𝑓 = βˆ…)
79 reldm0 5921 . . . . . . . . . . 11 (Rel 𝑓 β†’ (𝑓 = βˆ… ↔ dom 𝑓 = βˆ…))
8079biimpar 477 . . . . . . . . . 10 ((Rel 𝑓 ∧ dom 𝑓 = βˆ…) β†’ 𝑓 = βˆ…)
81 mbf0 25518 . . . . . . . . . 10 βˆ… ∈ MblFn
8280, 81eqeltrdi 2835 . . . . . . . . 9 ((Rel 𝑓 ∧ dom 𝑓 = βˆ…) β†’ 𝑓 ∈ MblFn)
8374, 78, 82syl2anc 583 . . . . . . . 8 ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ… = π‘Ž) β†’ 𝑓 ∈ MblFn)
8483gen2 1790 . . . . . . 7 βˆ€π‘“βˆ€π‘Ž((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ… = π‘Ž) β†’ 𝑓 ∈ MblFn)
85 ref 15065 . . . . . . . . . . . . . . 15 β„œ:β„‚βŸΆβ„
86 fco 6735 . . . . . . . . . . . . . . 15 ((β„œ:β„‚βŸΆβ„ ∧ 𝑓:π‘ŽβŸΆβ„‚) β†’ (β„œ ∘ 𝑓):π‘ŽβŸΆβ„)
8785, 86mpan 687 . . . . . . . . . . . . . 14 (𝑓:π‘ŽβŸΆβ„‚ β†’ (β„œ ∘ 𝑓):π‘ŽβŸΆβ„)
8887adantr 480 . . . . . . . . . . . . 13 ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) β†’ (β„œ ∘ 𝑓):π‘ŽβŸΆβ„)
8988ad2antrl 725 . . . . . . . . . . . 12 ((βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) ∧ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž)) β†’ (β„œ ∘ 𝑓):π‘ŽβŸΆβ„)
90 recncf 24777 . . . . . . . . . . . . . . . . 17 β„œ ∈ (ℂ–cn→ℝ)
9190elexi 3488 . . . . . . . . . . . . . . . 16 β„œ ∈ V
92 vex 3472 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
9391, 92coex 7920 . . . . . . . . . . . . . . 15 (β„œ ∘ 𝑓) ∈ V
9493resex 6023 . . . . . . . . . . . . . 14 ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ V
95 vuniex 7726 . . . . . . . . . . . . . 14 βˆͺ 𝑑 ∈ V
96 eqcom 2733 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = βˆͺ 𝑑 ↔ βˆͺ 𝑑 = 𝑏)
9796biimpi 215 . . . . . . . . . . . . . . . . . . 19 (𝑏 = βˆͺ 𝑑 β†’ βˆͺ 𝑑 = 𝑏)
9897adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ βˆͺ 𝑑 = 𝑏)
9998biantrud 531 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ ((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ↔ ((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏)))
100 eqid 2726 . . . . . . . . . . . . . . . . . . 19 β„‚ = β„‚
101 feq123 6701 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑 ∧ β„‚ = β„‚) β†’ (𝑔:π‘βŸΆβ„‚ ↔ ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚))
102100, 101mp3an3 1446 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ (𝑔:π‘βŸΆβ„‚ ↔ ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚))
103 reseq1 5969 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†’ (𝑔 β†Ύ 𝑠) = (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠))
104103eleq1d 2812 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†’ ((𝑔 β†Ύ 𝑠) ∈ MblFn ↔ (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn))
105104adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ ((𝑔 β†Ύ 𝑠) ∈ MblFn ↔ (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn))
106105ralbidv 3171 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ (βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn ↔ βˆ€π‘  ∈ 𝑑 (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn))
107102, 106anbi12d 630 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ ((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ↔ (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn)))
10899, 107bitr3d 281 . . . . . . . . . . . . . . . 16 ((𝑔 = ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ (((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) ↔ (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn)))
109 eleq1 2815 . . . . . . . . . . . . . . . . 17 (𝑔 = ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†’ (𝑔 ∈ MblFn ↔ ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn))
110109adantr 480 . . . . . . . . . . . . . . . 16 ((𝑔 = ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ (𝑔 ∈ MblFn ↔ ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn))
111108, 110imbi12d 344 . . . . . . . . . . . . . . 15 ((𝑔 = ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ ((((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) ↔ ((((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn) β†’ ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn)))
112111spc2gv 3584 . . . . . . . . . . . . . 14 ((((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ V ∧ βˆͺ 𝑑 ∈ V) β†’ (βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) β†’ ((((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn) β†’ ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn)))
11394, 95, 112mp2an 689 . . . . . . . . . . . . 13 (βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) β†’ ((((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn) β†’ ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn))
114 ax-resscn 11169 . . . . . . . . . . . . . . . . . 18 ℝ βŠ† β„‚
115 fss 6728 . . . . . . . . . . . . . . . . . 18 ((β„œ:β„‚βŸΆβ„ ∧ ℝ βŠ† β„‚) β†’ β„œ:β„‚βŸΆβ„‚)
11685, 114, 115mp2an 689 . . . . . . . . . . . . . . . . 17 β„œ:β„‚βŸΆβ„‚
117 fco 6735 . . . . . . . . . . . . . . . . 17 ((β„œ:β„‚βŸΆβ„‚ ∧ 𝑓:π‘ŽβŸΆβ„‚) β†’ (β„œ ∘ 𝑓):π‘ŽβŸΆβ„‚)
118116, 117mpan 687 . . . . . . . . . . . . . . . 16 (𝑓:π‘ŽβŸΆβ„‚ β†’ (β„œ ∘ 𝑓):π‘ŽβŸΆβ„‚)
119 ssun1 4167 . . . . . . . . . . . . . . . . . 18 𝑑 βŠ† (𝑑 βˆͺ {β„Ž})
120119unissi 4911 . . . . . . . . . . . . . . . . 17 βˆͺ 𝑑 βŠ† βˆͺ (𝑑 βˆͺ {β„Ž})
121 id 22 . . . . . . . . . . . . . . . . 17 (βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž β†’ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž)
122120, 121sseqtrid 4029 . . . . . . . . . . . . . . . 16 (βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž β†’ βˆͺ 𝑑 βŠ† π‘Ž)
123 fssres 6751 . . . . . . . . . . . . . . . 16 (((β„œ ∘ 𝑓):π‘ŽβŸΆβ„‚ ∧ βˆͺ 𝑑 βŠ† π‘Ž) β†’ ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚)
124118, 122, 123syl2an 595 . . . . . . . . . . . . . . 15 ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž) β†’ ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚)
125124adantlr 712 . . . . . . . . . . . . . 14 (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž) β†’ ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚)
126 elssuni 4934 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ÿ ∈ 𝑑 β†’ π‘Ÿ βŠ† βˆͺ 𝑑)
127126resabs1d 6006 . . . . . . . . . . . . . . . . . . . 20 (π‘Ÿ ∈ 𝑑 β†’ (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) = ((β„œ ∘ 𝑓) β†Ύ π‘Ÿ))
128 resco 6243 . . . . . . . . . . . . . . . . . . . 20 ((β„œ ∘ 𝑓) β†Ύ π‘Ÿ) = (β„œ ∘ (𝑓 β†Ύ π‘Ÿ))
129127, 128eqtrdi 2782 . . . . . . . . . . . . . . . . . . 19 (π‘Ÿ ∈ 𝑑 β†’ (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) = (β„œ ∘ (𝑓 β†Ύ π‘Ÿ)))
130129adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ π‘Ÿ ∈ 𝑑) β†’ (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) = (β„œ ∘ (𝑓 β†Ύ π‘Ÿ)))
131 elun1 4171 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ÿ ∈ 𝑑 β†’ π‘Ÿ ∈ (𝑑 βˆͺ {β„Ž}))
132 reseq2 5970 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = π‘Ÿ β†’ (𝑓 β†Ύ 𝑠) = (𝑓 β†Ύ π‘Ÿ))
133132eleq1d 2812 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = π‘Ÿ β†’ ((𝑓 β†Ύ 𝑠) ∈ MblFn ↔ (𝑓 β†Ύ π‘Ÿ) ∈ MblFn))
134133rspccva 3605 . . . . . . . . . . . . . . . . . . . . . 22 ((βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn ∧ π‘Ÿ ∈ (𝑑 βˆͺ {β„Ž})) β†’ (𝑓 β†Ύ π‘Ÿ) ∈ MblFn)
135131, 134sylan2 592 . . . . . . . . . . . . . . . . . . . . 21 ((βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn ∧ π‘Ÿ ∈ 𝑑) β†’ (𝑓 β†Ύ π‘Ÿ) ∈ MblFn)
136135adantll 711 . . . . . . . . . . . . . . . . . . . 20 (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ π‘Ÿ ∈ 𝑑) β†’ (𝑓 β†Ύ π‘Ÿ) ∈ MblFn)
137 fresin 6754 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:π‘ŽβŸΆβ„‚ β†’ (𝑓 β†Ύ π‘Ÿ):(π‘Ž ∩ π‘Ÿ)βŸΆβ„‚)
138 ismbfcn 25513 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓 β†Ύ π‘Ÿ):(π‘Ž ∩ π‘Ÿ)βŸΆβ„‚ β†’ ((𝑓 β†Ύ π‘Ÿ) ∈ MblFn ↔ ((β„œ ∘ (𝑓 β†Ύ π‘Ÿ)) ∈ MblFn ∧ (β„‘ ∘ (𝑓 β†Ύ π‘Ÿ)) ∈ MblFn)))
139137, 138syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:π‘ŽβŸΆβ„‚ β†’ ((𝑓 β†Ύ π‘Ÿ) ∈ MblFn ↔ ((β„œ ∘ (𝑓 β†Ύ π‘Ÿ)) ∈ MblFn ∧ (β„‘ ∘ (𝑓 β†Ύ π‘Ÿ)) ∈ MblFn)))
140139biimpd 228 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:π‘ŽβŸΆβ„‚ β†’ ((𝑓 β†Ύ π‘Ÿ) ∈ MblFn β†’ ((β„œ ∘ (𝑓 β†Ύ π‘Ÿ)) ∈ MblFn ∧ (β„‘ ∘ (𝑓 β†Ύ π‘Ÿ)) ∈ MblFn)))
141140ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ π‘Ÿ ∈ 𝑑) β†’ ((𝑓 β†Ύ π‘Ÿ) ∈ MblFn β†’ ((β„œ ∘ (𝑓 β†Ύ π‘Ÿ)) ∈ MblFn ∧ (β„‘ ∘ (𝑓 β†Ύ π‘Ÿ)) ∈ MblFn)))
142136, 141mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ π‘Ÿ ∈ 𝑑) β†’ ((β„œ ∘ (𝑓 β†Ύ π‘Ÿ)) ∈ MblFn ∧ (β„‘ ∘ (𝑓 β†Ύ π‘Ÿ)) ∈ MblFn))
143142simpld 494 . . . . . . . . . . . . . . . . . 18 (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ π‘Ÿ ∈ 𝑑) β†’ (β„œ ∘ (𝑓 β†Ύ π‘Ÿ)) ∈ MblFn)
144130, 143eqeltrd 2827 . . . . . . . . . . . . . . . . 17 (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ π‘Ÿ ∈ 𝑑) β†’ (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) ∈ MblFn)
145144ralrimiva 3140 . . . . . . . . . . . . . . . 16 ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) β†’ βˆ€π‘Ÿ ∈ 𝑑 (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) ∈ MblFn)
146 reseq2 5970 . . . . . . . . . . . . . . . . . 18 (π‘Ÿ = 𝑠 β†’ (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) = (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠))
147146eleq1d 2812 . . . . . . . . . . . . . . . . 17 (π‘Ÿ = 𝑠 β†’ ((((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) ∈ MblFn ↔ (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn))
148147cbvralvw 3228 . . . . . . . . . . . . . . . 16 (βˆ€π‘Ÿ ∈ 𝑑 (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) ∈ MblFn ↔ βˆ€π‘  ∈ 𝑑 (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn)
149145, 148sylib 217 . . . . . . . . . . . . . . 15 ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) β†’ βˆ€π‘  ∈ 𝑑 (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn)
150149adantr 480 . . . . . . . . . . . . . 14 (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž) β†’ βˆ€π‘  ∈ 𝑑 (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn)
151 pm2.27 42 . . . . . . . . . . . . . 14 ((((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn) β†’ (((((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn) β†’ ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn) β†’ ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn))
152125, 150, 151syl2anc 583 . . . . . . . . . . . . 13 (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž) β†’ (((((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn) β†’ ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn) β†’ ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn))
153113, 152mpan9 506 . . . . . . . . . . . 12 ((βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) ∧ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž)) β†’ ((β„œ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn)
154 vsnid 4660 . . . . . . . . . . . . . . 15 β„Ž ∈ {β„Ž}
155 elun2 4172 . . . . . . . . . . . . . . 15 (β„Ž ∈ {β„Ž} β†’ β„Ž ∈ (𝑑 βˆͺ {β„Ž}))
156 reseq2 5970 . . . . . . . . . . . . . . . . 17 (𝑠 = β„Ž β†’ (𝑓 β†Ύ 𝑠) = (𝑓 β†Ύ β„Ž))
157156eleq1d 2812 . . . . . . . . . . . . . . . 16 (𝑠 = β„Ž β†’ ((𝑓 β†Ύ 𝑠) ∈ MblFn ↔ (𝑓 β†Ύ β„Ž) ∈ MblFn))
158157rspcv 3602 . . . . . . . . . . . . . . 15 (β„Ž ∈ (𝑑 βˆͺ {β„Ž}) β†’ (βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn β†’ (𝑓 β†Ύ β„Ž) ∈ MblFn))
159154, 155, 158mp2b 10 . . . . . . . . . . . . . 14 (βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn β†’ (𝑓 β†Ύ β„Ž) ∈ MblFn)
160 resco 6243 . . . . . . . . . . . . . . 15 ((β„œ ∘ 𝑓) β†Ύ β„Ž) = (β„œ ∘ (𝑓 β†Ύ β„Ž))
161 fresin 6754 . . . . . . . . . . . . . . . . 17 (𝑓:π‘ŽβŸΆβ„‚ β†’ (𝑓 β†Ύ β„Ž):(π‘Ž ∩ β„Ž)βŸΆβ„‚)
162 ismbfcn 25513 . . . . . . . . . . . . . . . . 17 ((𝑓 β†Ύ β„Ž):(π‘Ž ∩ β„Ž)βŸΆβ„‚ β†’ ((𝑓 β†Ύ β„Ž) ∈ MblFn ↔ ((β„œ ∘ (𝑓 β†Ύ β„Ž)) ∈ MblFn ∧ (β„‘ ∘ (𝑓 β†Ύ β„Ž)) ∈ MblFn)))
163161, 162syl 17 . . . . . . . . . . . . . . . 16 (𝑓:π‘ŽβŸΆβ„‚ β†’ ((𝑓 β†Ύ β„Ž) ∈ MblFn ↔ ((β„œ ∘ (𝑓 β†Ύ β„Ž)) ∈ MblFn ∧ (β„‘ ∘ (𝑓 β†Ύ β„Ž)) ∈ MblFn)))
164163simprbda 498 . . . . . . . . . . . . . . 15 ((𝑓:π‘ŽβŸΆβ„‚ ∧ (𝑓 β†Ύ β„Ž) ∈ MblFn) β†’ (β„œ ∘ (𝑓 β†Ύ β„Ž)) ∈ MblFn)
165160, 164eqeltrid 2831 . . . . . . . . . . . . . 14 ((𝑓:π‘ŽβŸΆβ„‚ ∧ (𝑓 β†Ύ β„Ž) ∈ MblFn) β†’ ((β„œ ∘ 𝑓) β†Ύ β„Ž) ∈ MblFn)
166159, 165sylan2 592 . . . . . . . . . . . . 13 ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) β†’ ((β„œ ∘ 𝑓) β†Ύ β„Ž) ∈ MblFn)
167166ad2antrl 725 . . . . . . . . . . . 12 ((βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) ∧ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž)) β†’ ((β„œ ∘ 𝑓) β†Ύ β„Ž) ∈ MblFn)
168 uniun 4927 . . . . . . . . . . . . . . 15 βˆͺ (𝑑 βˆͺ {β„Ž}) = (βˆͺ 𝑑 βˆͺ βˆͺ {β„Ž})
169 unisnv 4924 . . . . . . . . . . . . . . . 16 βˆͺ {β„Ž} = β„Ž
170169uneq2i 4155 . . . . . . . . . . . . . . 15 (βˆͺ 𝑑 βˆͺ βˆͺ {β„Ž}) = (βˆͺ 𝑑 βˆͺ β„Ž)
171168, 170eqtri 2754 . . . . . . . . . . . . . 14 βˆͺ (𝑑 βˆͺ {β„Ž}) = (βˆͺ 𝑑 βˆͺ β„Ž)
172171, 121eqtr3id 2780 . . . . . . . . . . . . 13 (βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž β†’ (βˆͺ 𝑑 βˆͺ β„Ž) = π‘Ž)
173172ad2antll 726 . . . . . . . . . . . 12 ((βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) ∧ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž)) β†’ (βˆͺ 𝑑 βˆͺ β„Ž) = π‘Ž)
17489, 153, 167, 173mbfres2 25529 . . . . . . . . . . 11 ((βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) ∧ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž)) β†’ (β„œ ∘ 𝑓) ∈ MblFn)
175 imf 15066 . . . . . . . . . . . . . . 15 β„‘:β„‚βŸΆβ„
176 fco 6735 . . . . . . . . . . . . . . 15 ((β„‘:β„‚βŸΆβ„ ∧ 𝑓:π‘ŽβŸΆβ„‚) β†’ (β„‘ ∘ 𝑓):π‘ŽβŸΆβ„)
177175, 176mpan 687 . . . . . . . . . . . . . 14 (𝑓:π‘ŽβŸΆβ„‚ β†’ (β„‘ ∘ 𝑓):π‘ŽβŸΆβ„)
178177adantr 480 . . . . . . . . . . . . 13 ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) β†’ (β„‘ ∘ 𝑓):π‘ŽβŸΆβ„)
179178ad2antrl 725 . . . . . . . . . . . 12 ((βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) ∧ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž)) β†’ (β„‘ ∘ 𝑓):π‘ŽβŸΆβ„)
180 imcncf 24778 . . . . . . . . . . . . . . . . 17 β„‘ ∈ (ℂ–cn→ℝ)
181180elexi 3488 . . . . . . . . . . . . . . . 16 β„‘ ∈ V
182181, 92coex 7920 . . . . . . . . . . . . . . 15 (β„‘ ∘ 𝑓) ∈ V
183182resex 6023 . . . . . . . . . . . . . 14 ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ V
18497adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ βˆͺ 𝑑 = 𝑏)
185184biantrud 531 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ ((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ↔ ((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏)))
186 feq123 6701 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑 ∧ β„‚ = β„‚) β†’ (𝑔:π‘βŸΆβ„‚ ↔ ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚))
187100, 186mp3an3 1446 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ (𝑔:π‘βŸΆβ„‚ ↔ ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚))
188 reseq1 5969 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†’ (𝑔 β†Ύ 𝑠) = (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠))
189188eleq1d 2812 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†’ ((𝑔 β†Ύ 𝑠) ∈ MblFn ↔ (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn))
190189adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ ((𝑔 β†Ύ 𝑠) ∈ MblFn ↔ (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn))
191190ralbidv 3171 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ (βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn ↔ βˆ€π‘  ∈ 𝑑 (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn))
192187, 191anbi12d 630 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ ((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ↔ (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn)))
193185, 192bitr3d 281 . . . . . . . . . . . . . . . 16 ((𝑔 = ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ (((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) ↔ (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn)))
194 eleq1 2815 . . . . . . . . . . . . . . . . 17 (𝑔 = ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†’ (𝑔 ∈ MblFn ↔ ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn))
195194adantr 480 . . . . . . . . . . . . . . . 16 ((𝑔 = ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ (𝑔 ∈ MblFn ↔ ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn))
196193, 195imbi12d 344 . . . . . . . . . . . . . . 15 ((𝑔 = ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∧ 𝑏 = βˆͺ 𝑑) β†’ ((((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) ↔ ((((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn) β†’ ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn)))
197196spc2gv 3584 . . . . . . . . . . . . . 14 ((((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ V ∧ βˆͺ 𝑑 ∈ V) β†’ (βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) β†’ ((((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn) β†’ ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn)))
198183, 95, 197mp2an 689 . . . . . . . . . . . . 13 (βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) β†’ ((((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn) β†’ ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn))
199 fss 6728 . . . . . . . . . . . . . . . . . 18 ((β„‘:β„‚βŸΆβ„ ∧ ℝ βŠ† β„‚) β†’ β„‘:β„‚βŸΆβ„‚)
200175, 114, 199mp2an 689 . . . . . . . . . . . . . . . . 17 β„‘:β„‚βŸΆβ„‚
201 fco 6735 . . . . . . . . . . . . . . . . 17 ((β„‘:β„‚βŸΆβ„‚ ∧ 𝑓:π‘ŽβŸΆβ„‚) β†’ (β„‘ ∘ 𝑓):π‘ŽβŸΆβ„‚)
202200, 201mpan 687 . . . . . . . . . . . . . . . 16 (𝑓:π‘ŽβŸΆβ„‚ β†’ (β„‘ ∘ 𝑓):π‘ŽβŸΆβ„‚)
203 fssres 6751 . . . . . . . . . . . . . . . 16 (((β„‘ ∘ 𝑓):π‘ŽβŸΆβ„‚ ∧ βˆͺ 𝑑 βŠ† π‘Ž) β†’ ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚)
204202, 122, 203syl2an 595 . . . . . . . . . . . . . . 15 ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž) β†’ ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚)
205204adantlr 712 . . . . . . . . . . . . . 14 (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž) β†’ ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚)
206126resabs1d 6006 . . . . . . . . . . . . . . . . . . . 20 (π‘Ÿ ∈ 𝑑 β†’ (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) = ((β„‘ ∘ 𝑓) β†Ύ π‘Ÿ))
207 resco 6243 . . . . . . . . . . . . . . . . . . . 20 ((β„‘ ∘ 𝑓) β†Ύ π‘Ÿ) = (β„‘ ∘ (𝑓 β†Ύ π‘Ÿ))
208206, 207eqtrdi 2782 . . . . . . . . . . . . . . . . . . 19 (π‘Ÿ ∈ 𝑑 β†’ (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) = (β„‘ ∘ (𝑓 β†Ύ π‘Ÿ)))
209208adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ π‘Ÿ ∈ 𝑑) β†’ (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) = (β„‘ ∘ (𝑓 β†Ύ π‘Ÿ)))
210142simprd 495 . . . . . . . . . . . . . . . . . 18 (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ π‘Ÿ ∈ 𝑑) β†’ (β„‘ ∘ (𝑓 β†Ύ π‘Ÿ)) ∈ MblFn)
211209, 210eqeltrd 2827 . . . . . . . . . . . . . . . . 17 (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ π‘Ÿ ∈ 𝑑) β†’ (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) ∈ MblFn)
212211ralrimiva 3140 . . . . . . . . . . . . . . . 16 ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) β†’ βˆ€π‘Ÿ ∈ 𝑑 (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) ∈ MblFn)
213 reseq2 5970 . . . . . . . . . . . . . . . . . 18 (π‘Ÿ = 𝑠 β†’ (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) = (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠))
214213eleq1d 2812 . . . . . . . . . . . . . . . . 17 (π‘Ÿ = 𝑠 β†’ ((((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) ∈ MblFn ↔ (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn))
215214cbvralvw 3228 . . . . . . . . . . . . . . . 16 (βˆ€π‘Ÿ ∈ 𝑑 (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ π‘Ÿ) ∈ MblFn ↔ βˆ€π‘  ∈ 𝑑 (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn)
216212, 215sylib 217 . . . . . . . . . . . . . . 15 ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) β†’ βˆ€π‘  ∈ 𝑑 (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn)
217216adantr 480 . . . . . . . . . . . . . 14 (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž) β†’ βˆ€π‘  ∈ 𝑑 (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn)
218 pm2.27 42 . . . . . . . . . . . . . 14 ((((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn) β†’ (((((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn) β†’ ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn) β†’ ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn))
219205, 217, 218syl2anc 583 . . . . . . . . . . . . 13 (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž) β†’ (((((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑):βˆͺ π‘‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) β†Ύ 𝑠) ∈ MblFn) β†’ ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn) β†’ ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn))
220198, 219mpan9 506 . . . . . . . . . . . 12 ((βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) ∧ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž)) β†’ ((β„‘ ∘ 𝑓) β†Ύ βˆͺ 𝑑) ∈ MblFn)
221 resco 6243 . . . . . . . . . . . . . . 15 ((β„‘ ∘ 𝑓) β†Ύ β„Ž) = (β„‘ ∘ (𝑓 β†Ύ β„Ž))
222163simplbda 499 . . . . . . . . . . . . . . 15 ((𝑓:π‘ŽβŸΆβ„‚ ∧ (𝑓 β†Ύ β„Ž) ∈ MblFn) β†’ (β„‘ ∘ (𝑓 β†Ύ β„Ž)) ∈ MblFn)
223221, 222eqeltrid 2831 . . . . . . . . . . . . . 14 ((𝑓:π‘ŽβŸΆβ„‚ ∧ (𝑓 β†Ύ β„Ž) ∈ MblFn) β†’ ((β„‘ ∘ 𝑓) β†Ύ β„Ž) ∈ MblFn)
224159, 223sylan2 592 . . . . . . . . . . . . 13 ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) β†’ ((β„‘ ∘ 𝑓) β†Ύ β„Ž) ∈ MblFn)
225224ad2antrl 725 . . . . . . . . . . . 12 ((βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) ∧ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž)) β†’ ((β„‘ ∘ 𝑓) β†Ύ β„Ž) ∈ MblFn)
226179, 220, 225, 173mbfres2 25529 . . . . . . . . . . 11 ((βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) ∧ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž)) β†’ (β„‘ ∘ 𝑓) ∈ MblFn)
227 ismbfcn 25513 . . . . . . . . . . . . 13 (𝑓:π‘ŽβŸΆβ„‚ β†’ (𝑓 ∈ MblFn ↔ ((β„œ ∘ 𝑓) ∈ MblFn ∧ (β„‘ ∘ 𝑓) ∈ MblFn)))
228227adantr 480 . . . . . . . . . . . 12 ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) β†’ (𝑓 ∈ MblFn ↔ ((β„œ ∘ 𝑓) ∈ MblFn ∧ (β„‘ ∘ 𝑓) ∈ MblFn)))
229228ad2antrl 725 . . . . . . . . . . 11 ((βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) ∧ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž)) β†’ (𝑓 ∈ MblFn ↔ ((β„œ ∘ 𝑓) ∈ MblFn ∧ (β„‘ ∘ 𝑓) ∈ MblFn)))
230174, 226, 229mpbir2and 710 . . . . . . . . . 10 ((βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) ∧ ((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž)) β†’ 𝑓 ∈ MblFn)
231230ex 412 . . . . . . . . 9 (βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) β†’ (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž) β†’ 𝑓 ∈ MblFn))
232231alrimivv 1923 . . . . . . . 8 (βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) β†’ βˆ€π‘“βˆ€π‘Ž(((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž) β†’ 𝑓 ∈ MblFn))
233232a1i 11 . . . . . . 7 (𝑑 ∈ Fin β†’ (βˆ€π‘”βˆ€π‘(((𝑔:π‘βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑑 (𝑔 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑑 = 𝑏) β†’ 𝑔 ∈ MblFn) β†’ βˆ€π‘“βˆ€π‘Ž(((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ (𝑑 βˆͺ {β„Ž})(𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ (𝑑 βˆͺ {β„Ž}) = π‘Ž) β†’ 𝑓 ∈ MblFn)))
23435, 58, 65, 72, 84, 233findcard2 9166 . . . . . 6 (𝑆 ∈ Fin β†’ βˆ€π‘“βˆ€π‘Ž(((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = π‘Ž) β†’ 𝑓 ∈ MblFn))
235 2sp 2171 . . . . . 6 (βˆ€π‘“βˆ€π‘Ž(((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = π‘Ž) β†’ 𝑓 ∈ MblFn) β†’ (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = π‘Ž) β†’ 𝑓 ∈ MblFn))
2364, 234, 2353syl 18 . . . . 5 (πœ‘ β†’ (((𝑓:π‘ŽβŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝑓 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = π‘Ž) β†’ 𝑓 ∈ MblFn))
23716, 25, 236vtocl2g 3557 . . . 4 ((𝐴 ∈ V ∧ 𝐹 ∈ V) β†’ (πœ‘ β†’ (((𝐹:π΄βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝐹 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = 𝐴) β†’ 𝐹 ∈ MblFn)))
23810, 237mpcom 38 . . 3 (πœ‘ β†’ (((𝐹:π΄βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝐹 β†Ύ 𝑠) ∈ MblFn) ∧ βˆͺ 𝑆 = 𝐴) β†’ 𝐹 ∈ MblFn))
2393, 238mpan2d 691 . 2 (πœ‘ β†’ ((𝐹:π΄βŸΆβ„‚ ∧ βˆ€π‘  ∈ 𝑆 (𝐹 β†Ύ 𝑠) ∈ MblFn) β†’ 𝐹 ∈ MblFn))
2401, 2, 239mp2and 696 1 (πœ‘ β†’ 𝐹 ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395  βˆ€wal 1531   = wceq 1533   ∈ wcel 2098  βˆ€wral 3055  Vcvv 3468   βˆͺ cun 3941   ∩ cin 3942   βŠ† wss 3943  βˆ…c0 4317  {csn 4623  βˆͺ cuni 4902  dom cdm 5669   β†Ύ cres 5671   ∘ ccom 5673  Rel wrel 5674  βŸΆwf 6533  (class class class)co 7405  Fincfn 8941  β„‚cc 11110  β„cr 11111  β„œcre 15050  β„‘cim 15051  β€“cnβ†’ccncf 24751  MblFncmbf 25498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7667  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-2o 8468  df-er 8705  df-map 8824  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-z 12563  df-uz 12827  df-q 12937  df-rp 12981  df-xadd 13099  df-ioo 13334  df-ico 13336  df-icc 13337  df-fz 13491  df-fzo 13634  df-fl 13763  df-seq 13973  df-exp 14033  df-hash 14296  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-clim 15438  df-sum 15639  df-xmet 21233  df-met 21234  df-cncf 24753  df-ovol 25348  df-vol 25349  df-mbf 25503
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator