Theorem icccncfext 37705

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	. . . . . . . . . . . 12 |- J = ( topGen ` ran (,) )
2		retopon 21782	. . . . . . . . . . . 12 |- ( topGen ` ran (,) ) e. (TopOn ` RR )
3	1, 2	eqeltri 2503	. . . . . . . . . . 11 |- J e. (TopOn ` RR )
4		icccncfext.5	. . . . . . . . . . . 12 |- ( ph -> A e. RR )
5		icccncfext.6	. . . . . . . . . . . 12 |- ( ph -> B e. RR )
6	4, 5	iccssred 37551	. . . . . . . . . . 11 |- ( ph -> ( A [,] B ) C_ RR )
7		resttopon 20175	. . . . . . . . . . 11 |- ( ( J e. (TopOn ` RR ) /\ ( A [,] B ) C_ RR ) -> ( J ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) )
8	3, 6, 7	sylancr 667	. . . . . . . . . 10 |- ( ph -> ( J ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) )
9		icccncfext.8	. . . . . . . . . . . 12 |- ( ph -> K e. Top )
10		icccncfext.3	. . . . . . . . . . . 12 |- Y = U. K
11	9, 10	jctir 540	. . . . . . . . . . 11 |- ( ph -> ( K e. Top /\ Y = U. K ) )
12		istopon 19938	. . . . . . . . . . 11 |- ( K e. (TopOn ` Y ) <-> ( K e. Top /\ Y = U. K ) )
13	11, 12	sylibr 215	. . . . . . . . . 10 |- ( ph -> K e. (TopOn ` Y ) )
14		icccncfext.9	. . . . . . . . . 10 |- ( ph -> F e. ( ( J ↾t ( A [,] B ) ) Cn K ) )
15		cnf2 20263	. . . . . . . . . 10 |- ( ( ( J ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) /\ K e. (TopOn ` Y ) /\ F e. ( ( J ↾t ( A [,] B ) ) Cn K ) ) -> F : ( A [,] B ) --> Y )
16	8, 13, 14, 15	syl3anc 1264	. . . . . . . . 9 |- ( ph -> F : ( A [,] B ) --> Y )
17		ffn 5746	. . . . . . . . 9 |- ( F : ( A [,] B ) --> Y -> F Fn ( A [,] B ) )
18	16, 17	syl 17	. . . . . . . 8 |- ( ph -> F Fn ( A [,] B ) )
19		dffn3 5753	. . . . . . . 8 |- ( F Fn ( A [,] B ) <-> F : ( A [,] B ) --> ran F )
20	18, 19	sylib 199	. . . . . . 7 |- ( ph -> F : ( A [,] B ) --> ran F )
21	20	ffvelrnda 6037	. . . . . 6 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` y ) e. ran F )
22		fnfun 5691	. . . . . . . . . 10 |- ( F Fn ( A [,] B ) -> Fun F )
23	18, 22	syl 17	. . . . . . . . 9 |- ( ph -> Fun F )
24	4	rexrd 9697	. . . . . . . . . . 11 |- ( ph -> A e. RR* )
25	5	rexrd 9697	. . . . . . . . . . 11 |- ( ph -> B e. RR* )
26		icccncfext.7	. . . . . . . . . . 11 |- ( ph -> A <_ B )
27		lbicc2 11755	. . . . . . . . . . 11 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
28	24, 25, 26, 27	syl3anc 1264	. . . . . . . . . 10 |- ( ph -> A e. ( A [,] B ) )
29		fndm 5693	. . . . . . . . . . . 12 |- ( F Fn ( A [,] B ) -> dom F = ( A [,] B ) )
30	18, 29	syl 17	. . . . . . . . . . 11 |- ( ph -> dom F = ( A [,] B ) )
31	30	eqcomd 2430	. . . . . . . . . 10 |- ( ph -> ( A [,] B ) = dom F )
32	28, 31	eleqtrd 2509	. . . . . . . . 9 |- ( ph -> A e. dom F )
33		fvelrn 6030	. . . . . . . . 9 |- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. ran F )
34	23, 32, 33	syl2anc 665	. . . . . . . 8 |- ( ph -> ( F ` A ) e. ran F )
35		ubicc2 11756	. . . . . . . . . . 11 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
36	24, 25, 26, 35	syl3anc 1264	. . . . . . . . . 10 |- ( ph -> B e. ( A [,] B ) )
37	36, 31	eleqtrd 2509	. . . . . . . . 9 |- ( ph -> B e. dom F )
38		fvelrn 6030	. . . . . . . . 9 |- ( ( Fun F /\ B e. dom F ) -> ( F ` B ) e. ran F )
39	23, 37, 38	syl2anc 665	. . . . . . . 8 |- ( ph -> ( F ` B ) e. ran F )
40	34, 39	ifcld 3954	. . . . . . 7 |- ( ph -> if ( y < A , ( F ` A ) , ( F ` B ) ) e. ran F )
41	40	adantr 466	. . . . . 6 |- ( ( ph /\ -. y e. ( A [,] B ) ) -> if ( y < A , ( F ` A ) , ( F ` B ) ) e. ran F )
42	21, 41	ifclda 3943	. . . . 5 |- ( ph -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) e. ran F )
43	42	adantr 466	. . . 4 |- ( ( ph /\ y e. RR ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) e. ran F )
44		icccncfext.4	. . . . 5 |- G = ( x e. RR |-> if ( x e. ( A [,] B ) , ( F ` x ) , if ( x < A , ( F ` A ) , ( F ` B ) ) ) )
45		nfv 1755	. . . . . . 7 |- F/ y x e. ( A [,] B )
46		nfcv 2580	. . . . . . 7 |- F/_ y ( F ` x )
47		nfcv 2580	. . . . . . 7 |- F/_ y if ( x < A , ( F ` A ) , ( F ` B ) )
48	45, 46, 47	nfif 3940	. . . . . 6 |- F/_ y if ( x e. ( A [,] B ) , ( F ` x ) , if ( x < A , ( F ` A ) , ( F ` B ) ) )
49		nfv 1755	. . . . . . 7 |- F/ x y e. ( A [,] B )
50		icccncfext.1	. . . . . . . 8 |- F/_ x F
51		nfcv 2580	. . . . . . . 8 |- F/_ x y
52	50, 51	nffv 5888	. . . . . . 7 |- F/_ x ( F ` y )
53		nfv 1755	. . . . . . . 8 |- F/ x y < A
54		nfcv 2580	. . . . . . . . 9 |- F/_ x A
55	50, 54	nffv 5888	. . . . . . . 8 |- F/_ x ( F ` A )
56		nfcv 2580	. . . . . . . . 9 |- F/_ x B
57	50, 56	nffv 5888	. . . . . . . 8 |- F/_ x ( F ` B )
58	53, 55, 57	nfif 3940	. . . . . . 7 |- F/_ x if ( y < A , ( F ` A ) , ( F ` B ) )
59	49, 52, 58	nfif 3940	. . . . . 6 |- F/_ x if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) )
60		eleq1 2495	. . . . . . 7 |- ( x = y -> ( x e. ( A [,] B ) <-> y e. ( A [,] B ) ) )
61		fveq2 5881	. . . . . . 7 |- ( x = y -> ( F ` x ) = ( F ` y ) )
62		breq1 4426	. . . . . . . 8 |- ( x = y -> ( x < A <-> y < A ) )
63	62	ifbid 3933	. . . . . . 7 |- ( x = y -> if ( x < A , ( F ` A ) , ( F ` B ) ) = if ( y < A , ( F ` A ) , ( F ` B ) ) )
64	60, 61, 63	ifbieq12d 3938	. . . . . 6 |- ( 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 ) ) ) )
65	48, 59, 64	cbvmpt 4515	. . . . 5 |- ( 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 ) ) ) )
66	44, 65	eqtri 2451	. . . 4 |- G = ( y e. RR |-> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) )
67	43, 66	fmptd 6061	. . 3 |- ( ph -> G : RR --> ran F )
68	67	adantr 466	. . . . 5 |- ( ( ph /\ y e. RR ) -> G : RR --> ran F )
69		simplll 766	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) -> ph )
70		simplr 760	. . . . . . . . . . 11 |- ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) -> u e. ( K ↾t ran F ) )
71	69, 70	jca 534	. . . . . . . . . 10 |- ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) -> ( ph /\ u e. ( K ↾t ran F ) ) )
72		ssid 3483	. . . . . . . . . . . . . 14 |- ran F C_ ran F
73	72	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ran F C_ ran F )
74		frn 5752	. . . . . . . . . . . . . 14 |- ( F : ( A [,] B ) --> Y -> ran F C_ Y )
75	16, 74	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ran F C_ Y )
76		cnrest2 20300	. . . . . . . . . . . . 13 |- ( ( 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 ) ) ) )
77	13, 73, 75, 76	syl3anc 1264	. . . . . . . . . . . 12 |- ( ph -> ( F e. ( ( J ↾t ( A [,] B ) ) Cn K ) <-> F e. ( ( J ↾t ( A [,] B ) ) Cn ( K ↾t ran F ) ) ) )
78	14, 77	mpbid 213	. . . . . . . . . . 11 |- ( ph -> F e. ( ( J ↾t ( A [,] B ) ) Cn ( K ↾t ran F ) ) )
79	78	anim1i 570	. . . . . . . . . 10 |- ( ( ph /\ u e. ( K ↾t ran F ) ) -> ( F e. ( ( J ↾t ( A [,] B ) ) Cn ( K ↾t ran F ) ) /\ u e. ( K ↾t ran F ) ) )
80		cnima 20279	. . . . . . . . . 10 |- ( ( F e. ( ( J ↾t ( A [,] B ) ) Cn ( K ↾t ran F ) ) /\ u e. ( K ↾t ran F ) ) -> ( `' F " u ) e. ( J ↾t ( A [,] B ) ) )
81	71, 79, 80	3syl 18	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) -> ( `' F " u ) e. ( J ↾t ( A [,] B ) ) )
82		retop 21780	. . . . . . . . . . . . . 14 |- ( topGen ` ran (,) ) e. Top
83	1, 82	eqeltri 2503	. . . . . . . . . . . . 13 |- J e. Top
84	83	a1i 11	. . . . . . . . . . . 12 |- ( ph -> J e. Top )
85		reex 9637	. . . . . . . . . . . . . 14 |- RR e. _V
86	85	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> RR e. _V )
87	86, 6	ssexd 4571	. . . . . . . . . . . 12 |- ( ph -> ( A [,] B ) e. _V )
88	84, 87	jca 534	. . . . . . . . . . 11 |- ( ph -> ( J e. Top /\ ( A [,] B ) e. _V ) )
89	69, 88	syl 17	. . . . . . . . . 10 |- ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) -> ( J e. Top /\ ( A [,] B ) e. _V ) )
90		elrest 15325	. . . . . . . . . 10 |- ( ( 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 ) ) ) )
91	89, 90	syl 17	. . . . . . . . 9 |- ( ( ( ( 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 ) ) ) )
92	81, 91	mpbid 213	. . . . . . . 8 |- ( ( ( ( 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 ) ) )
93	69	3ad2ant1 1026	. . . . . . . . . . 11 |- ( ( ( ( ( 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 )
94		simpllr 767	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ y e. RR ) /\ u e. ( K ↾t ran F ) ) /\ ( G ` y ) e. u ) -> y e. RR )
95	94	3ad2ant1 1026	. . . . . . . . . . 11 |- ( ( ( ( ( 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 )
96		simp1r 1030	. . . . . . . . . . 11 |- ( ( ( ( ( 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 )
97	93, 95, 96	jca31 536	. . . . . . . . . 10 |- ( ( ( ( ( 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 ) )
98		simpll2 1045	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 )
99		iooretop 21784	. . . . . . . . . . . . . . . . 17 |- ( -oo (,) A ) e. ( topGen ` ran (,) )
100	99, 1	eleqtrri 2506	. . . . . . . . . . . . . . . 16 |- ( -oo (,) A ) e. J
101		iooretop 21784	. . . . . . . . . . . . . . . . 17 |- ( B (,) +oo ) e. ( topGen ` ran (,) )
102	101, 1	eleqtrri 2506	. . . . . . . . . . . . . . . 16 |- ( B (,) +oo ) e. J
103		unopn 19931	. . . . . . . . . . . . . . . 16 |- ( ( J e. Top /\ ( -oo (,) A ) e. J /\ ( B (,) +oo ) e. J ) -> ( ( -oo (,) A ) u. ( B (,) +oo ) ) e. J )
104	83, 100, 102, 103	mp3an 1360	. . . . . . . . . . . . . . 15 |- ( ( -oo (,) A ) u. ( B (,) +oo ) ) e. J
105		unopn 19931	. . . . . . . . . . . . . . 15 |- ( ( J e. Top /\ w e. J /\ ( ( -oo (,) A ) u. ( B (,) +oo ) ) e. J ) -> ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) e. J )
106	83, 104, 105	mp3an13 1351	. . . . . . . . . . . . . 14 |- ( w e. J -> ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) e. J )
107	98, 106	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 )
108		simpl1l 1056	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 ) )
109	108	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) )
110		simpl1r 1057	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 )
111	110	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 )
112		simpll3 1046	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) ) )
113		difreicc 11771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( A e. RR /\ B e. RR ) -> ( RR \ ( A [,] B ) ) = ( ( -oo (,) A ) u. ( B (,) +oo ) ) )
114	4, 5, 113	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> ( RR \ ( A [,] B ) ) = ( ( -oo (,) A ) u. ( B (,) +oo ) ) )
115	114	eqcomd 2430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ph -> ( ( -oo (,) A ) u. ( B (,) +oo ) ) = ( RR \ ( A [,] B ) ) )
116	115	eleq2d 2492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ph -> ( y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) <-> y e. ( RR \ ( A [,] B ) ) ) )
117	116	notbid 295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ph -> ( -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) <-> -. y e. ( RR \ ( A [,] B ) ) ) )
118	117	biimpa 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> -. y e. ( RR \ ( A [,] B ) ) )
119		eldif 3446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( y e. ( RR \ ( A [,] B ) ) <-> ( y e. RR /\ -. y e. ( A [,] B ) ) )
120	118, 119	sylnib 305	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> -. ( y e. RR /\ -. y e. ( A [,] B ) ) )
121		imnan 423	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( y e. RR -> -. -. y e. ( A [,] B ) ) <-> -. ( y e. RR /\ -. y e. ( A [,] B ) ) )
122	120, 121	sylibr 215	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( y e. RR -> -. -. y e. ( A [,] B ) ) )
123	122	imp 430	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) /\ y e. RR ) -> -. -. y e. ( A [,] B ) )
124	123	notnotrd 116	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) /\ y e. RR ) -> y e. ( A [,] B ) )
125	124	an32s 811	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ y e. RR ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. ( A [,] B ) )
126	125	adantlr 719	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. ( A [,] B ) )
127		simplll 766	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ph )
128	6	sselda 3464	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ y e. ( A [,] B ) ) -> y e. RR )
129	16	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ y e. ( A [,] B ) ) -> F : ( A [,] B ) --> Y )
130	129	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ y e. ( A [,] B ) ) /\ y e. ( A [,] B ) ) -> ( F ` y ) e. Y )
131	16, 28	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ph -> ( F ` A ) e. Y )
132	131	ad3antrrr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ y e. ( A [,] B ) ) /\ -. y e. ( A [,] B ) ) /\ y < A ) -> ( F ` A ) e. Y )
133	16, 36	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ph -> ( F ` B ) e. Y )
134	133	ad3antrrr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ y e. ( A [,] B ) ) /\ -. y e. ( A [,] B ) ) /\ -. y < A ) -> ( F ` B ) e. Y )
135	132, 134	ifclda 3943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ y e. ( A [,] B ) ) /\ -. y e. ( A [,] B ) ) -> if ( y < A , ( F ` A ) , ( F ` B ) ) e. Y )
136	130, 135	ifclda 3943	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ y e. ( A [,] B ) ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) e. Y )
137	66	fvmpt2 5973	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 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 ) ) ) )
138	128, 136, 137	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( G ` y ) = if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) )
139		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ y e. ( A [,] B ) ) -> y e. ( A [,] B ) )
140	139	iftrued 3919	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ y e. ( A [,] B ) ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) = ( F ` y ) )
141	138, 140	eqtrd 2463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( G ` y ) = ( F ` y ) )
142	141	eqcomd 2430	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` y ) = ( G ` y ) )
143	127, 126, 142	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( F ` y ) = ( G ` y ) )
144		simplr 760	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( G ` y ) e. u )
145	143, 144	eqeltrd 2507	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( F ` y ) e. u )
146	127, 18	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> F Fn ( A [,] B ) )
147		elpreima 6017	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( F Fn ( A [,] B ) -> ( y e. ( `' F " u ) <-> ( y e. ( A [,] B ) /\ ( F ` y ) e. u ) ) )
148	146, 147	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 ) ) )
149	126, 145, 148	mpbir2and 930	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> y e. ( `' F " u ) )
150	149	adantlr 719	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( 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 ) )
151		simplr 760	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( 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 ) ) )
152	150, 151	eleqtrd 2509	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( 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 ) ) )
153		elin 3649	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( w i^i ( A [,] B ) ) <-> ( y e. w /\ y e. ( A [,] B ) ) )
154	152, 153	sylib 199	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( 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 ) ) )
155	154	simpld 460	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( 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 )
156	155	ex 435	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 ) )
157	156	orrd 379	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) )
158	157	orcomd 389	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) ) )
159		elun 3606	. . . . . . . . . . . . . . 15 |- ( y e. ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) <-> ( y e. w \/ y e. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) )
160	158, 159	sylibr 215	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> y e. ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) )
161	109, 111, 112, 160	syl21anc 1263	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) ) ) )
162		imaundi 5267	. . . . . . . . . . . . . 14 |- ( G " ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) = ( ( G " w ) u. ( G " ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) )
163	109	simpld 460	. . . . . . . . . . . . . . . . . 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 ) -> ph )
164		toponss 19942	. . . . . . . . . . . . . . . . . . 19 |- ( ( J e. (TopOn ` RR ) /\ w e. J ) -> w C_ RR )
165	3, 98, 164	sylancr 667	. . . . . . . . . . . . . . . . . 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 C_ RR )
166	163, 165, 112	jca31 536	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 ) ) ) )
167		simplr 760	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
168		simpr 462	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
169	44	funmpt2 5638	. . . . . . . . . . . . . . . . . . . . . . 23 |- Fun G
170	169	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> Fun G )
171	170	ad5antr 738	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( 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 )
172		fvelima 5933	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( Fun G /\ y e. ( G " w ) ) -> E. z e. w ( G ` z ) = y )
173	171, 172	sylancom 671	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( 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 )
174		eqcom 2431	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( G ` z ) = y <-> y = ( G ` z ) )
175	174	biimpi 197	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( G ` z ) = y -> y = ( G ` z ) )
176	175	3ad2ant3 1028	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( 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 ) )
177		simp1ll 1068	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( 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 ) )
178		simp1lr 1069	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( 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 )
179		simp2 1006	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( 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 )
180		simp-5l 776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ( 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 ) )
181		simp-5r 777	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ( 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 ) ) )
182		simplr 760	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ( 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 )
183	180, 181, 182	jca31 536	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( 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 ) )
184		eleq1 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( y = z -> ( y e. ( A [,] B ) <-> z e. ( A [,] B ) ) )
185	184	anbi2d 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( y = z -> ( ( ph /\ y e. ( A [,] B ) ) <-> ( ph /\ z e. ( A [,] B ) ) ) )
186		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( y = z -> ( G ` y ) = ( G ` z ) )
187		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( y = z -> ( F ` y ) = ( F ` z ) )
188	186, 187	eqeq12d 2444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( y = z -> ( ( G ` y ) = ( F ` y ) <-> ( G ` z ) = ( F ` z ) ) )
189	185, 188	imbi12d 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( y = z -> ( ( ( ph /\ y e. ( A [,] B ) ) -> ( G ` y ) = ( F ` y ) ) <-> ( ( ph /\ z e. ( A [,] B ) ) -> ( G ` z ) = ( F ` z ) ) ) )
190	189, 141	chvarv 2072	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ z e. ( A [,] B ) ) -> ( G ` z ) = ( F ` z ) )
191	190	adant423 37340	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( G ` z ) = ( F ` z ) )
192	191	adantlllr 37334	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( G ` z ) = ( F ` z ) )
193		simp-4l 774	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ph )
194		simp-4r 775	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> w C_ RR )
195		simplr 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. w )
196		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. ( A [,] B ) )
197	195, 196	elind 3650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. ( w i^i ( A [,] B ) ) )
198		eqcom 2431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( `' F " u ) = ( w i^i ( A [,] B ) ) <-> ( w i^i ( A [,] B ) ) = ( `' F " u ) )
199	198	biimpi 197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( `' F " u ) = ( w i^i ( A [,] B ) ) -> ( w i^i ( A [,] B ) ) = ( `' F " u ) )
200	199	ad3antlr 735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( w i^i ( A [,] B ) ) = ( `' F " u ) )
201	197, 200	eleqtrd 2509	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. ( `' F " u ) )
202	201	adantlllr 37334	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> z e. ( `' F " u ) )
203		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) -> z e. ( `' F " u ) )
204	18	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) -> F Fn ( A [,] B ) )
205		elpreima 6017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( F Fn ( A [,] B ) -> ( z e. ( `' F " u ) <-> ( z e. ( A [,] B ) /\ ( F ` z ) e. u ) ) )
206	204, 205	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) -> ( z e. ( `' F " u ) <-> ( z e. ( A [,] B ) /\ ( F ` z ) e. u ) ) )
207	203, 206	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) -> ( z e. ( A [,] B ) /\ ( F ` z ) e. u ) )
208	207	simprd 464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ w C_ RR ) /\ z e. ( `' F " u ) ) -> ( F ` z ) e. u )
209	193, 194, 202, 208	syl21anc 1263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( F ` z ) e. u )
210	192, 209	eqeltrd 2507	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ph /\ w C_ RR ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ z e. w ) /\ z e. ( A [,] B ) ) -> ( G ` z ) e. u )
211	183, 210	sylancom 671	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( 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 )
212		simp-5l 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ph )
213		simp-4r 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( F ` A ) e. u )
214	212, 213	jca 534	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( ph /\ ( F ` A ) e. u ) )
215		simpllr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( F ` B ) e. u )
216		simp-5r 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> w C_ RR )
217		simplr 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> z e. w )
218	216, 217	sseldd 3465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> z e. RR )
219	214, 215, 218	jca31 536	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( 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 ) )
220	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( 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 ) ) ) ) )
221		breq1 4426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( y = z -> ( y < A <-> z < A ) )
222	221	ifbid 3933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( y = z -> if ( y < A , ( F ` A ) , ( F ` B ) ) = if ( z < A , ( F ` A ) , ( F ` B ) ) )
223	184, 187, 222	ifeq123d 37345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( 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 ) ) ) )
224	223	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( 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 ) ) ) )
225		simplr 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> z e. RR )
226		iffalse 3920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( -. 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 ) ) )
227	226	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( 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 ) ) )
228		simp-5r 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) /\ z < A ) -> ( F ` A ) e. u )
229		simp-4r 775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) /\ -. z < A ) -> ( F ` B ) e. u )
230	228, 229	ifclda 3943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( 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 )
231	227, 230	eqeltrd 2507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( 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 )
232	220, 224, 225, 231	fvmptd 5970	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( 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 ) ) ) )
233	232, 227	eqtrd 2463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( 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 ) ) )
234	233, 230	eqeltrd 2507	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. RR ) /\ -. z e. ( A [,] B ) ) -> ( G ` z ) e. u )
235	219, 234	sylancom 671	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ph /\ w C_ RR ) /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) /\ z e. w ) /\ -. z e. ( A [,] B ) ) -> ( G ` z ) e. u )
236	235	adantl4r 755	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( 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 )
237	211, 236	pm2.61dan 798	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( 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 )
238	177, 178, 179, 237	syl21anc 1263	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( 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 )
239	176, 238	eqeltrd 2507	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( 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 )
240	239	rexlimdv3a 2916	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( 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 ) )
241	173, 240	mpd 15	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( 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 )
242	241	ex 435	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( 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 ) )
243	242	alrimiv 1767	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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 ) )
244	166, 167, 168, 243	syl21anc 1263	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 ) )
245		dfss2 3453	. . . . . . . . . . . . . . . 16 |- ( ( G " w ) C_ u <-> A. y ( y e. ( G " w ) -> y e. u ) )
246	244, 245	sylibr 215	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 )
247		imaundi 5267	. . . . . . . . . . . . . . . . 17 |- ( G " ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) = ( ( G " ( -oo (,) A ) ) u. ( G " ( B (,) +oo ) ) )
248	169	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) -> Fun G )
249		fvelima 5933	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( Fun G /\ t e. ( G " ( -oo (,) A ) ) ) -> E. z e. ( -oo (,) A ) ( G ` z ) = t )
250	248, 249	sylancom 671	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) -> E. z e. ( -oo (,) A ) ( G ` z ) = t )
251		simp1l 1029	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) /\ z e. ( -oo (,) A ) /\ ( G ` z ) = t ) -> ph )
252		simp2 1006	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) /\ z e. ( -oo (,) A ) /\ ( G ` z ) = t ) -> z e. ( -oo (,) A ) )
253		simp3 1007	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) /\ z e. ( -oo (,) A ) /\ ( G ` z ) = t ) -> ( G ` z ) = t )
254	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> G = ( y e. RR |-> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) ) )
255	223	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( 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 ) ) ) )
256		elioore 11673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( z e. ( -oo (,) A ) -> z e. RR )
257	256	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> z e. RR )
258		elioo3g 11672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( z e. ( -oo (,) A ) <-> ( ( -oo e. RR* /\ A e. RR* /\ z e. RR* ) /\ ( -oo < z /\ z < A ) ) )
259	258	biimpi 197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( z e. ( -oo (,) A ) -> ( ( -oo e. RR* /\ A e. RR* /\ z e. RR* ) /\ ( -oo < z /\ z < A ) ) )
260	259	simprrd 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( z e. ( -oo (,) A ) -> z < A )
261	260	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> z < A )
262		ltnle 9720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( z e. RR /\ A e. RR ) -> ( z < A <-> -. A <_ z ) )
263	256, 4, 262	syl2anr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> ( z < A <-> -. A <_ z ) )
264	261, 263	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> -. A <_ z )
265	264	intn3an2d 1375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> -. ( z e. RR /\ A <_ z /\ z <_ B ) )
266	4, 5	jca 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ph -> ( A e. RR /\ B e. RR ) )
267	266	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> ( A e. RR /\ B e. RR ) )
268		elicc2 11706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( A e. RR /\ B e. RR ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
269	267, 268	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
270	265, 269	mtbird 302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> -. z e. ( A [,] B ) )
271	270	iffalsed 3922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( 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 ) ) )
272	260	iftrued 3919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( z e. ( -oo (,) A ) -> if ( z < A , ( F ` A ) , ( F ` B ) ) = ( F ` A ) )
273	272	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> if ( z < A , ( F ` A ) , ( F ` B ) ) = ( F ` A ) )
274	271, 273	eqtrd 2463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = ( F ` A ) )
275	131	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> ( F ` A ) e. Y )
276	274, 275	eqeltrd 2507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) e. Y )
277	254, 255, 257, 276	fvmptd 5970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ z e. ( -oo (,) A ) ) -> ( G ` z ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
278	277	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ z e. ( -oo (,) A ) ) /\ ( G ` z ) = t ) -> ( G ` z ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
279		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ z e. ( -oo (,) A ) ) /\ ( G ` z ) = t ) -> ( G ` z ) = t )
280	274	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ z e. ( -oo (,) A ) ) /\ ( G ` z ) = t ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = ( F ` A ) )
281	278, 279, 280	3eqtr3d 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ z e. ( -oo (,) A ) ) /\ ( G ` z ) = t ) -> t = ( F ` A ) )
282	251, 252, 253, 281	syl21anc 1263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) /\ z e. ( -oo (,) A ) /\ ( G ` z ) = t ) -> t = ( F ` A ) )
283	282	rexlimdv3a 2916	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) -> ( E. z e. ( -oo (,) A ) ( G ` z ) = t -> t = ( F ` A ) ) )
284	250, 283	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) -> t = ( F ` A ) )
285		elsn 4012	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( t e. { ( F ` A ) } <-> t = ( F ` A ) )
286	284, 285	sylibr 215	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ t e. ( G " ( -oo (,) A ) ) ) -> t e. { ( F ` A ) } )
287	286	ex 435	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( t e. ( G " ( -oo (,) A ) ) -> t e. { ( F ` A ) } ) )
288	287	ssrdv 3470	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( G " ( -oo (,) A ) ) C_ { ( F ` A ) } )
289	288	adantr 466	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( F ` A ) e. u ) -> ( G " ( -oo (,) A ) ) C_ { ( F ` A ) } )
290		simpr 462	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( F ` A ) e. u ) -> ( F ` A ) e. u )
291	290	snssd 4145	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( F ` A ) e. u ) -> { ( F ` A ) } C_ u )
292	289, 291	sstrd 3474	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( F ` A ) e. u ) -> ( G " ( -oo (,) A ) ) C_ u )
293	292	adantr 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( G " ( -oo (,) A ) ) C_ u )
294		fvelima 5933	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( Fun G /\ t e. ( G " ( B (,) +oo ) ) ) -> E. z e. ( B (,) +oo ) ( G ` z ) = t )
295	170, 294	sylan 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) -> E. z e. ( B (,) +oo ) ( G ` z ) = t )
296		simp1l 1029	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) /\ z e. ( B (,) +oo ) /\ ( G ` z ) = t ) -> ph )
297		simp2 1006	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) /\ z e. ( B (,) +oo ) /\ ( G ` z ) = t ) -> z e. ( B (,) +oo ) )
298		simp3 1007	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) /\ z e. ( B (,) +oo ) /\ ( G ` z ) = t ) -> ( G ` z ) = t )
299	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> G = ( y e. RR |-> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) ) )
300	223	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ z e. ( B (,) +oo ) ) /\ 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 ) ) ) )
301		elioore 11673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( z e. ( B (,) +oo ) -> z e. RR )
302	301	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> z e. RR )
303	16	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ z e. ( A [,] B ) ) -> ( F ` z ) e. Y )
304	303	adantlr 719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ z e. ( B (,) +oo ) ) /\ z e. ( A [,] B ) ) -> ( F ` z ) e. Y )
305	4	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> A e. RR )
306	5	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> B e. RR )
307	26	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> A <_ B )
308		elioo3g 11672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( z e. ( B (,) +oo ) <-> ( ( B e. RR* /\ +oo e. RR* /\ z e. RR* ) /\ ( B < z /\ z < +oo ) ) )
309	308	biimpi 197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( z e. ( B (,) +oo ) -> ( ( B e. RR* /\ +oo e. RR* /\ z e. RR* ) /\ ( B < z /\ z < +oo ) ) )
310	309	simprld 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( z e. ( B (,) +oo ) -> B < z )
311	310	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> B < z )
312	305, 306, 302, 307, 311	lelttrd 9800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> A < z )
313	305, 302, 312	ltnsymd 9791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> -. z < A )
314	313	iffalsed 3922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> if ( z < A , ( F ` A ) , ( F ` B ) ) = ( F ` B ) )
315	133	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> ( F ` B ) e. Y )
316	314, 315	eqeltrd 2507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> if ( z < A , ( F ` A ) , ( F ` B ) ) e. Y )
317	316	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ z e. ( B (,) +oo ) ) /\ -. z e. ( A [,] B ) ) -> if ( z < A , ( F ` A ) , ( F ` B ) ) e. Y )
318	304, 317	ifclda 3943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) e. Y )
319	299, 300, 302, 318	fvmptd 5970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> ( G ` z ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
320	319	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ z e. ( B (,) +oo ) ) /\ ( G ` z ) = t ) -> ( G ` z ) = if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) )
321		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ z e. ( B (,) +oo ) ) /\ ( G ` z ) = t ) -> ( G ` z ) = t )
322	306, 302	ltnled 9789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> ( B < z <-> -. z <_ B ) )
323	311, 322	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> -. z <_ B )
324	323	intn3an3d 1376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> -. ( z e. RR /\ A <_ z /\ z <_ B ) )
325	266	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> ( A e. RR /\ B e. RR ) )
326	325, 268	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
327	324, 326	mtbird 302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> -. z e. ( A [,] B ) )
328	327	iffalsed 3922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = if ( z < A , ( F ` A ) , ( F ` B ) ) )
329	328, 314	eqtrd 2463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ z e. ( B (,) +oo ) ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = ( F ` B ) )
330	329	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ z e. ( B (,) +oo ) ) /\ ( G ` z ) = t ) -> if ( z e. ( A [,] B ) , ( F ` z ) , if ( z < A , ( F ` A ) , ( F ` B ) ) ) = ( F ` B ) )
331	320, 321, 330	3eqtr3d 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ z e. ( B (,) +oo ) ) /\ ( G ` z ) = t ) -> t = ( F ` B ) )
332	296, 297, 298, 331	syl21anc 1263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) /\ z e. ( B (,) +oo ) /\ ( G ` z ) = t ) -> t = ( F ` B ) )
333	332	rexlimdv3a 2916	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) -> ( E. z e. ( B (,) +oo ) ( G ` z ) = t -> t = ( F ` B ) ) )
334	295, 333	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) -> t = ( F ` B ) )
335		elsn 4012	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( t e. { ( F ` B ) } <-> t = ( F ` B ) )
336	334, 335	sylibr 215	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ t e. ( G " ( B (,) +oo ) ) ) -> t e. { ( F ` B ) } )
337	336	ex 435	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( t e. ( G " ( B (,) +oo ) ) -> t e. { ( F ` B ) } ) )
338	337	ssrdv 3470	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( G " ( B (,) +oo ) ) C_ { ( F ` B ) } )
339	338	adantr 466	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( F ` B ) e. u ) -> ( G " ( B (,) +oo ) ) C_ { ( F ` B ) } )
340		simpr 462	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( F ` B ) e. u ) -> ( F ` B ) e. u )
341	340	snssd 4145	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( F ` B ) e. u ) -> { ( F ` B ) } C_ u )
342	339, 341	sstrd 3474	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( F ` B ) e. u ) -> ( G " ( B (,) +oo ) ) C_ u )
343	342	adantlr 719	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( G " ( B (,) +oo ) ) C_ u )
344	293, 343	unssd 3642	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( ( G " ( -oo (,) A ) ) u. ( G " ( B (,) +oo ) ) ) C_ u )
345	247, 344	syl5eqss 3508	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( F ` A ) e. u ) /\ ( F ` B ) e. u ) -> ( G " ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) C_ u )
346	163, 167, 168, 345	syl21anc 1263	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 " ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) C_ u )
347	246, 346	unssd 3642	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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. ( G " ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) C_ u )
348	162, 347	syl5eqss 3508	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) ) ) ) C_ u )
349		eleq2 2496	. . . . . . . . . . . . . . 15 |- ( v = ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( y e. v <-> y e. ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) )
350		imaeq2 5183	. . . . . . . . . . . . . . . 16 |- ( v = ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( G " v ) = ( G " ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) )
351	350	sseq1d 3491	. . . . . . . . . . . . . . 15 |- ( v = ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( ( G " v ) C_ u <-> ( G " ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) C_ u ) )
352	349, 351	anbi12d 715	. . . . . . . . . . . . . 14 |- ( v = ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) -> ( ( y e. v /\ ( G " v ) C_ u ) <-> ( y e. ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) /\ ( G " ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) C_ u ) ) )
353	352	rspcev 3182	. . . . . . . . . . . . 13 |- ( ( ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) e. J /\ ( y e. ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) /\ ( G " ( w u. ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) ) C_ u ) ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) )
354	107, 161, 348, 353	syl12anc 1262	. . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 ) -> E. v e. J ( y e. v /\ ( G " v ) C_ u ) )
355	83	a1i 11	. . . . . . . . . . . . . . . 16 |- ( w e. J -> J e. Top )
356		iooretop 21784	. . . . . . . . . . . . . . . . . 18 |- ( -oo (,) B ) e. ( topGen ` ran (,) )
357	356, 1	eleqtrri 2506	. . . . . . . . . . . . . . . . 17 |- ( -oo (,) B ) e. J
358		inopn 19927	. . . . . . . . . . . . . . . . 17 |- ( ( J e. Top /\ w e. J /\ ( -oo (,) B ) e. J ) -> ( w i^i ( -oo (,) B ) ) e. J )
359	83, 357, 358	mp3an13 1351	. . . . . . . . . . . . . . . 16 |- ( w e. J -> ( w i^i ( -oo (,) B ) ) e. J )
360	100	a1i 11	. . . . . . . . . . . . . . . 16 |- ( w e. J -> ( -oo (,) A ) e. J )
361		unopn 19931	. . . . . . . . . . . . . . . 16 |- ( ( J e. Top /\ ( w i^i ( -oo (,) B ) ) e. J /\ ( -oo (,) A ) e. J ) -> ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) e. J )
362	355, 359, 360, 361	syl3anc 1264	. . . . . . . . . . . . . . 15 |- ( w e. J -> ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) e. J )
363	362	3ad2ant2 1027	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ w e. J /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) -> ( ( w i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) e. J )
364	363	ad2antrr 730	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 i^i ( -oo (,) B ) ) u. ( -oo (,) A ) ) e. J )
365		simpll1 1044	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) )
366		simpll3 1046	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) ) )
367		simpr 462	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 )
368		simpll 758	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ ( `' F " u ) = ( w i^i ( A [,] B ) ) ) )
369	266	ad3antrrr 734	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) -> ( A e. RR /\ B e. RR ) )
370		eqimss 3516	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( RR \ ( A [,] B ) ) = ( ( -oo (,) A ) u. ( B (,) +oo ) ) -> ( RR \ ( A [,] B ) ) C_ ( ( -oo (,) A ) u. ( B (,) +oo ) ) )
371	113, 370	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A e. RR /\ B e. RR ) -> ( RR \ ( A [,] B ) ) C_ ( ( -oo (,) A ) u. ( B (,) +oo ) ) )
372		difcom 3882	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( RR \ ( A [,] B ) ) C_ ( ( -oo (,) A ) u. ( B (,) +oo ) ) <-> ( RR \ ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) C_ ( A [,] B ) )
373	371, 372	sylib 199	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A e. RR /\ B e. RR ) -> ( RR \ ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) C_ ( A [,] B ) )
374	369, 373	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) -> ( RR \ ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) C_ ( A [,] B ) )
375	374	adantr 466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> ( RR \ ( ( -oo (,) A ) u. ( B (,) +oo ) ) ) C_ ( A [,] B ) )
376		simp-4r 775	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> y e. RR )
377		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ph /\ y e. RR ) /\ ( G ` y ) e. u ) /\ -. ( F ` B ) e. u ) /\ -. y e. ( -oo (,) A ) ) -> -. y e. ( -oo (,) A ) )
378		elioore 11673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( y e. ( B (,) +oo ) -> y e. RR )
379	378	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ y e. ( B (,) +oo ) ) -> y e. RR )
380		elioo3g 11672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( y e. ( B (,) +oo ) <-> ( ( B e. RR* /\ +oo e. RR* /\ y e. RR* ) /\ ( B < y /\ y < +oo ) ) )
381	380	biimpi 197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( y e. ( B (,) +oo ) -> ( ( B e. RR* /\ +oo e. RR* /\ y e. RR* ) /\ ( B < y /\ y < +oo ) ) )
382	381	simprld 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( y e. ( B (,) +oo ) -> B < y )
383	382	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ y e. ( B (,) +oo ) ) -> B < y )
384	5	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ph /\ y e. ( B (,) +oo ) ) -> B e. RR )
385	384, 379	ltnled 9789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ y e. ( B (,) +oo ) ) -> ( B < y <-> -. y <_ B ) )
386	383, 385	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ph /\ y e. ( B (,) +oo ) ) -> -. y <_ B )
387	386	intn3an3d 1376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ y e. ( B (,) +oo ) ) -> -. ( y e. RR /\ A <_ y /\ y <_ B ) )
388	266	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ph /\ y e. ( B (,) +oo ) ) -> ( A e. RR /\ B e. RR ) )
389		elicc2 11706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( A e. RR /\ B e. RR ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
390	388, 389	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ y e. ( B (,) +oo ) ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
391	387, 390	mtbird 302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ y e. ( B (,) +oo ) ) -> -. y e. ( A [,] B ) )
392	391	iffalsed 3922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ y e. ( B (,) +oo ) ) -> if ( y e. ( A [,] B ) , ( F ` y ) , if ( y < A , ( F ` A ) , ( F ` B ) ) ) = if ( y < A , ( F ` A ) , ( F ` B