Theorem txhmeo 20866

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 20823	. . . . . 6 |- ( F e. ( J Homeo L ) -> F e. ( J Cn L ) )
3	1, 2	syl 17	. . . . 5 |- ( ph -> F e. ( J Cn L ) )
4		cntop1 20304	. . . . 5 |- ( F e. ( J Cn L ) -> J e. Top )
5	3, 4	syl 17	. . . 4 |- ( ph -> J e. Top )
6		txhmeo.1	. . . . 5 |- X = U. J
7	6	toptopon 19996	. . . 4 |- ( J e. Top <-> J e. (TopOn ` X ) )
8	5, 7	sylib 201	. . 3 |- ( ph -> J e. (TopOn ` X ) )
9		txhmeo.4	. . . . . 6 |- ( ph -> G e. ( K Homeo M ) )
10		hmeocn 20823	. . . . . 6 |- ( G e. ( K Homeo M ) -> G e. ( K Cn M ) )
11	9, 10	syl 17	. . . . 5 |- ( ph -> G e. ( K Cn M ) )
12		cntop1 20304	. . . . 5 |- ( G e. ( K Cn M ) -> K e. Top )
13	11, 12	syl 17	. . . 4 |- ( ph -> K e. Top )
14		txhmeo.2	. . . . 5 |- Y = U. K
15	14	toptopon 19996	. . . 4 |- ( K e. Top <-> K e. (TopOn ` Y ) )
16	13, 15	sylib 201	. . 3 |- ( ph -> K e. (TopOn ` Y ) )
17	8, 16	cnmpt1st 20731	. . . 4 |- ( ph -> ( x e. X , y e. Y |-> x ) e. ( ( J tX K ) Cn J ) )
18	8, 16, 17, 3	cnmpt21f 20735	. . 3 |- ( ph -> ( x e. X , y e. Y |-> ( F ` x ) ) e. ( ( J tX K ) Cn L ) )
19	8, 16	cnmpt2nd 20732	. . . 4 |- ( ph -> ( x e. X , y e. Y |-> y ) e. ( ( J tX K ) Cn K ) )
20	8, 16, 19, 11	cnmpt21f 20735	. . 3 |- ( ph -> ( x e. X , y e. Y |-> ( G ` y ) ) e. ( ( J tX K ) Cn M ) )
21	8, 16, 18, 20	cnmpt2t 20736	. 2 |- ( ph -> ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Cn ( L tX M ) ) )
22		vex 3059	. . . . . . . . . . 11 |- x e. _V
23		vex 3059	. . . . . . . . . . 11 |- y e. _V
24	22, 23	op1std 6829	. . . . . . . . . 10 |- ( u = <. x , y >. -> ( 1st ` u ) = x )
25	24	fveq2d 5891	. . . . . . . . 9 |- ( u = <. x , y >. -> ( F ` ( 1st ` u ) ) = ( F ` x ) )
26	22, 23	op2ndd 6830	. . . . . . . . . 10 |- ( u = <. x , y >. -> ( 2nd ` u ) = y )
27	26	fveq2d 5891	. . . . . . . . 9 |- ( u = <. x , y >. -> ( G ` ( 2nd ` u ) ) = ( G ` y ) )
28	25, 27	opeq12d 4187	. . . . . . . 8 |- ( u = <. x , y >. -> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. = <. ( F ` x ) , ( G ` y ) >. )
29	28	mpt2mpt 6414	. . . . . . 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 2470	. . . . . 6 |- ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( u e. ( X X. Y ) |-> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. )
31		eqid 2461	. . . . . . . . . 10 |- U. L = U. L
32	6, 31	cnf 20310	. . . . . . . . 9 |- ( F e. ( J Cn L ) -> F : X --> U. L )
33	3, 32	syl 17	. . . . . . . 8 |- ( ph -> F : X --> U. L )
34		xp1st 6849	. . . . . . . 8 |- ( u e. ( X X. Y ) -> ( 1st ` u ) e. X )
35		ffvelrn 6042	. . . . . . . 8 |- ( ( F : X --> U. L /\ ( 1st ` u ) e. X ) -> ( F ` ( 1st ` u ) ) e. U. L )
36	33, 34, 35	syl2an 484	. . . . . . 7 |- ( ( ph /\ u e. ( X X. Y ) ) -> ( F ` ( 1st ` u ) ) e. U. L )
37		eqid 2461	. . . . . . . . . 10 |- U. M = U. M
38	14, 37	cnf 20310	. . . . . . . . 9 |- ( G e. ( K Cn M ) -> G : Y --> U. M )
39	11, 38	syl 17	. . . . . . . 8 |- ( ph -> G : Y --> U. M )
40		xp2nd 6850	. . . . . . . 8 |- ( u e. ( X X. Y ) -> ( 2nd ` u ) e. Y )
41		ffvelrn 6042	. . . . . . . 8 |- ( ( G : Y --> U. M /\ ( 2nd ` u ) e. Y ) -> ( G ` ( 2nd ` u ) ) e. U. M )
42	39, 40, 41	syl2an 484	. . . . . . 7 |- ( ( ph /\ u e. ( X X. Y ) ) -> ( G ` ( 2nd ` u ) ) e. U. M )
43		opelxpi 4884	. . . . . . 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 671	. . . . . 6 |- ( ( ph /\ u e. ( X X. Y ) ) -> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. e. ( U. L X. U. M ) )
45	6, 31	hmeof1o 20827	. . . . . . . . . 10 |- ( F e. ( J Homeo L ) -> F : X -1-1-onto-> U. L )
46	1, 45	syl 17	. . . . . . . . 9 |- ( ph -> F : X -1-1-onto-> U. L )
47		f1ocnv 5848	. . . . . . . . 9 |- ( F : X -1-1-onto-> U. L -> `' F : U. L -1-1-onto-> X )
48		f1of 5836	. . . . . . . . 9 |- ( `' F : U. L -1-1-onto-> X -> `' F : U. L --> X )
49	46, 47, 48	3syl 18	. . . . . . . 8 |- ( ph -> `' F : U. L --> X )
50		xp1st 6849	. . . . . . . 8 |- ( v e. ( U. L X. U. M ) -> ( 1st ` v ) e. U. L )
51		ffvelrn 6042	. . . . . . . 8 |- ( ( `' F : U. L --> X /\ ( 1st ` v ) e. U. L ) -> ( `' F ` ( 1st ` v ) ) e. X )
52	49, 50, 51	syl2an 484	. . . . . . 7 |- ( ( ph /\ v e. ( U. L X. U. M ) ) -> ( `' F ` ( 1st ` v ) ) e. X )
53	14, 37	hmeof1o 20827	. . . . . . . . . 10 |- ( G e. ( K Homeo M ) -> G : Y -1-1-onto-> U. M )
54	9, 53	syl 17	. . . . . . . . 9 |- ( ph -> G : Y -1-1-onto-> U. M )
55		f1ocnv 5848	. . . . . . . . 9 |- ( G : Y -1-1-onto-> U. M -> `' G : U. M -1-1-onto-> Y )
56		f1of 5836	. . . . . . . . 9 |- ( `' G : U. M -1-1-onto-> Y -> `' G : U. M --> Y )
57	54, 55, 56	3syl 18	. . . . . . . 8 |- ( ph -> `' G : U. M --> Y )
58		xp2nd 6850	. . . . . . . 8 |- ( v e. ( U. L X. U. M ) -> ( 2nd ` v ) e. U. M )
59		ffvelrn 6042	. . . . . . . 8 |- ( ( `' G : U. M --> Y /\ ( 2nd ` v ) e. U. M ) -> ( `' G ` ( 2nd ` v ) ) e. Y )
60	57, 58, 59	syl2an 484	. . . . . . 7 |- ( ( ph /\ v e. ( U. L X. U. M ) ) -> ( `' G ` ( 2nd ` v ) ) e. Y )
61		opelxpi 4884	. . . . . . 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 671	. . . . . 6 |- ( ( ph /\ v e. ( U. L X. U. M ) ) -> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. e. ( X X. Y ) )
63	46	adantr 471	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> F : X -1-1-onto-> U. L )
64	34	ad2antrl 739	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 1st ` u ) e. X )
65	50	ad2antll 740	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 1st ` v ) e. U. L )
66		f1ocnvfvb 6202	. . . . . . . . . 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 1276	. . . . . . . . 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 2468	. . . . . . . . 9 |- ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) <-> ( F ` ( 1st ` u ) ) = ( 1st ` v ) )
69		eqcom 2468	. . . . . . . . 9 |- ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) <-> ( `' F ` ( 1st ` v ) ) = ( 1st ` u ) )
70	67, 68, 69	3bitr4g 296	. . . . . . . 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 471	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> G : Y -1-1-onto-> U. M )
72	40	ad2antrl 739	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 2nd ` u ) e. Y )
73	58	ad2antll 740	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 2nd ` v ) e. U. M )
74		f1ocnvfvb 6202	. . . . . . . . . 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 1276	. . . . . . . . 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 2468	. . . . . . . . 9 |- ( ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) <-> ( G ` ( 2nd ` u ) ) = ( 2nd ` v ) )
77		eqcom 2468	. . . . . . . . 9 |- ( ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) <-> ( `' G ` ( 2nd ` v ) ) = ( 2nd ` u ) )
78	75, 76, 77	3bitr4g 296	. . . . . . . 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 722	. . . . . . 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 6859	. . . . . . . 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 740	. . . . . . 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 6859	. . . . . . . 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 739	. . . . . . 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 294	. . . . . 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 6546	. . . . 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 469	. . . 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 3059	. . . . . . . 8 |- z e. _V
88		vex 3059	. . . . . . . 8 |- w e. _V
89	87, 88	op1std 6829	. . . . . . 7 |- ( v = <. z , w >. -> ( 1st ` v ) = z )
90	89	fveq2d 5891	. . . . . 6 |- ( v = <. z , w >. -> ( `' F ` ( 1st ` v ) ) = ( `' F ` z ) )
91	87, 88	op2ndd 6830	. . . . . . 7 |- ( v = <. z , w >. -> ( 2nd ` v ) = w )
92	91	fveq2d 5891	. . . . . 6 |- ( v = <. z , w >. -> ( `' G ` ( 2nd ` v ) ) = ( `' G ` w ) )
93	90, 92	opeq12d 4187	. . . . 5 |- ( v = <. z , w >. -> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. = <. ( `' F ` z ) , ( `' G ` w ) >. )
94	93	mpt2mpt 6414	. . . 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 2511	. . 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 20305	. . . . . 6 |- ( F e. ( J Cn L ) -> L e. Top )
97	3, 96	syl 17	. . . . 5 |- ( ph -> L e. Top )
98	31	toptopon 19996	. . . . 5 |- ( L e. Top <-> L e. (TopOn ` U. L ) )
99	97, 98	sylib 201	. . . 4 |- ( ph -> L e. (TopOn ` U. L ) )
100		cntop2 20305	. . . . . 6 |- ( G e. ( K Cn M ) -> M e. Top )
101	11, 100	syl 17	. . . . 5 |- ( ph -> M e. Top )
102	37	toptopon 19996	. . . . 5 |- ( M e. Top <-> M e. (TopOn ` U. M ) )
103	101, 102	sylib 201	. . . 4 |- ( ph -> M e. (TopOn ` U. M ) )
104	99, 103	cnmpt1st 20731	. . . . 5 |- ( ph -> ( z e. U. L , w e. U. M |-> z ) e. ( ( L tX M ) Cn L ) )
105		hmeocnvcn 20824	. . . . . 6 |- ( F e. ( J Homeo L ) -> `' F e. ( L Cn J ) )
106	1, 105	syl 17	. . . . 5 |- ( ph -> `' F e. ( L Cn J ) )
107	99, 103, 104, 106	cnmpt21f 20735	. . . 4 |- ( ph -> ( z e. U. L , w e. U. M |-> ( `' F ` z ) ) e. ( ( L tX M ) Cn J ) )
108	99, 103	cnmpt2nd 20732	. . . . 5 |- ( ph -> ( z e. U. L , w e. U. M |-> w ) e. ( ( L tX M ) Cn M ) )
109		hmeocnvcn 20824	. . . . . 6 |- ( G e. ( K Homeo M ) -> `' G e. ( M Cn K ) )
110	9, 109	syl 17	. . . . 5 |- ( ph -> `' G e. ( M Cn K ) )
111	99, 103, 108, 110	cnmpt21f 20735	. . . 4 |- ( ph -> ( z e. U. L , w e. U. M |-> ( `' G ` w ) ) e. ( ( L tX M ) Cn K ) )
112	99, 103, 107, 111	cnmpt2t 20736	. . 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 2539	. 2 |- ( ph -> `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( L tX M ) Cn ( J tX K ) ) )
114		ishmeo 20822	. 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 675	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 189   /\ wa 375   = wceq 1454   e. wcel 1897   <.cop 3985   U.cuni 4211   |-> cmpt 4474   X. cxp 4850   `'ccnv 4851   -->wf 5596   -1-1-onto->wf1o 5599   ` cfv 5600  (class class class)co 6314   |-> cmpt2 6316   1stc1st 6817   2ndc2nd 6818   Topctop 19965  TopOnctopon 19966   Cn ccn 20288   tX ctx 20623   Homeochmeo 20816

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-1st 6819  df-2nd 6820  df-map 7499  df-topgen 15390  df-top 19969  df-bases 19970  df-topon 19971  df-cn 20291  df-tx 20625  df-hmeo 20818

This theorem is referenced by:  xpstopnlem1  20872