Theorem txhmeo 15033

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 15019	. . . . . 6 |- ( F e. ( J Homeo L ) -> F e. ( J Cn L ) )
3	1, 2	syl 14	. . . . 5 |- ( ph -> F e. ( J Cn L ) )
4		cntop1 14915	. . . . 5 |- ( F e. ( J Cn L ) -> J e. Top )
5	3, 4	syl 14	. . . 4 |- ( ph -> J e. Top )
6		txhmeo.1	. . . . 5 |- X = U. J
7	6	toptopon 14732	. . . 4 |- ( J e. Top <-> J e. (TopOn ` X ) )
8	5, 7	sylib 122	. . 3 |- ( ph -> J e. (TopOn ` X ) )
9		txhmeo.4	. . . . . 6 |- ( ph -> G e. ( K Homeo M ) )
10		hmeocn 15019	. . . . . 6 |- ( G e. ( K Homeo M ) -> G e. ( K Cn M ) )
11	9, 10	syl 14	. . . . 5 |- ( ph -> G e. ( K Cn M ) )
12		cntop1 14915	. . . . 5 |- ( G e. ( K Cn M ) -> K e. Top )
13	11, 12	syl 14	. . . 4 |- ( ph -> K e. Top )
14		txhmeo.2	. . . . 5 |- Y = U. K
15	14	toptopon 14732	. . . 4 |- ( K e. Top <-> K e. (TopOn ` Y ) )
16	13, 15	sylib 122	. . 3 |- ( ph -> K e. (TopOn ` Y ) )
17	8, 16	cnmpt1st 15002	. . . 4 |- ( ph -> ( x e. X , y e. Y |-> x ) e. ( ( J tX K ) Cn J ) )
18	8, 16, 17, 3	cnmpt21f 15006	. . 3 |- ( ph -> ( x e. X , y e. Y |-> ( F ` x ) ) e. ( ( J tX K ) Cn L ) )
19	8, 16	cnmpt2nd 15003	. . . 4 |- ( ph -> ( x e. X , y e. Y |-> y ) e. ( ( J tX K ) Cn K ) )
20	8, 16, 19, 11	cnmpt21f 15006	. . 3 |- ( ph -> ( x e. X , y e. Y |-> ( G ` y ) ) e. ( ( J tX K ) Cn M ) )
21	8, 16, 18, 20	cnmpt2t 15007	. 2 |- ( ph -> ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Cn ( L tX M ) ) )
22		vex 2803	. . . . . . . . . . 11 |- x e. _V
23		vex 2803	. . . . . . . . . . 11 |- y e. _V
24	22, 23	op1std 6306	. . . . . . . . . 10 |- ( u = <. x , y >. -> ( 1st ` u ) = x )
25	24	fveq2d 5639	. . . . . . . . 9 |- ( u = <. x , y >. -> ( F ` ( 1st ` u ) ) = ( F ` x ) )
26	22, 23	op2ndd 6307	. . . . . . . . . 10 |- ( u = <. x , y >. -> ( 2nd ` u ) = y )
27	26	fveq2d 5639	. . . . . . . . 9 |- ( u = <. x , y >. -> ( G ` ( 2nd ` u ) ) = ( G ` y ) )
28	25, 27	opeq12d 3868	. . . . . . . 8 |- ( u = <. x , y >. -> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. = <. ( F ` x ) , ( G ` y ) >. )
29	28	mpompt 6108	. . . . . . 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 2233	. . . . . 6 |- ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( u e. ( X X. Y ) |-> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. )
31		eqid 2229	. . . . . . . . . 10 |- U. L = U. L
32	6, 31	cnf 14918	. . . . . . . . 9 |- ( F e. ( J Cn L ) -> F : X --> U. L )
33	3, 32	syl 14	. . . . . . . 8 |- ( ph -> F : X --> U. L )
34		xp1st 6323	. . . . . . . 8 |- ( u e. ( X X. Y ) -> ( 1st ` u ) e. X )
35		ffvelcdm 5776	. . . . . . . 8 |- ( ( F : X --> U. L /\ ( 1st ` u ) e. X ) -> ( F ` ( 1st ` u ) ) e. U. L )
36	33, 34, 35	syl2an 289	. . . . . . 7 |- ( ( ph /\ u e. ( X X. Y ) ) -> ( F ` ( 1st ` u ) ) e. U. L )
37		eqid 2229	. . . . . . . . . 10 |- U. M = U. M
38	14, 37	cnf 14918	. . . . . . . . 9 |- ( G e. ( K Cn M ) -> G : Y --> U. M )
39	11, 38	syl 14	. . . . . . . 8 |- ( ph -> G : Y --> U. M )
40		xp2nd 6324	. . . . . . . 8 |- ( u e. ( X X. Y ) -> ( 2nd ` u ) e. Y )
41		ffvelcdm 5776	. . . . . . . 8 |- ( ( G : Y --> U. M /\ ( 2nd ` u ) e. Y ) -> ( G ` ( 2nd ` u ) ) e. U. M )
42	39, 40, 41	syl2an 289	. . . . . . 7 |- ( ( ph /\ u e. ( X X. Y ) ) -> ( G ` ( 2nd ` u ) ) e. U. M )
43	36, 42	opelxpd 4756	. . . . . 6 |- ( ( ph /\ u e. ( X X. Y ) ) -> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. e. ( U. L X. U. M ) )
44	6, 31	hmeof1o 15023	. . . . . . . . . 10 |- ( F e. ( J Homeo L ) -> F : X -1-1-onto-> U. L )
45	1, 44	syl 14	. . . . . . . . 9 |- ( ph -> F : X -1-1-onto-> U. L )
46		f1ocnv 5593	. . . . . . . . 9 |- ( F : X -1-1-onto-> U. L -> `' F : U. L -1-1-onto-> X )
47		f1of 5580	. . . . . . . . 9 |- ( `' F : U. L -1-1-onto-> X -> `' F : U. L --> X )
48	45, 46, 47	3syl 17	. . . . . . . 8 |- ( ph -> `' F : U. L --> X )
49		xp1st 6323	. . . . . . . 8 |- ( v e. ( U. L X. U. M ) -> ( 1st ` v ) e. U. L )
50		ffvelcdm 5776	. . . . . . . 8 |- ( ( `' F : U. L --> X /\ ( 1st ` v ) e. U. L ) -> ( `' F ` ( 1st ` v ) ) e. X )
51	48, 49, 50	syl2an 289	. . . . . . 7 |- ( ( ph /\ v e. ( U. L X. U. M ) ) -> ( `' F ` ( 1st ` v ) ) e. X )
52	14, 37	hmeof1o 15023	. . . . . . . . . 10 |- ( G e. ( K Homeo M ) -> G : Y -1-1-onto-> U. M )
53	9, 52	syl 14	. . . . . . . . 9 |- ( ph -> G : Y -1-1-onto-> U. M )
54		f1ocnv 5593	. . . . . . . . 9 |- ( G : Y -1-1-onto-> U. M -> `' G : U. M -1-1-onto-> Y )
55		f1of 5580	. . . . . . . . 9 |- ( `' G : U. M -1-1-onto-> Y -> `' G : U. M --> Y )
56	53, 54, 55	3syl 17	. . . . . . . 8 |- ( ph -> `' G : U. M --> Y )
57		xp2nd 6324	. . . . . . . 8 |- ( v e. ( U. L X. U. M ) -> ( 2nd ` v ) e. U. M )
58		ffvelcdm 5776	. . . . . . . 8 |- ( ( `' G : U. M --> Y /\ ( 2nd ` v ) e. U. M ) -> ( `' G ` ( 2nd ` v ) ) e. Y )
59	56, 57, 58	syl2an 289	. . . . . . 7 |- ( ( ph /\ v e. ( U. L X. U. M ) ) -> ( `' G ` ( 2nd ` v ) ) e. Y )
60	51, 59	opelxpd 4756	. . . . . 6 |- ( ( ph /\ v e. ( U. L X. U. M ) ) -> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. e. ( X X. Y ) )
61	45	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> F : X -1-1-onto-> U. L )
62	34	ad2antrl 490	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 1st ` u ) e. X )
63	49	ad2antll 491	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 1st ` v ) e. U. L )
64		f1ocnvfvb 5916	. . . . . . . . . 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 ) ) )
65	61, 62, 63, 64	syl3anc 1271	. . . . . . . . 9 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( F ` ( 1st ` u ) ) = ( 1st ` v ) <-> ( `' F ` ( 1st ` v ) ) = ( 1st ` u ) ) )
66		eqcom 2231	. . . . . . . . 9 |- ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) <-> ( F ` ( 1st ` u ) ) = ( 1st ` v ) )
67		eqcom 2231	. . . . . . . . 9 |- ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) <-> ( `' F ` ( 1st ` v ) ) = ( 1st ` u ) )
68	65, 66, 67	3bitr4g 223	. . . . . . . 8 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) <-> ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) ) )
69	53	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> G : Y -1-1-onto-> U. M )
70	40	ad2antrl 490	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 2nd ` u ) e. Y )
71	57	ad2antll 491	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 2nd ` v ) e. U. M )
72		f1ocnvfvb 5916	. . . . . . . . . 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 ) ) )
73	69, 70, 71, 72	syl3anc 1271	. . . . . . . . 9 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( G ` ( 2nd ` u ) ) = ( 2nd ` v ) <-> ( `' G ` ( 2nd ` v ) ) = ( 2nd ` u ) ) )
74		eqcom 2231	. . . . . . . . 9 |- ( ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) <-> ( G ` ( 2nd ` u ) ) = ( 2nd ` v ) )
75		eqcom 2231	. . . . . . . . 9 |- ( ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) <-> ( `' G ` ( 2nd ` v ) ) = ( 2nd ` u ) )
76	73, 74, 75	3bitr4g 223	. . . . . . . 8 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) <-> ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) ) )
77	68, 76	anbi12d 473	. . . . . . 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 ) ) ) ) )
78		eqop 6335	. . . . . . . 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 ) ) ) ) )
79	78	ad2antll 491	. . . . . . 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 ) ) ) ) )
80		eqop 6335	. . . . . . . 8 |- ( u e. ( X X. Y ) -> ( u = <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. <-> ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) /\ ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) ) ) )
81	80	ad2antrl 490	. . . . . . 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 ) ) ) ) )
82	77, 79, 81	3bitr4rd 221	. . . . . 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 ) ) >. ) )
83	30, 43, 60, 82	f1ocnv2d 6222	. . . . 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 ) ) >. ) ) )
84	83	simprd 114	. . . 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 ) ) >. ) )
85		vex 2803	. . . . . . . 8 |- z e. _V
86		vex 2803	. . . . . . . 8 |- w e. _V
87	85, 86	op1std 6306	. . . . . . 7 |- ( v = <. z , w >. -> ( 1st ` v ) = z )
88	87	fveq2d 5639	. . . . . 6 |- ( v = <. z , w >. -> ( `' F ` ( 1st ` v ) ) = ( `' F ` z ) )
89	85, 86	op2ndd 6307	. . . . . . 7 |- ( v = <. z , w >. -> ( 2nd ` v ) = w )
90	89	fveq2d 5639	. . . . . 6 |- ( v = <. z , w >. -> ( `' G ` ( 2nd ` v ) ) = ( `' G ` w ) )
91	88, 90	opeq12d 3868	. . . . 5 |- ( v = <. z , w >. -> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. = <. ( `' F ` z ) , ( `' G ` w ) >. )
92	91	mpompt 6108	. . . 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 ) >. )
93	84, 92	eqtrdi 2278	. . 3 |- ( ph -> `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( z e. U. L , w e. U. M |-> <. ( `' F ` z ) , ( `' G ` w ) >. ) )
94		cntop2 14916	. . . . . 6 |- ( F e. ( J Cn L ) -> L e. Top )
95	3, 94	syl 14	. . . . 5 |- ( ph -> L e. Top )
96	31	toptopon 14732	. . . . 5 |- ( L e. Top <-> L e. (TopOn ` U. L ) )
97	95, 96	sylib 122	. . . 4 |- ( ph -> L e. (TopOn ` U. L ) )
98		cntop2 14916	. . . . . 6 |- ( G e. ( K Cn M ) -> M e. Top )
99	11, 98	syl 14	. . . . 5 |- ( ph -> M e. Top )
100	37	toptopon 14732	. . . . 5 |- ( M e. Top <-> M e. (TopOn ` U. M ) )
101	99, 100	sylib 122	. . . 4 |- ( ph -> M e. (TopOn ` U. M ) )
102	97, 101	cnmpt1st 15002	. . . . 5 |- ( ph -> ( z e. U. L , w e. U. M |-> z ) e. ( ( L tX M ) Cn L ) )
103		hmeocnvcn 15020	. . . . . 6 |- ( F e. ( J Homeo L ) -> `' F e. ( L Cn J ) )
104	1, 103	syl 14	. . . . 5 |- ( ph -> `' F e. ( L Cn J ) )
105	97, 101, 102, 104	cnmpt21f 15006	. . . 4 |- ( ph -> ( z e. U. L , w e. U. M |-> ( `' F ` z ) ) e. ( ( L tX M ) Cn J ) )
106	97, 101	cnmpt2nd 15003	. . . . 5 |- ( ph -> ( z e. U. L , w e. U. M |-> w ) e. ( ( L tX M ) Cn M ) )
107		hmeocnvcn 15020	. . . . . 6 |- ( G e. ( K Homeo M ) -> `' G e. ( M Cn K ) )
108	9, 107	syl 14	. . . . 5 |- ( ph -> `' G e. ( M Cn K ) )
109	97, 101, 106, 108	cnmpt21f 15006	. . . 4 |- ( ph -> ( z e. U. L , w e. U. M |-> ( `' G ` w ) ) e. ( ( L tX M ) Cn K ) )
110	97, 101, 105, 109	cnmpt2t 15007	. . 3 |- ( ph -> ( z e. U. L , w e. U. M |-> <. ( `' F ` z ) , ( `' G ` w ) >. ) e. ( ( L tX M ) Cn ( J tX K ) ) )
111	93, 110	eqeltrd 2306	. 2 |- ( ph -> `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( L tX M ) Cn ( J tX K ) ) )
112		ishmeo 15018	. 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 ) ) ) )
113	21, 111, 112	sylanbrc 417	1 |- ( ph -> ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Homeo ( L tX M ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1395   e. wcel 2200   <.cop 3670   U.cuni 3891   |-> cmpt 4148   X. cxp 4721   `'ccnv 4722   -->wf 5320   -1-1-onto->wf1o 5323   ` cfv 5324  (class class class)co 6013   e. cmpo 6015   1stc1st 6296   2ndc2nd 6297   Topctop 14711  TopOnctopon 14724   Cn ccn 14899   tX ctx 14966   Homeochmeo 15014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4202  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2802  df-sbc 3030  df-csb 3126  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-nul 3493  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-iun 3970  df-br 4087  df-opab 4149  df-mpt 4150  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-res 4735  df-ima 4736  df-iota 5284  df-fun 5326  df-fn 5327  df-f 5328  df-f1 5329  df-fo 5330  df-f1o 5331  df-fv 5332  df-ov 6016  df-oprab 6017  df-mpo 6018  df-1st 6298  df-2nd 6299  df-map 6814  df-topgen 13333  df-top 14712  df-topon 14725  df-bases 14757  df-cn 14902  df-tx 14967  df-hmeo 15015

This theorem is referenced by: (None)