Theorem cmpsub 18978

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 2438	. . . 4 |- U. ( J ↾t S ) = U. ( J ↾t S )
2	1	iscmp 18966	. . 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 18494	. . . . . 6 |- ( J e. Top -> X e. J )
6		ssexg 4433	. . . . . 6 |- ( ( S C_ X /\ X e. J ) -> S e. _V )
7	3, 5, 6	syl2anr 478	. . . . 5 |- ( ( J e. Top /\ S C_ X ) -> S e. _V )
8		resttop 18739	. . . . 5 |- ( ( J e. Top /\ S e. _V ) -> ( J ↾t S ) e. Top )
9	7, 8	syldan 470	. . . 4 |- ( ( J e. Top /\ S C_ X ) -> ( J ↾t S ) e. Top )
10		ibar 504	. . . . 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 2970	. . . . . . . . . . 11 |- t e. _V
15		eqeq1 2444	. . . . . . . . . . . 12 |- ( x = t -> ( x = ( y i^i S ) <-> t = ( y i^i S ) ) )
16	15	rexbidv 2731	. . . . . . . . . . 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 3101	. . . . . . . . . 10 |- ( t e. { x | E. y e. c x = ( y i^i S ) } <-> E. y e. c t = ( y i^i S ) )
18		selpw 3862	. . . . . . . . . . . . . 14 |- ( c e. ~P J <-> c C_ J )
19		ssel2 3346	. . . . . . . . . . . . . . . 16 |- ( ( c C_ J /\ y e. c ) -> y e. J )
20		ineq1 3540	. . . . . . . . . . . . . . . . . . 19 |- ( d = y -> ( d i^i S ) = ( y i^i S ) )
21	20	eqeq2d 2449	. . . . . . . . . . . . . . . . . 18 |- ( d = y -> ( t = ( d i^i S ) <-> t = ( y i^i S ) ) )
22	21	rspcev 3068	. . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . 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 2835	. . . . . . . . . . 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 753	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> J e. Top )
30	4	sseq2i 3376	. . . . . . . . . . . . . 14 |- ( S C_ X <-> S C_ U. J )
31		uniexg 6372	. . . . . . . . . . . . . . . 16 |- ( J e. Top -> U. J e. _V )
32		ssexg 4433	. . . . . . . . . . . . . . . 16 |- ( ( S C_ U. J /\ U. J e. _V ) -> S e. _V )
33	31, 32	sylan2 474	. . . . . . . . . . . . . . 15 |- ( ( S C_ U. J /\ J e. Top ) -> S e. _V )
34	33	ancoms 453	. . . . . . . . . . . . . 14 |- ( ( J e. Top /\ S C_ U. J ) -> S e. _V )
35	30, 34	sylan2b 475	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ S C_ X ) -> S e. _V )
36	35	adantr 465	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> S e. _V )
37		elrest 14358	. . . . . . . . . . . 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 661	. . . . . . . . . . 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 3357	. . . . . . . 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 2970	. . . . . . . . . 10 |- c e. _V
43	42	abrexex 6546	. . . . . . . . 9 |- { x | E. y e. c x = ( y i^i S ) } e. _V
44	43	elpw 3861	. . . . . . . 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 4094	. . . . . . . . . 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 2449	. . . . . . . . 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 3858	. . . . . . . . . . 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 3546	. . . . . . . . . 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 2919	. . . . . . . . 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 3066	. . . . . . 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 471	. . . . . 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 18741	. . . . . . . . . . 11 |- ( ( J e. Top /\ S C_ X ) -> S = U. ( J ↾t S ) )
56	55	ad2antrr 725	. . . . . . . . . 10 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> S = U. ( J ↾t S ) )
57		vex 2970	. . . . . . . . . . . . . 14 |- y e. _V
58	57	inex1 4428	. . . . . . . . . . . . 13 |- ( y i^i S ) e. _V
59	58	dfiun2 4199	. . . . . . . . . . . 12 |- U_ y e. c ( y i^i S ) = U. { x | E. y e. c x = ( y i^i S ) }
60		incom 3538	. . . . . . . . . . . . . 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 4187	. . . . . . . . . . . 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 2484	. . . . . . . . . . 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 4229	. . . . . . . . . . . 12 |- U_ y e. c ( S i^i y ) = ( S i^i U_ y e. c y )
65		uniiun 4218	. . . . . . . . . . . . . . . 16 |- U. c = U_ y e. c y
66	65	eqcomi 2442	. . . . . . . . . . . . . . 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 3547	. . . . . . . . . . . . 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 3538	. . . . . . . . . . . . . . 15 |- ( S i^i U. c ) = ( U. c i^i S )
70		sseqin2 3564	. . . . . . . . . . . . . . . 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 2482	. . . . . . . . . . . . . 14 |- ( S C_ U. c -> ( S i^i U. c ) = S )
73	72	adantl 466	. . . . . . . . . . . . 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 2470	. . . . . . . . . . . 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 2482	. . . . . . . . . . 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 2471	. . . . . . . . . 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 2452	. . . . . . . . 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 2446	. . . . . . . . . 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 2731	. . . . . . . . 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 2438	. . . . . . . . . 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 3534	. . . . . . . . . . . 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 3862	. . . . . . . . . . . . . 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 3341	. . . . . . . . . . . . . 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 2970	. . . . . . . . . . . . . . . 16 |- s e. _V
87		eqeq1 2444	. . . . . . . . . . . . . . . . 17 |- ( x = s -> ( x = ( y i^i S ) <-> s = ( y i^i S ) ) )
88	87	rexbidv 2731	. . . . . . . . . . . . . . . 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 3101	. . . . . . . . . . . . . . 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 2734	. . . . . . . . . . . . . 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 695	. . . . . . . . . . . 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 3540	. . . . . . . . . . . . . . . 16 |- ( y = ( f ` s ) -> ( y i^i S ) = ( ( f ` s ) i^i S ) )
95	94	eqeq2d 2449	. . . . . . . . . . . . . . 15 |- ( y = ( f ` s ) -> ( s = ( y i^i S ) <-> s = ( ( f ` s ) i^i S ) ) )
96	95	ac6sfi 7548	. . . . . . . . . . . . . 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 453	. . . . . . . . . . . . 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 466	. . . . . . . . . . . 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 5560	. . . . . . . . . . . . . . . . . . . . 21 |- ( f : t --> c -> ran f C_ c )
100	99	ad2antrl 727	. . . . . . . . . . . . . . . . . . . 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 2970	. . . . . . . . . . . . . . . . . . . . . 22 |- f e. _V
102	101	rnex 6507	. . . . . . . . . . . . . . . . . . . . 21 |- ran f e. _V
103	102	elpw 3861	. . . . . . . . . . . . . . . . . . . 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 756	. . . . . . . . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . . . . . 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 5554	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f : t --> c -> f Fn t )
108		dffn4 5621	. . . . . . . . . . . . . . . . . . . . . . . . 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 7582	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( t e. Fin /\ f : t -onto-> ran f ) -> ran f ~<_ t )
111	109, 110	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( t e. Fin /\ f : t --> c ) -> ran f ~<_ t )
112	111	adantll 713	. . . . . . . . . . . . . . . . . . . . . 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 713	. . . . . . . . . . . . . . . . . . . . 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 746	. . . . . . . . . . . . . . . . . . . 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 7526	. . . . . . . . . . . . . . . . . . . 20 |- ( ( t e. Fin /\ ran f ~<_ t ) -> ran f e. Fin )
116	106, 114, 115	syl2anc 661	. . . . . . . . . . . . . . . . . . 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 3535	. . . . . . . . . . . . . . . . . 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 5686	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( s = u -> ( f ` s ) = ( f ` u ) )
120	119	ineq1d 3546	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( s = u -> ( ( f ` s ) i^i S ) = ( ( f ` u ) i^i S ) )
121	118, 120	eqeq12d 2452	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s = u -> ( s = ( ( f ` s ) i^i S ) <-> u = ( ( f ` u ) i^i S ) ) )
122	121	rspccv 3065	. . . . . . . . . . . . . . . . . . . . . . . . 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 3565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( f ` u ) i^i S ) C_ ( f ` u )
125		sseq1 3372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( u e. t /\ u = ( ( f ` u ) i^i S ) /\ w e. u ) -> ( f : t --> c -> w e. ( f ` u ) ) )
132		fnfvelrn 5835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 474	. . . . . . . . . . . . . . . . . . . . . . . 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 5696	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f ` u ) e. _V
145		eleq2 2499	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( v = ( f ` u ) -> ( w e. v <-> w e. ( f ` u ) ) )
146		eleq1 2498	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( v = ( f ` u ) -> ( v e. ran f <-> ( f ` u ) e. ran f ) )
147	145, 146	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( v = ( f ` u ) -> ( ( w e. v /\ v e. ran f ) <-> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) )
148	144, 147	spcev 3059	. . . . . . . . . . . . . . . . . . . . . . . 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 1690	. . . . . . . . . . . . . . . . . . . . . 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 4089	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w e. U. t <-> E. u ( w e. u /\ u e. t ) )
152		eluni 4089	. . . . . . . . . . . . . . . . . . . . . 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 3357	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> U. t C_ U. ran f )
155	154	adantl 466	. . . . . . . . . . . . . . . . . . 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 3372	. . . . . . . . . . . . . . . . . . . 20 |- ( S = U. t -> ( S C_ U. ran f <-> U. t C_ U. ran f ) )
157	156	ad2antlr 726	. . . . . . . . . . . . . . . . . . 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 532	. . . . . . . . . . . . . . . . 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 1676	. . . . . . . . . . . . . . 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 4094	. . . . . . . . . . . . . . . 16 |- ( d = ran f -> U. d = U. ran f )
165	164	sseq2d 3379	. . . . . . . . . . . . . . 15 |- ( d = ran f -> ( S C_ U. d <-> S C_ U. ran f ) )
166	165	rspcev 3068	. . . . . . . . . . . . . 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 1688	. . . . . . . . . . . . 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 475	. . . . . . . . . 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 2836	. . . . . . . . 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 2801	. . 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 18977	. . 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 965   = wceq 1369   E.wex 1586   e. wcel 1756   {cab 2424   A.wral 2710   E.wrex 2711   _Vcvv 2967   i^i cin 3322   C_ wss 3323   ~Pcpw 3855   U.cuni 4086   U_ciun 4166   class class class wbr 4287   ran crn 4836   Fn wfn 5408   -->wf 5409   -onto->wfo 5411   ` cfv 5413  (class class class)co 6086   ~<_ cdom 7300   Fincfn 7302   ↾_t crest 14351   Topctop 18473   Compccmp 18964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-int 4124  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-1st 6572  df-2nd 6573  df-recs 6824  df-rdg 6858  df-1o 6912  df-oadd 6916  df-er 7093  df-en 7303  df-dom 7304  df-fin 7306  df-fi 7653  df-rest 14353  df-topgen 14374  df-top 18478  df-bases 18480  df-topon 18481  df-cmp 18965

This theorem is referenced by:  cmpcld  18980  uncmp  18981  hauscmplem  18984  1stckgenlem  19101  icccmp  20377  bndth  20505  ovolicc2  20980  stoweidlem50  29798  stoweidlem57  29805