Theorem cmphmp 10444

Description: The composition of two homeomorphisms is a homeomorphism.

Assertion

Ref	Expression
cmphmp	|- ((J e. Top /\ K e. Top /\ L e. Top) -> ((F e. (J Homeo K) /\ G e. (K Homeo L)) -> (G o. F) e. (J Homeo L)))

Proof of Theorem cmphmp

Step	Hyp	Ref	Expression
1		eqid 1473	. . . . . . . . 9 |- U.J = U.J
2		eqid 1473	. . . . . . . . 9 |- U.K = U.K
3	1, 2	hmeomap 10441	. . . . . . . 8 |- ((J e. Top /\ K e. Top) -> (F e. (J Homeo K) -> F:U.J-1-1-onto->U.K))
4	3	3adant3 798	. . . . . . 7 |- ((J e. Top /\ K e. Top /\ L e. Top) -> (F e. (J Homeo K) -> F:U.J-1-1-onto->U.K))
5		eqid 1473	. . . . . . . . 9 |- U.L = U.L
6	2, 5	hmeomap 10441	. . . . . . . 8 |- ((K e. Top /\ L e. Top) -> (G e. (K Homeo L) -> G:U.K-1-1-onto->U.L))
7	6	3adant1 796	. . . . . . 7 |- ((J e. Top /\ K e. Top /\ L e. Top) -> (G e. (K Homeo L) -> G:U.K-1-1-onto->U.L))
8	4, 7	anim12d 557	. . . . . 6 |- ((J e. Top /\ K e. Top /\ L e. Top) -> ((F e. (J Homeo K) /\ G e. (K Homeo L)) -> (F:U.J-1-1-onto->U.K /\ G:U.K-1-1-onto->U.L)))
9	8	imp 350	. . . . 5 |- (((J e. Top /\ K e. Top /\ L e. Top) /\ (F e. (J Homeo K) /\ G e. (K Homeo L))) -> (F:U.J-1-1-onto->U.K /\ G:U.K-1-1-onto->U.L))
10		pm3.22 438	. . . . 5 |- ((F:U.J-1-1-onto->U.K /\ G:U.K-1-1-onto->U.L) -> (G:U.K-1-1-onto->U.L /\ F:U.J-1-1-onto->U.K))
11		f1oco 3698	. . . . 5 |- ((G:U.K-1-1-onto->U.L /\ F:U.J-1-1-onto->U.K) -> (G o. F):U.J-1-1-onto->U.L)
12	9, 10, 11	3syl 20	. . . 4 |- (((J e. Top /\ K e. Top /\ L e. Top) /\ (F e. (J Homeo K) /\ G e. (K Homeo L))) -> (G o. F):U.J-1-1-onto->U.L)
13		hmeocnb 10443	. . . . . . . 8 |- ((J e. Top /\ K e. Top) -> (F e. (J Homeo K) -> A.x e. J (F"x) e. K))
14	13	3adant3 798	. . . . . . 7 |- ((J e. Top /\ K e. Top /\ L e. Top) -> (F e. (J Homeo K) -> A.x e. J (F"x) e. K))
15		hmeocnb 10443	. . . . . . . 8 |- ((K e. Top /\ L e. Top) -> (G e. (K Homeo L) -> A.y e. K (G"y) e. L))
16	15	3adant1 796	. . . . . . 7 |- ((J e. Top /\ K e. Top /\ L e. Top) -> (G e. (K Homeo L) -> A.y e. K (G"y) e. L))
17	14, 16	anim12d 557	. . . . . 6 |- ((J e. Top /\ K e. Top /\ L e. Top) -> ((F e. (J Homeo K) /\ G e. (K Homeo L)) -> (A.x e. J (F"x) e. K /\ A.y e. K (G"y) e. L)))
18	17	imp 350	. . . . 5 |- (((J e. Top /\ K e. Top /\ L e. Top) /\ (F e. (J Homeo K) /\ G e. (K Homeo L))) -> (A.x e. J (F"x) e. K /\ A.y e. K (G"y) e. L))
19		hbra1 1684	. . . . . . 7 |- (A.x e. J (F"x) e. K -> A.xA.x e. J (F"x) e. K)
20		ax-17 969	. . . . . . . 8 |- (y e. K -> A.x y e. K)
21		ax-17 969	. . . . . . . 8 |- ((G"y) e. L -> A.x(G"y) e. L)
22	20, 21	hbral 1683	. . . . . . 7 |- (A.y e. K (G"y) e. L -> A.xA.y e. K (G"y) e. L)
23	19, 22	hban 1007	. . . . . 6 |- ((A.x e. J (F"x) e. K /\ A.y e. K (G"y) e. L) -> A.x(A.x e. J (F"x) e. K /\ A.y e. K (G"y) e. L))
24		df-ral 1646	. . . . . . . 8 |- (A.x e. J (F"x) e. K <-> A.x(x e. J -> (F"x) e. K))
25		pm3.35 359	. . . . . . . . . . . . . 14 |- ((x e. J /\ (x e. J -> (F"x) e. K)) -> (F"x) e. K)
26		imaeq2 3394	. . . . . . . . . . . . . . . 16 |- (y = (F"x) -> (G"y) = (G"(F"x)))
27	26	eleq1d 1537	. . . . . . . . . . . . . . 15 |- (y = (F"x) -> ((G"y) e. L <-> (G"(F"x)) e. L))
28	27	rcla4v 1869	. . . . . . . . . . . . . 14 |- ((F"x) e. K -> (A.y e. K (G"y) e. L -> (G"(F"x)) e. L))
29	25, 28	syl 10	. . . . . . . . . . . . 13 |- ((x e. J /\ (x e. J -> (F"x) e. K)) -> (A.y e. K (G"y) e. L -> (G"(F"x)) e. L))
30	29	ex 373	. . . . . . . . . . . 12 |- (x e. J -> ((x e. J -> (F"x) e. K) -> (A.y e. K (G"y) e. L -> (G"(F"x)) e. L)))
31	30	imp3a 361	. . . . . . . . . . 11 |- (x e. J -> (((x e. J -> (F"x) e. K) /\ A.y e. K (G"y) e. L) -> (G"(F"x)) e. L))
32		imaco 3493	. . . . . . . . . . . . . 14 |- ((G o. F)"x) = (G"(F"x))
33	32	eqcomi 1476	. . . . . . . . . . . . 13 |- (G"(F"x)) = ((G o. F)"x)
34	33	eleq1i 1534	. . . . . . . . . . . 12 |- ((G"(F"x)) e. L <-> ((G o. F)"x) e. L)
35	34	biimp 151	. . . . . . . . . . 11 |- ((G"(F"x)) e. L -> ((G o. F)"x) e. L)
36	31, 35	syl6com 53	. . . . . . . . . 10 |- (((x e. J -> (F"x) e. K) /\ A.y e. K (G"y) e. L) -> (x e. J -> ((G o. F)"x) e. L))
37	36	ex 373	. . . . . . . . 9 |- ((x e. J -> (F"x) e. K) -> (A.y e. K (G"y) e. L -> (x e. J -> ((G o. F)"x) e. L)))
38	37	a4s 982	. . . . . . . 8 |- (A.x(x e. J -> (F"x) e. K) -> (A.y e. K (G"y) e. L -> (x e. J -> ((G o. F)"x) e. L)))
39	24, 38	sylbi 199	. . . . . . 7 |- (A.x e. J (F"x) e. K -> (A.y e. K (G"y) e. L -> (x e. J -> ((G o. F)"x) e. L)))
40	39	imp 350	. . . . . 6 |- ((A.x e. J (F"x) e. K /\ A.y e. K (G"y) e. L) -> (x e. J -> ((G o. F)"x) e. L))
41	23, 40	r19.21ai 1709	. . . . 5 |- ((A.x e. J (F"x) e. K /\ A.y e. K (G"y) e. L) -> A.x e. J ((G o. F)"x) e. L)
42	18, 41	syl 10	. . . 4 |- (((J e. Top /\ K e. Top /\ L e. Top) /\ (F e. (J Homeo K) /\ G e. (K Homeo L))) -> A.x e. J ((G o. F)"x) e. L)
43		hmeocna 10442	. . . . . . . 8 |- ((J e. Top /\ K e. Top) -> (F e. (J Homeo K) -> A.y e. K (`'F"y) e. J))
44	43	3adant3 798	. . . . . . 7 |- ((J e. Top /\ K e. Top /\ L e. Top) -> (F e. (J Homeo K) -> A.y e. K (`'F"y) e. J))
45		hmeocna 10442	. . . . . . . 8 |- ((K e. Top /\ L e. Top) -> (G e. (K Homeo L) -> A.x e. L (`'G"x) e. K))
46	45	3adant1 796	. . . . . . 7 |- ((J e. Top /\ K e. Top /\ L e. Top) -> (G e. (K Homeo L) -> A.x e. L (`'G"x) e. K))
47	44, 46	anim12d 557	. . . . . 6 |- ((J e. Top /\ K e. Top /\ L e. Top) -> ((F e. (J Homeo K) /\ G e. (K Homeo L)) -> (A.y e. K (`'F"y) e. J /\ A.x e. L (`'G"x) e. K)))
48	47	imp 350	. . . . 5 |- (((J e. Top /\ K e. Top /\ L e. Top) /\ (F e. (J Homeo K) /\ G e. (K Homeo L))) -> (A.y e. K (`'F"y) e. J /\ A.x e. L (`'G"x) e. K))
49		ax-17 969	. . . . . . 7 |- (A.y e. K (`'F"y) e. J -> A.xA.y e. K (`'F"y) e. J)
50		hbra1 1684	. . . . . . 7 |- (A.x e. L (`'G"x) e. K -> A.xA.x e. L (`'G"x) e. K)
51	49, 50	hban 1007	. . . . . 6 |- ((A.y e. K (`'F"y) e. J /\ A.x e. L (`'G"x) e. K) -> A.x(A.y e. K (`'F"y) e. J /\ A.x e. L (`'G"x) e. K))
52		df-ral 1646	. . . . . . . 8 |- (A.x e. L (`'G"x) e. K <-> A.x(x e. L -> (`'G"x) e. K))
53		pm3.35 359	. . . . . . . . . . . . . 14 |- ((x e. L /\ (x e. L -> (`'G"x) e. K)) -> (`'G"x) e. K)
54		imaeq2 3394	. . . . . . . . . . . . . . . 16 |- (y = (`'G"x) -> (`'F"y) = (`'F"(`'G"x)))
55	54	eleq1d 1537	. . . . . . . . . . . . . . 15 |- (y = (`'G"x) -> ((`'F"y) e. J <-> (`'F"(`'G"x)) e. J))
56	55	rcla4v 1869	. . . . . . . . . . . . . 14 |- ((`'G"x) e. K -> (