Theorem cmpsub 20357

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 2428	. . . 4 |- U. ( J ↾t S ) = U. ( J ↾t S )
2	1	iscmp 20345	. . 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 19878	. . . . . 6 |- ( J e. Top -> X e. J )
6		ssexg 4513	. . . . . 6 |- ( ( S C_ X /\ X e. J ) -> S e. _V )
7	3, 5, 6	syl2anr 480	. . . . 5 |- ( ( J e. Top /\ S C_ X ) -> S e. _V )
8		resttop 20118	. . . . 5 |- ( ( J e. Top /\ S e. _V ) -> ( J ↾t S ) e. Top )
9	7, 8	syldan 472	. . . 4 |- ( ( J e. Top /\ S C_ X ) -> ( J ↾t S ) e. Top )
10		ibar 506	. . . . 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 204	. . . 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 17	. . 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 260	. 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 3025	. . . . . . . . . . 11 |- t e. _V
15		eqeq1 2432	. . . . . . . . . . . 12 |- ( x = t -> ( x = ( y i^i S ) <-> t = ( y i^i S ) ) )
16	15	rexbidv 2878	. . . . . . . . . . 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 3160	. . . . . . . . . 10 |- ( t e. { x | E. y e. c x = ( y i^i S ) } <-> E. y e. c t = ( y i^i S ) )
18		selpw 3931	. . . . . . . . . . . . . 14 |- ( c e. ~P J <-> c C_ J )
19		ssel2 3402	. . . . . . . . . . . . . . . 16 |- ( ( c C_ J /\ y e. c ) -> y e. J )
20		ineq1 3600	. . . . . . . . . . . . . . . . . . 19 |- ( d = y -> ( d i^i S ) = ( y i^i S ) )
21	20	eqeq2d 2438	. . . . . . . . . . . . . . . . . 18 |- ( d = y -> ( t = ( d i^i S ) <-> t = ( y i^i S ) ) )
22	21	rspcev 3125	. . . . . . . . . . . . . . . . 17 |- ( ( y e. J /\ t = ( y i^i S ) ) -> E. d e. J t = ( d i^i S ) )
23	22	ex 435	. . . . . . . . . . . . . . . 16 |- ( y e. J -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) )
24	19, 23	syl 17	. . . . . . . . . . . . . . 15 |- ( ( c C_ J /\ y e. c ) -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) )
25	24	ex 435	. . . . . . . . . . . . . 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 198	. . . . . . . . . . . . 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 467	. . . . . . . . . . . 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 2854	. . . . . . . . . . 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 758	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> J e. Top )
30	4	sseq2i 3432	. . . . . . . . . . . . . 14 |- ( S C_ X <-> S C_ U. J )
31		uniexg 6546	. . . . . . . . . . . . . . . 16 |- ( J e. Top -> U. J e. _V )
32		ssexg 4513	. . . . . . . . . . . . . . . 16 |- ( ( S C_ U. J /\ U. J e. _V ) -> S e. _V )
33	31, 32	sylan2 476	. . . . . . . . . . . . . . 15 |- ( ( S C_ U. J /\ J e. Top ) -> S e. _V )
34	33	ancoms 454	. . . . . . . . . . . . . 14 |- ( ( J e. Top /\ S C_ U. J ) -> S e. _V )
35	30, 34	sylan2b 477	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ S C_ X ) -> S e. _V )
36	35	adantr 466	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> S e. _V )
37		elrest 15269	. . . . . . . . . . . 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 665	. . . . . . . . . . 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 237	. . . . . . . . . 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 220	. . . . . . . . 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 3413	. . . . . . . 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 3025	. . . . . . . . . 10 |- c e. _V
43	42	abrexex 6725	. . . . . . . . 9 |- { x | E. y e. c x = ( y i^i S ) } e. _V
44	43	elpw 3930	. . . . . . . 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 215	. . . . . . 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 4170	. . . . . . . . . 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 2438	. . . . . . . . 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 3927	. . . . . . . . . . 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 3606	. . . . . . . . . 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 2971	. . . . . . . . 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 321	. . . . . . . 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 3123	. . . . . . 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 473	. . . . . 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 435	. . . . 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 20120	. . . . . . . . . . 11 |- ( ( J e. Top /\ S C_ X ) -> S = U. ( J ↾t S ) )
56	55	ad2antrr 730	. . . . . . . . . 10 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> S = U. ( J ↾t S ) )
57		vex 3025	. . . . . . . . . . . . . 14 |- y e. _V
58	57	inex1 4508	. . . . . . . . . . . . 13 |- ( y i^i S ) e. _V
59	58	dfiun2 4276	. . . . . . . . . . . 12 |- U_ y e. c ( y i^i S ) = U. { x | E. y e. c x = ( y i^i S ) }
60		incom 3598	. . . . . . . . . . . . . 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 4264	. . . . . . . . . . . 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 2476	. . . . . . . . . . 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 4306	. . . . . . . . . . . 12 |- U_ y e. c ( S i^i y ) = ( S i^i U_ y e. c y )
65		uniiun 4295	. . . . . . . . . . . . . . . 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 3607	. . . . . . . . . . . . 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 3598	. . . . . . . . . . . . . . 15 |- ( S i^i U. c ) = ( U. c i^i S )
70		sseqin2 3624	. . . . . . . . . . . . . . . 16 |- ( S C_ U. c <-> ( U. c i^i S ) = S )
71	70	biimpi 197	. . . . . . . . . . . . . . 15 |- ( S C_ U. c -> ( U. c i^i S ) = S )
72	69, 71	syl5eq 2474	. . . . . . . . . . . . . 14 |- ( S C_ U. c -> ( S i^i U. c ) = S )
73	72	adantl 467	. . . . . . . . . . . . 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 2462	. . . . . . . . . . . 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 2474	. . . . . . . . . . 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 2463	. . . . . . . . . 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 2443	. . . . . . . . 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 2430	. . . . . . . . . 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 2878	. . . . . . . . 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 321	. . . . . . . 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 2428	. . . . . . . . . 10 |- S = S
82	81	a1bi 338	. . . . . . . . 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 3592	. . . . . . . . . . . 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 3931	. . . . . . . . . . . . . 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 3397	. . . . . . . . . . . . . 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 3025	. . . . . . . . . . . . . . . 16 |- s e. _V
87		eqeq1 2432	. . . . . . . . . . . . . . . . 17 |- ( x = s -> ( x = ( y i^i S ) <-> s = ( y i^i S ) ) )
88	87	rexbidv 2878	. . . . . . . . . . . . . . . 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 3160	. . . . . . . . . . . . . . 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 2796	. . . . . . . . . . . . . 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 274	. . . . . . . . . . . . 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 699	. . . . . . . . . . . 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 252	. . . . . . . . . . 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 3600	. . . . . . . . . . . . . . . 16 |- ( y = ( f ` s ) -> ( y i^i S ) = ( ( f ` s ) i^i S ) )
95	94	eqeq2d 2438	. . . . . . . . . . . . . . 15 |- ( y = ( f ` s ) -> ( s = ( y i^i S ) <-> s = ( ( f ` s ) i^i S ) ) )
96	95	ac6sfi 7768	. . . . . . . . . . . . . 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 454	. . . . . . . . . . . . 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 467	. . . . . . . . . . . 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 5695	. . . . . . . . . . . . . . . . . . . . 21 |- ( f : t --> c -> ran f C_ c )
100	99	ad2antrl 732	. . . . . . . . . . . . . . . . . . . 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 3025	. . . . . . . . . . . . . . . . . . . . . 22 |- f e. _V
102	101	rnex 6685	. . . . . . . . . . . . . . . . . . . . 21 |- ran f e. _V
103	102	elpw 3930	. . . . . . . . . . . . . . . . . . . 20 |- ( ran f e. ~P c <-> ran f C_ c )
104	100, 103	sylibr 215	. . . . . . . . . . . . . . . . . . 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 764	. . . . . . . . . . . . . . . . . . . . 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 730	. . . . . . . . . . . . . . . . . . . 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 5689	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f : t --> c -> f Fn t )
108		dffn4 5759	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f Fn t <-> f : t -onto-> ran f )
109	107, 108	sylib 199	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f : t --> c -> f : t -onto-> ran f )
110		fodomfi 7803	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( t e. Fin /\ f : t -onto-> ran f ) -> ran f ~<_ t )
111	109, 110	sylan2 476	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( t e. Fin /\ f : t --> c ) -> ran f ~<_ t )
112	111	adantll 718	. . . . . . . . . . . . . . . . . . . . . 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 718	. . . . . . . . . . . . . . . . . . . . 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 751	. . . . . . . . . . . . . . . . . . . 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 7746	. . . . . . . . . . . . . . . . . . . 20 |- ( ( t e. Fin /\ ran f ~<_ t ) -> ran f e. Fin )
116	106, 114, 115	syl2anc 665	. . . . . . . . . . . . . . . . . . 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 3593	. . . . . . . . . . . . . . . . . 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 5825	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( s = u -> ( f ` s ) = ( f ` u ) )
120	119	ineq1d 3606	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( s = u -> ( ( f ` s ) i^i S ) = ( ( f ` u ) i^i S ) )
121	118, 120	eqeq12d 2443	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s = u -> ( s = ( ( f ` s ) i^i S ) <-> u = ( ( f ` u ) i^i S ) ) )
122	121	rspccv 3122	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A. s e. t s = ( ( f ` s ) i^i S ) -> ( u e. t -> u = ( ( f ` u ) i^i S ) ) )
123		pm2.27 40	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( u e. t -> ( ( u e. t -> u = ( ( f ` u ) i^i S ) ) -> u = ( ( f ` u ) i^i S ) ) )
124		inss1 3625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( f ` u ) i^i S ) C_ ( f ` u )
125		sseq1 3428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( u = ( ( f ` u ) i^i S ) -> ( u C_ ( f ` u ) <-> ( ( f ` u ) i^i S ) C_ ( f ` u ) ) )
126	124, 125	mpbiri 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( u = ( ( f ` u ) i^i S ) -> u C_ ( f ` u ) )
127		ssel 3401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( u C_ ( f ` u ) -> ( w e. u -> w e. ( f ` u ) ) )
128	127	a1dd 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( u C_ ( f ` u ) -> ( w e. u -> ( f : t --> c -> w e. ( f ` u ) ) ) )
129	126, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( u e. t /\ u = ( ( f ` u ) i^i S ) /\ w e. u ) -> ( f : t --> c -> w e. ( f ` u ) ) )
132		fnfvelrn 5978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( f Fn t /\ u e. t ) -> ( f ` u ) e. ran f )
133	132	expcom 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( u e. t -> ( f Fn t -> ( f ` u ) e. ran f ) )
134	133	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 45	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 82	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 430	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 84	. . . . . . . . . . . . . . . . . . . . . . . . . 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 431	. . . . . . . . . . . . . . . . . . . . . . . . 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 476	. . . . . . . . . . . . . . . . . . . . . . . 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 5835	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f ` u ) e. _V
145		eleq2 2495	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( v = ( f ` u ) -> ( w e. v <-> w e. ( f ` u ) ) )
146		eleq1 2494	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( v = ( f ` u ) -> ( v e. ran f <-> ( f ` u ) e. ran f ) )
147	145, 146	anbi12d 715	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( v = ( f ` u ) -> ( ( w e. v /\ v e. ran f ) <-> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) )
148	144, 147	spcev 3116	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) -> E. v ( w e. v /\ v e. ran f ) )
149	143, 148	syl6 34	. . . . . . . . . . . . . . . . . . . . . . 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 1772	. . . . . . . . . . . . . . . . . . . . . 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 4165	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w e. U. t <-> E. u ( w e. u /\ u e. t ) )
152		eluni 4165	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w e. U. ran f <-> E. v ( w e. v /\ v e. ran f ) )
153	150, 151, 152	3imtr4g 273	. . . . . . . . . . . . . . . . . . . . 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 3413	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> U. t C_ U. ran f )
155	154	adantl 467	. . . . . . . . . . . . . . . . . . 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 3428	. . . . . . . . . . . . . . . . . . . 20 |- ( S = U. t -> ( S C_ U. ran f <-> U. t C_ U. ran f ) )
157	156	ad2antlr 731	. . . . . . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . . . . . 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 534	. . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . . 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 1758	. . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . 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 81	. . . . . . . . . . . . 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 4170	. . . . . . . . . . . . . . . 16 |- ( d = ran f -> U. d = U. ran f )
165	164	sseq2d 3435	. . . . . . . . . . . . . . 15 |- ( d = ran f -> ( S C_ U. d <-> S C_ U. ran f ) )
166	165	rspcev 3125	. . . . . . . . . . . . . 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 1770	. . . . . . . . . . . . 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 72	. . . . . . . . . . . 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 477	. . . . . . . . . 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 2856	. . . . . . . . 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 221	. . . . . . . 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 238	. . . . . . 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 435	. . . . . 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 81	. . . . 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 45	. . . 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 2783	. . 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 20356	. . 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 193	. 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 256	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 187   /\ wa 370   /\ w3a 982   = wceq 1437   E.wex 1657   e. wcel 1872   {cab 2414   A.wral 2714   E.wrex 2715   _Vcvv 3022   i^i cin 3378   C_ wss 3379   ~Pcpw 3924   U.cuni 4162   U_ciun 4242   class class class wbr 4366   ran crn 4797   Fn wfn 5539   -->wf 5540   -onto->wfo 5542   ` cfv 5544  (class class class)co 6249   ~<_ cdom 7522   Fincfn 7524   ↾_t crest 15262   Topctop 19859   Compccmp 20343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-reu 2721  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-int 4199  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-om 6651  df-1st 6751  df-2nd 6752  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-1o 7137  df-oadd 7141  df-er 7318  df-en 7525  df-dom 7526  df-fin 7528  df-fi 7878  df-rest 15264  df-topgen 15285  df-top 19863  df-bases 19864  df-topon 19865  df-cmp 20344

This theorem is referenced by:  cmpcld  20359  uncmp  20360  hauscmplem  20363  1stckgenlem  20510  icccmp  21785  bndth  21928  ovolicc2  22418  stoweidlem50  37794  stoweidlem57  37801