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	biimpi	$⊢ b = ⋃ t \to ⋃ t = b$
98	97	adantl	$⊢ (g = {(ℜ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to ⋃ t = b$
99	98	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))$
100		eqid	$⊢ ℂ = ℂ$
101		feq123	$⊢ (g = {(ℜ \circ f) ↾}_{⋃ t} \land b = ⋃ t \land ℂ = ℂ) \to (g : b ⟶ ℂ \leftrightarrow ({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ)$
102	100 101	mp3an3	$⊢ (g = {(ℜ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to (g : b ⟶ ℂ \leftrightarrow ({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ)$
103		reseq1	$⊢ g = {(ℜ \circ f) ↾}_{⋃ t} \to {g ↾}_{s} = {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s}$
104	103	eleq1d	$⊢ g = {(ℜ \circ f) ↾}_{⋃ t} \to ({g ↾}_{s} \in MblFn \leftrightarrow {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn)$
105	104	adantr	$⊢ (g = {(ℜ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to ({g ↾}_{s} \in MblFn \leftrightarrow {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn)$
106	105	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)$
107	102 106	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))$
108	99 107	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))$
109		eleq1	$⊢ g = {(ℜ \circ f) ↾}_{⋃ t} \to (g \in MblFn \leftrightarrow {(ℜ \circ f) ↾}_{⋃ t} \in MblFn)$
110	109	adantr	$⊢ (g = {(ℜ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to (g \in MblFn \leftrightarrow {(ℜ \circ f) ↾}_{⋃ t} \in MblFn)$
111	108 110	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))$
112	111	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))$
113	94 95 112	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)$
114		ax-resscn	$⊢ ℝ \subseteq ℂ$
115		fss	$⊢ (ℜ : ℂ ⟶ ℝ \land ℝ \subseteq ℂ) \to ℜ : ℂ ⟶ ℂ$
116	85 114 115	mp2an	$⊢ ℜ : ℂ ⟶ ℂ$
117		fco	$⊢ (ℜ : ℂ ⟶ ℂ \land f : a ⟶ ℂ) \to (ℜ \circ f) : a ⟶ ℂ$
118	116 117	mpan	$⊢ f : a ⟶ ℂ \to (ℜ \circ f) : a ⟶ ℂ$
119		ssun1	$⊢ t \subseteq t \cup \{h\}$
120	119	unissi	$⊢ ⋃ t \subseteq ⋃ (t \cup \{h\})$
121		id	$⊢ ⋃ (t \cup \{h\}) = a \to ⋃ (t \cup \{h\}) = a$
122	120 121	sseqtrid	$⊢ ⋃ (t \cup \{h\}) = a \to ⋃ t \subseteq a$
123		fssres	$⊢ ((ℜ \circ f) : a ⟶ ℂ \land ⋃ t \subseteq a) \to ({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ$
124	118 122 123	syl2an	$⊢ (f : a ⟶ ℂ \land ⋃ (t \cup \{h\}) = a) \to ({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ$
125	124	adantlr	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a) \to ({(ℜ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ$
126		elssuni	$⊢ r \in t \to r \subseteq ⋃ t$
127	126	resabs1d	$⊢ r \in t \to {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{r} = {(ℜ \circ f) ↾}_{r}$
128		resco	$⊢ {(ℜ \circ f) ↾}_{r} = ℜ \circ ({f ↾}_{r})$
129	127 128	eqtrdi	$⊢ r \in t \to {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{r} = ℜ \circ ({f ↾}_{r})$
130	129	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})$
131		elun1	$⊢ r \in t \to r \in (t \cup \{h\})$
132		reseq2	$⊢ s = r \to {f ↾}_{s} = {f ↾}_{r}$
133	132	eleq1d	$⊢ s = r \to ({f ↾}_{s} \in MblFn \leftrightarrow {f ↾}_{r} \in MblFn)$
134	133	rspccva	$⊢ (\forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn \land r \in (t \cup \{h\})) \to {f ↾}_{r} \in MblFn$
135	131 134	sylan2	$⊢ (\forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn \land r \in t) \to {f ↾}_{r} \in MblFn$
136	135	adantll	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land r \in t) \to {f ↾}_{r} \in MblFn$
137		fresin	$⊢ f : a ⟶ ℂ \to ({f ↾}_{r}) : a \cap r ⟶ ℂ$
138		ismbfcn	$⊢ ({f ↾}_{r}) : a \cap r ⟶ ℂ \to ({f ↾}_{r} \in MblFn \leftrightarrow (ℜ \circ ({f ↾}_{r}) \in MblFn \land ℑ \circ ({f ↾}_{r}) \in MblFn))$
139	137 138	syl	$⊢ f : a ⟶ ℂ \to ({f ↾}_{r} \in MblFn \leftrightarrow (ℜ \circ ({f ↾}_{r}) \in MblFn \land ℑ \circ ({f ↾}_{r}) \in MblFn))$
140	139	biimpd	$⊢ f : a ⟶ ℂ \to ({f ↾}_{r} \in MblFn \to (ℜ \circ ({f ↾}_{r}) \in MblFn \land ℑ \circ ({f ↾}_{r}) \in MblFn))$
141	140	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))$
142	136 141	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)$
143	142	simpld	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land r \in t) \to ℜ \circ ({f ↾}_{r}) \in MblFn$
144	130 143	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$
145	144	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$
146		reseq2	$⊢ r = s \to {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{r} = {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s}$
147	146	eleq1d	$⊢ r = s \to ({({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{r} \in MblFn \leftrightarrow {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn)$
148	147	cbvralvw	$⊢ \forall r \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{r} \in MblFn \leftrightarrow \forall s \in t {({(ℜ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn$
149	145 148	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$
150	149	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$
151		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)$
152	125 150 151	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)$
153	113 152	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$
154		vsnid	$⊢ h \in \{h\}$
155		elun2	$⊢ h \in \{h\} \to h \in (t \cup \{h\})$
156		reseq2	$⊢ s = h \to {f ↾}_{s} = {f ↾}_{h}$
157	156	eleq1d	$⊢ s = h \to ({f ↾}_{s} \in MblFn \leftrightarrow {f ↾}_{h} \in MblFn)$
158	157	rspcv	$⊢ h \in (t \cup \{h\}) \to (\forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn \to {f ↾}_{h} \in MblFn)$
159	154 155 158	mp2b	$⊢ \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn \to {f ↾}_{h} \in MblFn$
160		resco	$⊢ {(ℜ \circ f) ↾}_{h} = ℜ \circ ({f ↾}_{h})$
161		fresin	$⊢ f : a ⟶ ℂ \to ({f ↾}_{h}) : a \cap h ⟶ ℂ$
162		ismbfcn	$⊢ ({f ↾}_{h}) : a \cap h ⟶ ℂ \to ({f ↾}_{h} \in MblFn \leftrightarrow (ℜ \circ ({f ↾}_{h}) \in MblFn \land ℑ \circ ({f ↾}_{h}) \in MblFn))$
163	161 162	syl	$⊢ f : a ⟶ ℂ \to ({f ↾}_{h} \in MblFn \leftrightarrow (ℜ \circ ({f ↾}_{h}) \in MblFn \land ℑ \circ ({f ↾}_{h}) \in MblFn))$
164	163	simprbda	$⊢ (f : a ⟶ ℂ \land {f ↾}_{h} \in MblFn) \to ℜ \circ ({f ↾}_{h}) \in MblFn$
165	160 164	eqeltrid	$⊢ (f : a ⟶ ℂ \land {f ↾}_{h} \in MblFn) \to {(ℜ \circ f) ↾}_{h} \in MblFn$
166	159 165	sylan2	$⊢ (f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \to {(ℜ \circ f) ↾}_{h} \in MblFn$
167	166	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$
168		uniun	$⊢ ⋃ (t \cup \{h\}) = ⋃ t \cup ⋃ \{h\}$
169		vex	$⊢ h \in V$
170	169	unisn	$⊢ ⋃ \{h\} = h$
171	170	uneq2i	$⊢ ⋃ t \cup ⋃ \{h\} = ⋃ t \cup h$
172	168 171	eqtri	$⊢ ⋃ (t \cup \{h\}) = ⋃ t \cup h$
173	172 121	eqtr3id	$⊢ ⋃ (t \cup \{h\}) = a \to ⋃ t \cup h = a$
174	173	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$
175	89 153 167 174	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$
176		imf	$⊢ ℑ : ℂ ⟶ ℝ$
177		fco	$⊢ (ℑ : ℂ ⟶ ℝ \land f : a ⟶ ℂ) \to (ℑ \circ f) : a ⟶ ℝ$
178	176 177	mpan	$⊢ f : a ⟶ ℂ \to (ℑ \circ f) : a ⟶ ℝ$
179	178	adantr	$⊢ (f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \to (ℑ \circ f) : a ⟶ ℝ$
180	179	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 ⟶ ℝ$
181		imcncf	$⊢ ℑ : ℂ \underset{cn}{⟶} ℝ$
182	181	elexi	$⊢ ℑ \in V$
183	182 92	coex	$⊢ ℑ \circ f \in V$
184	183	resex	$⊢ {(ℑ \circ f) ↾}_{⋃ t} \in V$
185	97	adantl	$⊢ (g = {(ℑ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to ⋃ t = b$
186	185	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))$
187		feq123	$⊢ (g = {(ℑ \circ f) ↾}_{⋃ t} \land b = ⋃ t \land ℂ = ℂ) \to (g : b ⟶ ℂ \leftrightarrow ({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ)$
188	100 187	mp3an3	$⊢ (g = {(ℑ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to (g : b ⟶ ℂ \leftrightarrow ({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ)$
189		reseq1	$⊢ g = {(ℑ \circ f) ↾}_{⋃ t} \to {g ↾}_{s} = {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s}$
190	189	eleq1d	$⊢ g = {(ℑ \circ f) ↾}_{⋃ t} \to ({g ↾}_{s} \in MblFn \leftrightarrow {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn)$
191	190	adantr	$⊢ (g = {(ℑ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to ({g ↾}_{s} \in MblFn \leftrightarrow {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn)$
192	191	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)$
193	188 192	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))$
194	186 193	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))$
195		eleq1	$⊢ g = {(ℑ \circ f) ↾}_{⋃ t} \to (g \in MblFn \leftrightarrow {(ℑ \circ f) ↾}_{⋃ t} \in MblFn)$
196	195	adantr	$⊢ (g = {(ℑ \circ f) ↾}_{⋃ t} \land b = ⋃ t) \to (g \in MblFn \leftrightarrow {(ℑ \circ f) ↾}_{⋃ t} \in MblFn)$
197	194 196	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))$
198	197	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))$
199	184 95 198	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)$
200		fss	$⊢ (ℑ : ℂ ⟶ ℝ \land ℝ \subseteq ℂ) \to ℑ : ℂ ⟶ ℂ$
201	176 114 200	mp2an	$⊢ ℑ : ℂ ⟶ ℂ$
202		fco	$⊢ (ℑ : ℂ ⟶ ℂ \land f : a ⟶ ℂ) \to (ℑ \circ f) : a ⟶ ℂ$
203	201 202	mpan	$⊢ f : a ⟶ ℂ \to (ℑ \circ f) : a ⟶ ℂ$
204		fssres	$⊢ ((ℑ \circ f) : a ⟶ ℂ \land ⋃ t \subseteq a) \to ({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ$
205	203 122 204	syl2an	$⊢ (f : a ⟶ ℂ \land ⋃ (t \cup \{h\}) = a) \to ({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ$
206	205	adantlr	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land ⋃ (t \cup \{h\}) = a) \to ({(ℑ \circ f) ↾}_{⋃ t}) : ⋃ t ⟶ ℂ$
207	126	resabs1d	$⊢ r \in t \to {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{r} = {(ℑ \circ f) ↾}_{r}$
208		resco	$⊢ {(ℑ \circ f) ↾}_{r} = ℑ \circ ({f ↾}_{r})$
209	207 208	eqtrdi	$⊢ r \in t \to {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{r} = ℑ \circ ({f ↾}_{r})$
210	209	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})$
211	142	simprd	$⊢ ((f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \land r \in t) \to ℑ \circ ({f ↾}_{r}) \in MblFn$
212	210 211	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$
213	212	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$
214		reseq2	$⊢ r = s \to {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{r} = {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s}$
215	214	eleq1d	$⊢ r = s \to ({({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{r} \in MblFn \leftrightarrow {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn)$
216	215	cbvralvw	$⊢ \forall r \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{r} \in MblFn \leftrightarrow \forall s \in t {({(ℑ \circ f) ↾}_{⋃ t}) ↾}_{s} \in MblFn$
217	213 216	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$
218	217	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$
219		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)$
220	206 218 219	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)$
221	199 220	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$
222		resco	$⊢ {(ℑ \circ f) ↾}_{h} = ℑ \circ ({f ↾}_{h})$
223	163	simplbda	$⊢ (f : a ⟶ ℂ \land {f ↾}_{h} \in MblFn) \to ℑ \circ ({f ↾}_{h}) \in MblFn$
224	222 223	eqeltrid	$⊢ (f : a ⟶ ℂ \land {f ↾}_{h} \in MblFn) \to {(ℑ \circ f) ↾}_{h} \in MblFn$
225	159 224	sylan2	$⊢ (f : a ⟶ ℂ \land \forall s \in (t \cup \{h\}) {f ↾}_{s} \in MblFn) \to {(ℑ \circ f) ↾}_{h} \in MblFn$
226	225	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$
227	180 221 226 174	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$
228		ismbfcn	$⊢ f : a ⟶ ℂ \to (f \in MblFn \leftrightarrow (ℜ \circ f \in MblFn \land ℑ \circ f \in MblFn))$
229	228	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))$
230	229	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))$
231	175 227 230	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$
232	231	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)$
233	232	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)$
234	233	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))$
235	35 58 65 72 84 234	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)$
236		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)$
237	2 235 236	3syl	$⊢ φ \to (((f : a ⟶ ℂ \land \forall s \in S {f ↾}_{s} \in MblFn) \land ⋃ S = a) \to f \in MblFn)$
238	16 25 237	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))$
239	10 238	mpcom	$⊢ φ \to (((F : A ⟶ ℂ \land \forall s \in S {F ↾}_{s} \in MblFn) \land ⋃ S = A) \to F \in MblFn)$
240	4 239	mpan2d	$⊢ φ \to ((F : A ⟶ ℂ \land \forall s \in S {F ↾}_{s} \in MblFn) \to F \in MblFn)$
241	1 3 240	mp2and	$⊢ φ \to F \in MblFn$

Metamath Proof Explorer

Theorem mbfresfi

Proof