Theorem txhmeo 21606

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 21563	. . . . . 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 21044	. . . . 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 20722	. . . 4 |- ( J e. Top <-> J e. (TopOn ` X ) )
8	5, 7	sylib 208	. . 3 |- ( ph -> J e. (TopOn ` X ) )
9		txhmeo.4	. . . . . 6 |- ( ph -> G e. ( K Homeo M ) )
10		hmeocn 21563	. . . . . 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 21044	. . . . 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 20722	. . . 4 |- ( K e. Top <-> K e. (TopOn ` Y ) )
16	13, 15	sylib 208	. . 3 |- ( ph -> K e. (TopOn ` Y ) )
17	8, 16	cnmpt1st 21471	. . . 4 |- ( ph -> ( x e. X , y e. Y |-> x ) e. ( ( J tX K ) Cn J ) )
18	8, 16, 17, 3	cnmpt21f 21475	. . 3 |- ( ph -> ( x e. X , y e. Y |-> ( F ` x ) ) e. ( ( J tX K ) Cn L ) )
19	8, 16	cnmpt2nd 21472	. . . 4 |- ( ph -> ( x e. X , y e. Y |-> y ) e. ( ( J tX K ) Cn K ) )
20	8, 16, 19, 11	cnmpt21f 21475	. . 3 |- ( ph -> ( x e. X , y e. Y |-> ( G ` y ) ) e. ( ( J tX K ) Cn M ) )
21	8, 16, 18, 20	cnmpt2t 21476	. 2 |- ( ph -> ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Cn ( L tX M ) ) )
22		vex 3203	. . . . . . . . . . 11 |- x e. _V
23		vex 3203	. . . . . . . . . . 11 |- y e. _V
24	22, 23	op1std 7178	. . . . . . . . . 10 |- ( u = <. x , y >. -> ( 1st ` u ) = x )
25	24	fveq2d 6195	. . . . . . . . 9 |- ( u = <. x , y >. -> ( F ` ( 1st ` u ) ) = ( F ` x ) )
26	22, 23	op2ndd 7179	. . . . . . . . . 10 |- ( u = <. x , y >. -> ( 2nd ` u ) = y )
27	26	fveq2d 6195	. . . . . . . . 9 |- ( u = <. x , y >. -> ( G ` ( 2nd ` u ) ) = ( G ` y ) )
28	25, 27	opeq12d 4410	. . . . . . . 8 |- ( u = <. x , y >. -> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. = <. ( F ` x ) , ( G ` y ) >. )
29	28	mpt2mpt 6752	. . . . . . 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 2631	. . . . . 6 |- ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) = ( u e. ( X X. Y ) |-> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. )
31		eqid 2622	. . . . . . . . . 10 |- U. L = U. L
32	6, 31	cnf 21050	. . . . . . . . 9 |- ( F e. ( J Cn L ) -> F : X --> U. L )
33	3, 32	syl 17	. . . . . . . 8 |- ( ph -> F : X --> U. L )
34		xp1st 7198	. . . . . . . 8 |- ( u e. ( X X. Y ) -> ( 1st ` u ) e. X )
35		ffvelrn 6357	. . . . . . . 8 |- ( ( F : X --> U. L /\ ( 1st ` u ) e. X ) -> ( F ` ( 1st ` u ) ) e. U. L )
36	33, 34, 35	syl2an 494	. . . . . . 7 |- ( ( ph /\ u e. ( X X. Y ) ) -> ( F ` ( 1st ` u ) ) e. U. L )
37		eqid 2622	. . . . . . . . . 10 |- U. M = U. M
38	14, 37	cnf 21050	. . . . . . . . 9 |- ( G e. ( K Cn M ) -> G : Y --> U. M )
39	11, 38	syl 17	. . . . . . . 8 |- ( ph -> G : Y --> U. M )
40		xp2nd 7199	. . . . . . . 8 |- ( u e. ( X X. Y ) -> ( 2nd ` u ) e. Y )
41		ffvelrn 6357	. . . . . . . 8 |- ( ( G : Y --> U. M /\ ( 2nd ` u ) e. Y ) -> ( G ` ( 2nd ` u ) ) e. U. M )
42	39, 40, 41	syl2an 494	. . . . . . 7 |- ( ( ph /\ u e. ( X X. Y ) ) -> ( G ` ( 2nd ` u ) ) e. U. M )
43		opelxpi 5148	. . . . . . 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 693	. . . . . 6 |- ( ( ph /\ u e. ( X X. Y ) ) -> <. ( F ` ( 1st ` u ) ) , ( G ` ( 2nd ` u ) ) >. e. ( U. L X. U. M ) )
45	6, 31	hmeof1o 21567	. . . . . . . . . 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 6149	. . . . . . . . 9 |- ( F : X -1-1-onto-> U. L -> `' F : U. L -1-1-onto-> X )
48		f1of 6137	. . . . . . . . 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 7198	. . . . . . . 8 |- ( v e. ( U. L X. U. M ) -> ( 1st ` v ) e. U. L )
51		ffvelrn 6357	. . . . . . . 8 |- ( ( `' F : U. L --> X /\ ( 1st ` v ) e. U. L ) -> ( `' F ` ( 1st ` v ) ) e. X )
52	49, 50, 51	syl2an 494	. . . . . . 7 |- ( ( ph /\ v e. ( U. L X. U. M ) ) -> ( `' F ` ( 1st ` v ) ) e. X )
53	14, 37	hmeof1o 21567	. . . . . . . . . 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 6149	. . . . . . . . 9 |- ( G : Y -1-1-onto-> U. M -> `' G : U. M -1-1-onto-> Y )
56		f1of 6137	. . . . . . . . 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 7199	. . . . . . . 8 |- ( v e. ( U. L X. U. M ) -> ( 2nd ` v ) e. U. M )
59		ffvelrn 6357	. . . . . . . 8 |- ( ( `' G : U. M --> Y /\ ( 2nd ` v ) e. U. M ) -> ( `' G ` ( 2nd ` v ) ) e. Y )
60	57, 58, 59	syl2an 494	. . . . . . 7 |- ( ( ph /\ v e. ( U. L X. U. M ) ) -> ( `' G ` ( 2nd ` v ) ) e. Y )
61		opelxpi 5148	. . . . . . 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 693	. . . . . 6 |- ( ( ph /\ v e. ( U. L X. U. M ) ) -> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. e. ( X X. Y ) )
63	46	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> F : X -1-1-onto-> U. L )
64	34	ad2antrl 764	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 1st ` u ) e. X )
65	50	ad2antll 765	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 1st ` v ) e. U. L )
66		f1ocnvfvb 6535	. . . . . . . . . 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 1326	. . . . . . . . 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 2629	. . . . . . . . 9 |- ( ( 1st ` v ) = ( F ` ( 1st ` u ) ) <-> ( F ` ( 1st ` u ) ) = ( 1st ` v ) )
69		eqcom 2629	. . . . . . . . 9 |- ( ( 1st ` u ) = ( `' F ` ( 1st ` v ) ) <-> ( `' F ` ( 1st ` v ) ) = ( 1st ` u ) )
70	67, 68, 69	3bitr4g 303	. . . . . . . 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 481	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> G : Y -1-1-onto-> U. M )
72	40	ad2antrl 764	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 2nd ` u ) e. Y )
73	58	ad2antll 765	. . . . . . . . . 10 |- ( ( ph /\ ( u e. ( X X. Y ) /\ v e. ( U. L X. U. M ) ) ) -> ( 2nd ` v ) e. U. M )
74		f1ocnvfvb 6535	. . . . . . . . . 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 1326	. . . . . . . . 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 2629	. . . . . . . . 9 |- ( ( 2nd ` v ) = ( G ` ( 2nd ` u ) ) <-> ( G ` ( 2nd ` u ) ) = ( 2nd ` v ) )
77		eqcom 2629	. . . . . . . . 9 |- ( ( 2nd ` u ) = ( `' G ` ( 2nd ` v ) ) <-> ( `' G ` ( 2nd ` v ) ) = ( 2nd ` u ) )
78	75, 76, 77	3bitr4g 303	. . . . . . . 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 747	. . . . . . 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 7208	. . . . . . . 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 765	. . . . . . 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 7208	. . . . . . . 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 764	. . . . . . 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 301	. . . . . 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 6886	. . . . 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 479	. . . 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 3203	. . . . . . . 8 |- z e. _V
88		vex 3203	. . . . . . . 8 |- w e. _V
89	87, 88	op1std 7178	. . . . . . 7 |- ( v = <. z , w >. -> ( 1st ` v ) = z )
90	89	fveq2d 6195	. . . . . 6 |- ( v = <. z , w >. -> ( `' F ` ( 1st ` v ) ) = ( `' F ` z ) )
91	87, 88	op2ndd 7179	. . . . . . 7 |- ( v = <. z , w >. -> ( 2nd ` v ) = w )
92	91	fveq2d 6195	. . . . . 6 |- ( v = <. z , w >. -> ( `' G ` ( 2nd ` v ) ) = ( `' G ` w ) )
93	90, 92	opeq12d 4410	. . . . 5 |- ( v = <. z , w >. -> <. ( `' F ` ( 1st ` v ) ) , ( `' G ` ( 2nd ` v ) ) >. = <. ( `' F ` z ) , ( `' G ` w ) >. )
94	93	mpt2mpt 6752	. . . 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 2672	. . 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 21045	. . . . . 6 |- ( F e. ( J Cn L ) -> L e. Top )
97	3, 96	syl 17	. . . . 5 |- ( ph -> L e. Top )
98	31	toptopon 20722	. . . . 5 |- ( L e. Top <-> L e. (TopOn ` U. L ) )
99	97, 98	sylib 208	. . . 4 |- ( ph -> L e. (TopOn ` U. L ) )
100		cntop2 21045	. . . . . 6 |- ( G e. ( K Cn M ) -> M e. Top )
101	11, 100	syl 17	. . . . 5 |- ( ph -> M e. Top )
102	37	toptopon 20722	. . . . 5 |- ( M e. Top <-> M e. (TopOn ` U. M ) )
103	101, 102	sylib 208	. . . 4 |- ( ph -> M e. (TopOn ` U. M ) )
104	99, 103	cnmpt1st 21471	. . . . 5 |- ( ph -> ( z e. U. L , w e. U. M |-> z ) e. ( ( L tX M ) Cn L ) )
105		hmeocnvcn 21564	. . . . . 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 21475	. . . 4 |- ( ph -> ( z e. U. L , w e. U. M |-> ( `' F ` z ) ) e. ( ( L tX M ) Cn J ) )
108	99, 103	cnmpt2nd 21472	. . . . 5 |- ( ph -> ( z e. U. L , w e. U. M |-> w ) e. ( ( L tX M ) Cn M ) )
109		hmeocnvcn 21564	. . . . . 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 21475	. . . 4 |- ( ph -> ( z e. U. L , w e. U. M |-> ( `' G ` w ) ) e. ( ( L tX M ) Cn K ) )
112	99, 103, 107, 111	cnmpt2t 21476	. . 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 2701	. 2 |- ( ph -> `' ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( L tX M ) Cn ( J tX K ) ) )
114		ishmeo 21562	. 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 698	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 196   /\ wa 384   = wceq 1483   e. wcel 1990   <.cop 4183   U.cuni 4436   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   -->wf 5884   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   1stc1st 7166   2ndc2nd 7167   Topctop 20698  TopOnctopon 20715   Cn ccn 21028   tX ctx 21363   Homeochmeo 21556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-map 7859  df-topgen 16104  df-top 20699  df-topon 20716  df-bases 20750  df-cn 21031  df-tx 21365  df-hmeo 21558

This theorem is referenced by:  xpstopnlem1  21612