Theorem cmpsub 17417

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 2404	. . . 4 |- U. ( J ↾t S ) = U. ( J ↾t S )
2	1	iscmp 17405	. . 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 20	. . . . . 6 |- ( S C_ X -> S C_ X )
4		cmpsub.1	. . . . . . 7 |- X = U. J
5	4	topopn 16934	. . . . . 6 |- ( J e. Top -> X e. J )
6		ssexg 4309	. . . . . 6 |- ( ( S C_ X /\ X e. J ) -> S e. _V )
7	3, 5, 6	syl2anr 465	. . . . 5 |- ( ( J e. Top /\ S C_ X ) -> S e. _V )
8		resttop 17178	. . . . 5 |- ( ( J e. Top /\ S e. _V ) -> ( J ↾t S ) e. Top )
9	7, 8	syldan 457	. . . 4 |- ( ( J e. Top /\ S C_ X ) -> ( J ↾t S ) e. Top )
10		ibar 491	. . . . 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 193	. . . 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 249	. 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 2919	. . . . . . . . . . 11 |- t e. _V
15		eqeq1 2410	. . . . . . . . . . . 12 |- ( x = t -> ( x = ( y i^i S ) <-> t = ( y i^i S ) ) )
16	15	rexbidv 2687	. . . . . . . . . . 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 3042	. . . . . . . . . 10 |- ( t e. { x | E. y e. c x = ( y i^i S ) } <-> E. y e. c t = ( y i^i S ) )
18		vex 2919	. . . . . . . . . . . . . . 15 |- c e. _V
19	18	elpw 3765	. . . . . . . . . . . . . 14 |- ( c e. ~P J <-> c C_ J )
20		ssel2 3303	. . . . . . . . . . . . . . . 16 |- ( ( c C_ J /\ y e. c ) -> y e. J )
21		ineq1 3495	. . . . . . . . . . . . . . . . . . 19 |- ( d = y -> ( d i^i S ) = ( y i^i S ) )
22	21	eqeq2d 2415	. . . . . . . . . . . . . . . . . 18 |- ( d = y -> ( t = ( d i^i S ) <-> t = ( y i^i S ) ) )
23	22	rspcev 3012	. . . . . . . . . . . . . . . . 17 |- ( ( y e. J /\ t = ( y i^i S ) ) -> E. d e. J t = ( d i^i S ) )
24	23	ex 424	. . . . . . . . . . . . . . . 16 |- ( y e. J -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) )
25	20, 24	syl 16	. . . . . . . . . . . . . . 15 |- ( ( c C_ J /\ y e. c ) -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) )
26	25	ex 424	. . . . . . . . . . . . . 14 |- ( c C_ J -> ( y e. c -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) ) )
27	19, 26	sylbi 188	. . . . . . . . . . . . 13 |- ( c e. ~P J -> ( y e. c -> ( t = ( y i^i S ) -> E. d e. J t = ( d i^i S ) ) ) )
28	27	adantl 453	. . . . . . . . . . . 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 ) ) ) )
29	28	rexlimdv 2789	. . . . . . . . . . 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 ) ) )
30		simpll 731	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> J e. Top )
31	4	sseq2i 3333	. . . . . . . . . . . . . 14 |- ( S C_ X <-> S C_ U. J )
32		uniexg 4665	. . . . . . . . . . . . . . . 16 |- ( J e. Top -> U. J e. _V )
33		ssexg 4309	. . . . . . . . . . . . . . . 16 |- ( ( S C_ U. J /\ U. J e. _V ) -> S e. _V )
34	32, 33	sylan2 461	. . . . . . . . . . . . . . 15 |- ( ( S C_ U. J /\ J e. Top ) -> S e. _V )
35	34	ancoms 440	. . . . . . . . . . . . . 14 |- ( ( J e. Top /\ S C_ U. J ) -> S e. _V )
36	31, 35	sylan2b 462	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ S C_ X ) -> S e. _V )
37	36	adantr 452	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) -> S e. _V )
38		elrest 13610	. . . . . . . . . . . 12 |- ( ( J e. Top /\ S e. _V ) -> ( t e. ( J ↾t S ) <-> E. d e. J t = ( d i^i S ) ) )
39	30, 37, 38	syl2anc 643	. . . . . . . . . . 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 ) ) )
40	29, 39	sylibrd 226	. . . . . . . . . 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 ) ) )
41	17, 40	syl5bi 209	. . . . . . . . 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 ) ) )
42	41	ssrdv 3314	. . . . . . . 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 ) )
43	18	abrexex 5942	. . . . . . . . 9 |- { x | E. y e. c x = ( y i^i S ) } e. _V
44	43	elpw 3765	. . . . . . . 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	42, 44	sylibr 204	. . . . . . 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 3984	. . . . . . . . . 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 2415	. . . . . . . . 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 3762	. . . . . . . . . . 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 3501	. . . . . . . . . 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 2871	. . . . . . . . 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 312	. . . . . . . 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 3010	. . . . . . 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 458	. . . . . 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 424	. . . . 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 17180	. . . . . . . . . . 11 |- ( ( J e. Top /\ S C_ X ) -> S = U. ( J ↾t S ) )
56	55	ad2antrr 707	. . . . . . . . . 10 |- ( ( ( ( J e. Top /\ S C_ X ) /\ c e. ~P J ) /\ S C_ U. c ) -> S = U. ( J ↾t S ) )
57		vex 2919	. . . . . . . . . . . . . 14 |- y e. _V
58	57	inex1 4304	. . . . . . . . . . . . 13 |- ( y i^i S ) e. _V
59	58	dfiun2 4085	. . . . . . . . . . . 12 |- U_ y e. c ( y i^i S ) = U. { x | E. y e. c x = ( y i^i S ) }
60		incom 3493	. . . . . . . . . . . . . 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 4074	. . . . . . . . . . . 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 2450	. . . . . . . . . . 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 4115	. . . . . . . . . . . 12 |- U_ y e. c ( S i^i y ) = ( S i^i U_ y e. c y )
65		uniiun 4104	. . . . . . . . . . . . . . . 16 |- U. c = U_ y e. c y
66	65	eqcomi 2408	. . . . . . . . . . . . . . 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 3502	. . . . . . . . . . . . 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 3493	. . . . . . . . . . . . . . 15 |- ( S i^i U. c ) = ( U. c i^i S )
70		sseqin2 3520	. . . . . . . . . . . . . . . 16 |- ( S C_ U. c <-> ( U. c i^i S ) = S )
71	70	biimpi 187	. . . . . . . . . . . . . . 15 |- ( S C_ U. c -> ( U. c i^i S ) = S )
72	69, 71	syl5eq 2448	. . . . . . . . . . . . . 14 |- ( S C_ U. c -> ( S i^i U. c ) = S )
73	72	adantl 453	. . . . . . . . . . . . 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 2436	. . . . . . . . . . . 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 2448	. . . . . . . . . . 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 2437	. . . . . . . . . 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 2418	. . . . . . . . 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 2412	. . . . . . . . . 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 2687	. . . . . . . . 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 312	. . . . . . . 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 2404	. . . . . . . . . 10 |- S = S
82	81	a1bi 328	. . . . . . . . 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 3490	. . . . . . . . . . . 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	14	elpw 3765	. . . . . . . . . . . . . 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 3298	. . . . . . . . . . . . . 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 2919	. . . . . . . . . . . . . . . 16 |- s e. _V
87		eqeq1 2410	. . . . . . . . . . . . . . . . 17 |- ( x = s -> ( x = ( y i^i S ) <-> s = ( y i^i S ) ) )
88	87	rexbidv 2687	. . . . . . . . . . . . . . . 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 3042	. . . . . . . . . . . . . . 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 2690	. . . . . . . . . . . . . 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 263	. . . . . . . . . . . . 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 677	. . . . . . . . . . . 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 241	. . . . . . . . . . 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 3495	. . . . . . . . . . . . . . . 16 |- ( y = ( f ` s ) -> ( y i^i S ) = ( ( f ` s ) i^i S ) )
95	94	eqeq2d 2415	. . . . . . . . . . . . . . 15 |- ( y = ( f ` s ) -> ( s = ( y i^i S ) <-> s = ( ( f ` s ) i^i S ) ) )
96	95	ac6sfi 7310	. . . . . . . . . . . . . 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 440	. . . . . . . . . . . . 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 453	. . . . . . . . . . . 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 5556	. . . . . . . . . . . . . . . . . . . . 21 |- ( f : t --> c -> ran f C_ c )
100	99	ad2antrl 709	. . . . . . . . . . . . . . . . . . . 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 2919	. . . . . . . . . . . . . . . . . . . . . 22 |- f e. _V
102	101	rnex 5092	. . . . . . . . . . . . . . . . . . . . 21 |- ran f e. _V
103	102	elpw 3765	. . . . . . . . . . . . . . . . . . . 20 |- ( ran f e. ~P c <-> ran f C_ c )
104	100, 103	sylibr 204	. . . . . . . . . . . . . . . . . . 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 734	. . . . . . . . . . . . . . . . . . . . 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 707	. . . . . . . . . . . . . . . . . . . 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 5550	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f : t --> c -> f Fn t )
108		dffn4 5618	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f Fn t <-> f : t -onto-> ran f )
109	107, 108	sylib 189	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f : t --> c -> f : t -onto-> ran f )
110		fodomfi 7344	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( t e. Fin /\ f : t -onto-> ran f ) -> ran f ~<_ t )
111	109, 110	sylan2 461	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( t e. Fin /\ f : t --> c ) -> ran f ~<_ t )
112	111	adantll 695	. . . . . . . . . . . . . . . . . . . . . 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 695	. . . . . . . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . . . . . . 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 7289	. . . . . . . . . . . . . . . . . . . 20 |- ( ( t e. Fin /\ ran f ~<_ t ) -> ran f e. Fin )
116	106, 114, 115	syl2anc 643	. . . . . . . . . . . . . . . . . . 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		elin 3490	. . . . . . . . . . . . . . . . . . 19 |- ( ran f e. ( ~P c i^i Fin ) <-> ( ran f e. ~P c /\ ran f e. Fin ) )
118	104, 116, 117	sylanbrc 646	. . . . . . . . . . . . . . . . . 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 ) )
119		id 20	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( s = u -> s = u )
120		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( s = u -> ( f ` s ) = ( f ` u ) )
121	120	ineq1d 3501	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( s = u -> ( ( f ` s ) i^i S ) = ( ( f ` u ) i^i S ) )
122	119, 121	eqeq12d 2418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s = u -> ( s = ( ( f ` s ) i^i S ) <-> u = ( ( f ` u ) i^i S ) ) )
123	122	rspccv 3009	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A. s e. t s = ( ( f ` s ) i^i S ) -> ( u e. t -> u = ( ( f ` u ) i^i S ) ) )
124		pm2.27 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( u e. t -> ( ( u e. t -> u = ( ( f ` u ) i^i S ) ) -> u = ( ( f ` u ) i^i S ) ) )
125		inss1 3521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( f ` u ) i^i S ) C_ ( f ` u )
126		sseq1 3329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( u = ( ( f ` u ) i^i S ) -> ( u C_ ( f ` u ) <-> ( ( f ` u ) i^i S ) C_ ( f ` u ) ) )
127	125, 126	mpbiri 225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( u = ( ( f ` u ) i^i S ) -> u C_ ( f ` u ) )
128		ssel 3302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( u C_ ( f ` u ) -> ( w e. u -> w e. ( f ` u ) ) )
129	128	a1dd 44	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( u C_ ( f ` u ) -> ( w e. u -> ( f : t --> c -> w e. ( f ` u ) ) ) )
130	127, 129	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( u = ( ( f ` u ) i^i S ) -> ( w e. u -> ( f : t --> c -> w e. ( f ` u ) ) ) )
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( u e. t -> ( u = ( ( f ` u ) i^i S ) -> ( w e. u -> ( f : t --> c -> w e. ( f ` u ) ) ) ) )
132	131	3imp 1147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( u e. t /\ u = ( ( f ` u ) i^i S ) /\ w e. u ) -> ( f : t --> c -> w e. ( f ` u ) ) )
133		fnfvelrn 5826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( f Fn t /\ u e. t ) -> ( f ` u ) e. ran f )
134	133	expcom 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( u e. t -> ( f Fn t -> ( f ` u ) e. ran f ) )
135	134	3ad2ant1 978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( u e. t /\ u = ( ( f ` u ) i^i S ) /\ w e. u ) -> ( f Fn t -> ( f ` u ) e. ran f ) )
136	107, 135	syl5 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( u e. t /\ u = ( ( f ` u ) i^i S ) /\ w e. u ) -> ( f : t --> c -> ( f ` u ) e. ran f ) )
137	132, 136	jcad 520	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
138	137	3exp 1152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
139	124, 138	syld 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
140	139	com3r 75	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
141	140	imp 419	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
142	141	com3l 77	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
143	142	impcom 420	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
144	123, 143	sylan2 461	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
145		fvex 5701	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f ` u ) e. _V
146		eleq2 2465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( v = ( f ` u ) -> ( w e. v <-> w e. ( f ` u ) ) )
147		eleq1 2464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( v = ( f ` u ) -> ( v e. ran f <-> ( f ` u ) e. ran f ) )
148	146, 147	anbi12d 692	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( v = ( f ` u ) -> ( ( w e. v /\ v e. ran f ) <-> ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) ) )
149	145, 148	spcev 3003	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( w e. ( f ` u ) /\ ( f ` u ) e. ran f ) -> E. v ( w e. v /\ v e. ran f ) )
150	144, 149	syl6 31	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
151	150	exlimdv 1643	. . . . . . . . . . . . . . . . . . . . . 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 ) ) )
152		eluni 3978	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w e. U. t <-> E. u ( w e. u /\ u e. t ) )
153		eluni 3978	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w e. U. ran f <-> E. v ( w e. v /\ v e. ran f ) )
154	151, 152, 153	3imtr4g 262	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> ( w e. U. t -> w e. U. ran f ) )
155	154	ssrdv 3314	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f : t --> c /\ A. s e. t s = ( ( f ` s ) i^i S ) ) -> U. t C_ U. ran f )
156	155	adantl 453	. . . . . . . . . . . . . . . . . . 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 )
157		sseq1 3329	. . . . . . . . . . . . . . . . . . . 20 |- ( S = U. t -> ( S C_ U. ran f <-> U. t C_ U. ran f ) )
158	157	ad2antlr 708	. . . . . . . . . . . . . . . . . . 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 ) )
159	156, 158	mpbird 224	. . . . . . . . . . . . . . . . . 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 )
160	118, 159	jca 519	. . . . . . . . . . . . . . . . 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 ) )
161	160	ex 424	. . . . . . . . . . . . . . . 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 ) ) )
162	161	eximdv 1629	. . . . . . . . . . . . . . 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 ) ) )
163	162	ex 424	. . . . . . . . . . . . . 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 ) ) ) )
164	163	com23 74	. . . . . . . . . . . . 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 ) ) ) )
165		unieq 3984	. . . . . . . . . . . . . . . 16 |- ( d = ran f -> U. d = U. ran f )
166	165	sseq2d 3336	. . . . . . . . . . . . . . 15 |- ( d = ran f -> ( S C_ U. d <-> S C_ U. ran f ) )
167	166	rspcev 3012	. . . . . . . . . . . . . 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 )
168	167	exlimiv 1641	. . . . . . . . . . . . 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 )
169	164, 168	syl8 67	. . . . . . . . . . . 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 ) ) )
170	98, 169	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 ) )
171	93, 170	sylan2b 462	. . . . . . . . . 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 ) )
172	171	rexlimdva 2790	. . . . . . . . 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 ) )
173	82, 172	syl5bir 210	. . . . . . . 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 ) )
174	80, 173	sylbird 227	. . . . . . 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 ) )
175	174	ex 424	. . . . . 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 ) ) )
176	175	com23 74	. . . . 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 ) ) )
177	54, 176	syld 42	. . . 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 ) ) )
178	177	ralrimdva 2756	. . 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 ) ) )
179	4	cmpsublem 17416	. . 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 ) ) )
180	178, 179	impbid 184	. 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 ) ) )
181	13, 180	bitrd 245	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 177   /\ wa 359   /\ w3a 936   E.wex 1547   = wceq 1649   e. wcel 1721   {cab 2390   A.wral 2666   E.wrex 2667   _Vcvv 2916   i^i cin 3279   C_ wss 3280   ~Pcpw 3759   U.cuni 3975   U_ciun 4053   class class class wbr 4172   ran crn 4838   Fn wfn 5408   -->wf 5409   -onto->wfo 5411   ` cfv 5413  (class class class)co 6040   ~<_ cdom 7066   Fincfn 7068   ↾_t crest 13603   Topctop 16913   Compccmp 17403

This theorem is referenced by:  cmpcld  17419  uncmp  17420  hauscmplem  17423  1stckgenlem  17538  icccmp  18809  bndth  18936  ovolicc2  19371  stoweidlem50  27666  stoweidlem57  27673

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-en 7069  df-dom 7070  df-fin 7072  df-fi 7374  df-rest 13605  df-topgen 13622  df-top 16918  df-bases 16920  df-topon 16921  df-cmp 17404