Theorem txhmeo 19503

Description: Lift a pair of homeomorphisms on the factors to a homeomorphism of product topologies. (Contributed by Mario Carneiro, 2-Sep-2015.)

Hypotheses

Ref	Expression
txhmeo.1	|- X = U. J
txhmeo.2	|- Y = U. K
txhmeo.3	|- ( ph -> F e. ( J Homeo L ) )
txhmeo.4	|- ( ph -> G e. ( K Homeo M ) )

Assertion

Ref	Expression
txhmeo	|- ( ph -> ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Homeo ( L tX M ) ) )

Distinct variable groups:   x, y, F   x, J, y   x, K, y   ph, x, y   x, G, y   x, L, y   x, X, y   x, Y, y   x, M, y

Proof of Theorem txhmeo

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

Step	Hyp	Ref	Expression
1		txhmeo.3	. . . . . 6 |- ( ph -> F e. ( J Homeo L ) )
2		hmeocn 19460	. . . . . 6 |- ( F e. ( J Homeo L ) -> F e. ( J Cn L ) )
3	1, 2	syl 16	. . . . 5 |- ( ph -> F e. ( J Cn L ) )
4		cntop1 18971	. . . . 5 |- ( F e. ( J Cn L ) -> J e. Top )
5	3, 4	syl 16	. . . 4 |- ( ph -> J e. Top )
6		txhmeo.1	. . . . 5 |- X = U. J
7	6	toptopon 18665	. . . 4 |- ( J e. Top <-> J e. (TopOn ` X ) )
8	5, 7	sylib 196	. . 3 |- ( ph -> J e. (TopOn ` X ) )
9		txhmeo.4	. . . . . 6 |- ( ph -> G e. ( K Homeo M ) )
10		hmeocn 19460	. . . . . 6 |- ( G e. ( K Homeo M ) -> G e. ( K Cn M ) )
11	9, 10	syl 16	. . . . 5 |- ( ph -> G e. ( K Cn M ) )
12		cntop1 18971	. . . . 5 |- ( G e. ( K Cn M ) -> K e. Top )
13	11, 12	syl 16	. . . 4 |- ( ph -> K e. Top )
14		txhmeo.2	. . . . 5 |- Y = U. K
15	14	toptopon 18665	. . . 4 |- ( K e. Top <-> K e. (TopOn ` Y ) )
16	13, 15	sylib 196	. . 3 |- ( ph -> K e. (TopOn ` Y ) )
17	8, 16	cnmpt1st 19368	. . . 4 |- ( ph -> ( x e. X , y e. Y |-> x ) e. ( ( J tX K ) Cn J ) )
18	8, 16, 17, 3	cnmpt21f 19372	. . 3 |- ( ph -> ( x e. X , y e. Y |-> ( F ` x ) ) e. ( ( J tX K ) Cn L ) )
19	8, 16	cnmpt2nd 19369	. . . 4 |- ( ph -> ( x e. X , y e. Y |-> y ) e. ( ( J tX K ) Cn K ) )
20	8, 16, 19, 11	cnmpt21f 19372	. . 3 |- ( ph -> ( x e. X , y e. Y |-> ( G ` y ) ) e. ( ( J tX K ) Cn M ) )
21	8, 16, 18, 20	cnmpt2t 19373	. 2 |- ( ph -> ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Cn ( L tX M ) ) )
22		vex 3075	. . . . . . . . . . 11 |- x e. _V
23		vex 3075	. . . . . . . . . . 11 |- y e. _V
24	22, 23	op1std 6692	. . . . . . . . . 10 |- ( u = <. x , y >. -> ( 1st ` u ) = x )
25	24	fveq2d 5798	. . . . . . . . 9 |- ( u = <. x , y >. -> ( F ` ( 1st ` u ) ) = ( F ` x ) )
26	22, 23	op2ndd 6693	. . . . . . . . . 10 |- ( u = <. x , y >. -> ( 2nd ` u ) = y )
27	26	fveq2d 5798	. . . . . . . . 9 |- ( u = <. x , y >. -> ( G ` ( 2nd ` u ) ) = ( G ` y ) )
28	25, 27	opeq12d 4170	. . . . . . . 8 |- ( u = <. x , y >. -> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. = <. ( F ` x ) , ( G ` y ) >. )
29	28	mpt2mpt 6287	. . . . . . 7 |- ( u e. ( X X. Y ) |-> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. ) = ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. )
30	29	eqcomi 2465	. . . . . 6 |- ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( u e. ( X X. Y ) |-> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. )
31		eqid 2452	. . . . . . . . . 10 |- U. L = U. L
32	6, 31	cnf 18977	. . . . . . . . 9 |- ( F e. ( J Cn L ) -> F : X --> U. L )
33	3, 32	syl 16	. . . . . . . 8 |- ( ph -> F : X --> U. L )
34		xp1st 6711	. . . . . . . 8 |- ( u e. ( X X. Y ) -> ( 1st ` u ) e. X )
35		ffvelrn 5945	. . . . . . . 8 |- ( ( F : X --> U. L /\ ( 1st ` u ) e. X ) -> ( F ` ( 1st ` u ) ) e. U. L )
36	33, 34, 35	syl2an 477	. . . . . . 7 |- ( ( ph /\ u e. ( X X. Y ) ) -> ( F ` ( 1st ` u ) ) e. U. L )
37		eqid 2452	. . . . . . . . . 10 |- U. M = U. M
38	14, 37	cnf 18977	. . . . . . . . 9 |- ( G e. ( K Cn M ) -> G : Y --> U. M )
39	11, 38	syl 16	. . . . . . . 8 |- ( ph -> G : Y --> U. M )
40		xp2nd 6712	. . . . . . . 8 |- ( u e. ( X X. Y ) -> ( 2nd ` u ) e. Y )
41		ffvelrn 5945	. . . . . . . 8 |- ( ( G : Y --> U. M /\ ( 2nd ` u ) e. Y ) -> ( G ` ( 2nd ` u ) ) e. U. M )
42	39, 40, 41	syl2an 477	. . . . . . 7 |- ( ( ph /\ u e. ( X X. Y ) ) -> ( G ` ( 2nd ` u ) ) e. U. M )
43		opelxpi 4974	. . . . . . 7 |- ( ( ( F ` ( 1st ` u ) ) e. U. L /\ ( G ` ( 2nd ` u ) ) e. U. M ) -> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. e. ( U. L X. U. M ) )
44	36, 42, 43	syl2anc 661	. . . . . 6 |- ( ( ph /\ u e. ( X X. Y ) ) -> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. e. ( U. L X. U. M ) )
45	6, 31	hmeof1o 19464	. . . . . . . . . 10 |- ( F e. ( J Homeo L ) -> F : X -1-1-onto-> U. L )
46	1, 45	syl 16	. . . . . . . . 9 |- ( ph -> F : X -1-1-onto-> U. L )
47		f1ocnv 5756	. . . . . . . . 9 |- ( F : X -1-1-onto-> U. L -> `' F : U. L -1-1-onto-> X )
48		f1of 5744	. . . . . . . . 9 |- ( `' F : U. L -1-1-onto-> X -> `' F : U. L --> X )
49	46, 47, 48	3syl 20	. . . . . . . 8 |- ( ph -> `' F : U. L --> X )
50		xp1st 6711	. . . . . . . 8 |- ( v e. ( U. L X. U. M ) -> ( 1st ` v ) e. U. L )
51		ffvelrn 5945	. . . . . . . 8 |- ( ( `' F : U. L --> X /\ ( 1st ` v ) e. U. L ) -> ( `' F ` ( 1st ` v ) ) e. X )
52	49, 50, 51	syl2an 477	. . . . . . 7 |- ( ( ph /\ v e. ( U. L X. U. M ) ) -> ( `' F ` ( 1st ` v ) ) e. X )
53	14, 37	hmeof1o 19464	. . . . . . . . . 10 |- ( G e. ( K Homeo M ) -> G : Y -1-1-onto-> U. M )
54	9, 53	syl 16	. . . . . . . . 9 |- ( ph -> G : Y -1-1-onto-> U. M )
55		f1ocnv 5756	. . . . . . . . 9 |- ( G : Y -1-1-onto-> U. M -> `' G : U. M -1-1-onto-> Y )
56		f1of 5744	. . . . . . . . 9 |- ( `' G : U. M -1-1-onto-> Y -> `' G : U. M --> Y )
57	54, 55, 56	3syl 20	. . . . . . . 8 |- ( ph -> `' G : U. M --> Y )
58		xp2nd 6712	. . . . . . . 8 |- ( v e. ( U. L X. U. M ) -> ( 2nd ` v ) e. U. M )
59		ffvelrn 5945	. . . . . . . 8 |- ( ( `' G : U. M --> Y /\ ( 2nd ` v ) e. U. M ) -> ( `' G ` ( 2nd ` v ) ) e. Y )
60	57, 58, 59	syl2an 477	. . . . . . 7 |- ( ( ph /\ v e. ( U. L X. U. M ) ) -> ( `' G ` ( 2nd ` v ) ) e. Y )
61		opelxpi 4974	. . . . . . 7 |- ( ( ( `' F ` ( 1st ` v ) ) e. X /\ ( `' G ` ( 2nd ` v ) ) e. Y ) -> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. e. ( X X. Y ) )
62	52, 60, 61	syl2anc 661	. . . . . 6 |- ( ( ph /\ v e. ( U. L X. U. M ) ) -> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. e. ( X X. Y ) )
63	46	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> F : X -1-1-onto-> U. L )
64	34	ad2antrl 727	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 1st ` u ) e. X )
65	50	ad2antll 728	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 1st ` v ) e. U. L )
66		f1ocnvfvb 6090	. . . . . . . . . 10 |- ( ( F : X -1-1-onto-> U. L /\ ( 1st ` u ) e. X /\ ( 1st ` v ) e. U. L ) -> ( ( F ` ( 1st ` u ) ) = ( 1st ` v ) <-> ( `' F ` ( 1st ` v ) ) = ( 1st ` u ) ) )
67	63, 64, 65, 66	syl3anc 1219	. . . . . . . . 9 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( F ` ( 1st ` u ) ) = ( 1st ` v ) <-> ( `' F ` ( 1st ` v ) ) = ( 1st ` u ) ) )
68		eqcom 2461	. . . . . . . . 9 |- ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) <-> ( F ` ( 1st ` u ) ) = ( 1st ` v ) )
69		eqcom 2461	. . . . . . . . 9 |- ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) <-> ( `' F ` ( 1st ` v ) ) = ( 1st ` u ) )
70	67, 68, 69	3bitr4g 288	. . . . . . . 8 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) <-> ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) ) )
71	54	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> G : Y -1-1-onto-> U. M )
72	40	ad2antrl 727	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 2nd ` u ) e. Y )
73	58	ad2antll 728	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 2nd ` v ) e. U. M )
74		f1ocnvfvb 6090	. . . . . . . . . 10 |- ( ( G : Y -1-1-onto-> U. M /\ ( 2nd ` u ) e. Y /\ ( 2nd ` v ) e. U. M ) -> ( ( G ` ( 2nd ` u ) ) = ( 2nd ` v ) <-> ( `' G ` ( 2nd ` v ) ) = ( 2nd ` u ) ) )
75	71, 72, 73, 74	syl3anc 1219	. . . . . . . . 9 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( G ` ( 2nd ` u ) ) = ( 2nd ` v ) <-> ( `' G ` ( 2nd ` v ) ) = ( 2nd ` u ) ) )
76		eqcom 2461	. . . . . . . . 9 |- ( ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) <-> ( G ` ( 2nd ` u ) ) = ( 2nd ` v ) )
77		eqcom 2461	. . . . . . . . 9 |- ( ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) <-> ( `' G ` ( 2nd ` v ) ) = ( 2nd ` u ) )
78	75, 76, 77	3bitr4g 288	. . . . . . . 8 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) <-> ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) ) )
79	70, 78	anbi12d 710	. . . . . . 7 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) /\ ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) ) <-> ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) /\ ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) ) ) )
80		eqop 6721	. . . . . . . 8 |- ( v e. ( U. L X. U. M ) -> ( v = <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. <-> ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) /\ ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) ) ) )
81	80	ad2antll 728	. . . . . . 7 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( v = <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. <-> ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) /\ ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) ) ) )
82		eqop 6721	. . . . . . . 8 |- ( u e. ( X X. Y ) -> ( u = <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. <-> ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) /\ ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) ) ) )
83	82	ad2antrl 727	. . . . . . 7 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( u = <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. <-> ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) /\ ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) ) ) )
84	79, 81, 83	3bitr4rd 286	. . . . . 6 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( u = <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. <-> v = <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. ) )
85	30, 44, 62, 84	f1ocnv2d 6416	. . . . 5 |- ( ph -> ( ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) : ( X X. Y ) -1-1-onto-> ( U. L X. U. M ) /\ `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( v e. ( U. L X. U. M ) |-> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. ) ) )
86	85	simprd 463	. . . 4 |- ( ph -> `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( v e. ( U. L X. U. M ) |-> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. ) )
87		vex 3075	. . . . . . . 8 |- z e. _V
88		vex 3075	. . . . . . . 8 |- w e. _V
89	87, 88	op1std 6692	. . . . . . 7 |- ( v = <. z , w >. -> ( 1st ` v ) = z )
90	89	fveq2d 5798	. . . . . 6 |- ( v = <. z , w >. -> ( `' F ` ( 1st ` v ) ) = ( `' F ` z ) )
91	87, 88	op2ndd 6693	. . . . . . 7 |- ( v = <. z , w >. -> ( 2nd ` v ) = w )
92	91	fveq2d 5798	. . . . . 6 |- ( v = <. z , w >. -> ( `' G ` ( 2nd ` v ) ) = ( `' G ` w ) )
93	90, 92	opeq12d 4170	. . . . 5 |- ( v = <. z , w >. -> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. = <. ( `' F ` z ) , ( `' G ` w ) >. )
94	93	mpt2mpt 6287	. . . 4 |- ( v e. ( U. L X. U. M ) |-> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. ) = ( z e. U. L , w e. U. M |-> <. ( `' F ` z ) , ( `' G ` w ) >. )
95	86, 94	syl6eq 2509	. . 3 |- ( ph -> `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( z e. U. L , w e. U. M |-> <. ( `' F ` z ) , ( `' G ` w ) >. ) )
96		cntop2 18972	. . . . . 6 |- ( F e. ( J Cn L ) -> L e. Top )
97	3, 96	syl 16	. . . . 5 |- ( ph -> L e. Top )
98	31	toptopon 18665	. . . . 5 |- ( L e. Top <-> L e. (TopOn ` U. L ) )
99	97, 98	sylib 196	. . . 4 |- ( ph -> L e. (TopOn ` U. L ) )
100		cntop2 18972	. . . . . 6 |- ( G e. ( K Cn M ) -> M e. Top )
101	11, 100	syl 16	. . . . 5 |- ( ph -> M e. Top )
102	37	toptopon 18665	. . . . 5 |- ( M e. Top <-> M e. (TopOn ` U. M ) )
103	101, 102	sylib 196	. . . 4 |- ( ph -> M e. (TopOn ` U. M ) )
104	99, 103	cnmpt1st 19368	. . . . 5 |- ( ph -> ( z e. U. L , w e. U. M |-> z ) e. ( ( L tX M ) Cn L ) )
105		hmeocnvcn 19461	. . . . . 6 |- ( F e. ( J Homeo L ) -> `' F e. ( L Cn J ) )
106	1, 105	syl 16	. . . . 5 |- ( ph -> `' F e. ( L Cn J ) )
107	99, 103, 104, 106	cnmpt21f 19372	. . . 4 |- ( ph -> ( z e. U. L , w e. U. M |-> ( `' F ` z ) ) e. ( ( L tX M ) Cn J ) )
108	99, 103	cnmpt2nd 19369	. . . . 5 |- ( ph -> ( z e. U. L , w e. U. M |-> w ) e. ( ( L tX M ) Cn M ) )
109		hmeocnvcn 19461	. . . . . 6 |- ( G e. ( K Homeo M ) -> `' G e. ( M Cn K ) )
110	9, 109	syl 16	. . . . 5 |- ( ph -> `' G e. ( M Cn K ) )
111	99, 103, 108, 110	cnmpt21f 19372	. . . 4 |- ( ph -> ( z e. U. L , w e. U. M |-> ( `' G ` w ) ) e. ( ( L tX M ) Cn K ) )
112	99, 103, 107, 111	cnmpt2t 19373	. . 3 |- ( ph -> ( z e. U. L , w e. U. M |-> <. ( `' F ` z ) , ( `' G ` w ) >. ) e. ( ( L tX M ) Cn ( J tX K ) ) )
113	95, 112	eqeltrd 2540	. 2 |- ( ph -> `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( L tX M ) Cn ( J tX K ) ) )
114		ishmeo 19459	. 2 |- ( ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Homeo ( L tX M ) ) <-> ( ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Cn ( L tX M ) ) /\ `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( L tX M ) Cn ( J tX K ) ) ) )
115	21, 113, 114	sylanbrc 664	1 |- ( ph -> ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Homeo ( L tX M ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1370   e. wcel 1758   <.cop 3986   U.cuni 4194   |-> cmpt 4453   X. cxp 4941   `'ccnv 4942   -->wf 5517   -1-1-onto->wf1o 5520   ` cfv 5521  (class class class)co 6195   |-> cmpt2 6197   1stc1st 6680   2ndc2nd 6681   Topctop 18625  TopOnctopon 18626   Cn ccn 18955   tX ctx 19260   Homeochmeo 19453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431  ax-sep 4516  ax-nul 4524  ax-pow 4573  ax-pr 4634  ax-un 6477

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2265  df-mo 2266  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-ne 2647  df-ral 2801  df-rex 2802  df-rab 2805  df-v 3074  df-sbc 3289  df-csb 3391  df-dif 3434  df-un 3436  df-in 3438  df-ss 3445  df-nul 3741  df-if 3895  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4195  df-iun 4276  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4739  df-xp 4949  df-rel 4950  df-cnv 4951  df-co 4952  df-dm 4953  df-rn 4954  df-res 4955  df-ima 4956  df-iota 5484  df-fun 5523  df-fn 5524  df-f 5525  df-f1 5526  df-fo 5527  df-f1o 5528  df-fv 5529  df-ov 6198  df-oprab 6199  df-mpt2 6200  df-1st 6682  df-2nd 6683  df-map 7321  df-topgen 14496  df-top 18630  df-bases 18632  df-topon 18633  df-cn 18958  df-tx 19262  df-hmeo 19455

This theorem is referenced by:  xpstopnlem1  19509