Theorem mbfresfi

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

	Ref	Expression
Hypotheses	mbfresfi.1	|- ( ph -> F : A --> CC )
	mbfresfi.2	|- ( ph -> S e. Fin )
	mbfresfi.3	|- ( ph -> A. s e. S ( F |` s ) e. MblFn )
	mbfresfi.4	|- ( ph -> U. S = A )
Assertion	mbfresfi	|- ( ph -> F e. MblFn )

Proof

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