Theorem cnmpt21 20673

Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)

Hypotheses

Ref	Expression
cnmpt21.j	|- ( ph -> J e. (TopOn ` X ) )
cnmpt21.k	|- ( ph -> K e. (TopOn ` Y ) )
cnmpt21.a	|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )
cnmpt21.l	|- ( ph -> L e. (TopOn ` Z ) )
cnmpt21.b	|- ( ph -> ( z e. Z |-> B ) e. ( L Cn M ) )
cnmpt21.c	|- ( z = A -> B = C )

Assertion

Ref	Expression
cnmpt21	|- ( ph -> ( x e. X , y e. Y |-> C ) e. ( ( J tX K ) Cn M ) )

Distinct variable groups:   z, A   z, J   x, y, z, L   ph, x, y, z   x, X, y, z   x, M, y, z   x, Y, y, z   z, K   x, Z, y, z   x, B, y   z, C

Allowed substitution hints:   A( x, y)   B( z)   C( x, y)   J( x, y)   K( x, y)

Proof of Theorem cnmpt21

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

Step	Hyp	Ref	Expression
1		df-ov 6305	. . . . . . . . . 10 |- ( x ( x e. X , y e. Y |-> A ) y ) = ( ( x e. X , y e. Y |-> A ) ` <. x , y >. )
2		simprl 762	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. X /\ y e. Y ) ) -> x e. X )
3		simprr 764	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. X /\ y e. Y ) ) -> y e. Y )
4		cnmpt21.j	. . . . . . . . . . . . . . . 16 |- ( ph -> J e. (TopOn ` X ) )
5		cnmpt21.k	. . . . . . . . . . . . . . . 16 |- ( ph -> K e. (TopOn ` Y ) )
6		txtopon 20593	. . . . . . . . . . . . . . . 16 |- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( J tX K ) e. (TopOn ` ( X X. Y ) ) )
7	4, 5, 6	syl2anc 665	. . . . . . . . . . . . . . 15 |- ( ph -> ( J tX K ) e. (TopOn ` ( X X. Y ) ) )
8		cnmpt21.l	. . . . . . . . . . . . . . 15 |- ( ph -> L e. (TopOn ` Z ) )
9		cnmpt21.a	. . . . . . . . . . . . . . 15 |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )
10		cnf2 20252	. . . . . . . . . . . . . . 15 |- ( ( ( J tX K ) e. (TopOn ` ( X X. Y ) ) /\ L e. (TopOn ` Z ) /\ ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) ) -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z )
11	7, 8, 9, 10	syl3anc 1264	. . . . . . . . . . . . . 14 |- ( ph -> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z )
12		eqid 2422	. . . . . . . . . . . . . . 15 |- ( x e. X , y e. Y |-> A ) = ( x e. X , y e. Y |-> A )
13	12	fmpt2 6871	. . . . . . . . . . . . . 14 |- ( A. x e. X A. y e. Y A e. Z <-> ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z )
14	11, 13	sylibr 215	. . . . . . . . . . . . 13 |- ( ph -> A. x e. X A. y e. Y A e. Z )
15		rsp2 2799	. . . . . . . . . . . . 13 |- ( A. x e. X A. y e. Y A e. Z -> ( ( x e. X /\ y e. Y ) -> A e. Z ) )
16	14, 15	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( ( x e. X /\ y e. Y ) -> A e. Z ) )
17	16	imp 430	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. X /\ y e. Y ) ) -> A e. Z )
18	12	ovmpt4g 6430	. . . . . . . . . . 11 |- ( ( x e. X /\ y e. Y /\ A e. Z ) -> ( x ( x e. X , y e. Y |-> A ) y ) = A )
19	2, 3, 17, 18	syl3anc 1264	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( x ( x e. X , y e. Y |-> A ) y ) = A )
20	1, 19	syl5eqr 2477	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( ( x e. X , y e. Y |-> A ) ` <. x , y >. ) = A )
21	20	fveq2d 5882	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( ( z e. Z |-> B ) ` ( ( x e. X , y e. Y |-> A ) ` <. x , y >. ) ) = ( ( z e. Z |-> B ) ` A ) )
22		cnmpt21.b	. . . . . . . . . . . . . . 15 |- ( ph -> ( z e. Z |-> B ) e. ( L Cn M ) )
23		cntop2 20244	. . . . . . . . . . . . . . 15 |- ( ( z e. Z |-> B ) e. ( L Cn M ) -> M e. Top )
24	22, 23	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> M e. Top )
25		eqid 2422	. . . . . . . . . . . . . . 15 |- U. M = U. M
26	25	toptopon 19935	. . . . . . . . . . . . . 14 |- ( M e. Top <-> M e. (TopOn ` U. M ) )
27	24, 26	sylib 199	. . . . . . . . . . . . 13 |- ( ph -> M e. (TopOn ` U. M ) )
28		cnf2 20252	. . . . . . . . . . . . 13 |- ( ( L e. (TopOn ` Z ) /\ M e. (TopOn ` U. M ) /\ ( z e. Z |-> B ) e. ( L Cn M ) ) -> ( z e. Z |-> B ) : Z --> U. M )
29	8, 27, 22, 28	syl3anc 1264	. . . . . . . . . . . 12 |- ( ph -> ( z e. Z |-> B ) : Z --> U. M )
30		eqid 2422	. . . . . . . . . . . . 13 |- ( z e. Z |-> B ) = ( z e. Z |-> B )
31	30	fmpt 6055	. . . . . . . . . . . 12 |- ( A. z e. Z B e. U. M <-> ( z e. Z |-> B ) : Z --> U. M )
32	29, 31	sylibr 215	. . . . . . . . . . 11 |- ( ph -> A. z e. Z B e. U. M )
33	32	adantr 466	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y e. Y ) ) -> A. z e. Z B e. U. M )
34		cnmpt21.c	. . . . . . . . . . . 12 |- ( z = A -> B = C )
35	34	eleq1d 2491	. . . . . . . . . . 11 |- ( z = A -> ( B e. U. M <-> C e. U. M ) )
36	35	rspcv 3178	. . . . . . . . . 10 |- ( A e. Z -> ( A. z e. Z B e. U. M -> C e. U. M ) )
37	17, 33, 36	sylc 62	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. Y ) ) -> C e. U. M )
38	34, 30	fvmptg 5959	. . . . . . . . 9 |- ( ( A e. Z /\ C e. U. M ) -> ( ( z e. Z |-> B ) ` A ) = C )
39	17, 37, 38	syl2anc 665	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( ( z e. Z |-> B ) ` A ) = C )
40	21, 39	eqtrd 2463	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( ( z e. Z |-> B ) ` ( ( x e. X , y e. Y |-> A ) ` <. x , y >. ) ) = C )
41		opelxpi 4882	. . . . . . . 8 |- ( ( x e. X /\ y e. Y ) -> <. x , y >. e. ( X X. Y ) )
42		fvco3 5955	. . . . . . . 8 |- ( ( ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z /\ <. x , y >. e. ( X X. Y ) ) -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( z e. Z |-> B ) ` ( ( x e. X , y e. Y |-> A ) ` <. x , y >. ) ) )
43	11, 41, 42	syl2an 479	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( z e. Z |-> B ) ` ( ( x e. X , y e. Y |-> A ) ` <. x , y >. ) ) )
44		df-ov 6305	. . . . . . . 8 |- ( x ( x e. X , y e. Y |-> C ) y ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. )
45		eqid 2422	. . . . . . . . . 10 |- ( x e. X , y e. Y |-> C ) = ( x e. X , y e. Y |-> C )
46	45	ovmpt4g 6430	. . . . . . . . 9 |- ( ( x e. X /\ y e. Y /\ C e. U. M ) -> ( x ( x e. X , y e. Y |-> C ) y ) = C )
47	2, 3, 37, 46	syl3anc 1264	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( x ( x e. X , y e. Y |-> C ) y ) = C )
48	44, 47	syl5eqr 2477	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) = C )
49	40, 43, 48	3eqtr4d 2473	. . . . . 6 |- ( ( ph /\ ( x e. X /\ y e. Y ) ) -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) )
50	49	ralrimivva 2846	. . . . 5 |- ( ph -> A. x e. X A. y e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) )
51		nfv 1751	. . . . . 6 |- F/ u A. y e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. )
52		nfcv 2584	. . . . . . 7 |- F/_ x Y
53		nfcv 2584	. . . . . . . . . 10 |- F/_ x ( z e. Z |-> B )
54		nfmpt21 6369	. . . . . . . . . 10 |- F/_ x ( x e. X , y e. Y |-> A )
55	53, 54	nfco 5016	. . . . . . . . 9 |- F/_ x ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) )
56		nfcv 2584	. . . . . . . . 9 |- F/_ x <. u , v >.
57	55, 56	nffv 5885	. . . . . . . 8 |- F/_ x ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. )
58		nfmpt21 6369	. . . . . . . . 9 |- F/_ x ( x e. X , y e. Y |-> C )
59	58, 56	nffv 5885	. . . . . . . 8 |- F/_ x ( ( x e. X , y e. Y |-> C ) ` <. u , v >. )
60	57, 59	nfeq 2595	. . . . . . 7 |- F/ x ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. )
61	52, 60	nfral 2811	. . . . . 6 |- F/ x A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. )
62		nfv 1751	. . . . . . . 8 |- F/ v ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. )
63		nfcv 2584	. . . . . . . . . . 11 |- F/_ y ( z e. Z |-> B )
64		nfmpt22 6370	. . . . . . . . . . 11 |- F/_ y ( x e. X , y e. Y |-> A )
65	63, 64	nfco 5016	. . . . . . . . . 10 |- F/_ y ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) )
66		nfcv 2584	. . . . . . . . . 10 |- F/_ y <. x , v >.
67	65, 66	nffv 5885	. . . . . . . . 9 |- F/_ y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. )
68		nfmpt22 6370	. . . . . . . . . 10 |- F/_ y ( x e. X , y e. Y |-> C )
69	68, 66	nffv 5885	. . . . . . . . 9 |- F/_ y ( ( x e. X , y e. Y |-> C ) ` <. x , v >. )
70	67, 69	nfeq 2595	. . . . . . . 8 |- F/ y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , v >. )
71		opeq2 4185	. . . . . . . . . 10 |- ( y = v -> <. x , y >. = <. x , v >. )
72	71	fveq2d 5882	. . . . . . . . 9 |- ( y = v -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. ) )
73	71	fveq2d 5882	. . . . . . . . 9 |- ( y = v -> ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , v >. ) )
74	72, 73	eqeq12d 2444	. . . . . . . 8 |- ( y = v -> ( ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) <-> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , v >. ) ) )
75	62, 70, 74	cbvral 3051	. . . . . . 7 |- ( A. y e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) <-> A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , v >. ) )
76		opeq1 4184	. . . . . . . . . 10 |- ( x = u -> <. x , v >. = <. u , v >. )
77	76	fveq2d 5882	. . . . . . . . 9 |- ( x = u -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. ) = ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) )
78	76	fveq2d 5882	. . . . . . . . 9 |- ( x = u -> ( ( x e. X , y e. Y |-> C ) ` <. x , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) )
79	77, 78	eqeq12d 2444	. . . . . . . 8 |- ( x = u -> ( ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , v >. ) <-> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) ) )
80	79	ralbidv 2864	. . . . . . 7 |- ( x = u -> ( A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , v >. ) <-> A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) ) )
81	75, 80	syl5bb 260	. . . . . 6 |- ( x = u -> ( A. y e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) <-> A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) ) )
82	51, 61, 81	cbvral 3051	. . . . 5 |- ( A. x e. X A. y e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. x , y >. ) = ( ( x e. X , y e. Y |-> C ) ` <. x , y >. ) <-> A. u e. X A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) )
83	50, 82	sylib 199	. . . 4 |- ( ph -> A. u e. X A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) )
84		fveq2 5878	. . . . . 6 |- ( w = <. u , v >. -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` w ) = ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) )
85		fveq2 5878	. . . . . 6 |- ( w = <. u , v >. -> ( ( x e. X , y e. Y |-> C ) ` w ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) )
86	84, 85	eqeq12d 2444	. . . . 5 |- ( w = <. u , v >. -> ( ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` w ) = ( ( x e. X , y e. Y |-> C ) ` w ) <-> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) ) )
87	86	ralxp 4992	. . . 4 |- ( A. w e. ( X X. Y ) ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` w ) = ( ( x e. X , y e. Y |-> C ) ` w ) <-> A. u e. X A. v e. Y ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` <. u , v >. ) = ( ( x e. X , y e. Y |-> C ) ` <. u , v >. ) )
88	83, 87	sylibr 215	. . 3 |- ( ph -> A. w e. ( X X. Y ) ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` w ) = ( ( x e. X , y e. Y |-> C ) ` w ) )
89		fco 5753	. . . . . 6 |- ( ( ( z e. Z |-> B ) : Z --> U. M /\ ( x e. X , y e. Y |-> A ) : ( X X. Y ) --> Z ) -> ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) : ( X X. Y ) --> U. M )
90	29, 11, 89	syl2anc 665	. . . . 5 |- ( ph -> ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) : ( X X. Y ) --> U. M )
91		ffn 5743	. . . . 5 |- ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) : ( X X. Y ) --> U. M -> ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) Fn ( X X. Y ) )
92	90, 91	syl 17	. . . 4 |- ( ph -> ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) Fn ( X X. Y ) )
93	37	ralrimivva 2846	. . . . . 6 |- ( ph -> A. x e. X A. y e. Y C e. U. M )
94	45	fmpt2 6871	. . . . . 6 |- ( A. x e. X A. y e. Y C e. U. M <-> ( x e. X , y e. Y |-> C ) : ( X X. Y ) --> U. M )
95	93, 94	sylib 199	. . . . 5 |- ( ph -> ( x e. X , y e. Y |-> C ) : ( X X. Y ) --> U. M )
96		ffn 5743	. . . . 5 |- ( ( x e. X , y e. Y |-> C ) : ( X X. Y ) --> U. M -> ( x e. X , y e. Y |-> C ) Fn ( X X. Y ) )
97	95, 96	syl 17	. . . 4 |- ( ph -> ( x e. X , y e. Y |-> C ) Fn ( X X. Y ) )
98		eqfnfv 5988	. . . 4 |- ( ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) Fn ( X X. Y ) /\ ( x e. X , y e. Y |-> C ) Fn ( X X. Y ) ) -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) = ( x e. X , y e. Y |-> C ) <-> A. w e. ( X X. Y ) ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` w ) = ( ( x e. X , y e. Y |-> C ) ` w ) ) )
99	92, 97, 98	syl2anc 665	. . 3 |- ( ph -> ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) = ( x e. X , y e. Y |-> C ) <-> A. w e. ( X X. Y ) ( ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) ` w ) = ( ( x e. X , y e. Y |-> C ) ` w ) ) )
100	88, 99	mpbird 235	. 2 |- ( ph -> ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) = ( x e. X , y e. Y |-> C ) )
101		cnco 20269	. . 3 |- ( ( ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) /\ ( z e. Z |-> B ) e. ( L Cn M ) ) -> ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) e. ( ( J tX K ) Cn M ) )
102	9, 22, 101	syl2anc 665	. 2 |- ( ph -> ( ( z e. Z |-> B ) o. ( x e. X , y e. Y |-> A ) ) e. ( ( J tX K ) Cn M ) )
103	100, 102	eqeltrrd 2511	1 |- ( ph -> ( x e. X , y e. Y |-> C ) e. ( ( J tX K ) Cn M ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1868   A.wral 2775   <.cop 4002   U.cuni 4216   |-> cmpt 4479   X. cxp 4848   o. ccom 4854   Fn wfn 5593   -->wf 5594   ` cfv 5598  (class class class)co 6302   |-> cmpt2 6304   Topctop 19904  TopOnctopon 19905   Cn ccn 20227   tX ctx 20562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-fv 5606  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-1st 6804  df-2nd 6805  df-map 7479  df-topgen 15330  df-top 19908  df-bases 19909  df-topon 19910  df-cn 20230  df-tx 20564

This theorem is referenced by:  cnmpt21f  20674  xkofvcn  20686  xkohmeo  20817  qustgplem  21122  prdstmdd  21125  divcn  21887  htpycom  21994  htpycc  21998  reparphti  22015  pcocn  22035  pcohtpylem  22037  pcopt  22040  pcopt2  22041  pcoass  22042  pcorevlem  22044  dipcn  26345