Theorem cnpco 7766

Description: The composition of two continuous functions at point P is a continuous function at point P. Bourbaki TG I.9. (Contributed by FL, 31-Dec-2006.) Warning: The HTML proof page is 0.5MB in size.

Hypothesis

Ref	Expression
cnpco.1	|- X = U.J

Assertion

Ref	Expression
cnpco	|- (((J e. Top /\ L e. Top /\ P e. X) /\ (K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P)))) -> (G o. F) e. ((J CnP L)` P))

Proof of Theorem cnpco

Step	Hyp	Ref	Expression
1		fco 3642	. . . 4 |- ((G:U.K-->U.L /\ F:X-->U.K) -> (G o. F):X-->U.L)
2		eqid 1478	. . . . . 6 |- U.K = U.K
3		eqid 1478	. . . . . 6 |- U.L = U.L
4	2, 3	cnpf 7760	. . . . 5 |- (((K e. Top /\ L e. Top /\ (F` P) e. U.K) /\ G e. ((K CnP L)` (F` P))) -> G:U.K-->U.L)
5		3simp1 790	. . . . . . 7 |- ((K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P))) -> K e. Top)
6	5	adantl 390	. . . . . 6 |- (((J e. Top /\ L e. Top /\ P e. X) /\ (K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P)))) -> K e. Top)
7		3simp2 791	. . . . . . 7 |- ((J e. Top /\ L e. Top /\ P e. X) -> L e. Top)
8	7	adantr 391	. . . . . 6 |- (((J e. Top /\ L e. Top /\ P e. X) /\ (K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P)))) -> L e. Top)
9		ffvelrn 3820	. . . . . . 7 |- ((F:U.J-->U.K /\ P e. U.J) -> (F` P) e. U.K)
10		cnpco.1	. . . . . . . . . . . . 13 |- X = U.J
11	10	eleq2i 1541	. . . . . . . . . . . 12 |- (P e. X <-> P e. U.J)
12		pm3.2 283	. . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ K e. Top /\ P e. U.J) -> (F e. ((J CnP K)` P) -> ((J e. Top /\ K e. Top /\ P e. U.J) /\ F e. ((J CnP K)` P))))
13	12	3exp 834	. . . . . . . . . . . . . . . . . 18 |- (J e. Top -> (K e. Top -> (P e. U.J -> (F e. ((J CnP K)` P) -> ((J e. Top /\ K e. Top /\ P e. U.J) /\ F e. ((J CnP K)` P))))))
14	13	com34 36	. . . . . . . . . . . . . . . . 17 |- (J e. Top -> (K e. Top -> (F e. ((J CnP K)` P) -> (P e. U.J -> ((J e. Top /\ K e. Top /\ P e. U.J) /\ F e. ((J CnP K)` P))))))
15	14	com13 33	. . . . . . . . . . . . . . . 16 |- (F e. ((J CnP K)` P) -> (K e. Top -> (J e. Top -> (P e. U.J -> ((J e. Top /\ K e. Top /\ P e. U.J) /\ F e. ((J CnP K)` P))))))
16	15	a1i 8	. . . . . . . . . . . . . . 15 |- (G e. ((K CnP L)` (F` P)) -> (F e. ((J CnP K)` P) -> (K e. Top -> (J e. Top -> (P e. U.J -> ((J e. Top /\ K e. Top /\ P e. U.J) /\ F e. ((J CnP K)` P)))))))
17	16	com13 33	. . . . . . . . . . . . . 14 |- (K e. Top -> (F e. ((J CnP K)` P) -> (G e. ((K CnP L)` (F` P)) -> (J e. Top -> (P e. U.J -> ((J e. Top /\ K e. Top /\ P e. U.J) /\ F e. ((J CnP K)` P)))))))
18	17	3imp 829	. . . . . . . . . . . . 13 |- ((K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P))) -> (J e. Top -> (P e. U.J -> ((J e. Top /\ K e. Top /\ P e. U.J) /\ F e. ((J CnP K)` P)))))
19	18	com13 33	. . . . . . . . . . . 12 |- (P e. U.J -> (J e. Top -> ((K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P))) -> ((J e. Top /\ K e. Top /\ P e. U.J) /\ F e. ((J CnP K)` P)))))
20	11, 19	sylbi 199	. . . . . . . . . . 11 |- (P e. X -> (J e. Top -> ((K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P))) -> ((J e. Top /\ K e. Top /\ P e. U.J) /\ F e. ((J CnP K)` P)))))
21	20	com12 11	. . . . . . . . . 10 |- (J e. Top -> (P e. X -> ((K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P))) -> ((J e. Top /\ K e. Top /\ P e. U.J) /\ F e. ((J CnP K)` P)))))
22	21	a1d 12	. . . . . . . . 9 |- (J e. Top -> (L e. Top -> (P e. X -> ((K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P))) -> ((J e. Top /\ K e. Top /\ P e. U.J) /\ F e. ((J CnP K)` P))))))
23	22	3imp1 848	. . . . . . . 8 |- (((J e. Top /\ L e. Top /\ P e. X) /\ (K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P)))) -> ((J e. Top /\ K e. Top /\ P e. U.J) /\ F e. ((J CnP K)` P)))
24		eqid 1478	. . . . . . . . 9 |- U.J = U.J
25	24, 2	cnpf 7760	. . . . . . . 8 |- (((J e. Top /\ K e. Top /\ P e. U.J) /\ F e. ((J CnP K)` P)) -> F:U.J-->U.K)
26	23, 25	syl 10	. . . . . . 7 |- (((J e. Top /\ L e. Top /\ P e. X) /\ (K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P)))) -> F:U.J-->U.K)
27		3simp3 792	. . . . . . . . 9 |- ((J e. Top /\ L e. Top /\ P e. X) -> P e. X)
28	27, 10	syl6eleq 1561	. . . . . . . 8 |- ((J e. Top /\ L e. Top /\ P e. X) -> P e. U.J)
29	28	adantr 391	. . . . . . 7 |- (((J e. Top /\ L e. Top /\ P e. X) /\ (K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P)))) -> P e. U.J)
30	9, 26, 29	sylanc 473	. . . . . 6 |- (((J e. Top /\ L e. Top /\ P e. X) /\ (K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P)))) -> (F` P) e. U.K)
31	6, 8, 30	3jca 821	. . . . 5 |- (((J e. Top /\ L e. Top /\ P e. X) /\ (K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P)))) -> (K e. Top /\ L e. Top /\ (F` P) e. U.K))
32		3simp3 792	. . . . . 6 |- ((K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P))) -> G e. ((K CnP L)` (F` P)))
33	32	adantl 390	. . . . 5 |- (((J e. Top /\ L e. Top /\ P e. X) /\ (K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P)))) -> G e. ((K CnP L)` (F` P)))
34	4, 31, 33	sylanc 473	. . . 4 |- (((J e. Top /\ L e. Top /\ P e. X) /\ (K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P)))) -> G:U.K-->U.L)
35		pm3.2 283	. . . . . . . . . . . . 13 |- ((J e. Top /\ K e. Top /\ P e. X) -> (F e. ((J CnP K)` P) -> ((J e. Top /\ K e. Top /\ P e. X) /\ F e. ((J CnP K)` P))))
36	35	3exp 834	. . . . . . . . . . . 12 |- (J e. Top -> (K e. Top -> (P e. X -> (F e. ((J CnP K)` P) -> ((J e. Top /\ K e. Top /\ P e. X) /\ F e. ((J CnP K)` P))))))
37	36	com14 38	. . . . . . . . . . 11 |- (F e. ((J CnP K)` P) -> (K e. Top -> (P e. X -> (J e. Top -> ((J e. Top /\ K e. Top /\ P e. X) /\ F e. ((J CnP K)` P))))))
38	37	a1i 8	. . . . . . . . . 10 |- (G e. ((K CnP L)` (F` P)) -> (F e. ((J CnP K)` P) -> (K e. Top -> (P e. X -> (J e. Top -> ((J e. Top /\ K e. Top /\ P e. X) /\ F e. ((J CnP K)` P)))))))
39	38	com13 33	. . . . . . . . 9 |- (K e. Top -> (F e. ((J CnP K)` P) -> (G e. ((K CnP L)` (F` P)) -> (P e. X -> (J e. Top -> ((J e. Top /\ K e. Top /\ P e. X) /\ F e. ((J CnP K)` P)))))))
40	39	3imp 829	. . . . . . . 8 |- ((K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P))) -> (P e. X -> (J e. Top -> ((J e. Top /\ K e. Top /\ P e. X) /\ F e. ((J CnP K)` P)))))
41	40	com13 33	. . . . . . 7 |- (J e. Top -> (P e. X -> ((K e. Top /\ F e. ((J CnP K)` P) /\ G e. ((K CnP L)` (F` P))) -> ((J e. Top /\ K e. Top /\ P e. X) /\ F e. ((J CnP K)` P)))))
42	41	a1d 12	. . . . . 6 |- (J e. Top -> (L e. Top -> (