Theorem cmpsub 18845

Description: Two equivalent ways of describing a compact subset of a topological space. Inspired by Sue E. Goodman's Beginning Topology. (Contributed by Jeff Hankins, 22-Jun-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)

Hypothesis

Ref	Expression
cmpsub.1	|- X = U. J

Assertion

Ref	Expression
cmpsub	|- ( ( J e. Top /\ S C_ X ) -> ( ( J ↾t S ) e. Comp <-> A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )

Distinct variable groups:   c, d, J   S, c, d   X, c, d

Proof of Theorem cmpsub

Dummy variables x y f s t u v w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2433	. . . 4 |- U. ( J ↾t S ) = U. ( J ↾t S )
2	1	iscmp 18833	. . 3 |- ( ( J ↾t S ) e. Comp <-> ( ( J ↾t S ) e. Top /\ A. s e. ~P ( J ↾t S ) ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) ) )
3		id 22	. . . . . 6 |- ( S C_ X -> S C_ X )
4		cmpsub.1	. . . . . . 7 |- X = U. J
5	4	topopn 18361	. . . . . 6 |- ( J e. Top -> X e. J )
6		ssexg 4426	. . . . . 6 |- ( ( S C_ X /\ X e. J ) -> S e. _V )
7	3, 5, 6	syl2anr 475	. . . . 5 |- ( ( J e. Top /\ S C_ X ) -> S e. _V )
8		resttop 18606	. . . . 5 |- ( ( J e. Top /\ S e. _V ) -> ( J ↾t S ) e. Top )
9	7, 8	syldan 467	. . . 4 |- ( ( J e. Top /\ S C_ X ) -> ( J ↾t S ) e. Top )
10		ibar 501	. . . . 5 |- ( ( J ↾t S ) e. Top -> ( A. s e. ~P ( J ↾t S ) ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) <-> ( ( J ↾t S ) e. Top /\ A. s e. ~P ( J ↾t S ) ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) ) ) )
11	10	bicomd 201	. . . 4 |- ( ( J ↾t S ) e. Top -> ( ( ( J ↾t S ) e. Top /\ A. s e. ~P ( J ↾t S ) ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) ) <-> A. s e. ~P ( J ↾t S ) ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) ) )
12	9, 11	syl 16	. . 3 |- ( ( J e. Top /\ S C_ X ) -> ( ( ( J ↾t S ) e. Top /\ A. s e. ~P ( J ↾t S ) ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) ) <-> A. s e. ~P ( J ↾t S ) ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) ) )
13	2, 12	syl5bb 257	. 2 |- ( ( J e. Top /\ S C_ X ) -> ( ( J ↾t S ) e. Comp <-> A. s e. ~P ( J ↾t S ) ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) ) )
14		vex 2965	. . . . . . . . . . 11 |- t e. _V
15		eqeq1 2439	. . . . . . . . . . . 12 |- ( x = t -> ( x = ( y i^i S ) <-> t = ( y i^i S ) ) )
16	15	rexbidv 2726	. . . . . . . . . . 11 |- ( x = t -> ( E. y e. c x = ( y i^i S ) <-> E. y e. c t = ( y i^i S ) ) )
17	14, 16	elab 3095	. . . . . . . . . 10 |- ( t e. { x | E. y e. c x = ( y i^i S ) } <-> E. y e. c t = ( y i^i S ) )
18		selpw 3855	. . . . . . . . . . . . . 14 |- ( c e. ~P J <-> c C_ J )
19		ssel2 3339	. . . . . . . . . . . . . . . 16 |- ( ( c C_ J /\ y e. c ) -> y e. J )
20		ineq1 3533	. . . . . . . . . . . . . . . . . . 19 |- ( d = y -> ( d i^i S ) = ( y i^i S ) )
21	20	eqeq2d 2444	. . . . . . . . . . . . . . . . . 18 |- ( d = y -> ( t = ( d i^i S ) <-> t = ( y i^i S ) ) )
22	21	rspcev 3062	. . . . . . . . . . . . . . . . 17 |- ( ( y e. J /\ t = ( y i^i S ) ) -> E. d e. J t = ( d i^i S ) )
23	22	ex 434	. . . . . . . . . . . . . . . 16 |- ( y e. J -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) )
24	19, 23	syl 16	. . . . . . . . . . . . . . 15 |- ( ( c C_ J /\ y e. c ) -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) )
25	24	ex 434	. . . . . . . . . . . . . 14 |- ( c C_ J -> ( y e. c -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) ) )
26	18, 25	sylbi 195	. . . . . . . . . . . . 13 |- ( c e. ~P J -> ( y e. c -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) ) )
27	26	adantl 463	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( y e. c -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) ) )
28	27	rexlimdv 2830	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( E. y e. c t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) )
29		simpll 746	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> J e. Top )
30	4	sseq2i 3369	. . . . . . . . . . . . . 14 |- ( S C_ X <-> S C_ U. J )
31		uniexg 6366	. . . . . . . . . . . . . . . 16 |- ( J e. Top -> U. J e. _V )
32		ssexg 4426	. . . . . . . . . . . . . . . 16 |- ( ( S C_ U. J /\ U. J e. _V ) -> S e. _V )
33	31, 32	sylan2 471	. . . . . . . . . . . . . . 15 |- ( ( S C_ U. J /\ J e. Top ) -> S e. _V )
34	33	ancoms 450	. . . . . . . . . . . . . 14 |- ( ( J e. Top /\ S C_ U. J ) -> S e. _V )
35	30, 34	sylan2b 472	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ S C_ X ) -> S e. _V )
36	35	adantr 462	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> S e. _V )
37		elrest 14349	. . . . . . . . . . . 12 |- ( ( J e. Top /\ S e. _V ) -> ( t e. ( J ↾t S ) <-> E. d e. J t = ( d i^i S ) ) )
38	29, 36, 37	syl2anc 654	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( t e. ( J ↾t S ) <-> E. d e. J t = ( d i^i S ) ) )
39	28, 38	sylibrd 234	. . . . . . . . . 10 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( E. y e. c t = ( y i^i S ) -> t e. ( J ↾t S ) ) )
40	17, 39	syl5bi 217	. . . . . . . . 9 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( t e. { x | E. y e. c x = ( y i^i S ) } -> t e. ( J ↾t S ) ) )
41	40	ssrdv 3350	. . . . . . . 8 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> { x | E. y e. c x = ( y i^i S ) } C_ ( J ↾t S ) )
42		vex 2965	. . . . . . . . . 10 |- c e. _V
43	42	abrexex 6540	. . . . . . . . 9 |- { x | E. y e. c x = ( y i^i S ) } e. _V
44	43	elpw 3854	. . . . . . . 8 |- ( { x | E. y e. c x = ( y i^i S ) } e. ~P ( J ↾t S ) <-> { x | E. y e. c x = ( y i^i S ) } C_ ( J ↾t S ) )
45	41, 44	sylibr 212	. . . . . . 7 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> { x | E. y e. c x = ( y i^i S ) } e. ~P ( J ↾t S ) )
46		unieq 4087	. . . . . . . . . 10 |- ( s = { x | E. y e. c x = ( y i^i S ) } -> U. s = U. { x | E. y e. c x = ( y i^i S ) } )
47	46	eqeq2d 2444	. . . . . . . . 9 |- ( s = { x | E. y e. c x = ( y i^i S ) } -> ( U. ( J ↾t S ) = U. s <-> U. ( J ↾t S ) = U. { x | E. y e. c x = ( y i^i S ) } ) )
48		pweq 3851	. . . . . . . . . . 11 |- ( s = { x | E. y e. c x = ( y i^i S ) } -> ~P s = ~P { x | E. y e. c x = ( y i^i S ) } )
49	48	ineq1d 3539	. . . . . . . . . 10 |- ( s = { x | E. y e. c x = ( y i^i S ) } -> ( ~P s i^i Fin ) = ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) )
50	49	rexeqdv 2914	. . . . . . . . 9 |- ( s = { x | E. y e. c x = ( y i^i S ) } -> ( E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t <-> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J ↾t S ) = U. t ) )
51	47, 50	imbi12d 320	. . . . . . . 8 |- ( s = { x | E. y e. c x = ( y i^i S ) } -> ( ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) <-> ( U. ( J ↾t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J ↾t S ) = U. t ) ) )
52	51	rspcva 3060	. . . . . . 7 |- ( ( { x | E. y e. c x = ( y i^i S ) } e. ~P ( J ↾t S ) /\ A. s e. ~P ( J ↾t S ) ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) ) -> ( U. ( J ↾t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J ↾t S ) = U. t ) )
53	45, 52	sylan 468	. . . . . 6 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ A. s e. ~P ( J ↾t S ) ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) ) -> ( U. ( J ↾t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J ↾t S ) = U. t ) )
54	53	ex 434	. . . . 5 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( A. s e. ~P ( J ↾t S ) ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) -> ( U. ( J ↾t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J ↾t S ) = U. t ) ) )
55	4	restuni 18608	. . . . . . . . . . 11 |- ( ( J e. Top /\ S C_ X ) -> S = U. ( J ↾t S ) )
56	55	ad2antrr 718	. . . . . . . . . 10 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> S = U. ( J ↾t S ) )
57		vex 2965	. . . . . . . . . . . . . 14 |- y e. _V
58	57	inex1 4421	. . . . . . . . . . . . 13 |- ( y i^i S ) e. _V
59	58	dfiun2 4192	. . . . . . . . . . . 12 |- U_ y e. c ( y i^i S ) = U. { x | E. y e. c x = ( y i^i S ) }
60		incom 3531	. . . . . . . . . . . . . 14 |- ( y i^i S ) = ( S i^i y )
61	60	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ y e. c ) -> ( y i^i S ) = ( S i^i y ) )
62	61	iuneq2dv 4180	. . . . . . . . . . . 12 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> U_ y e. c ( y i^i S ) = U_ y e. c ( S i^i y ) )
63	59, 62	syl5eqr 2479	. . . . . . . . . . 11 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> U. { x | E. y e. c x = ( y i^i S ) } = U_ y e. c ( S i^i y ) )
64		iunin2 4222	. . . . . . . . . . . 12 |- U_ y e. c ( S i^i y ) = ( S i^i U_ y e. c y )
65		uniiun 4211	. . . . . . . . . . . . . . . 16 |- U. c = U_ y e. c y
66	65	eqcomi 2437	. . . . . . . . . . . . . . 15 |- U_ y e. c y = U. c
67	66	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> U_ y e. c y = U. c )
68	67	ineq2d 3540	. . . . . . . . . . . . 13 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( S i^i U_ y e. c y ) = ( S i^i U. c ) )
69		incom 3531	. . . . . . . . . . . . . . 15 |- ( S i^i U. c ) = ( U. c i^i S )
70		sseqin2 3557	. . . . . . . . . . . . . . . 16 |- ( S C_ U. c <-> ( U. c i^i S ) = S )
71	70	biimpi 194	. . . . . . . . . . . . . . 15 |- ( S C_ U. c -> ( U. c i^i S ) = S )
72	69, 71	syl5eq 2477	. . . . . . . . . . . . . 14 |- ( S C_ U. c -> ( S i^i U. c ) = S )
73	72	adantl 463	. . . . . . . . . . . . 13 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( S i^i U. c ) = S )
74	68, 73	eqtrd 2465	. . . . . . . . . . . 12 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( S i^i U_ y e. c y ) = S )
75	64, 74	syl5eq 2477	. . . . . . . . . . 11 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> U_ y e. c ( S i^i y ) = S )
76	63, 75	eqtr2d 2466	. . . . . . . . . 10 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> S = U. { x | E. y e. c x = ( y i^i S ) } )
77	56, 76	eqeq12d 2447	. . . . . . . . 9 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( S = S <-> U. ( J ↾t S ) = U. { x | E. y e. c x = ( y i^i S ) } ) )
78	56	eqeq1d 2441	. . . . . . . . . 10 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( S = U. t <-> U. ( J ↾t S ) = U. t ) )
79	78	rexbidv 2726	. . . . . . . . 9 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) S = U. t <-> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J ↾t S ) = U. t ) )
80	77, 79	imbi12d 320	. . . . . . . 8 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( ( S = S -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) S = U. t ) <-> ( U. ( J ↾t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J ↾t S ) = U. t ) ) )
81		eqid 2433	. . . . . . . . . 10 |- S = S
82	81	a1bi 337	. . . . . . . . 9 |- ( E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) S = U. t <-> ( S = S -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) S = U. t ) )
83		elin 3527	. . . . . . . . . . . 12 |- ( t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) <-> ( t e. ~P { x | E. y e. c x = ( y i^i S ) } /\ t e. Fin ) )
84		selpw 3855	. . . . . . . . . . . . . 14 |- ( t e. ~P { x | E. y e. c x = ( y i^i S ) } <-> t C_ { x | E. y e. c x = ( y i^i S ) } )
85		dfss3 3334	. . . . . . . . . . . . . 14 |- ( t C_ { x | E. y e. c x = ( y i^i S ) } <-> A. s e. t s e. { x | E. y e. c x = ( y i^i S ) } )
86		vex 2965	. . . . . . . . . . . . . . . 16 |- s e. _V
87		eqeq1 2439	. . . . . . . . . . . . . . . . 17 |- ( x = s -> ( x = ( y i^i S ) <-> s = ( y i^i S ) ) )
88	87	rexbidv 2726	. . . . . . . . . . . . . . . 16 |- ( x = s -> ( E. y e. c x = ( y i^i S ) <-> E. y e. c s = ( y i^i S ) ) )
89	86, 88	elab 3095	. . . . . . . . . . . . . . 15 |- ( s e. { x | E. y e. c x = ( y i^i S ) } <-> E. y e. c s = ( y i^i S ) )
90	89	ralbii 2729	. . . . . . . . . . . . . 14 |- ( A. s e. t s e. { x | E. y e. c x = ( y i^i S ) } <-> A. s e. t E. y e. c s = ( y i^i S ) )
91	84, 85, 90	3bitri 271	. . . . . . . . . . . . 13 |- ( t e. ~P { x | E. y e. c x = ( y i^i S ) } <-> A. s e. t E. y e. c s = ( y i^i S ) )
92	91	anbi1i 688	. . . . . . . . . . . 12 |- ( ( t e. ~P { x | E. y e. c x = ( y i^i S ) } /\ t e. Fin ) <-> ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) )
93	83, 92	bitri 249	. . . . . . . . . . 11 |- ( t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) <-> ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) )
94		ineq1 3533	. . . . . . . . . . . . . . . 16 |- ( y = ( f ` s ) -> ( y i^i S ) = ( ( f ` s ) i^i S ) )
95	94	eqeq2d 2444	. . . . . . . . . . . . . . 15 |- ( y = ( f ` s ) -> ( s = ( y i^i S ) <-> s = ( ( f ` s ) i^i S ) ) )
96	95	ac6sfi 7544	. . . . . . . . . . . . . 14 |- ( ( t e. Fin /\ A. s e. t E. y e. c s = ( y i^i S ) ) -> E. f ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) )
97	96	ancoms 450	. . . . . . . . . . . . 13 |- ( ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) -> E. f ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) )
98	97	adantl 463	. . . . . . . . . . . 12 |- ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) -> E. f ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) )
99		frn 5553	. . . . . . . . . . . . . . . . . . . . 21 |- ( f : t --> c -> ran f C_ c )
100	99	ad2antrl 720	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> ran f C_ c )
101		vex 2965	. . . . . . . . . . . . . . . . . . . . . 22 |- f e. _V
102	101	rnex 6501	. . . . . . . . . . . . . . . . . . . . 21 |- ran f e. _V
103	102	elpw 3854	. . . . . . . . . . . . . . . . . . . 20 |- ( ran f e. ~P c <-> ran f C_ c )
104	100, 103	sylibr 212	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> ran f e. ~P c )
105		simprr 749	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) -> t e. Fin )
106	105	ad2antrr 718	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> t e. Fin )
107		ffn 5547	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f : t --> c -> f Fn t )
108		dffn4 5614	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f Fn t <-> f : t -onto-> ran f )
109	107, 108	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f : t --> c -> f : t -onto-> ran f )
110		fodomfi 7578	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( t e. Fin /\ f : t -onto-> ran f ) -> ran f ~<_ t )
111	109, 110	sylan2 471	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( t e. Fin /\ f : t --> c ) -> ran f ~<_ t )
112	111	adantll 706	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) /\ f : t --> c ) -> ran f ~<_ t )
113	112	adantll 706	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ f : t --> c ) -> ran f ~<_ t )
114	113	ad2ant2r 739	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> ran f ~<_ t )
115		domfi 7522	. . . . . . . . . . . . . . . . . . . 20 |- ( ( t e. Fin /\ ran f ~<_ t ) -> ran f e. Fin )
116	106, 114, 115	syl2anc 654	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> ran f e. Fin )
117	104, 116	elind 3528	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> ran f e. ( ~P c i^i Fin ) )
118		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( s = u -> s = u )
119		fveq2 5679	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( s = u -> ( f ` s ) = ( f ` u ) )
120	119	ineq1d 3539	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( s = u -> ( ( f ` s ) i^i S ) = ( ( f ` u ) i^i S ) )
121	118, 120	eqeq12d 2447	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s = u -> ( s = ( ( f ` s ) i^i S ) <-> u = ( ( f ` u ) i^i S ) ) )
122	121	rspccv 3059	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A. s e. t s = ( ( f ` s ) i^i S ) -> ( u e. t -> u = ( ( f ` u ) i^i S ) ) )
123		pm2.27 39	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( u e. t -> ( ( u e. t -> u = ( ( f ` u ) i^i S ) ) -> u = ( ( f ` u ) i^i S ) ) )
124		inss1 3558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( f ` u ) i^i S ) C_ ( f ` u )
125		sseq1 3365	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( u = ( ( f ` u ) i^i S ) -> ( u C_ ( f ` u ) <-> ( ( f ` u ) i^i S ) C_ ( f ` u ) ) )
126	124, 125	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( u = ( ( f ` u ) i^i S ) -> u C_ ( f ` u ) )
127		ssel 3338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( u C_ ( f ` u ) -> ( w e. u -> w e. ( f ` u ) ) )
128	127	a1dd 46	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( u C_ ( f ` u ) -> ( w e. u -> ( f : t --> c -> w e. ( f ` u ) ) ) )
129	126, 128	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( u = ( ( f ` u ) i^i S ) -> ( w e. u -> ( f : t --> c -> w e. ( f ` u ) ) ) )
130	129	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( u e. t -> ( u = ( ( f ` u ) i^i S ) -> ( w e. u -> ( f : t --> c -> w e. ( f ` u ) ) ) ) )
131	130	3imp 1174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( u e. t /\ u = ( ( f ` u ) i^i S ) /\ w e. u ) -> ( f : t --> c -> w e. ( f ` u ) ) )
132		fnfvelrn 5828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( f Fn t /\ u e. t ) -> ( f ` u ) e. ran f )
133	132	expcom 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( u e. t -> ( f Fn t -> ( f ` u ) e. ran f ) )
134	133	3ad2ant1 1002	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( u e. t /\ u = ( ( f ` u ) i^i S ) /\ w e. u ) -> ( f Fn t -> ( f ` u ) e. ran f ) )
135	107, 134	syl5 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( u e. t /\ u = ( ( f ` u ) i^i S ) /\ w e. u ) -> ( f : t --> c -> ( f ` u ) e. ran f ) )
136	131, 135	jcad 530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( u e. t /\ u = ( ( f ` u ) i^i S ) /\ w e. u ) -> ( f : t --> c -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) )
137	136	3exp 1179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( u e. t -> ( u = ( ( f ` u ) i^i S ) -> ( w e. u -> ( f : t --> c -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) ) ) )
138	123, 137	syld 44	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( u e. t -> ( ( u e. t -> u = ( ( f ` u ) i^i S ) ) -> ( w e. u -> ( f : t --> c -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) ) ) )
139	138	com3r 79	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( w e. u -> ( u e. t -> ( ( u e. t -> u = ( ( f ` u ) i^i S ) ) -> ( f : t --> c -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) ) ) )
140	139	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( w e. u /\ u e. t ) -> ( ( u e. t -> u = ( ( f ` u ) i^i S ) ) -> ( f : t --> c -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) ) )
141	140	com3l 81	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( u e. t -> u = ( ( f ` u ) i^i S ) ) -> ( f : t --> c -> ( ( w e. u /\ u e. t ) -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) ) )
142	141	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( f : t --> c /\ ( u e. t -> u = ( ( f ` u ) i^i S ) ) ) -> ( ( w e. u /\ u e. t ) -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) )
143	122, 142	sylan2 471	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> ( ( w e. u /\ u e. t ) -> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) )
144		fvex 5689	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f ` u ) e. _V
145		eleq2 2494	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( v = ( f ` u ) -> ( w e. v <-> w e. ( f ` u ) ) )
146		eleq1 2493	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( v = ( f ` u ) -> ( v e. ran f <-> ( f ` u ) e. ran f ) )
147	145, 146	anbi12d 703	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( v = ( f ` u ) -> ( ( w e. v /\ v e. ran f ) <-> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) )
148	144, 147	spcev 3053	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) -> E. v ( w e. v /\ v e. ran f ) )
149	143, 148	syl6 33	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> ( ( w e. u /\ u e. t ) -> E. v ( w e. v /\ v e. ran f ) ) )
150	149	exlimdv 1689	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> ( E. u ( w e. u /\ u e. t ) -> E. v ( w e. v /\ v e. ran f ) ) )
151		eluni 4082	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w e. U. t <-> E. u ( w e. u /\ u e. t ) )
152		eluni 4082	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w e. U. ran f <-> E. v ( w e. v /\ v e. ran f ) )
153	150, 151, 152	3imtr4g 270	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> ( w e. U. t -> w e. U. ran f ) )
154	153	ssrdv 3350	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> U. t C_ U. ran f )
155	154	adantl 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> U. t C_ U. ran f )
156		sseq1 3365	. . . . . . . . . . . . . . . . . . . 20 |- ( S = U. t -> ( S C_ U. ran f <-> U. t C_ U. ran f ) )
157	156	ad2antlr 719	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> ( S C_ U. ran f <-> U. t C_ U. ran f ) )
158	155, 157	mpbird 232	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> S C_ U. ran f )
159	117, 158	jca 529	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) /\ ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) ) -> ( ran f e. ( ~P c i^i Fin ) /\ S C_ U. ran f ) )
160	159	ex 434	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) -> ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> ( ran f e. ( ~P c i^i Fin ) /\ S C_ U. ran f ) ) )
161	160	eximdv 1675	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) /\ S = U. t ) -> ( E. f ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> E. f ( ran f e. ( ~P c i^i Fin ) /\ S C_ U. ran f ) ) )
162	161	ex 434	. . . . . . . . . . . . . 14 |- ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) -> ( S = U. t -> ( E. f ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> E. f ( ran f e. ( ~P c i^i Fin ) /\ S C_ U. ran f ) ) ) )
163	162	com23 78	. . . . . . . . . . . . 13 |- ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) -> ( E. f ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> ( S = U. t -> E. f ( ran f e. ( ~P c i^i Fin ) /\ S C_ U. ran f ) ) ) )
164		unieq 4087	. . . . . . . . . . . . . . . 16 |- ( d = ran f -> U. d = U. ran f )
165	164	sseq2d 3372	. . . . . . . . . . . . . . 15 |- ( d = ran f -> ( S C_ U. d <-> S C_ U. ran f ) )
166	165	rspcev 3062	. . . . . . . . . . . . . 14 |- ( ( ran f e. ( ~P c i^i Fin ) /\ S C_ U. ran f ) -> E. d e. ( ~P c i^i Fin ) S C_ U. d )
167	166	exlimiv 1687	. . . . . . . . . . . . 13 |- ( E. f ( ran f e. ( ~P c i^i Fin ) /\ S C_ U. ran f ) -> E. d e. ( ~P c i^i Fin ) S C_ U. d )
168	163, 167	syl8 70	. . . . . . . . . . . 12 |- ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) -> ( E. f ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> ( S = U. t -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )
169	98, 168	mpd 15	. . . . . . . . . . 11 |- ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ ( A. s e. t E. y e. c s = ( y i^i S ) /\ t e. Fin ) ) -> ( S = U. t -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) )
170	93, 169	sylan2b 472	. . . . . . . . . 10 |- ( ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) /\ t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) ) -> ( S = U. t -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) )
171	170	rexlimdva 2831	. . . . . . . . 9 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) S = U. t -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) )
172	82, 171	syl5bir 218	. . . . . . . 8 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( ( S = S -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) S = U. t ) -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) )
173	80, 172	sylbird 235	. . . . . . 7 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> ( ( U. ( J ↾t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J ↾t S ) = U. t ) -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) )
174	173	ex 434	. . . . . 6 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( S C_ U. c -> ( ( U. ( J ↾t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J ↾t S ) = U. t ) -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )
175	174	com23 78	. . . . 5 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( ( U. ( J ↾t S ) = U. { x | E. y e. c x = ( y i^i S ) } -> E. t e. ( ~P { x | E. y e. c x = ( y i^i S ) } i^i Fin ) U. ( J ↾t S ) = U. t ) -> ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )
176	54, 175	syld 44	. . . 4 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> ( A. s e. ~P ( J ↾t S ) ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) -> ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )
177	176	ralrimdva 2796	. . 3 |- ( ( J e. Top /\ S C_ X ) -> ( A. s e. ~P ( J ↾t S ) ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) -> A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )
178	4	cmpsublem 18844	. . 3 |- ( ( J e. Top /\ S C_ X ) -> ( A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) -> A. s e. ~P ( J ↾t S ) ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) ) )
179	177, 178	impbid 191	. 2 |- ( ( J e. Top /\ S C_ X ) -> ( A. s e. ~P ( J ↾t S ) ( U. ( J ↾t S ) = U. s -> E. t e. ( ~P s i^i Fin ) U. ( J ↾t S ) = U. t ) <-> A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )
180	13, 179	bitrd 253	1 |- ( ( J e. Top /\ S C_ X ) -> ( ( J ↾t S ) e. Comp <-> A. c e. ~P J ( S C_ U. c -> E. d e. ( ~P c i^i Fin ) S C_ U. d ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 958   = wceq 1362   E.wex 1589   e. wcel 1755   {cab 2419   A.wral 2705   E.wrex 2706   _Vcvv 2962   i^i cin 3315   C_ wss 3316   ~Pcpw 3848   U.cuni 4079   U_ciun 4159   class class class wbr 4280   ran crn 4828   Fn wfn 5401   -->wf 5402   -onto->wfo 5404   ` cfv 5406  (class class class)co 6080   ~<_ cdom 7296   Fincfn 7298   ↾_t crest 14342   Topctop 18340   Compccmp 18831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-om 6466  df-1st 6566  df-2nd 6567  df-recs 6818  df-rdg 6852  df-1o 6908  df-oadd 6912  df-er 7089  df-en 7299  df-dom 7300  df-fin 7302  df-fi 7649  df-rest 14344  df-topgen 14365  df-top 18345  df-bases 18347  df-topon 18348  df-cmp 18832

This theorem is referenced by:  cmpcld  18847  uncmp  18848  hauscmplem  18851  1stckgenlem  18968  icccmp  20244  bndth  20372  ovolicc2  20847  stoweidlem50  29691  stoweidlem57  29698