Theorem ftc1lem3

Description: Lemma for ftc1 . (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 8-Sep-2015)

	Ref	Expression
Hypotheses	ftc1.g	|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
	ftc1.a	|- ( ph -> A e. RR )
	ftc1.b	|- ( ph -> B e. RR )
	ftc1.le	|- ( ph -> A <_ B )
	ftc1.s	|- ( ph -> ( A (,) B ) C_ D )
	ftc1.d	|- ( ph -> D C_ RR )
	ftc1.i	|- ( ph -> F e. L^1 )
	ftc1.c	|- ( ph -> C e. ( A (,) B ) )
	ftc1.f	|- ( ph -> F e. ( ( K CnP L ) ` C ) )
	ftc1.j	|- J = ( L |`t RR )
	ftc1.k	|- K = ( L |`t D )
	ftc1.l	|- L = ( TopOpen ` CCfld )
Assertion	ftc1lem3	|- ( ph -> F : D --> CC )

Proof

Step	Hyp	Ref	Expression
1		ftc1.g	|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
2		ftc1.a	|- ( ph -> A e. RR )
3		ftc1.b	|- ( ph -> B e. RR )
4		ftc1.le	|- ( ph -> A <_ B )
5		ftc1.s	|- ( ph -> ( A (,) B ) C_ D )
6		ftc1.d	|- ( ph -> D C_ RR )
7		ftc1.i	|- ( ph -> F e. L^1 )
8		ftc1.c	|- ( ph -> C e. ( A (,) B ) )
9		ftc1.f	|- ( ph -> F e. ( ( K CnP L ) ` C ) )
10		ftc1.j	|- J = ( L |`t RR )
11		ftc1.k	|- K = ( L |`t D )
12		ftc1.l	|- L = ( TopOpen ` CCfld )
13	12	cnfldtopon	|- L e. ( TopOn ` CC )
14		ax-resscn	|- RR C_ CC
15	6 14	sstrdi	|- ( ph -> D C_ CC )
16		resttopon	|- ( ( L e. ( TopOn ` CC ) /\ D C_ CC ) -> ( L |`t D ) e. ( TopOn ` D ) )
17	13 15 16	sylancr	|- ( ph -> ( L |`t D ) e. ( TopOn ` D ) )
18	11 17	eqeltrid	|- ( ph -> K e. ( TopOn ` D ) )
19	13	a1i	|- ( ph -> L e. ( TopOn ` CC ) )
20		cnpf2	|- ( ( K e. ( TopOn ` D ) /\ L e. ( TopOn ` CC ) /\ F e. ( ( K CnP L ) ` C ) ) -> F : D --> CC )
21	18 19 9 20	syl3anc	|- ( ph -> F : D --> CC )