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