Theorem icccncfext 31549

Description: A continuous function on a closed interval can be extended to a continuous function on the whole real line. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
icccncfext.1	|- F/_ x F
icccncfext.2	|- J = ( topGen ` ran (,) )
icccncfext.3	|- Y = U. K
icccncfext.4	|- G = ( x e. RR |-> if ( x e. ( A [,] B ) , ( F ` x ) , if ( x < A , ( F ` A ) , ( F ` B ) ) ) )
icccncfext.5	|- ( ph -> A e. RR )
icccncfext.6	|- ( ph -> B e. RR )
icccncfext.7	|- ( ph -> A <_ B )
icccncfext.8	|- ( ph -> K e. Top )
icccncfext.9	|- ( ph -> F e. ( ( J ↾t ( A [,] B ) ) Cn K ) )

Assertion

Ref	Expression
icccncfext	|- ( ph -> ( G e. ( J Cn ( K ↾t ran F ) ) /\ ( G |` ( A [,] B ) ) = F ) )

Distinct variable groups:   x, A   x, B   ph, x

Allowed substitution hints:   F( x)   G( x)   J( x)   K( x)   Y( x)

Proof of Theorem icccncfext

Dummy variables t w y z v u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		icccncfext.2	. . . . . . . . . . . . . . . . . 18 |- J = ( topGen ` ran (,) )
2		retopon 21138	. . . . . . . . . . . . . . . . . 18 |- ( topGen ` ran (,) ) e. (TopOn ` RR )
3	1, 2	eqeltri 2551	. . . . . . . . . . . . . . . . 17 |- J e. (TopOn ` RR )
4	3	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> J e. (TopOn ` RR ) )
5		icccncfext.5	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A e. RR )
6		icccncfext.6	. . . . . . . . . . . . . . . . . 18 |- ( ph -> B e. RR )
7	5, 6	jca 532	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( A e. RR /\ B e. RR ) )
8		iccssre 11618	. . . . . . . . . . . . . . . . 17 |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
9	7, 8	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( A [,] B ) C_ RR )
10	4, 9	jca 532	. . . . . . . . . . . . . . 15 |- ( ph -> ( J e. (TopOn ` RR ) /\ ( A [,] B ) C_ RR ) )
11		resttopon 19530	. . . . . . . . . . . . . . 15 |- ( ( J e. (TopOn ` RR ) /\ ( A [,] B ) C_ RR ) -> ( J ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) )
12	10, 11	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ( J ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) )
13		icccncfext.8	. . . . . . . . . . . . . . . 16 |- ( ph -> K e. Top )
14		icccncfext.3	. . . . . . . . . . . . . . . 16 |- Y = U. K
15	13, 14	jctir 538	. . . . . . . . . . . . . . 15 |- ( ph -> ( K e. Top /\ Y = U. K ) )
16		istopon 19295	. . . . . . . . . . . . . . 15 |- ( K e. (TopOn ` Y ) <-> ( K e. Top /\ Y = U. K ) )
17	15, 16	sylibr 212	. . . . . . . . . . . . . 14 |- ( ph -> K e. (TopOn ` Y ) )
18		icccncfext.9	. . . . . . . . . . . . . 14 |- ( ph -> F e. ( ( J ↾t ( A [,] B ) ) Cn K ) )
19	12, 17, 18	3jca 1176	. . . . . . . . . . . . 13 |- ( ph -> ( ( J ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) /\ K e. (TopOn ` Y ) /\ F e. ( ( J ↾t ( A [,] B ) ) Cn K ) ) )
20		cnf2 19618	. . . . . . . . . . . . 13 |- ( ( ( J ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) /\ K e. (TopOn ` Y ) /\ F e. ( ( J ↾t ( A [,] B ) ) Cn K ) ) -> F : ( A [,] B ) --> Y )
21	19, 20	syl 16	. . . . . . . . . . . 12 |- ( ph -> F : ( A [,] B ) --> Y )
22		ffn 5737	. . . . . . . . . . . 12 |- ( F : ( A [,] B ) --> Y -> F Fn ( A [,] B ) )
23	21, 22	syl 16	. . . . . . . . . . 11 |- ( ph -> F Fn ( A [,] B ) )
24		dffn3 5744	. . . . . . . . . . 11 |- ( F Fn ( A [,] B ) <-> F : ( A [,] B ) --> ran F )
25	23, 24	sylib 196	. . . . . . . . . 10 |- ( ph -> F : ( A [,] B ) --> ran F )
26	25	ffvelrnda 6032	. . . . . . . . 9 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` y ) e. ran F )
27		fnfun 5684	. . . . . . . . . . . . . . 15 |- ( F Fn ( A [,] B ) -> Fun F )
28	23, 27	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> Fun F )
29	5	rexrd 9655	. . . . . . . . . . . . . . . . 17 |- ( ph -> A e. RR* )
30	6	rexrd 9655	. . . . . . . . . . . . . . . . 17 |- ( ph -> B e. RR* )
31		icccncfext.7	. . . . . . . . . . . . . . . . 17 |- ( ph -> A <_ B )
32	29, 30, 31	3jca 1176	. . . . . . . . . . . . . . . 16 |- ( ph -> ( A e. RR* /\ B e. RR* /\ A <_ B ) )
33		lbicc2 11648	. . . . . . . . . . . . . . . 16 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
34	32, 33	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> A e. ( A [,] B ) )
35		fndm 5686	. . . . . . . . . . . . . . . . 17 |- ( F Fn ( A [,] B ) -> dom F = ( A [,] B ) )
36	23, 35	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> dom F = ( A [,] B ) )
37	36	eqcomd 2475	. . . . . . . . . . . . . . 15 |- ( ph -> ( A [,] B ) = dom F )
38	34, 37	eleqtrd 2557	. . . . . . . . . . . . . 14 |- ( ph -> A e. dom F )
39	28, 38	jca 532	. . . . . . . . . . . . 13 |- ( ph -> ( Fun F /\ A e. dom F ) )
40		fvelrn 6025	. . . . . . . . . . . . 13 |- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. ran F )
41	39, 40	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( F ` A ) e. ran F )
42		ubicc2 11649	. . . . . . . . . . . . . . . 16 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
43	32, 42	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> B e. ( A [,] B ) )
44	43, 37	eleqtrd 2557	. . . . . . . . . . . . . 14 |- ( ph -> B e. dom F )
45	28, 44	jca 532	. . . . . . . . . . . . 13 |- ( ph -> ( Fun F /\ B e. dom F ) )
46		fvelrn 6025	. . . . . . . . . . . . 13 |- ( ( Fun F /\ B e. dom F ) -> ( F ` B ) e. ran F )
47	45, 46	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( F ` B ) e. ran F )
48	41, 47	jca 532	. . . . . . . . . . 11 |- ( ph -> ( ( F ` A ) e. ran F /\ ( F ` B ) e. ran F ) )
49		ifcl 3987	. . . . . . . . . . 11 |- ( ( ( F ` A ) e. ran F /\ ( F ` B ) e. ran F ) -> if ( y < A , ( F ` A ) , ( F ` B ) ) e. ran F )
50	48, 49	syl 16	. . . . . . . . . 10 |- ( ph -> if ( y < A , ( F ` A ) , ( F ` B ) ) e. ran F )
51	50	adantr 465	. . . . . . . . 9 |- ( ( ph /\ -. y e. ( A [,] B ) ) -> if ( y < A , ( F ` A ) , ( F ` B ) ) e. ran F )
52	26, 51	ifclda 3977	. . . . . . . 8 |- ( ph -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) e. ran F )
53	52	adantr 465	. . . . . . 7 |- ( ( ph /\ y e. RR ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) e. ran F )
54	53	ralrimiva 2881	. . . . . 6 |- ( ph -> A. y e. RR if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) e. ran F )
55		icccncfext.4	. . . . . . . 8 |- G = ( x e. RR |-> if ( x e. ( A [,] B ) , ( F ` x ) , if ( x < A , ( F ` A ) , ( F ` B ) ) ) )
56		nfcv 2629	. . . . . . . . . . 11 |- F/_ y x
57		nfcv 2629	. . . . . . . . . . 11 |- F/_ y ( A [,] B )
58	56, 57	nfel 2642	. . . . . . . . . 10 |- F/ y x e. ( A [,] B )
59		nfcv 2629	. . . . . . . . . 10 |- F/_ y ( F ` x )
60		nfcv 2629	. . . . . . . . . 10 |- F/_ y if ( x < A , ( F ` A ) , ( F ` B ) )
61	58, 59, 60	nfif 3974	. . . . . . . . 9 |- F/_ y if ( x e. ( A [,] B ) , ( F ` x ) , if ( x < A , ( F ` A ) , ( F ` B ) ) )
62		nfcv 2629	. . . . . . . . . . 11 |- F/_ x y
63		nfcv 2629	. . . . . . . . . . 11 |- F/_ x ( A [,] B )
64	62, 63	nfel 2642	. . . . . . . . . 10 |- F/ x y e. ( A [,] B )
65		icccncfext.1	. . . . . . . . . . 11 |- F/_ x F
66	65, 62	nffv 5879	. . . . . . . . . 10 |- F/_ x ( F ` y )
67		nfv 1683	. . . . . . . . . . 11 |- F/ x y < A
68		nfcv 2629	. . . . . . . . . . . 12 |- F/_ x A
69	65, 68	nffv 5879	. . . . . . . . . . 11 |- F/_ x ( F ` A )
70		nfcv 2629	. . . . . . . . . . . 12 |- F/_ x B
71	65, 70	nffv 5879	. . . . . . . . . . 11 |- F/_ x ( F ` B )
72	67, 69, 71	nfif 3974	. . . . . . . . . 10 |- F/_ x if ( y < A , ( F ` A ) , ( F ` B ) )
73	64, 66, 72	nfif 3974	. . . . . . . . 9 |- F/_ x if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) )
74		eleq1 2539	. . . . . . . . . 10 |- ( x = y -> ( x e. ( A [,] B ) <-> y e. ( A [,] B ) ) )
75		fveq2 5872	. . . . . . . . . 10 |- ( x = y -> ( F ` x ) = ( F ` y ) )
76		breq1 4456	. . . . . . . . . . 11 |- ( x = y -> ( x < A <-> y < A ) )
77	76	ifbid 3967	. . . . . . . . . 10 |- ( x = y -> if ( x < A , ( F ` A ) , ( F ` B ) ) = if ( y < A , ( F ` A ) , ( F ` B ) ) )
78	74, 75, 77	ifbieq12d 3972	. . . . . . . . 9 |- ( x = y -> if ( x e. ( A [,] B ) , ( F ` x ) , if ( x < A , ( F ` A ) , ( F ` B ) ) ) = if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) )
79	61, 73, 78	cbvmpt 4543	. . . . . . . 8 |- ( x e. RR |-> if ( x e. ( A [,] B ) , ( F ` x ) , if ( x < A , ( F ` A ) , ( F ` B ) ) ) ) = ( y e. RR |-> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) )
80	55, 79	eqtri 2496	. . . . . . 7 |- G = ( y e. RR |-> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) )
81	80	fmpt 6053	. . . . . 6 |- ( A. y e. RR if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) e. ran F <-> G : RR --> ran F )
82	54, 81	sylib 196	. . . . 5 |- ( ph -> G : RR --> ran F )
83	82	adantr 465	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> G : RR --> ran F )
84		simplll 757	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) -> ph )
85		simplr 754	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) -> u e. ( K ↾t ran F ) )
86	84, 85	jca 532	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) -> ( ph /\ u e. ( K ↾t ran F ) ) )
87		ssid 3528	. . . . . . . . . . . . . . . . . . 19 |- ran F C_ ran F
88	87	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ran F C_ ran F )
89		frn 5743	. . . . . . . . . . . . . . . . . . 19 |- ( F : ( A [,] B ) --> Y -> ran F C_ Y )
90	21, 89	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ran F C_ Y )
91	17, 88, 90	3jca 1176	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( K e. (TopOn ` Y ) /\ ran F C_ ran F /\ ran F C_ Y ) )
92		cnrest2 19655	. . . . . . . . . . . . . . . . 17 |- ( ( K e. (TopOn ` Y ) /\ ran F C_ ran F /\ ran F C_ Y ) -> ( F e. ( ( J ↾t ( A [,] B ) ) Cn K ) <-> F e. ( ( J ↾t ( A [,] B ) ) Cn ( K ↾t ran F ) ) ) )
93	91, 92	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( F e. ( ( J ↾t ( A [,] B ) ) Cn K ) <-> F e. ( ( J ↾t ( A [,] B ) ) Cn ( K ↾t ran F ) ) ) )
94	18, 93	mpbid 210	. . . . . . . . . . . . . . 15 |- ( ph -> F e. ( ( J ↾t ( A [,] B ) ) Cn ( K ↾t ran F ) ) )
95	94	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( K ↾t ran F ) ) -> F e. ( ( J ↾t ( A [,] B ) ) Cn ( K ↾t ran F ) ) )
96		simpr 461	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( K ↾t ran F ) ) -> u e. ( K ↾t ran F ) )
97	95, 96	jca 532	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( K ↾t ran F ) ) -> ( F e. ( ( J ↾t ( A [,] B ) ) Cn ( K ↾t ran F ) ) /\ u e. ( K ↾t ran F ) ) )
98		cnima 19634	. . . . . . . . . . . . 13 |- ( ( F e. ( ( J ↾t ( A [,] B ) ) Cn ( K ↾t ran F ) ) /\ u e. ( K ↾t ran F ) ) -> ( `' F " u ) e. ( J ↾t ( A [,] B ) ) )
99	86, 97, 98	3syl 20	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) -> ( `' F " u ) e. ( J ↾t ( A [,] B ) ) )
100	2	topontopi 19301	. . . . . . . . . . . . . . . . 17 |- ( topGen ` ran (,) ) e. Top
101	1, 100	eqeltri 2551	. . . . . . . . . . . . . . . 16 |- J e. Top
102	101	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> J e. Top )
103		reex 9595	. . . . . . . . . . . . . . . . 17 |- RR e. _V
104	103	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> RR e. _V )
105	104, 9	ssexd 4600	. . . . . . . . . . . . . . 15 |- ( ph -> ( A [,] B ) e. _V )
106	102, 105	jca 532	. . . . . . . . . . . . . 14 |- ( ph -> ( J e. Top /\ ( A [,] B ) e. _V ) )
107	84, 106	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) -> ( J e. Top /\ ( A [,] B ) e. _V ) )
108		elrest 14700	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ ( A [,] B ) e. _V ) -> ( ( `' F " u ) e. ( J ↾t ( A [,] B ) ) <-> E. w e. J ( `' F " u ) = ( w i^i ( A [,] B ) ) ) )
109	107, 108	syl 16	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) -> ( ( `' F " u ) e. ( J ↾t ( A [,] B ) ) <-> E. w e. J ( `' F " u ) = ( w i^i ( A [,] B ) ) ) )
110	99, 109	mpbid 210	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) -> E. w e. J ( `' F " u ) = ( w i^i ( A [,] B ) ) )
111	84	3ad2ant1 1017	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ph )
112		simpr 461	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. RR ) -> y e. RR )
113	112	ad2antrr 725	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) -> y e. RR )
114	113	3ad2ant1 1017	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> y e. RR )
115		simp1r 1021	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( G ` y ) e. u )
116	111, 114, 115	jca31 534	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) )
117		simp2 997	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> w e. J )
118		simp3 998	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( `' F " u ) = ( w i^i ( A [,] B ) ) )
119	116, 117, 118	3jca 1176	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) )
120		simpll2 1036	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> w e. J )
121	101	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( w e. J -> J e. Top )
122		id 22	. . . . . . . . . . . . . . . . . . . . 21 |- ( w e. J -> w e. J )
123		iooretop 21141	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( -oo (,) A ) e. ( topGen ` ran (,) )
124	123, 1	eleqtrri 2554	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -oo (,) A ) e. J
125		iooretop 21141	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( B (,) +oo ) e. ( topGen ` ran (,) )
126	125, 1	eleqtrri 2554	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( B (,) +oo ) e. J
127		unopn 19281	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( J e. Top /\ ( -oo (,) A ) e. J /\ ( B (,) +oo ) e. J ) -> ( ( -oo (,) A ) u. ( B (,) +oo ) ) e. J )
128	101, 124, 126, 127	mp3an 1324	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( -oo (,) A ) u. ( B (,) +oo ) ) e. J
129	128	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( w e. J -> ( ( -oo (,) A ) u. ( B (,) +oo ) ) e. J )
130	121, 122, 129	3jca 1176	. . . . . . . . . . . . . . . . . . . 20 |- ( w e. J -> ( J e. Top /\ w e. J /\ ( ( -oo (,) A ) u. ( B (,) +oo ) ) e. J ) )
131		unopn 19281	. . . . . . . . . . . . . . . . . . . 20 |- ( ( J e. Top /\ w e. J /\ ( ( -oo (,) A ) u. ( B (,) +oo ) ) e. J ) -> ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) e. J )
132	130, 131	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( w e. J -> ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) e. J )
133	120, 132	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) e. J )
134		simpl1l 1047	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) -> ( ph /\ y e. RR ) )
135	134	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( ph /\ y e. RR ) )
136		simpl1r 1048	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) -> ( G ` y ) e. u )
137	136	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( G ` y ) e. u )
138		simpll3 1037	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( `' F " u ) = ( w i^i ( A [,] B ) ) )
139	135, 137, 138	jca31 534	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) )
140		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ y e. RR ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ph )
141		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ y e. RR ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) )
142		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ y e. RR ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. RR )
143	140, 141, 142	jca31 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ y e. RR ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) /\ y e. RR ) )
144		difreicc 11664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( A e. RR /\ B e. RR ) -> ( RR \ ( A [,] B ) ) = ( ( -oo (,) A ) u. ( B (,) +oo ) ) )
145	7, 144	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ph -> ( RR \ ( A [,] B ) ) = ( ( -oo (,) A ) u. ( B (,) +oo ) ) )
146		eqcom 2476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( RR \ ( A [,] B ) ) = ( ( -oo (,) A ) u. ( B (,) +oo ) ) <-> ( ( -oo (,) A ) u. ( B (,) +oo ) ) = ( RR \ ( A [,] B ) ) )
147	146	imbi2i 312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ph -> ( RR \ ( A [,] B ) ) = ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) <-> ( ph -> ( ( -oo (,) A ) u. ( B (,) +oo ) ) = ( RR \ ( A [,] B ) ) ) )
148	145, 147	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ph -> ( ( -oo (,) A ) u. ( B (,) +oo ) ) = ( RR \ ( A [,] B ) ) )
149	148	eleq2d 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ph -> ( y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) <-> y e. ( RR \ ( A [,] B ) ) ) )
150	149	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ph -> ( -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) <-> -. y e. ( RR \ ( A [,] B ) ) ) )
151	150	biimpd 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ph -> ( -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) -> -. y e. ( RR \ ( A [,] B ) ) ) )
152	151	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> -. y e. ( RR \ ( A [,] B ) ) )
153		eldif 3491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( y e. ( RR \ ( A [,] B ) ) <-> ( y e. RR /\ -. y e. ( A [,] B ) ) )
154	152, 153	sylnib 304	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> -. ( y e. RR /\ -. y e. ( A [,] B ) ) )
155		imnan 422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( y e. RR -> -. -. y e. ( A [,] B ) ) <-> -. ( y e. RR /\ -. y e. ( A [,] B ) ) )
156	154, 155	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( y e. RR -> -. -. y e. ( A [,] B ) ) )
157	156	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) /\ y e. RR ) -> -. -. y e. ( A [,] B ) )
158	157	notnotrd 113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) /\ y e. RR ) -> y e. ( A [,] B ) )
159	143, 158	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ y e. RR ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. ( A [,] B ) )
160	159	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. ( A [,] B ) )
161		simplll 757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ph )
162	161, 160	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( ph /\ y e. ( A [,] B ) ) )
163	9	sselda 3509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ y e. ( A [,] B ) ) -> y e. RR )
164	21	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ph /\ y e. ( A [,] B ) ) -> F : ( A [,] B ) --> Y )
165	164	ffvelrnda 6032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ph /\ y e. ( A [,] B ) ) /\ y e. ( A [,] B ) ) -> ( F ` y ) e. Y )
166	21, 34	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ph -> ( F : ( A [,] B ) --> Y /\ A e. ( A [,] B ) ) )
167		ffvelrn 6030	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( F : ( A [,] B ) --> Y /\ A e. ( A [,] B ) ) -> ( F ` A ) e. Y )
168	166, 167	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ph -> ( F ` A ) e. Y )
169	168	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( ph /\ y e. ( A [,] B ) ) /\ -. y e. ( A [,] B ) ) /\ y < A ) -> ( F ` A ) e. Y )
170	90, 47	sseldd 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ph -> ( F ` B ) e. Y )
171	170	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( ph /\ y e. ( A [,] B ) ) /\ -. y e. ( A [,] B ) ) /\ -. y < A ) -> ( F ` B ) e. Y )
172	169, 171	ifclda 3977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ph /\ y e. ( A [,] B ) ) /\ -. y e. ( A [,] B ) ) -> if ( y < A , ( F ` A ) , ( F ` B ) ) e. Y )
173	165, 172	ifclda 3977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ y e. ( A [,] B ) ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) e. Y )
174	163, 173	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( y e. RR /\ if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) e. Y ) )
175	80	fvmpt2 5964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( y e. RR /\ if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) e. Y ) -> ( G ` y ) = if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) )
176	174, 175	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( G ` y ) = if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) )
177		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ y e. ( A [,] B ) ) -> y e. ( A [,] B ) )
178		iftrue 3951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( y e. ( A [,] B ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) = ( F ` y ) )
179	177, 178	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ y e. ( A [,] B ) ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) = ( F ` y ) )
180	176, 179	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( G ` y ) = ( F ` y ) )
181	180	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` y ) = ( G ` y ) )
182	162, 181	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( F ` y ) = ( G ` y ) )
183		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( G ` y ) e. u )
184	182, 183	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( F ` y ) e. u )
185	160, 184	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( y e. ( A [,] B ) /\ ( F ` y ) e. u ) )
186	161, 23	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> F Fn ( A [,] B ) )
187		elpreima 6008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( F Fn ( A [,] B ) -> ( y e. ( `' F " u ) <-> ( y e. ( A [,] B ) /\ ( F ` y ) e. u ) ) )
188	186, 187	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( y e. ( `' F " u ) <-> ( y e. ( A [,] B ) /\ ( F ` y ) e. u ) ) )
189	185, 188	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. ( `' F " u ) )
190	189	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. ( `' F " u ) )
191		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( `' F " u ) = ( w i^i ( A [,] B ) ) )
192	190, 191	eleqtrd 2557	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. ( w i^i ( A [,] B ) ) )
193		elin 3692	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. ( w i^i ( A [,] B ) ) <-> ( y e. w /\ y e. ( A [,] B ) ) )
194	192, 193	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( y e. w /\ y e. ( A [,] B ) ) )
195	194	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. w )
196	195	ex 434	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) -> y e. w ) )
197	196	orrd 378	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) \/ y e. w ) )
198	197	orcomd 388	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( y e. w \/ y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) )
199		elun 3650	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) <-> ( y e. w \/ y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) )
200	198, 199	sylibr 212	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> y e. ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) )
201	139, 200	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> y e. ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) )
202		imaundi 5424	. . . . . . . . . . . . . . . . . . . . 21 |- ( G " ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) = ( ( G " w ) u. ( G " ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) )
203	202	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( G " ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) = ( ( G " w ) u. ( G " ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) )
204	135	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ph )
205	3	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( w e. J -> J e. (TopOn ` RR ) )
206	205, 122	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( w e. J -> ( J e. (TopOn ` RR ) /\ w e. J ) )
207		toponss 19299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( J e. (TopOn ` RR ) /\ w e. J ) -> w C_ RR )
208	206, 207	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( w e. J -> w C_ RR )
209	120, 208	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> w C_ RR )
210	204, 209	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( ph /\ w C_ RR ) )
211	210, 138	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) )
212		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( F ` A ) e. u )
213	211, 212	jca 532	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) )
214		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( F ` B ) e. u )
215	213, 214	jca 532	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) )
216		nfv 1683	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/ y ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u )
217	55	funmpt2 5631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- Fun G
218	217	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> Fun G )
219	218	ad5antr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) -> Fun G )
220		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) -> y e. ( G " w ) )
221	219, 220	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) -> ( Fun G /\ y e. ( G " w ) ) )
222		fvelima 5926	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( Fun G /\ y e. ( G " w ) ) -> E. z e. w ( G ` z ) = y )
223	221, 222	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) -> E. z e. w ( G ` z ) = y )
224		eqcom 2476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( G ` z ) = y <-> y = ( G ` z ) )
225	224	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( G ` z ) = y -> y = ( G ` z ) )
226	225	3ad2ant3 1019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) /\ z e. w /\ ( G ` z ) = y ) -> y = ( G ` z ) )
227		simp1ll 1059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) /\ z e. w /\ ( G ` z ) = y ) -> ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) )
228		simp1lr 1060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) /\ z e. w /\ ( G ` z ) = y ) -> ( F ` B ) e. u )
229		simp2 997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) /\ z e. w /\ ( G ` z ) = y ) -> z e. w )
230	227, 228, 229	jca31 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) /\ z e. w /\ ( G ` z ) = y ) -> ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) )
231		simp-5l 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( ph /\ w C_ RR ) )
232		simp-5r 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( `' F " u ) = ( w i^i ( A [,] B ) ) )
233		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. w )
234	231, 232, 233	jca31 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) )
235		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. ( A [,] B ) )
236	234, 235	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) )
237		simp-4l 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ph )
238		simpllr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( `' F " u ) = ( w i^i ( A [,] B ) ) )
239		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. w )
240	237, 238, 239	jca31 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) )
241		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. ( A [,] B ) )
242	240, 241	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) )
243		simplll 757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ph )
244		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. ( A [,] B ) )
245	243, 244	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( ph /\ z e. ( A [,] B ) ) )
246		nfv 1683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- F/ y ( ( ph /\ z e. ( A [,] B ) ) -> ( G ` z ) = ( F ` z ) )
247		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( y = z -> ( y e. ( A [,] B ) <-> z e. ( A [,] B ) ) )
248	247	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( y = z -> ( ( ph /\ y e. ( A [,] B ) ) <-> ( ph /\ z e. ( A [,] B ) ) ) )
249		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( y = z -> ( G ` y ) = ( G ` z ) )
250		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( y = z -> ( F ` y ) = ( F ` z ) )
251	249, 250	eqeq12d 2489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( y = z -> ( ( G ` y ) = ( F ` y ) <-> ( G ` z ) = ( F ` z ) ) )
252	248, 251	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( y = z -> ( ( ( ph /\ y e. ( A [,] B ) ) -> ( G ` y ) = ( F ` y ) ) <-> ( ( ph /\ z e. ( A [,] B ) ) -> ( G ` z ) = ( F ` z ) ) ) )
253	246, 252, 180	chvar 1982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ z e. ( A [,] B ) ) -> ( G ` z ) = ( F ` z ) )
254	245, 253	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( G ` z ) = ( F ` z ) )
255	242, 254	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( G ` z ) = ( F ` z ) )
256		simp-4r 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> w C_ RR )
257		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. w )
258	257, 244	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( z e. w /\ z e. ( A [,] B ) ) )
259		elin 3692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( z e. ( w i^i ( A [,] B ) ) <-> ( z e. w /\ z e. ( A [,] B ) ) )
260	258, 259	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. ( w i^i ( A [,] B ) ) )
261		eqcom 2476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( `' F " u ) = ( w i^i ( A [,] B ) ) <-> ( w i^i ( A [,] B ) ) = ( `' F " u ) )
262	261	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( `' F " u ) = ( w i^i ( A [,] B ) ) -> ( w i^i ( A [,] B ) ) = ( `' F " u ) )
263	262	ad3antlr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( w i^i ( A [,] B ) ) = ( `' F " u ) )
264	260, 263	eleqtrd 2557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. ( `' F " u ) )
265	242, 264	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. ( `' F " u ) )
266	237, 256, 265	jca31 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) )
267		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) -> z e. ( `' F " u ) )
268	23	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) -> F Fn ( A [,] B ) )
269		elpreima 6008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( F Fn ( A [,] B ) -> ( z e. ( `' F " u ) <-> ( z e. ( A [,] B ) /\ ( F ` z ) e. u ) ) )
270	268, 269	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) -> ( z e. ( `' F " u ) <-> ( z e. ( A [,] B ) /\ ( F ` z ) e. u ) ) )
271	267, 270	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) -> ( z e. ( A [,] B ) /\ ( F ` z ) e. u ) )
272	271	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) -> ( F ` z ) e. u )
273	266, 272	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( F ` z ) e. u )
274	255, 273	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( G ` z ) e. u )
275	236, 274	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( G ` z ) e. u )
276		simp-6l 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ph )
277		simp-6r 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> w C_ RR )
278		simp-4r 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( F ` A ) e. u )
279	276, 277, 278	jca31 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) )
280		simpllr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( F ` B ) e. u )
281		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> z e. w )
282	279, 280, 281	jca31 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) )
283		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> -. z e. ( A [,] B ) )
284	282, 283	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) )
285		simp-5l 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ph )
286		simp-4r 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( F ` A ) e. u )
287	285, 286	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( ph /\ ( F ` A ) e. u ) )
288		simpllr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( F ` B ) e. u )
289		simp-5r 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> w C_ RR )
290		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> z e. w )
291	289, 290	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( w C_ RR /\ z e. w ) )
292		ssel2 3504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( w C_ RR /\ z e. w ) -> z e. RR )
293	291, 292	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> z e. RR )
294	287, 288, 293	jca31 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) )
295		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> -. z e. ( A [,] B ) )
296	294, 295	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) )
297	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> G = ( y e. RR |-> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) ) )
298		breq1 4456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( y = z -> ( y < A <-> z < A ) )
299		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( y = z -> ( F ` A ) = ( F ` A ) )
300		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( y = z -> ( F ` B ) = ( F ` B ) )
301	298, 299, 300	ifeq123d 31337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( y = z -> if ( y < A , ( F ` A ) , ( F ` B ) ) = if ( z < A , ( F ` A ) , ( F ` B ) ) )
302	247, 250, 301	ifeq123d 31337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( y = z -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
303	302	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) /\ y = z ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
304		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> z e. RR )
305		iffalse 3954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( -. z e. ( A [,] B ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = if ( z < A , ( F ` A ) , ( F ` B ) ) )
306	305	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = if ( z < A , ( F ` A ) , ( F ` B ) ) )
307		simp-5r 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) /\ z < A ) -> ( F ` A ) e. u )
308		simp-4r 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) /\ -. z < A ) -> ( F ` B ) e. u )
309	307, 308	ifclda 3977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> if ( z < A , ( F ` A ) , ( F ` B ) ) e. u )
310	306, 309	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) e. u )
311	310	idi 2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) e. u )
312	297, 303, 304, 311	fvmptd 5962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> ( G ` z ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
313	312, 306	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> ( G ` z ) = if ( z < A , ( F ` A ) , ( F ` B ) ) )
314	313, 309	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> ( G ` z ) e. u )
315	296, 314	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( G ` z ) e. u )
316	284, 315	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( G ` z ) e. u )
317	275, 316	pm2.61dan 789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) -> ( G ` z ) e. u )
318	230, 317	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) /\ z e. w /\ ( G ` z ) = y ) -> ( G ` z ) e. u )
319	226, 318	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) /\ z e. w /\ ( G ` z ) = y ) -> y e. u )
320	319	3exp 1195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) -> ( z e. w -> ( ( G ` z ) = y -> y e. u ) ) )
321	320	rexlimdv 2957	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) -> ( E. z e. w ( G ` z ) = y -> y e. u ) )
322	223, 321	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ y e. ( G " w ) ) -> y e. u )
323	322	ex 434	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( y e. ( G " w ) -> y e. u ) )
324	216, 323	alrimi 1825	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> A. y ( y e. ( G " w ) -> y e. u ) )
325	215, 324	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> A. y ( y e. ( G " w ) -> y e. u ) )
326		dfss2 3498	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( G " w ) C_ u <-> A. y ( y e. ( G " w ) -> y e. u ) )
327	325, 326	sylibr 212	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( G " w ) C_ u )
328	204, 212, 214	jca31 534	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) )
329		imaundi 5424	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( G " ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) = ( ( G " ( -oo (,) A ) ) u. ( G " ( B (,) +oo ) ) )
330		nfv 1683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- F/ t ph
331	217	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) -> Fun G )
332		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) -> t e. ( G " ( -oo (,) A ) ) )
333	331, 332	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) -> ( Fun G /\ t e. ( G " ( -oo (,) A ) ) ) )
334		fvelima 5926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( Fun G /\ t e. ( G " ( -oo (,) A ) ) ) -> E. z e. ( -oo (,) A ) ( G ` z ) = t )
335	333, 334	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) -> E. z e. ( -oo (,) A ) ( G ` z ) = t )
336		simp1l 1020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) /\ z e. ( -oo (,) A ) /\ ( G ` z ) = t ) -> ph )
337		simp2 997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) /\ z e. ( -oo (,) A ) /\ ( G ` z ) = t ) -> z e. ( -oo (,) A ) )
338	336, 337	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) /\ z e. ( -oo (,) A ) /\ ( G ` z ) = t ) -> ( ph /\ z e. ( -oo (,) A ) ) )
339		simp3 998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) /\ z e. ( -oo (,) A ) /\ ( G ` z ) = t ) -> ( G ` z ) = t )
340	338, 339	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) /\ z e. ( -oo (,) A ) /\ ( G ` z ) = t ) -> ( ( ph /\ z e. ( -oo (,) A ) ) /\ ( G ` z ) = t ) )
341		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ph /\ z e. ( -oo (,) A ) ) /\ ( G ` z ) = t ) -> ( G ` z ) = t )
342	341	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ph /\ z e. ( -oo (,) A ) ) /\ ( G ` z ) = t ) -> t = ( G ` z ) )
343	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> G = ( y e. RR |-> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) ) )
344	302	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ph /\ z e. ( -oo (,) A ) ) /\ y = z ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
345		elioore 11571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( z e. ( -oo (,) A ) -> z e. RR )
346	345	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> z e. RR )
347		elioo3g 11570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( z e. ( -oo (,) A ) <-> ( ( -oo e. RR* /\ A e. RR* /\ z e. RR* ) /\ ( -oo < z /\ z < A ) ) )
348	347	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( z e. ( -oo (,) A ) -> ( ( -oo e. RR* /\ A e. RR* /\ z e. RR* ) /\ ( -oo < z /\ z < A ) ) )
349	348	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( z e. ( -oo (,) A ) -> ( -oo < z /\ z < A ) )
350	349	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( z e. ( -oo (,) A ) -> z < A )
351	350	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> z < A )
352	5, 345	anim12ci 567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> ( z e. RR /\ A e. RR ) )
353		ltnle 9676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( z e. RR /\ A e. RR ) -> ( z < A <-> -. A <_ z ) )
354	352, 353	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> ( z < A <-> -. A <_ z ) )
355	351, 354	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> -. A <_ z )
356		3mix2 1166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( -. A <_ z -> ( -. z e. RR \/ -. A <_ z \/ -. z <_ B ) )
357		3ianor 990	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( -. ( z e. RR /\ A <_ z /\ z <_ B ) <-> ( -. z e. RR \/ -. A <_ z \/ -. z <_ B ) )
358	356, 357	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( -. A <_ z -> -. ( z e. RR /\ A <_ z /\ z <_ B ) )
359	355, 358	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> -. ( z e. RR /\ A <_ z /\ z <_ B ) )
360	7	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> ( A e. RR /\ B e. RR ) )
361		elicc2 11601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( A e. RR /\ B e. RR ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
362	360, 361	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
363	359, 362	mtbird 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> -. z e. ( A [,] B ) )
364	363, 305	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = if ( z < A , ( F ` A ) , ( F ` B ) ) )
365		iftrue 3951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( z < A -> if ( z < A , ( F ` A ) , ( F ` B ) ) = ( F ` A ) )
366	350, 365	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( z e. ( -oo (,) A ) -> if ( z < A , ( F ` A ) , ( F ` B ) ) = ( F ` A ) )
367	366	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> if ( z < A , ( F ` A ) , ( F ` B ) ) = ( F ` A ) )
368	364, 367	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = ( F ` A ) )
369	168	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> ( F ` A ) e. Y )
370	368, 369	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) e. Y )
371	343, 344, 346, 370	fvmptd 5962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> ( G ` z ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
372	371	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ph /\ z e. ( -oo (,) A ) ) /\ ( G ` z ) = t ) -> ( G ` z ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B )