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 33427
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 6940 . . . . . . 7 (𝑆 ∈ Fin → 𝑆 ∈ V)
64, 5syl 17 . . . . . 6 (𝜑 𝑆 ∈ V)
73, 6eqeltrrd 2700 . . . . 5 (𝜑𝐴 ∈ V)
8 fex 6475 . . . . . . 7 ((𝐹:𝐴⟶ℂ ∧ 𝐴 ∈ V) → 𝐹 ∈ V)
98ex 450 . . . . . 6 (𝐹:𝐴⟶ℂ → (𝐴 ∈ V → 𝐹 ∈ V))
101, 9syl 17 . . . . 5 (𝜑 → (𝐴 ∈ V → 𝐹 ∈ V))
117, 10jcai 558 . . . 4 (𝜑 → (𝐴 ∈ V ∧ 𝐹 ∈ V))
12 feq2 6014 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑓:𝑎⟶ℂ ↔ 𝑓:𝐴⟶ℂ))
1312anbi1d 740 . . . . . . . 8 (𝑎 = 𝐴 → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ↔ (𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn)))
14 eqeq2 2631 . . . . . . . 8 (𝑎 = 𝐴 → ( 𝑆 = 𝑎 𝑆 = 𝐴))
1513, 14anbi12d 746 . . . . . . 7 (𝑎 = 𝐴 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) ↔ ((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴)))
1615imbi1d 331 . . . . . 6 (𝑎 = 𝐴 → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝑓 ∈ MblFn)))
1716imbi2d 330 . . . . 5 (𝑎 = 𝐴 → ((𝜑 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn)) ↔ (𝜑 → (((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝑓 ∈ MblFn))))
18 feq1 6013 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓:𝐴⟶ℂ ↔ 𝐹:𝐴⟶ℂ))
19 reseq1 5379 . . . . . . . . . . 11 (𝑓 = 𝐹 → (𝑓𝑠) = (𝐹𝑠))
2019eleq1d 2684 . . . . . . . . . 10 (𝑓 = 𝐹 → ((𝑓𝑠) ∈ MblFn ↔ (𝐹𝑠) ∈ MblFn))
2120ralbidv 2983 . . . . . . . . 9 (𝑓 = 𝐹 → (∀𝑠𝑆 (𝑓𝑠) ∈ MblFn ↔ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn))
2218, 21anbi12d 746 . . . . . . . 8 (𝑓 = 𝐹 → ((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn)))
2322anbi1d 740 . . . . . . 7 (𝑓 = 𝐹 → (((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) ↔ ((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴)))
24 eleq1 2687 . . . . . . 7 (𝑓 = 𝐹 → (𝑓 ∈ MblFn ↔ 𝐹 ∈ MblFn))
2523, 24imbi12d 334 . . . . . 6 (𝑓 = 𝐹 → ((((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝑓 ∈ MblFn) ↔ (((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝐹 ∈ MblFn)))
2625imbi2d 330 . . . . 5 (𝑓 = 𝐹 → ((𝜑 → (((𝑓:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝑓 ∈ MblFn)) ↔ (𝜑 → (((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝐹 ∈ MblFn))))
27 rzal 4064 . . . . . . . . . . . 12 (𝑟 = ∅ → ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn)
2827biantrud 528 . . . . . . . . . . 11 (𝑟 = ∅ → (𝑓:𝑎⟶ℂ ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn)))
2928bicomd 213 . . . . . . . . . 10 (𝑟 = ∅ → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ↔ 𝑓:𝑎⟶ℂ))
30 unieq 4435 . . . . . . . . . . . 12 (𝑟 = ∅ → 𝑟 = ∅)
31 uni0 4456 . . . . . . . . . . . 12 ∅ = ∅
3230, 31syl6eq 2670 . . . . . . . . . . 11 (𝑟 = ∅ → 𝑟 = ∅)
3332eqeq1d 2622 . . . . . . . . . 10 (𝑟 = ∅ → ( 𝑟 = 𝑎 ↔ ∅ = 𝑎))
3429, 33anbi12d 746 . . . . . . . . 9 (𝑟 = ∅ → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) ↔ (𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎)))
3534imbi1d 331 . . . . . . . 8 (𝑟 = ∅ → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn)))
36352albidv 1849 . . . . . . 7 (𝑟 = ∅ → (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑓𝑎((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn)))
37 raleq 3133 . . . . . . . . . . . 12 (𝑟 = 𝑡 → (∀𝑠𝑟 (𝑓𝑠) ∈ MblFn ↔ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn))
3837anbi2d 739 . . . . . . . . . . 11 (𝑟 = 𝑡 → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn)))
39 unieq 4435 . . . . . . . . . . . 12 (𝑟 = 𝑡 𝑟 = 𝑡)
4039eqeq1d 2622 . . . . . . . . . . 11 (𝑟 = 𝑡 → ( 𝑟 = 𝑎 𝑡 = 𝑎))
4138, 40anbi12d 746 . . . . . . . . . 10 (𝑟 = 𝑡 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) ↔ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎)))
4241imbi1d 331 . . . . . . . . 9 (𝑟 = 𝑡 → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎) → 𝑓 ∈ MblFn)))
43422albidv 1849 . . . . . . . 8 (𝑟 = 𝑡 → (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎) → 𝑓 ∈ MblFn)))
44 simpl 473 . . . . . . . . . . . . 13 ((𝑓 = 𝑔𝑎 = 𝑏) → 𝑓 = 𝑔)
45 simpr 477 . . . . . . . . . . . . 13 ((𝑓 = 𝑔𝑎 = 𝑏) → 𝑎 = 𝑏)
4644, 45feq12d 6020 . . . . . . . . . . . 12 ((𝑓 = 𝑔𝑎 = 𝑏) → (𝑓:𝑎⟶ℂ ↔ 𝑔:𝑏⟶ℂ))
47 reseq1 5379 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝑓𝑠) = (𝑔𝑠))
4847adantr 481 . . . . . . . . . . . . . 14 ((𝑓 = 𝑔𝑎 = 𝑏) → (𝑓𝑠) = (𝑔𝑠))
4948eleq1d 2684 . . . . . . . . . . . . 13 ((𝑓 = 𝑔𝑎 = 𝑏) → ((𝑓𝑠) ∈ MblFn ↔ (𝑔𝑠) ∈ MblFn))
5049ralbidv 2983 . . . . . . . . . . . 12 ((𝑓 = 𝑔𝑎 = 𝑏) → (∀𝑠𝑡 (𝑓𝑠) ∈ MblFn ↔ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn))
5146, 50anbi12d 746 . . . . . . . . . . 11 ((𝑓 = 𝑔𝑎 = 𝑏) → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ↔ (𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn)))
52 eqeq2 2631 . . . . . . . . . . . 12 (𝑎 = 𝑏 → ( 𝑡 = 𝑎 𝑡 = 𝑏))
5352adantl 482 . . . . . . . . . . 11 ((𝑓 = 𝑔𝑎 = 𝑏) → ( 𝑡 = 𝑎 𝑡 = 𝑏))
5451, 53anbi12d 746 . . . . . . . . . 10 ((𝑓 = 𝑔𝑎 = 𝑏) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎) ↔ ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏)))
55 eleq1 2687 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑓 ∈ MblFn ↔ 𝑔 ∈ MblFn))
5655adantr 481 . . . . . . . . . 10 ((𝑓 = 𝑔𝑎 = 𝑏) → (𝑓 ∈ MblFn ↔ 𝑔 ∈ MblFn))
5754, 56imbi12d 334 . . . . . . . . 9 ((𝑓 = 𝑔𝑎 = 𝑏) → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn)))
5857cbval2v 2283 . . . . . . . 8 (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑡 (𝑓𝑠) ∈ MblFn) ∧ 𝑡 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn))
5943, 58syl6bb 276 . . . . . . 7 (𝑟 = 𝑡 → (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn)))
60 raleq 3133 . . . . . . . . . . 11 (𝑟 = (𝑡 ∪ {}) → (∀𝑠𝑟 (𝑓𝑠) ∈ MblFn ↔ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn))
6160anbi2d 739 . . . . . . . . . 10 (𝑟 = (𝑡 ∪ {}) → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn)))
62 unieq 4435 . . . . . . . . . . 11 (𝑟 = (𝑡 ∪ {}) → 𝑟 = (𝑡 ∪ {}))
6362eqeq1d 2622 . . . . . . . . . 10 (𝑟 = (𝑡 ∪ {}) → ( 𝑟 = 𝑎 (𝑡 ∪ {}) = 𝑎))
6461, 63anbi12d 746 . . . . . . . . 9 (𝑟 = (𝑡 ∪ {}) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) ↔ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)))
6564imbi1d 331 . . . . . . . 8 (𝑟 = (𝑡 ∪ {}) → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → 𝑓 ∈ MblFn)))
66652albidv 1849 . . . . . . 7 (𝑟 = (𝑡 ∪ {}) → (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → 𝑓 ∈ MblFn)))
67 raleq 3133 . . . . . . . . . . 11 (𝑟 = 𝑆 → (∀𝑠𝑟 (𝑓𝑠) ∈ MblFn ↔ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn))
6867anbi2d 739 . . . . . . . . . 10 (𝑟 = 𝑆 → ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ↔ (𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn)))
69 unieq 4435 . . . . . . . . . . 11 (𝑟 = 𝑆 𝑟 = 𝑆)
7069eqeq1d 2622 . . . . . . . . . 10 (𝑟 = 𝑆 → ( 𝑟 = 𝑎 𝑆 = 𝑎))
7168, 70anbi12d 746 . . . . . . . . 9 (𝑟 = 𝑆 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) ↔ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎)))
7271imbi1d 331 . . . . . . . 8 (𝑟 = 𝑆 → ((((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn)))
73722albidv 1849 . . . . . . 7 (𝑟 = 𝑆 → (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑟 (𝑓𝑠) ∈ MblFn) ∧ 𝑟 = 𝑎) → 𝑓 ∈ MblFn) ↔ ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn)))
74 frel 6037 . . . . . . . . . 10 (𝑓:𝑎⟶ℂ → Rel 𝑓)
7574adantr 481 . . . . . . . . 9 ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → Rel 𝑓)
76 fdm 6038 . . . . . . . . . 10 (𝑓:𝑎⟶ℂ → dom 𝑓 = 𝑎)
77 eqcom 2627 . . . . . . . . . . 11 (∅ = 𝑎𝑎 = ∅)
7877biimpi 206 . . . . . . . . . 10 (∅ = 𝑎𝑎 = ∅)
7976, 78sylan9eq 2674 . . . . . . . . 9 ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → dom 𝑓 = ∅)
80 reldm0 5332 . . . . . . . . . . 11 (Rel 𝑓 → (𝑓 = ∅ ↔ dom 𝑓 = ∅))
8180biimpar 502 . . . . . . . . . 10 ((Rel 𝑓 ∧ dom 𝑓 = ∅) → 𝑓 = ∅)
82 0mbf 33426 . . . . . . . . . 10 ∅ ∈ MblFn
8381, 82syl6eqel 2707 . . . . . . . . 9 ((Rel 𝑓 ∧ dom 𝑓 = ∅) → 𝑓 ∈ MblFn)
8475, 79, 83syl2anc 692 . . . . . . . 8 ((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn)
8584gen2 1721 . . . . . . 7 𝑓𝑎((𝑓:𝑎⟶ℂ ∧ ∅ = 𝑎) → 𝑓 ∈ MblFn)
86 ref 13833 . . . . . . . . . . . . . . 15 ℜ:ℂ⟶ℝ
87 fco 6045 . . . . . . . . . . . . . . 15 ((ℜ:ℂ⟶ℝ ∧ 𝑓:𝑎⟶ℂ) → (ℜ ∘ 𝑓):𝑎⟶ℝ)
8886, 87mpan 705 . . . . . . . . . . . . . 14 (𝑓:𝑎⟶ℂ → (ℜ ∘ 𝑓):𝑎⟶ℝ)
8988adantr 481 . . . . . . . . . . . . 13 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → (ℜ ∘ 𝑓):𝑎⟶ℝ)
9089ad2antrl 763 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → (ℜ ∘ 𝑓):𝑎⟶ℝ)
91 recncf 22686 . . . . . . . . . . . . . . . . 17 ℜ ∈ (ℂ–cn→ℝ)
9291elexi 3208 . . . . . . . . . . . . . . . 16 ℜ ∈ V
93 vex 3198 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
9492, 93coex 7103 . . . . . . . . . . . . . . 15 (ℜ ∘ 𝑓) ∈ V
9594resex 5431 . . . . . . . . . . . . . 14 ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ V
96 vuniex 6939 . . . . . . . . . . . . . 14 𝑡 ∈ V
97 eqcom 2627 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑡 𝑡 = 𝑏)
9897biimpi 206 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑡 𝑡 = 𝑏)
9998adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → 𝑡 = 𝑏)
10099biantrud 528 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ↔ ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏)))
101 eqid 2620 . . . . . . . . . . . . . . . . . . 19 ℂ = ℂ
102 feq123 6022 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡 ∧ ℂ = ℂ) → (𝑔:𝑏⟶ℂ ↔ ((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ))
103101, 102mp3an3 1411 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (𝑔:𝑏⟶ℂ ↔ ((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ))
104 reseq1 5379 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) → (𝑔𝑠) = (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠))
105104eleq1d 2684 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) → ((𝑔𝑠) ∈ MblFn ↔ (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
106105adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔𝑠) ∈ MblFn ↔ (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
107106ralbidv 2983 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (∀𝑠𝑡 (𝑔𝑠) ∈ MblFn ↔ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
108103, 107anbi12d 746 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ↔ (((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)))
109100, 108bitr3d 270 . . . . . . . . . . . . . . . 16 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) ↔ (((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)))
110 eleq1 2687 . . . . . . . . . . . . . . . . 17 (𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) → (𝑔 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
111110adantr 481 . . . . . . . . . . . . . . . 16 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (𝑔 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
112109, 111imbi12d 334 . . . . . . . . . . . . . . 15 ((𝑔 = ((ℜ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ↔ ((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)))
113112spc2gv 3291 . . . . . . . . . . . . . 14 ((((ℜ ∘ 𝑓) ↾ 𝑡) ∈ V ∧ 𝑡 ∈ V) → (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)))
11495, 96, 113mp2an 707 . . . . . . . . . . . . 13 (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
115 ax-resscn 9978 . . . . . . . . . . . . . . . . . 18 ℝ ⊆ ℂ
116 fss 6043 . . . . . . . . . . . . . . . . . 18 ((ℜ:ℂ⟶ℝ ∧ ℝ ⊆ ℂ) → ℜ:ℂ⟶ℂ)
11786, 115, 116mp2an 707 . . . . . . . . . . . . . . . . 17 ℜ:ℂ⟶ℂ
118 fco 6045 . . . . . . . . . . . . . . . . 17 ((ℜ:ℂ⟶ℂ ∧ 𝑓:𝑎⟶ℂ) → (ℜ ∘ 𝑓):𝑎⟶ℂ)
119117, 118mpan 705 . . . . . . . . . . . . . . . 16 (𝑓:𝑎⟶ℂ → (ℜ ∘ 𝑓):𝑎⟶ℂ)
120 ssun1 3768 . . . . . . . . . . . . . . . . . 18 𝑡 ⊆ (𝑡 ∪ {})
121120unissi 4452 . . . . . . . . . . . . . . . . 17 𝑡 (𝑡 ∪ {})
122 id 22 . . . . . . . . . . . . . . . . 17 ( (𝑡 ∪ {}) = 𝑎 (𝑡 ∪ {}) = 𝑎)
123121, 122syl5sseq 3645 . . . . . . . . . . . . . . . 16 ( (𝑡 ∪ {}) = 𝑎 𝑡𝑎)
124 fssres 6057 . . . . . . . . . . . . . . . 16 (((ℜ ∘ 𝑓):𝑎⟶ℂ ∧ 𝑡𝑎) → ((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
125119, 123, 124syl2an 494 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ (𝑡 ∪ {}) = 𝑎) → ((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
126125adantlr 750 . . . . . . . . . . . . . 14 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → ((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
127 elssuni 4458 . . . . . . . . . . . . . . . . . . . . 21 (𝑟𝑡𝑟 𝑡)
128127resabs1d 5416 . . . . . . . . . . . . . . . . . . . 20 (𝑟𝑡 → (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = ((ℜ ∘ 𝑓) ↾ 𝑟))
129 resco 5627 . . . . . . . . . . . . . . . . . . . 20 ((ℜ ∘ 𝑓) ↾ 𝑟) = (ℜ ∘ (𝑓𝑟))
130128, 129syl6eq 2670 . . . . . . . . . . . . . . . . . . 19 (𝑟𝑡 → (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (ℜ ∘ (𝑓𝑟)))
131130adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (ℜ ∘ (𝑓𝑟)))
132 elun1 3772 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟𝑡𝑟 ∈ (𝑡 ∪ {}))
133 reseq2 5380 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = 𝑟 → (𝑓𝑠) = (𝑓𝑟))
134133eleq1d 2684 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = 𝑟 → ((𝑓𝑠) ∈ MblFn ↔ (𝑓𝑟) ∈ MblFn))
135134rspccva 3303 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn ∧ 𝑟 ∈ (𝑡 ∪ {})) → (𝑓𝑟) ∈ MblFn)
136132, 135sylan2 491 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn ∧ 𝑟𝑡) → (𝑓𝑟) ∈ MblFn)
137136adantll 749 . . . . . . . . . . . . . . . . . . . 20 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (𝑓𝑟) ∈ MblFn)
138 fresin 6060 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓:𝑎⟶ℂ → (𝑓𝑟):(𝑎𝑟)⟶ℂ)
139 ismbfcn 23379 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑟):(𝑎𝑟)⟶ℂ → ((𝑓𝑟) ∈ MblFn ↔ ((ℜ ∘ (𝑓𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓𝑟)) ∈ MblFn)))
140138, 139syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:𝑎⟶ℂ → ((𝑓𝑟) ∈ MblFn ↔ ((ℜ ∘ (𝑓𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓𝑟)) ∈ MblFn)))
141140biimpd 219 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:𝑎⟶ℂ → ((𝑓𝑟) ∈ MblFn → ((ℜ ∘ (𝑓𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓𝑟)) ∈ MblFn)))
142141ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → ((𝑓𝑟) ∈ MblFn → ((ℜ ∘ (𝑓𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓𝑟)) ∈ MblFn)))
143137, 142mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → ((ℜ ∘ (𝑓𝑟)) ∈ MblFn ∧ (ℑ ∘ (𝑓𝑟)) ∈ MblFn))
144143simpld 475 . . . . . . . . . . . . . . . . . 18 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (ℜ ∘ (𝑓𝑟)) ∈ MblFn)
145131, 144eqeltrd 2699 . . . . . . . . . . . . . . . . 17 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn)
146145ralrimiva 2963 . . . . . . . . . . . . . . . 16 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ∀𝑟𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn)
147 reseq2 5380 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑠 → (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠))
148147eleq1d 2684 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑠 → ((((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn ↔ (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
149148cbvralv 3166 . . . . . . . . . . . . . . . 16 (∀𝑟𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn ↔ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
150146, 149sylib 208 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
151150adantr 481 . . . . . . . . . . . . . 14 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
152 pm2.27 42 . . . . . . . . . . . . . 14 ((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → (((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
153126, 151, 152syl2anc 692 . . . . . . . . . . . . 13 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → (((((ℜ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℜ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
154114, 153mpan9 486 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → ((ℜ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)
155 vsnid 4200 . . . . . . . . . . . . . . 15 ∈ {}
156 elun2 3773 . . . . . . . . . . . . . . 15 ( ∈ {} → ∈ (𝑡 ∪ {}))
157 reseq2 5380 . . . . . . . . . . . . . . . . 17 (𝑠 = → (𝑓𝑠) = (𝑓))
158157eleq1d 2684 . . . . . . . . . . . . . . . 16 (𝑠 = → ((𝑓𝑠) ∈ MblFn ↔ (𝑓) ∈ MblFn))
159158rspcv 3300 . . . . . . . . . . . . . . 15 ( ∈ (𝑡 ∪ {}) → (∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn → (𝑓) ∈ MblFn))
160155, 156, 159mp2b 10 . . . . . . . . . . . . . 14 (∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn → (𝑓) ∈ MblFn)
161 resco 5627 . . . . . . . . . . . . . . 15 ((ℜ ∘ 𝑓) ↾ ) = (ℜ ∘ (𝑓))
162 fresin 6060 . . . . . . . . . . . . . . . . 17 (𝑓:𝑎⟶ℂ → (𝑓):(𝑎)⟶ℂ)
163 ismbfcn 23379 . . . . . . . . . . . . . . . . 17 ((𝑓):(𝑎)⟶ℂ → ((𝑓) ∈ MblFn ↔ ((ℜ ∘ (𝑓)) ∈ MblFn ∧ (ℑ ∘ (𝑓)) ∈ MblFn)))
164162, 163syl 17 . . . . . . . . . . . . . . . 16 (𝑓:𝑎⟶ℂ → ((𝑓) ∈ MblFn ↔ ((ℜ ∘ (𝑓)) ∈ MblFn ∧ (ℑ ∘ (𝑓)) ∈ MblFn)))
165164simprbda 652 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ (𝑓) ∈ MblFn) → (ℜ ∘ (𝑓)) ∈ MblFn)
166161, 165syl5eqel 2703 . . . . . . . . . . . . . 14 ((𝑓:𝑎⟶ℂ ∧ (𝑓) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ ) ∈ MblFn)
167160, 166sylan2 491 . . . . . . . . . . . . 13 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ((ℜ ∘ 𝑓) ↾ ) ∈ MblFn)
168167ad2antrl 763 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → ((ℜ ∘ 𝑓) ↾ ) ∈ MblFn)
169 uniun 4447 . . . . . . . . . . . . . . 15 (𝑡 ∪ {}) = ( 𝑡 {})
170 vex 3198 . . . . . . . . . . . . . . . . 17 ∈ V
171170unisn 4442 . . . . . . . . . . . . . . . 16 {} =
172171uneq2i 3756 . . . . . . . . . . . . . . 15 ( 𝑡 {}) = ( 𝑡)
173169, 172eqtri 2642 . . . . . . . . . . . . . 14 (𝑡 ∪ {}) = ( 𝑡)
174173, 122syl5eqr 2668 . . . . . . . . . . . . 13 ( (𝑡 ∪ {}) = 𝑎 → ( 𝑡) = 𝑎)
175174ad2antll 764 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → ( 𝑡) = 𝑎)
17690, 154, 168, 175mbfres2 23393 . . . . . . . . . . 11 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → (ℜ ∘ 𝑓) ∈ MblFn)
177 imf 13834 . . . . . . . . . . . . . . 15 ℑ:ℂ⟶ℝ
178 fco 6045 . . . . . . . . . . . . . . 15 ((ℑ:ℂ⟶ℝ ∧ 𝑓:𝑎⟶ℂ) → (ℑ ∘ 𝑓):𝑎⟶ℝ)
179177, 178mpan 705 . . . . . . . . . . . . . 14 (𝑓:𝑎⟶ℂ → (ℑ ∘ 𝑓):𝑎⟶ℝ)
180179adantr 481 . . . . . . . . . . . . 13 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → (ℑ ∘ 𝑓):𝑎⟶ℝ)
181180ad2antrl 763 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → (ℑ ∘ 𝑓):𝑎⟶ℝ)
182 imcncf 22687 . . . . . . . . . . . . . . . . 17 ℑ ∈ (ℂ–cn→ℝ)
183182elexi 3208 . . . . . . . . . . . . . . . 16 ℑ ∈ V
184183, 93coex 7103 . . . . . . . . . . . . . . 15 (ℑ ∘ 𝑓) ∈ V
185184resex 5431 . . . . . . . . . . . . . 14 ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ V
18698adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → 𝑡 = 𝑏)
187186biantrud 528 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ↔ ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏)))
188 feq123 6022 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡 ∧ ℂ = ℂ) → (𝑔:𝑏⟶ℂ ↔ ((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ))
189101, 188mp3an3 1411 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (𝑔:𝑏⟶ℂ ↔ ((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ))
190 reseq1 5379 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) → (𝑔𝑠) = (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠))
191190eleq1d 2684 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) → ((𝑔𝑠) ∈ MblFn ↔ (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
192191adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔𝑠) ∈ MblFn ↔ (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
193192ralbidv 2983 . . . . . . . . . . . . . . . . . 18 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (∀𝑠𝑡 (𝑔𝑠) ∈ MblFn ↔ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
194189, 193anbi12d 746 . . . . . . . . . . . . . . . . 17 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ↔ (((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)))
195187, 194bitr3d 270 . . . . . . . . . . . . . . . 16 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) ↔ (((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)))
196 eleq1 2687 . . . . . . . . . . . . . . . . 17 (𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) → (𝑔 ∈ MblFn ↔ ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
197196adantr 481 . . . . . . . . . . . . . . . 16 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → (𝑔 ∈ MblFn ↔ ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
198195, 197imbi12d 334 . . . . . . . . . . . . . . 15 ((𝑔 = ((ℑ ∘ 𝑓) ↾ 𝑡) ∧ 𝑏 = 𝑡) → ((((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ↔ ((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)))
199198spc2gv 3291 . . . . . . . . . . . . . 14 ((((ℑ ∘ 𝑓) ↾ 𝑡) ∈ V ∧ 𝑡 ∈ V) → (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)))
200185, 96, 199mp2an 707 . . . . . . . . . . . . 13 (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
201 fss 6043 . . . . . . . . . . . . . . . . . 18 ((ℑ:ℂ⟶ℝ ∧ ℝ ⊆ ℂ) → ℑ:ℂ⟶ℂ)
202177, 115, 201mp2an 707 . . . . . . . . . . . . . . . . 17 ℑ:ℂ⟶ℂ
203 fco 6045 . . . . . . . . . . . . . . . . 17 ((ℑ:ℂ⟶ℂ ∧ 𝑓:𝑎⟶ℂ) → (ℑ ∘ 𝑓):𝑎⟶ℂ)
204202, 203mpan 705 . . . . . . . . . . . . . . . 16 (𝑓:𝑎⟶ℂ → (ℑ ∘ 𝑓):𝑎⟶ℂ)
205 fssres 6057 . . . . . . . . . . . . . . . 16 (((ℑ ∘ 𝑓):𝑎⟶ℂ ∧ 𝑡𝑎) → ((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
206204, 123, 205syl2an 494 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ (𝑡 ∪ {}) = 𝑎) → ((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
207206adantlr 750 . . . . . . . . . . . . . 14 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → ((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ)
208127resabs1d 5416 . . . . . . . . . . . . . . . . . . . 20 (𝑟𝑡 → (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = ((ℑ ∘ 𝑓) ↾ 𝑟))
209 resco 5627 . . . . . . . . . . . . . . . . . . . 20 ((ℑ ∘ 𝑓) ↾ 𝑟) = (ℑ ∘ (𝑓𝑟))
210208, 209syl6eq 2670 . . . . . . . . . . . . . . . . . . 19 (𝑟𝑡 → (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (ℑ ∘ (𝑓𝑟)))
211210adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (ℑ ∘ (𝑓𝑟)))
212143simprd 479 . . . . . . . . . . . . . . . . . 18 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (ℑ ∘ (𝑓𝑟)) ∈ MblFn)
213211, 212eqeltrd 2699 . . . . . . . . . . . . . . . . 17 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ 𝑟𝑡) → (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn)
214213ralrimiva 2963 . . . . . . . . . . . . . . . 16 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ∀𝑟𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn)
215 reseq2 5380 . . . . . . . . . . . . . . . . . 18 (𝑟 = 𝑠 → (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) = (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠))
216215eleq1d 2684 . . . . . . . . . . . . . . . . 17 (𝑟 = 𝑠 → ((((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn ↔ (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn))
217216cbvralv 3166 . . . . . . . . . . . . . . . 16 (∀𝑟𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑟) ∈ MblFn ↔ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
218214, 217sylib 208 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
219218adantr 481 . . . . . . . . . . . . . 14 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn)
220 pm2.27 42 . . . . . . . . . . . . . 14 ((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → (((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
221207, 219, 220syl2anc 692 . . . . . . . . . . . . 13 (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → (((((ℑ ∘ 𝑓) ↾ 𝑡): 𝑡⟶ℂ ∧ ∀𝑠𝑡 (((ℑ ∘ 𝑓) ↾ 𝑡) ↾ 𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn))
222200, 221mpan9 486 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → ((ℑ ∘ 𝑓) ↾ 𝑡) ∈ MblFn)
223 resco 5627 . . . . . . . . . . . . . . 15 ((ℑ ∘ 𝑓) ↾ ) = (ℑ ∘ (𝑓))
224164simplbda 653 . . . . . . . . . . . . . . 15 ((𝑓:𝑎⟶ℂ ∧ (𝑓) ∈ MblFn) → (ℑ ∘ (𝑓)) ∈ MblFn)
225223, 224syl5eqel 2703 . . . . . . . . . . . . . 14 ((𝑓:𝑎⟶ℂ ∧ (𝑓) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ ) ∈ MblFn)
226160, 225sylan2 491 . . . . . . . . . . . . 13 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → ((ℑ ∘ 𝑓) ↾ ) ∈ MblFn)
227226ad2antrl 763 . . . . . . . . . . . 12 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → ((ℑ ∘ 𝑓) ↾ ) ∈ MblFn)
228181, 222, 227, 175mbfres2 23393 . . . . . . . . . . 11 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → (ℑ ∘ 𝑓) ∈ MblFn)
229 ismbfcn 23379 . . . . . . . . . . . . 13 (𝑓:𝑎⟶ℂ → (𝑓 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ∈ MblFn ∧ (ℑ ∘ 𝑓) ∈ MblFn)))
230229adantr 481 . . . . . . . . . . . 12 ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) → (𝑓 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ∈ MblFn ∧ (ℑ ∘ 𝑓) ∈ MblFn)))
231230ad2antrl 763 . . . . . . . . . . 11 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → (𝑓 ∈ MblFn ↔ ((ℜ ∘ 𝑓) ∈ MblFn ∧ (ℑ ∘ 𝑓) ∈ MblFn)))
232176, 228, 231mpbir2and 956 . . . . . . . . . 10 ((∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) ∧ ((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎)) → 𝑓 ∈ MblFn)
233232ex 450 . . . . . . . . 9 (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → 𝑓 ∈ MblFn))
234233alrimivv 1854 . . . . . . . 8 (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → 𝑓 ∈ MblFn))
235234a1i 11 . . . . . . 7 (𝑡 ∈ Fin → (∀𝑔𝑏(((𝑔:𝑏⟶ℂ ∧ ∀𝑠𝑡 (𝑔𝑠) ∈ MblFn) ∧ 𝑡 = 𝑏) → 𝑔 ∈ MblFn) → ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠 ∈ (𝑡 ∪ {})(𝑓𝑠) ∈ MblFn) ∧ (𝑡 ∪ {}) = 𝑎) → 𝑓 ∈ MblFn)))
23636, 59, 66, 73, 85, 235findcard2 8185 . . . . . 6 (𝑆 ∈ Fin → ∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn))
237 2sp 2054 . . . . . 6 (∀𝑓𝑎(((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn) → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn))
2384, 236, 2373syl 18 . . . . 5 (𝜑 → (((𝑓:𝑎⟶ℂ ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ MblFn) ∧ 𝑆 = 𝑎) → 𝑓 ∈ MblFn))
23917, 26, 238vtocl2g 3265 . . . 4 ((𝐴 ∈ V ∧ 𝐹 ∈ V) → (𝜑 → (((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝐹 ∈ MblFn)))
24011, 239mpcom 38 . . 3 (𝜑 → (((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) ∧ 𝑆 = 𝐴) → 𝐹 ∈ MblFn))
2413, 240mpan2d 709 . 2 (𝜑 → ((𝐹:𝐴⟶ℂ ∧ ∀𝑠𝑆 (𝐹𝑠) ∈ MblFn) → 𝐹 ∈ MblFn))
2421, 2, 241mp2and 714 1 (𝜑𝐹 ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wal 1479   = wceq 1481  wcel 1988  wral 2909  Vcvv 3195  cun 3565  cin 3566  wss 3567  c0 3907  {csn 4168   cuni 4427  dom cdm 5104  cres 5106  ccom 5108  Rel wrel 5109  wf 5872  (class class class)co 6635  Fincfn 7940  cc 9919  cr 9920  cre 13818  cim 13819  cnccncf 22660  MblFncmbf 23364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-of 6882  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-er 7727  df-map 7844  df-pm 7845  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-sup 8333  df-inf 8334  df-oi 8400  df-card 8750  df-cda 8975  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-n0 11278  df-z 11363  df-uz 11673  df-q 11774  df-rp 11818  df-xadd 11932  df-ioo 12164  df-ico 12166  df-icc 12167  df-fz 12312  df-fzo 12450  df-fl 12576  df-seq 12785  df-exp 12844  df-hash 13101  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-clim 14200  df-sum 14398  df-xmet 19720  df-met 19721  df-cncf 22662  df-ovol 23214  df-vol 23215  df-mbf 23369
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator