Theorem cmpsub 19136

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 2454	. . . 4 |- U. ( J ↾t S ) = U. ( J ↾t S )
2	1	iscmp 19124	. . 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 18652	. . . . . 6 |- ( J e. Top -> X e. J )
6		ssexg 4547	. . . . . 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 18897	. . . . 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 3081	. . . . . . . . . . 11 |- t e. _V
15		eqeq1 2458	. . . . . . . . . . . 12 |- ( x = t -> ( x = ( y i^i S ) <-> t = ( y i^i S ) ) )
16	15	rexbidv 2868	. . . . . . . . . . 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 3213	. . . . . . . . . 10 |- ( t e. { x | E. y e. c x = ( y i^i S ) } <-> E. y e. c t = ( y i^i S ) )
18		selpw 3976	. . . . . . . . . . . . . 14 |- ( c e. ~P J <-> c C_ J )
19		ssel2 3460	. . . . . . . . . . . . . . . 16 |- ( ( c C_ J /\ y e. c ) -> y e. J )
20		ineq1 3654	. . . . . . . . . . . . . . . . . . 19 |- ( d = y -> ( d i^i S ) = ( y i^i S ) )
21	20	eqeq2d 2468	. . . . . . . . . . . . . . . . . 18 |- ( d = y -> ( t = ( d i^i S ) <-> t = ( y i^i S ) ) )
22	21	rspcev 3179	. . . . . . . . . . . . . . . . 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 2946	. . . . . . . . . . 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 3490	. . . . . . . . . . . . . 14 |- ( S C_ X <-> S C_ U. J )
31		uniexg 6488	. . . . . . . . . . . . . . . 16 |- ( J e. Top -> U. J e. _V )
32		ssexg 4547	. . . . . . . . . . . . . . . 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 14486	. . . . . . . . . . . 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 3471	. . . . . . . 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 3081	. . . . . . . . . 10 |- c e. _V
43	42	abrexex 6662	. . . . . . . . 9 |- { x | E. y e. c x = ( y i^i S ) } e. _V
44	43	elpw 3975	. . . . . . . 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 4208	. . . . . . . . . 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 2468	. . . . . . . . 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 3972	. . . . . . . . . . 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 3660	. . . . . . . . . 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 3030	. . . . . . . . 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 3177	. . . . . . 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 18899	. . . . . . . . . . 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 3081	. . . . . . . . . . . . . 14 |- y e. _V
58	57	inex1 4542	. . . . . . . . . . . . 13 |- ( y i^i S ) e. _V
59	58	dfiun2 4313	. . . . . . . . . . . 12 |- U_ y e. c ( y i^i S ) = U. { x | E. y e. c x = ( y i^i S ) }
60		incom 3652	. . . . . . . . . . . . . 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 4301	. . . . . . . . . . . 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 2509	. . . . . . . . . . 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 4343	. . . . . . . . . . . 12 |- U_ y e. c ( S i^i y ) = ( S i^i U_ y e. c y )
65		uniiun 4332	. . . . . . . . . . . . . . . 16 |- U. c = U_ y e. c y
66	65	eqcomi 2467	. . . . . . . . . . . . . . 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 3661	. . . . . . . . . . . . 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 3652	. . . . . . . . . . . . . . 15 |- ( S i^i U. c ) = ( U. c i^i S )
70		sseqin2 3678	. . . . . . . . . . . . . . . 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 2507	. . . . . . . . . . . . . 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 2495	. . . . . . . . . . . 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 2507	. . . . . . . . . . 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 2496	. . . . . . . . . 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 2476	. . . . . . . . 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 2456	. . . . . . . . . 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 2868	. . . . . . . . 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 2454	. . . . . . . . . 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 3648	. . . . . . . . . . . 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 3976	. . . . . . . . . . . . . 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 3455	. . . . . . . . . . . . . 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 3081	. . . . . . . . . . . . . . . 16 |- s e. _V
87		eqeq1 2458	. . . . . . . . . . . . . . . . 17 |- ( x = s -> ( x = ( y i^i S ) <-> s = ( y i^i S ) ) )
88	87	rexbidv 2868	. . . . . . . . . . . . . . . 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 3213	. . . . . . . . . . . . . . 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 2839	. . . . . . . . . . . . . 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 3654	. . . . . . . . . . . . . . . 16 |- ( y = ( f ` s ) -> ( y i^i S ) = ( ( f ` s ) i^i S ) )
95	94	eqeq2d 2468	. . . . . . . . . . . . . . 15 |- ( y = ( f ` s ) -> ( s = ( y i^i S ) <-> s = ( ( f ` s ) i^i S ) ) )
96	95	ac6sfi 7668	. . . . . . . . . . . . . 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 5674	. . . . . . . . . . . . . . . . . . . . 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 3081	. . . . . . . . . . . . . . . . . . . . . 22 |- f e. _V
102	101	rnex 6623	. . . . . . . . . . . . . . . . . . . . 21 |- ran f e. _V
103	102	elpw 3975	. . . . . . . . . . . . . . . . . . . 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 5668	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f : t --> c -> f Fn t )
108		dffn4 5735	. . . . . . . . . . . . . . . . . . . . . . . . 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 7702	. . . . . . . . . . . . . . . . . . . . . . . 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 7646	. . . . . . . . . . . . . . . . . . . 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 3649	. . . . . . . . . . . . . . . . . 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 5800	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( s = u -> ( f ` s ) = ( f ` u ) )
120	119	ineq1d 3660	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( s = u -> ( ( f ` s ) i^i S ) = ( ( f ` u ) i^i S ) )
121	118, 120	eqeq12d 2476	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s = u -> ( s = ( ( f ` s ) i^i S ) <-> u = ( ( f ` u ) i^i S ) ) )
122	121	rspccv 3176	. . . . . . . . . . . . . . . . . . . . . . . . 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 3679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( f ` u ) i^i S ) C_ ( f ` u )
125		sseq1 3486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( u e. t /\ u = ( ( f ` u ) i^i S ) /\ w e. u ) -> ( f : t --> c -> w e. ( f ` u ) ) )
132		fnfvelrn 5950	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5810	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f ` u ) e. _V
145		eleq2 2527	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( v = ( f ` u ) -> ( w e. v <-> w e. ( f ` u ) ) )
146		eleq1 2526	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3170	. . . . . . . . . . . . . . . . . . . . . . . 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 1691	. . . . . . . . . . . . . . . . . . . . . 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 4203	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w e. U. t <-> E. u ( w e. u /\ u e. t ) )
152		eluni 4203	. . . . . . . . . . . . . . . . . . . . . 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 3471	. . . . . . . . . . . . . . . . . . . 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 3486	. . . . . . . . . . . . . . . . . . . 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 1677	. . . . . . . . . . . . . . 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 4208	. . . . . . . . . . . . . . . 16 |- ( d = ran f -> U. d = U. ran f )
165	164	sseq2d 3493	. . . . . . . . . . . . . . 15 |- ( d = ran f -> ( S C_ U. d <-> S C_ U. ran f ) )
166	165	rspcev 3179	. . . . . . . . . . . . . 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 1689	. . . . . . . . . . . . 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 2947	. . . . . . . . 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 2912	. . 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 19135	. . 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 1370   E.wex 1587   e. wcel 1758   {cab 2439   A.wral 2799   E.wrex 2800   _Vcvv 3078   i^i cin 3436   C_ wss 3437   ~Pcpw 3969   U.cuni 4200   U_ciun 4280   class class class wbr 4401   ran crn 4950   Fn wfn 5522   -->wf 5523   -onto->wfo 5525   ` cfv 5527  (class class class)co 6201   ~<_ cdom 7419   Fincfn 7421   ↾_t crest 14479   Topctop 18631   Compccmp 19122

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4512  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640  ax-un 6483

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-tp 3991  df-op 3993  df-uni 4201  df-int 4238  df-iun 4282  df-br 4402  df-opab 4460  df-mpt 4461  df-tr 4495  df-eprel 4741  df-id 4745  df-po 4750  df-so 4751  df-fr 4788  df-we 4790  df-ord 4831  df-on 4832  df-lim 4833  df-suc 4834  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-f 5531  df-f1 5532  df-fo 5533  df-f1o 5534  df-fv 5535  df-ov 6204  df-oprab 6205  df-mpt2 6206  df-om 6588  df-1st 6688  df-2nd 6689  df-recs 6943  df-rdg 6977  df-1o 7031  df-oadd 7035  df-er 7212  df-en 7422  df-dom 7423  df-fin 7425  df-fi 7773  df-rest 14481  df-topgen 14502  df-top 18636  df-bases 18638  df-topon 18639  df-cmp 19123

This theorem is referenced by:  cmpcld  19138  uncmp  19139  hauscmplem  19142  1stckgenlem  19259  icccmp  20535  bndth  20663  ovolicc2  21138  stoweidlem50  29994  stoweidlem57  30001