mbfresfi

Description: Measurability of a piecewise function across arbitrarily many subsets. (Contributed by Brendan Leahy, 31-Mar-2018)

	Ref	Expression
Hypotheses	mbfresfi.1	$⊢ φ \to F : A ⟶ ℂ$
	mbfresfi.2	$⊢ φ \to S \in Fin$
	mbfresfi.3	$⊢ φ \to \forall s \in S {F ↾}_{s} \in MblFn$
	mbfresfi.4	$⊢ φ \to ⋃ S = A$
Assertion	mbfresfi	$⊢ φ \to F \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		mbfresfi.1	$⊢ φ \to F : A ⟶ ℂ$
2		mbfresfi.2	$⊢ φ \to S \in Fin$
3		mbfresfi.3	$⊢ φ \to \forall s \in S {F ↾}_{s} \in MblFn$
4		mbfresfi.4	$⊢ φ \to ⋃ S = A$
5	2	uniexd	$⊢ φ \to ⋃ S \in V$
6	4 5	eqeltrrd	$⊢ φ \to A \in V$
7		fex	$⊢ (F : A ⟶ ℂ \land A \in V) \to F \in V$
8	7	ex	$⊢ F : A ⟶ ℂ \to (A \in V \to F \in V)$
9	1 8	syl	$⊢ φ \to (A \in V \to F \in V)$
10	6 9	jcai	$⊢ φ \to (A \in V \land F \in V)$
11		feq2	$⊢ a = A \to (f : a ⟶ ℂ \leftrightarrow f : A ⟶ ℂ)$
12	11	anbi1d	$⊢ a = A \to ((f : a ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \leftrightarrow (f : A ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn))$
13		eqeq2	$⊢ a = A \to (⋃ S = a \leftrightarrow ⋃ S = A)$
14	12 13	anbi12d	$⊢ a = A \to (((f : a ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = a) \leftrightarrow ((f : A ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = A))$
15	14	imbi1d	$⊢ a = A \to ((((f : a ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = a) \to f \in MblFn) \leftrightarrow (((f : A ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = A) \to f \in MblFn))$
16	15	imbi2d	$⊢ a = A \to ((φ \to (((f : a ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = a) \to f \in MblFn)) \leftrightarrow (φ \to (((f : A ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = A) \to f \in MblFn)))$
17		feq1	$⊢ f = F \to (f : A ⟶ ℂ \leftrightarrow F : A ⟶ ℂ)$
18		reseq1	$⊢ f = F \to {f ↾}_{s} = {F ↾}_{s}$
19	18	eleq1d	$⊢ f = F \to ({f ↾}_{s} \in MblFn \leftrightarrow {F ↾}_{s} \in MblFn)$
20	19	ralbidv	$⊢ f = F \to (\forall s \in S {f ↾}_{s} \in MblFn \leftrightarrow \forall s \in S {F ↾}_{s} \in MblFn)$
21	17 20	anbi12d	$⊢ f = F \to ((f : A ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \leftrightarrow (F : A ⟶ ℂ \land \forall s \in S {F ↾}_{s} \in MblFn))$
22	21	anbi1d	$⊢ f = F \to (((f : A ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = A) \leftrightarrow ((F : A ⟶ ℂ \land \forall s \in S {F ↾}_{s} \in MblFn) \land ⋃ S = A))$
23		eleq1	$⊢ f = F \to (f \in MblFn \leftrightarrow F \in MblFn)$
24	22 23	imbi12d	$⊢ f = F \to ((((f : A ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = A) \to f \in MblFn) \leftrightarrow (((F : A ⟶ ℂ \land \forall s \in S {F ↾}_{s} \in MblFn) \land ⋃ S = A) \to F \in MblFn))$
25	24	imbi2d	$⊢ f = F \to ((φ \to (((f : A ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = A) \to f \in MblFn)) \leftrightarrow (φ \to (((F : A ⟶ ℂ \land \forall s \in S {F ↾}_{s} \in MblFn) \land ⋃ S = A) \to F \in MblFn)))$
26		rzal	$⊢ r = \emptyset \to \forall s \in r {f ↾}_{s} \in MblFn$
27	26	biantrud	$⊢ r = \emptyset \to (f : a ⟶ ℂ \leftrightarrow (f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn))$
28	27	bicomd	$⊢ r = \emptyset \to ((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \leftrightarrow f : a ⟶ ℂ)$
29		unieq	$⊢ r = \emptyset \to ⋃ r = ⋃ \emptyset$
30		uni0	$⊢ ⋃ \emptyset = \emptyset$
31	29 30	eqtrdi	$⊢ r = \emptyset \to ⋃ r = \emptyset$
32	31	eqeq1d	$⊢ r = \emptyset \to (⋃ r = a \leftrightarrow \emptyset = a)$
33	28 32	anbi12d	$⊢ r = \emptyset \to (((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \land ⋃ r = a) \leftrightarrow (f : a ⟶ ℂ \land \emptyset = a))$
34	33	imbi1d	$⊢ r = \emptyset \to ((((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \land ⋃ r = a) \to f \in MblFn) \leftrightarrow ((f : a ⟶ ℂ \land \emptyset = a) \to f \in MblFn))$
35	34	2albidv	$⊢ r = \emptyset \to (\forall f \forall a (((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \land ⋃ r = a) \to f \in MblFn) \leftrightarrow \forall f \forall a ((f : a ⟶ ℂ \land \emptyset = a) \to f \in MblFn))$
36		raleq	$⊢ r = t \to (\forall s \in r {f ↾}_{s} \in MblFn \leftrightarrow \forall s \in t {f ↾}_{s} \in MblFn)$
37	36	anbi2d	$⊢ r = t \to ((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \leftrightarrow (f : a ⟶ ℂ \land \forall s \in t {f ↾}_{s} \in MblFn))$
38		unieq	$⊢ r = t \to ⋃ r = ⋃ t$
39	38	eqeq1d	$⊢ r = t \to (⋃ r = a \leftrightarrow ⋃ t = a)$
40	37 39	anbi12d	$⊢ r = t \to (((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \land ⋃ r = a) \leftrightarrow ((f : a ⟶ ℂ \land \forall s \in t {f ↾}_{s} \in MblFn) \land ⋃ t = a))$
41	40	imbi1d	$⊢ r = t \to ((((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \land ⋃ r = a) \to f \in MblFn) \leftrightarrow (((f : a ⟶ ℂ \land \forall s \in t {f ↾}_{s} \in MblFn) \land ⋃ t = a) \to f \in MblFn))$
42	41	2albidv	$⊢ r = t \to (\forall f \forall a (((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \land ⋃ r = a) \to f \in MblFn) \leftrightarrow \forall f \forall a (((f : a ⟶ ℂ \land \forall s \in t {f ↾}_{s} \in MblFn) \land ⋃ t = a) \to f \in MblFn))$
43		simpl	$⊢ (f = g \land a = b) \to f = g$
44		simpr	$⊢ (f = g \land a = b) \to a = b$
45	43 44	feq12d	$⊢ (f = g \land a = b) \to (f : a ⟶ ℂ \leftrightarrow g : b ⟶ ℂ)$
46		reseq1	$⊢ f = g \to {f ↾}_{s} = {g ↾}_{s}$
47	46	adantr	$⊢ (f = g \land a = b) \to {f ↾}_{s} = {g ↾}_{s}$
48	47	eleq1d	$⊢ (f = g \land a = b) \to ({f ↾}_{s} \in MblFn \leftrightarrow {g ↾}_{s} \in MblFn)$
49	48	ralbidv	$⊢ (f = g \land a = b) \to (\forall s \in t {f ↾}_{s} \in MblFn \leftrightarrow \forall s \in t {g ↾}_{s} \in MblFn)$
50	45 49	anbi12d	$⊢ (f = g \land a = b) \to ((f : a ⟶ ℂ \land \forall s \in t {f ↾}_{s} \in MblFn) \leftrightarrow (g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn))$
51		eqeq2	$⊢ a = b \to (⋃ t = a \leftrightarrow ⋃ t = b)$
52	51	adantl	$⊢ (f = g \land a = b) \to (⋃ t = a \leftrightarrow ⋃ t = b)$
53	50 52	anbi12d	$⊢ (f = g \land a = b) \to (((f : a ⟶ ℂ \land \forall s \in t {f ↾}_{s} \in MblFn) \land ⋃ t = a) \leftrightarrow ((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b))$
54		eleq1	$⊢ f = g \to (f \in MblFn \leftrightarrow g \in MblFn)$
55	54	adantr	$⊢ (f = g \land a = b) \to (f \in MblFn \leftrightarrow g \in MblFn)$
56	53 55	imbi12d	$⊢ (f = g \land a = b) \to ((((f : a ⟶ ℂ \land \forall s \in t {f ↾}_{s} \in MblFn) \land ⋃ t = a) \to f \in MblFn) \leftrightarrow (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn))$
57	56	cbval2vw	$⊢ \forall f \forall a (((f : a ⟶ ℂ \land \forall s \in t {f ↾}_{s} \in MblFn) \land ⋃ t = a) \to f \in MblFn) \leftrightarrow \forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn)$
58	42 57	bitrdi	$⊢ r = t \to (\forall f \forall a (((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \land ⋃ r = a) \to f \in MblFn) \leftrightarrow \forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn))$
59		raleq	$⊢ r = t \cup \{h\} \to (\forall s \in r {f ↾}_{s} \in MblFn \leftrightarrow \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn)$
60	59	anbi2d	$⊢ r = t \cup \{h\} \to ((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \leftrightarrow (f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn))$
61		unieq	$⊢ r = t \cup \{h\} \to ⋃ r = ⋃ (t \cup \{h\})$
62	61	eqeq1d	$⊢ r = t \cup \{h\} \to (⋃ r = a \leftrightarrow ⋃ (t \cup \{h\}) = a)$
63	60 62	anbi12d	$⊢ r = t \cup \{h\} \to (((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \land ⋃ r = a) \leftrightarrow ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a))$
64	63	imbi1d	$⊢ r = t \cup \{h\} \to ((((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \land ⋃ r = a) \to f \in MblFn) \leftrightarrow (((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a) \to f \in MblFn))$
65	64	2albidv	$⊢ r = t \cup \{h\} \to (\forall f \forall a (((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \land ⋃ r = a) \to f \in MblFn) \leftrightarrow \forall f \forall a (((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a) \to f \in MblFn))$
66		raleq	$⊢ r = S \to (\forall s \in r {f ↾}_{s} \in MblFn \leftrightarrow \forall s \in S {f ↾}_{s} \in MblFn)$
67	66	anbi2d	$⊢ r = S \to ((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \leftrightarrow (f : a ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn))$
68		unieq	$⊢ r = S \to ⋃ r = ⋃ S$
69	68	eqeq1d	$⊢ r = S \to (⋃ r = a \leftrightarrow ⋃ S = a)$
70	67 69	anbi12d	$⊢ r = S \to (((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \land ⋃ r = a) \leftrightarrow ((f : a ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = a))$
71	70	imbi1d	$⊢ r = S \to ((((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \land ⋃ r = a) \to f \in MblFn) \leftrightarrow (((f : a ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = a) \to f \in MblFn))$
72	71	2albidv	$⊢ r = S \to (\forall f \forall a (((f : a ⟶ ℂ \land \forall s \in r {f ↾}_{s} \in MblFn) \land ⋃ r = a) \to f \in MblFn) \leftrightarrow \forall f \forall a (((f : a ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = a) \to f \in MblFn))$
73		frel	$⊢ f : a ⟶ ℂ \to Rel f$
74	73	adantr	$⊢ (f : a ⟶ ℂ \land \emptyset = a) \to Rel f$
75		fdm	$⊢ f : a ⟶ ℂ \to dom f = a$
76		eqcom	$⊢ \emptyset = a \leftrightarrow a = \emptyset$
77	76	biimpi	$⊢ \emptyset = a \to a = \emptyset$
78	75 77	sylan9eq	$⊢ (f : a ⟶ ℂ \land \emptyset = a) \to dom f = \emptyset$
79		reldm0	$⊢ Rel f \to (f = \emptyset \leftrightarrow dom f = \emptyset)$
80	79	biimpar	$⊢ (Rel f \land dom f = \emptyset) \to f = \emptyset$
81		mbf0	$⊢ \emptyset \in MblFn$
82	80 81	eqeltrdi	$⊢ (Rel f \land dom f = \emptyset) \to f \in MblFn$
83	74 78 82	syl2anc	$⊢ (f : a ⟶ ℂ \land \emptyset = a) \to f \in MblFn$
84	83	gen2	$⊢ \forall f \forall a ((f : a ⟶ ℂ \land \emptyset = a) \to f \in MblFn)$
85		ref	$⊢ ℜ : ℂ ⟶ ℝ$
86		fco	$⊢ (ℜ : ℂ ⟶ ℝ \land f : a ⟶ ℂ) \to (ℜ \circ f) : a ⟶ ℝ$
87	85 86	mpan	$⊢ f : a ⟶ ℂ \to (ℜ \circ f) : a ⟶ ℝ$
88	87	adantr	$⊢ (f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \to (ℜ \circ f) : a ⟶ ℝ$
89	88	ad2antrl	$⊢ (\forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \land ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a)) \to (ℜ \circ f) : a ⟶ ℝ$
90		recncf	$⊢ ℜ : ℂ \underset{cn}{⟶} ℝ$
91	90	elexi	$⊢ ℜ \in V$
92		vex	$⊢ f \in V$
93	91 92	coex	$⊢ ℜ \circ f \in V$
94	93	resex	$⊢ {(ℜ \circ f) ↾}_{⋃ t} \in V$
95		vuniex	$⊢ ⋃ t \in V$
96		eqcom	$⊢ b = ⋃ t \leftrightarrow ⋃ t = b$
97	96	bilani	$⊢ (g = {(ℜ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to ⋃ t = b$
98	97	biantrud	$⊢ (g = {(ℜ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to ((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \leftrightarrow ((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b))$
99		eqid	$⊢ ℂ = ℂ$
100		feq123	$⊢ (g = {(ℜ \circ f) ↾}_{⋃ t} \land b = ⋃ t \land ℂ = ℂ) \to (g : b ⟶ ℂ \leftrightarrow ({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ)$
101	99 100	mp3an3	$⊢ (g = {(ℜ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to (g : b ⟶ ℂ \leftrightarrow ({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ)$
102		reseq1	$⊢ g = {(ℜ \circ f) ↾}_{⋃ t} \to {g ↾}_{s} = {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s}$
103	102	eleq1d	$⊢ g = {(ℜ \circ f) ↾}_{⋃ t} \to ({g ↾}_{s} \in MblFn \leftrightarrow {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn)$
104	103	adantr	$⊢ (g = {(ℜ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to ({g ↾}_{s} \in MblFn \leftrightarrow {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn)$
105	104	ralbidv	$⊢ (g = {(ℜ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to (\forall s \in t {g ↾}_{s} \in MblFn \leftrightarrow \forall s \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn)$
106	101 105	anbi12d	$⊢ (g = {(ℜ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to ((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \leftrightarrow (({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn))$
107	98 106	bitr3d	$⊢ (g = {(ℜ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \leftrightarrow (({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn))$
108		eleq1	$⊢ g = {(ℜ \circ f) ↾}_{⋃ t} \to (g \in MblFn \leftrightarrow {(ℜ \circ f) ↾}_{⋃ t} \in MblFn)$
109	108	adantr	$⊢ (g = {(ℜ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to (g \in MblFn \leftrightarrow {(ℜ \circ f) ↾}_{⋃ t} \in MblFn)$
110	107 109	imbi12d	$⊢ (g = {(ℜ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to ((((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \leftrightarrow ((({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn) \to {(ℜ \circ f) ↾}_{⋃ t} \in MblFn))$
111	110	spc2gv	$⊢ ({(ℜ \circ f) ↾}_{⋃ t} \in V \land ⋃ t \in V) \to (\forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \to ((({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn) \to {(ℜ \circ f) ↾}_{⋃ t} \in MblFn))$
112	94 95 111	mp2an	$⊢ \forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \to ((({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn) \to {(ℜ \circ f) ↾}_{⋃ t} \in MblFn)$
113		ax-resscn	$⊢ ℝ \subseteq ℂ$
114		fss	$⊢ (ℜ : ℂ ⟶ ℝ \land ℝ \subseteq ℂ) \to ℜ : ℂ ⟶ ℂ$
115	85 113 114	mp2an	$⊢ ℜ : ℂ ⟶ ℂ$
116		fco	$⊢ (ℜ : ℂ ⟶ ℂ \land f : a ⟶ ℂ) \to (ℜ \circ f) : a ⟶ ℂ$
117	115 116	mpan	$⊢ f : a ⟶ ℂ \to (ℜ \circ f) : a ⟶ ℂ$
118		ssun1	$⊢ t \subseteq t \cup \{h\}$
119	118	unissi	$⊢ ⋃ t \subseteq ⋃ (t \cup \{h\})$
120		id	$⊢ ⋃ (t \cup \{h\}) = a \to ⋃ (t \cup \{h\}) = a$
121	119 120	sseqtrid	$⊢ ⋃ (t \cup \{h\}) = a \to ⋃ t \subseteq a$
122		fssres	$⊢ ((ℜ \circ f) : a ⟶ ℂ \land ⋃ t \subseteq a) \to ({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ$
123	117 121 122	syl2an	$⊢ (f : a ⟶ ℂ \land ⋃ (t \cup \{h\}) = a) \to ({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ$
124	123	adantlr	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a) \to ({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ$
125		elssuni	$⊢ r \in t \to r \subseteq ⋃ t$
126	125	resabs1d	$⊢ r \in t \to {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{r} = {(ℜ \circ f) ↾}_{r}$
127		resco	$⊢ {(ℜ \circ f) ↾}_{r} = ℜ \circ ({f ↾}_{r})$
128	126 127	eqtrdi	$⊢ r \in t \to {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{r} = ℜ \circ ({f ↾}_{r})$
129	128	adantl	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land r \in t) \to {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{r} = ℜ \circ ({f ↾}_{r})$
130		elun1	$⊢ r \in t \to r \in (t \cup \{h\})$
131		reseq2	$⊢ s = r \to {f ↾}_{s} = {f ↾}_{r}$
132	131	eleq1d	$⊢ s = r \to ({f ↾}_{s} \in MblFn \leftrightarrow {f ↾}_{r} \in MblFn)$
133	132	rspccva	$⊢ (\forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn \land r \in (t \cup \{h\})) \to {f ↾}_{r} \in MblFn$
134	130 133	sylan2	$⊢ (\forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn \land r \in t) \to {f ↾}_{r} \in MblFn$
135	134	adantll	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land r \in t) \to {f ↾}_{r} \in MblFn$
136		fresin	$⊢ f : a ⟶ ℂ \to ({f ↾}_{r}) : a \cap r ⟶ ℂ$
137		ismbfcn	$⊢ ({f ↾}_{r}) : a \cap r ⟶ ℂ \to ({f ↾}_{r} \in MblFn \leftrightarrow (ℜ \circ ({f ↾}_{r}) \in MblFn \land ℑ \circ ({f ↾}_{r}) \in MblFn))$
138	136 137	syl	$⊢ f : a ⟶ ℂ \to ({f ↾}_{r} \in MblFn \leftrightarrow (ℜ \circ ({f ↾}_{r}) \in MblFn \land ℑ \circ ({f ↾}_{r}) \in MblFn))$
139	138	biimpd	$⊢ f : a ⟶ ℂ \to ({f ↾}_{r} \in MblFn \to (ℜ \circ ({f ↾}_{r}) \in MblFn \land ℑ \circ ({f ↾}_{r}) \in MblFn))$
140	139	ad2antrr	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land r \in t) \to ({f ↾}_{r} \in MblFn \to (ℜ \circ ({f ↾}_{r}) \in MblFn \land ℑ \circ ({f ↾}_{r}) \in MblFn))$
141	135 140	mpd	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land r \in t) \to (ℜ \circ ({f ↾}_{r}) \in MblFn \land ℑ \circ ({f ↾}_{r}) \in MblFn)$
142	141	simpld	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land r \in t) \to ℜ \circ ({f ↾}_{r}) \in MblFn$
143	129 142	eqeltrd	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land r \in t) \to {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{r} \in MblFn$
144	143	ralrimiva	$⊢ (f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \to \forall r \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{r} \in MblFn$
145		reseq2	$⊢ r = s \to {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{r} = {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s}$
146	145	eleq1d	$⊢ r = s \to ({({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{r} \in MblFn \leftrightarrow {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn)$
147	146	cbvralvw	$⊢ \forall r \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{r} \in MblFn \leftrightarrow \forall s \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn$
148	144 147	sylib	$⊢ (f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \to \forall s \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn$
149	148	adantr	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a) \to \forall s \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn$
150		pm2.27	$⊢ (({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn) \to (((({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn) \to {(ℜ \circ f) ↾}_{⋃ t} \in MblFn) \to {(ℜ \circ f) ↾}_{⋃ t} \in MblFn)$
151	124 149 150	syl2anc	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a) \to (((({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn) \to {(ℜ \circ f) ↾}_{⋃ t} \in MblFn) \to {(ℜ \circ f) ↾}_{⋃ t} \in MblFn)$
152	112 151	mpan9	$⊢ (\forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \land ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a)) \to {(ℜ \circ f) ↾}_{⋃ t} \in MblFn$
153		vsnid	$⊢ h \in \{h\}$
154		elun2	$⊢ h \in \{h\} \to h \in (t \cup \{h\})$
155		reseq2	$⊢ s = h \to {f ↾}_{s} = {f ↾}_{h}$
156	155	eleq1d	$⊢ s = h \to ({f ↾}_{s} \in MblFn \leftrightarrow {f ↾}_{h} \in MblFn)$
157	156	rspcv	$⊢ h \in (t \cup \{h\}) \to (\forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn \to {f ↾}_{h} \in MblFn)$
158	153 154 157	mp2b	$⊢ \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn \to {f ↾}_{h} \in MblFn$
159		resco	$⊢ {(ℜ \circ f) ↾}_{h} = ℜ \circ ({f ↾}_{h})$
160		fresin	$⊢ f : a ⟶ ℂ \to ({f ↾}_{h}) : a \cap h ⟶ ℂ$
161		ismbfcn	$⊢ ({f ↾}_{h}) : a \cap h ⟶ ℂ \to ({f ↾}_{h} \in MblFn \leftrightarrow (ℜ \circ ({f ↾}_{h}) \in MblFn \land ℑ \circ ({f ↾}_{h}) \in MblFn))$
162	160 161	syl	$⊢ f : a ⟶ ℂ \to ({f ↾}_{h} \in MblFn \leftrightarrow (ℜ \circ ({f ↾}_{h}) \in MblFn \land ℑ \circ ({f ↾}_{h}) \in MblFn))$
163	162	simprbda	$⊢ (f : a ⟶ ℂ \land {f ↾}_{h} \in MblFn) \to ℜ \circ ({f ↾}_{h}) \in MblFn$
164	159 163	eqeltrid	$⊢ (f : a ⟶ ℂ \land {f ↾}_{h} \in MblFn) \to {(ℜ \circ f) ↾}_{h} \in MblFn$
165	158 164	sylan2	$⊢ (f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \to {(ℜ \circ f) ↾}_{h} \in MblFn$
166	165	ad2antrl	$⊢ (\forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \land ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a)) \to {(ℜ \circ f) ↾}_{h} \in MblFn$
167		uniun	$⊢ ⋃ (t \cup \{h\}) = ⋃ t \cup ⋃ \{h\}$
168		unisnv	$⊢ ⋃ \{h\} = h$
169	168	uneq2i	$⊢ ⋃ t \cup ⋃ \{h\} = ⋃ t \cup h$
170	167 169	eqtri	$⊢ ⋃ (t \cup \{h\}) = ⋃ t \cup h$
171	170 120	eqtr3id	$⊢ ⋃ (t \cup \{h\}) = a \to ⋃ t \cup h = a$
172	171	ad2antll	$⊢ (\forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \land ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a)) \to ⋃ t \cup h = a$
173	89 152 166 172	mbfres2	$⊢ (\forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \land ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a)) \to ℜ \circ f \in MblFn$
174		imf	$⊢ ℑ : ℂ ⟶ ℝ$
175		fco	$⊢ (ℑ : ℂ ⟶ ℝ \land f : a ⟶ ℂ) \to (ℑ \circ f) : a ⟶ ℝ$
176	174 175	mpan	$⊢ f : a ⟶ ℂ \to (ℑ \circ f) : a ⟶ ℝ$
177	176	adantr	$⊢ (f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \to (ℑ \circ f) : a ⟶ ℝ$
178	177	ad2antrl	$⊢ (\forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \land ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a)) \to (ℑ \circ f) : a ⟶ ℝ$
179		imcncf	$⊢ ℑ : ℂ \underset{cn}{⟶} ℝ$
180	179	elexi	$⊢ ℑ \in V$
181	180 92	coex	$⊢ ℑ \circ f \in V$
182	181	resex	$⊢ {(ℑ \circ f) ↾}_{⋃ t} \in V$
183	96	bilani	$⊢ (g = {(ℑ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to ⋃ t = b$
184	183	biantrud	$⊢ (g = {(ℑ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to ((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \leftrightarrow ((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b))$
185		feq123	$⊢ (g = {(ℑ \circ f) ↾}_{⋃ t} \land b = ⋃ t \land ℂ = ℂ) \to (g : b ⟶ ℂ \leftrightarrow ({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ)$
186	99 185	mp3an3	$⊢ (g = {(ℑ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to (g : b ⟶ ℂ \leftrightarrow ({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ)$
187		reseq1	$⊢ g = {(ℑ \circ f) ↾}_{⋃ t} \to {g ↾}_{s} = {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s}$
188	187	eleq1d	$⊢ g = {(ℑ \circ f) ↾}_{⋃ t} \to ({g ↾}_{s} \in MblFn \leftrightarrow {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn)$
189	188	adantr	$⊢ (g = {(ℑ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to ({g ↾}_{s} \in MblFn \leftrightarrow {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn)$
190	189	ralbidv	$⊢ (g = {(ℑ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to (\forall s \in t {g ↾}_{s} \in MblFn \leftrightarrow \forall s \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn)$
191	186 190	anbi12d	$⊢ (g = {(ℑ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to ((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \leftrightarrow (({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn))$
192	184 191	bitr3d	$⊢ (g = {(ℑ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \leftrightarrow (({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn))$
193		eleq1	$⊢ g = {(ℑ \circ f) ↾}_{⋃ t} \to (g \in MblFn \leftrightarrow {(ℑ \circ f) ↾}_{⋃ t} \in MblFn)$
194	193	adantr	$⊢ (g = {(ℑ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to (g \in MblFn \leftrightarrow {(ℑ \circ f) ↾}_{⋃ t} \in MblFn)$
195	192 194	imbi12d	$⊢ (g = {(ℑ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to ((((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \leftrightarrow ((({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn) \to {(ℑ \circ f) ↾}_{⋃ t} \in MblFn))$
196	195	spc2gv	$⊢ ({(ℑ \circ f) ↾}_{⋃ t} \in V \land ⋃ t \in V) \to (\forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \to ((({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn) \to {(ℑ \circ f) ↾}_{⋃ t} \in MblFn))$
197	182 95 196	mp2an	$⊢ \forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \to ((({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn) \to {(ℑ \circ f) ↾}_{⋃ t} \in MblFn)$
198		fss	$⊢ (ℑ : ℂ ⟶ ℝ \land ℝ \subseteq ℂ) \to ℑ : ℂ ⟶ ℂ$
199	174 113 198	mp2an	$⊢ ℑ : ℂ ⟶ ℂ$
200		fco	$⊢ (ℑ : ℂ ⟶ ℂ \land f : a ⟶ ℂ) \to (ℑ \circ f) : a ⟶ ℂ$
201	199 200	mpan	$⊢ f : a ⟶ ℂ \to (ℑ \circ f) : a ⟶ ℂ$
202		fssres	$⊢ ((ℑ \circ f) : a ⟶ ℂ \land ⋃ t \subseteq a) \to ({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ$
203	201 121 202	syl2an	$⊢ (f : a ⟶ ℂ \land ⋃ (t \cup \{h\}) = a) \to ({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ$
204	203	adantlr	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a) \to ({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ$
205	125	resabs1d	$⊢ r \in t \to {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{r} = {(ℑ \circ f) ↾}_{r}$
206		resco	$⊢ {(ℑ \circ f) ↾}_{r} = ℑ \circ ({f ↾}_{r})$
207	205 206	eqtrdi	$⊢ r \in t \to {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{r} = ℑ \circ ({f ↾}_{r})$
208	207	adantl	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land r \in t) \to {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{r} = ℑ \circ ({f ↾}_{r})$
209	141	simprd	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land r \in t) \to ℑ \circ ({f ↾}_{r}) \in MblFn$
210	208 209	eqeltrd	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land r \in t) \to {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{r} \in MblFn$
211	210	ralrimiva	$⊢ (f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \to \forall r \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{r} \in MblFn$
212		reseq2	$⊢ r = s \to {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{r} = {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s}$
213	212	eleq1d	$⊢ r = s \to ({({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{r} \in MblFn \leftrightarrow {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn)$
214	213	cbvralvw	$⊢ \forall r \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{r} \in MblFn \leftrightarrow \forall s \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn$
215	211 214	sylib	$⊢ (f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \to \forall s \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn$
216	215	adantr	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a) \to \forall s \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn$
217		pm2.27	$⊢ (({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn) \to (((({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn) \to {(ℑ \circ f) ↾}_{⋃ t} \in MblFn) \to {(ℑ \circ f) ↾}_{⋃ t} \in MblFn)$
218	204 216 217	syl2anc	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a) \to (((({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ \land \forall s \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn) \to {(ℑ \circ f) ↾}_{⋃ t} \in MblFn) \to {(ℑ \circ f) ↾}_{⋃ t} \in MblFn)$
219	197 218	mpan9	$⊢ (\forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \land ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a)) \to {(ℑ \circ f) ↾}_{⋃ t} \in MblFn$
220		resco	$⊢ {(ℑ \circ f) ↾}_{h} = ℑ \circ ({f ↾}_{h})$
221	162	simplbda	$⊢ (f : a ⟶ ℂ \land {f ↾}_{h} \in MblFn) \to ℑ \circ ({f ↾}_{h}) \in MblFn$
222	220 221	eqeltrid	$⊢ (f : a ⟶ ℂ \land {f ↾}_{h} \in MblFn) \to {(ℑ \circ f) ↾}_{h} \in MblFn$
223	158 222	sylan2	$⊢ (f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \to {(ℑ \circ f) ↾}_{h} \in MblFn$
224	223	ad2antrl	$⊢ (\forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \land ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a)) \to {(ℑ \circ f) ↾}_{h} \in MblFn$
225	178 219 224 172	mbfres2	$⊢ (\forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \land ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a)) \to ℑ \circ f \in MblFn$
226		ismbfcn	$⊢ f : a ⟶ ℂ \to (f \in MblFn \leftrightarrow (ℜ \circ f \in MblFn \land ℑ \circ f \in MblFn))$
227	226	adantr	$⊢ (f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \to (f \in MblFn \leftrightarrow (ℜ \circ f \in MblFn \land ℑ \circ f \in MblFn))$
228	227	ad2antrl	$⊢ (\forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \land ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a)) \to (f \in MblFn \leftrightarrow (ℜ \circ f \in MblFn \land ℑ \circ f \in MblFn))$
229	173 225 228	mpbir2and	$⊢ (\forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \land ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a)) \to f \in MblFn$
230	229	ex	$⊢ \forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \to (((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a) \to f \in MblFn)$
231	230	alrimivv	$⊢ \forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \to \forall f \forall a (((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a) \to f \in MblFn)$
232	231	a1i	$⊢ t \in Fin \to (\forall g \forall b (((g : b ⟶ ℂ \land \forall s \in t {g ↾}_{s} \in MblFn) \land ⋃ t = b) \to g \in MblFn) \to \forall f \forall a (((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a) \to f \in MblFn))$
233	35 58 65 72 84 232	findcard2	$⊢ S \in Fin \to \forall f \forall a (((f : a ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = a) \to f \in MblFn)$
234		2sp	$⊢ \forall f \forall a (((f : a ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = a) \to f \in MblFn) \to (((f : a ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = a) \to f \in MblFn)$
235	2 233 234	3syl	$⊢ φ \to (((f : a ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = a) \to f \in MblFn)$
236	16 25 235	vtocl2g	$⊢ (A \in V \land F \in V) \to (φ \to (((F : A ⟶ ℂ \land \forall s \in S {F ↾}_{s} \in MblFn) \land ⋃ S = A) \to F \in MblFn))$
237	10 236	mpcom	$⊢ φ \to (((F : A ⟶ ℂ \land \forall s \in S {F ↾}_{s} \in MblFn) \land ⋃ S = A) \to F \in MblFn)$
238	4 237	mpan2d	$⊢ φ \to ((F : A ⟶ ℂ \land \forall s \in S {F ↾}_{s} \in MblFn) \to F \in MblFn)$
239	1 3 238	mp2and	$⊢ φ \to F \in MblFn$

Metamath Proof Explorer

Theorem mbfresfi

Proof