Theorem cmpfi 19011

Description: If a topology is compact and a collection of closed sets has the finite intersection property, its intersection is nonempty. (Contributed by Jeff Hankins, 25-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)

Assertion

Ref	Expression
cmpfi	|- ( J e. Top -> ( J e. Comp <-> A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) ) )

Distinct variable group:   x, J

Proof of Theorem cmpfi

Dummy variables r v w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpwi 3869	. . . 4 |- ( y e. ~P J -> y C_ J )
2		0ss 3666	. . . . . . . . . . 11 |- (/) C_ y
3		0fin 7540	. . . . . . . . . . 11 |- (/) e. Fin
4		elfpw 7613	. . . . . . . . . . 11 |- ( (/) e. ( ~P y i^i Fin ) <-> ( (/) C_ y /\ (/) e. Fin ) )
5	2, 3, 4	mpbir2an 911	. . . . . . . . . 10 |- (/) e. ( ~P y i^i Fin )
6		simprr 756	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. J = U. y )
7		simprl 755	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> y = (/) )
8	7	unieqd 4101	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. y = U. (/) )
9	6, 8	eqtrd 2475	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. J = U. (/) )
10		unieq 4099	. . . . . . . . . . . 12 |- ( z = (/) -> U. z = U. (/) )
11	10	eqeq2d 2454	. . . . . . . . . . 11 |- ( z = (/) -> ( U. J = U. z <-> U. J = U. (/) ) )
12	11	rspcev 3073	. . . . . . . . . 10 |- ( ( (/) e. ( ~P y i^i Fin ) /\ U. J = U. (/) ) -> E. z e. ( ~P y i^i Fin ) U. J = U. z )
13	5, 9, 12	sylancr 663	. . . . . . . . 9 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> E. z e. ( ~P y i^i Fin ) U. J = U. z )
14	13	expr 615	. . . . . . . 8 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) )
15		vn0 3644	. . . . . . . . . 10 |- _V =/= (/)
16		iineq1 4185	. . . . . . . . . . . . . 14 |- ( y = (/) -> |^|_ r e. y ( U. J \ r ) = |^|_ r e. (/) ( U. J \ r ) )
17	16	adantl 466	. . . . . . . . . . . . 13 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> |^|_ r e. y ( U. J \ r ) = |^|_ r e. (/) ( U. J \ r ) )
18		0iin 4228	. . . . . . . . . . . . 13 |- |^|_ r e. (/) ( U. J \ r ) = _V
19	17, 18	syl6eq 2491	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> |^|_ r e. y ( U. J \ r ) = _V )
20	19	eqeq1d 2451	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> _V = (/) ) )
21	20	necon3bbid 2642	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> ( -. |^|_ r e. y ( U. J \ r ) = (/) <-> _V =/= (/) ) )
22	15, 21	mpbiri 233	. . . . . . . . 9 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> -. |^|_ r e. y ( U. J \ r ) = (/) )
23	22	pm2.21d 106	. . . . . . . 8 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> ( |^|_ r e. y ( U. J \ r ) = (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) )
24	14, 23	2thd 240	. . . . . . 7 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> ( ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) <-> ( |^|_ r e. y ( U. J \ r ) = (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) ) )
25		uniss 4112	. . . . . . . . . . . 12 |- ( y C_ J -> U. y C_ U. J )
26	25	ad2antlr 726	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> U. y C_ U. J )
27		eqss 3371	. . . . . . . . . . . 12 |- ( U. y = U. J <-> ( U. y C_ U. J /\ U. J C_ U. y ) )
28	27	baib 896	. . . . . . . . . . 11 |- ( U. y C_ U. J -> ( U. y = U. J <-> U. J C_ U. y ) )
29	26, 28	syl 16	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( U. y = U. J <-> U. J C_ U. y ) )
30		eqcom 2445	. . . . . . . . . 10 |- ( U. y = U. J <-> U. J = U. y )
31		ssdif0 3737	. . . . . . . . . 10 |- ( U. J C_ U. y <-> ( U. J \ U. y ) = (/) )
32	29, 30, 31	3bitr3g 287	. . . . . . . . 9 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( U. J = U. y <-> ( U. J \ U. y ) = (/) ) )
33		iindif2 4239	. . . . . . . . . . . 12 |- ( y =/= (/) -> |^|_ r e. y ( U. J \ r ) = ( U. J \ U_ r e. y r ) )
34	33	adantl 466	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> |^|_ r e. y ( U. J \ r ) = ( U. J \ U_ r e. y r ) )
35		uniiun 4223	. . . . . . . . . . . 12 |- U. y = U_ r e. y r
36	35	difeq2i 3471	. . . . . . . . . . 11 |- ( U. J \ U. y ) = ( U. J \ U_ r e. y r )
37	34, 36	syl6eqr 2493	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> |^|_ r e. y ( U. J \ r ) = ( U. J \ U. y ) )
38	37	eqeq1d 2451	. . . . . . . . 9 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> ( U. J \ U. y ) = (/) ) )
39	32, 38	bitr4d 256	. . . . . . . 8 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( U. J = U. y <-> |^|_ r e. y ( U. J \ r ) = (/) ) )
40		imassrn 5180	. . . . . . . . . . . 12 |- ( ( r e. y |-> ( U. J \ r ) ) " z ) C_ ran ( r e. y |-> ( U. J \ r ) )
41		df-ima 4853	. . . . . . . . . . . . . 14 |- ( ( r e. J |-> ( U. J \ r ) ) " y ) = ran ( ( r e. J |-> ( U. J \ r ) ) |` y )
42		resmpt 5156	. . . . . . . . . . . . . . . 16 |- ( y C_ J -> ( ( r e. J |-> ( U. J \ r ) ) |` y ) = ( r e. y |-> ( U. J \ r ) ) )
43	42	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( J e. Top /\ y C_ J ) -> ( ( r e. J |-> ( U. J \ r ) ) |` y ) = ( r e. y |-> ( U. J \ r ) ) )
44	43	rneqd 5067	. . . . . . . . . . . . . 14 |- ( ( J e. Top /\ y C_ J ) -> ran ( ( r e. J |-> ( U. J \ r ) ) |` y ) = ran ( r e. y |-> ( U. J \ r ) ) )
45	41, 44	syl5eq 2487	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ y C_ J ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) = ran ( r e. y |-> ( U. J \ r ) ) )
46	45	ad2antrr 725	. . . . . . . . . . . 12 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ~P y i^i Fin ) ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) = ran ( r e. y |-> ( U. J \ r ) ) )
47	40, 46	syl5sseqr 3405	. . . . . . . . . . 11 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ~P y i^i Fin ) ) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) C_ ( ( r e. J |-> ( U. J \ r ) ) " y ) )
48		funmpt 5454	. . . . . . . . . . . 12 |- Fun ( r e. y |-> ( U. J \ r ) )
49		elfpw 7613	. . . . . . . . . . . . . 14 |- ( z e. ( ~P y i^i Fin ) <-> ( z C_ y /\ z e. Fin ) )
50	49	simprbi 464	. . . . . . . . . . . . 13 |- ( z e. ( ~P y i^i Fin ) -> z e. Fin )
51	50	adantl 466	. . . . . . . . . . . 12 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ~P y i^i Fin ) ) -> z e. Fin )
52		imafi 7604	. . . . . . . . . . . 12 |- ( ( Fun ( r e. y |-> ( U. J \ r ) ) /\ z e. Fin ) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) e. Fin )
53	48, 51, 52	sylancr 663	. . . . . . . . . . 11 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ~P y i^i Fin ) ) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) e. Fin )
54		elfpw 7613	. . . . . . . . . . 11 |- ( ( ( r e. y |-> ( U. J \ r ) ) " z ) e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) <-> ( ( ( r e. y |-> ( U. J \ r ) ) " z ) C_ ( ( r e. J |-> ( U. J \ r ) ) " y ) /\ ( ( r e. y |-> ( U. J \ r ) ) " z ) e. Fin ) )
55	47, 53, 54	sylanbrc 664	. . . . . . . . . 10 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ~P y i^i Fin ) ) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) )
56		eqid 2443	. . . . . . . . . . . . . . . . 17 |- U. J = U. J
57	56	topopn 18519	. . . . . . . . . . . . . . . 16 |- ( J e. Top -> U. J e. J )
58		difexg 4440	. . . . . . . . . . . . . . . 16 |- ( U. J e. J -> ( U. J \ r ) e. _V )
59	57, 58	syl 16	. . . . . . . . . . . . . . 15 |- ( J e. Top -> ( U. J \ r ) e. _V )
60	59	ralrimivw 2800	. . . . . . . . . . . . . 14 |- ( J e. Top -> A. r e. y ( U. J \ r ) e. _V )
61		eqid 2443	. . . . . . . . . . . . . . 15 |- ( r e. y |-> ( U. J \ r ) ) = ( r e. y |-> ( U. J \ r ) )
62	61	fnmpt 5537	. . . . . . . . . . . . . 14 |- ( A. r e. y ( U. J \ r ) e. _V -> ( r e. y |-> ( U. J \ r ) ) Fn y )
63	60, 62	syl 16	. . . . . . . . . . . . 13 |- ( J e. Top -> ( r e. y |-> ( U. J \ r ) ) Fn y )
64	63	ad3antrrr 729	. . . . . . . . . . . 12 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> ( r e. y |-> ( U. J \ r ) ) Fn y )
65		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) )
66		elfpw 7613	. . . . . . . . . . . . . . 15 |- ( w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) <-> ( w C_ ( ( r e. J |-> ( U. J \ r ) ) " y ) /\ w e. Fin ) )
67	65, 66	sylib 196	. . . . . . . . . . . . . 14 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> ( w C_ ( ( r e. J |-> ( U. J \ r ) ) " y ) /\ w e. Fin ) )
68	67	simpld 459	. . . . . . . . . . . . 13 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> w C_ ( ( r e. J |-> ( U. J \ r ) ) " y ) )
69	45	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) = ran ( r e. y |-> ( U. J \ r ) ) )
70	68, 69	sseqtrd 3392	. . . . . . . . . . . 12 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> w C_ ran ( r e. y |-> ( U. J \ r ) ) )
71	67	simprd 463	. . . . . . . . . . . 12 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> w e. Fin )
72		fipreima 7617	. . . . . . . . . . . 12 |- ( ( ( r e. y |-> ( U. J \ r ) ) Fn y /\ w C_ ran ( r e. y |-> ( U. J \ r ) ) /\ w e. Fin ) -> E. z e. ( ~P y i^i Fin ) ( ( r e. y |-> ( U. J \ r ) ) " z ) = w )
73	64, 70, 71, 72	syl3anc 1218	. . . . . . . . . . 11 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> E. z e. ( ~P y i^i Fin ) ( ( r e. y |-> ( U. J \ r ) ) " z ) = w )
74		eqcom 2445	. . . . . . . . . . . 12 |- ( ( ( r e. y |-> ( U. J \ r ) ) " z ) = w <-> w = ( ( r e. y |-> ( U. J \ r ) ) " z ) )
75	74	rexbii 2740	. . . . . . . . . . 11 |- ( E. z e. ( ~P y i^i Fin ) ( ( r e. y |-> ( U. J \ r ) ) " z ) = w <-> E. z e. ( ~P y i^i Fin ) w = ( ( r e. y |-> ( U. J \ r ) ) " z ) )
76	73, 75	sylib 196	. . . . . . . . . 10 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> E. z e. ( ~P y i^i Fin ) w = ( ( r e. y |-> ( U. J \ r ) ) " z ) )
77		simpr 461	. . . . . . . . . . . 12 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w = ( ( r e. y |-> ( U. J \ r ) ) " z ) ) -> w = ( ( r e. y |-> ( U. J \ r ) ) " z ) )
78	77	inteqd 4133	. . . . . . . . . . 11 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w = ( ( r e. y |-> ( U. J \ r ) ) " z ) ) -> |^| w = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) )
79	78	eqeq2d 2454	. . . . . . . . . 10 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w = ( ( r e. y |-> ( U. J \ r ) ) " z ) ) -> ( (/) = |^| w <-> (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) )
80	55, 76, 79	rexxfrd 4507	. . . . . . . . 9 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) (/) = |^| w <-> E. z e. ( ~P y i^i Fin ) (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) )
81		0ex 4422	. . . . . . . . . 10 |- (/) e. _V
82		imassrn 5180	. . . . . . . . . . . . 13 |- ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ran ( r e. J |-> ( U. J \ r ) )
83		eqid 2443	. . . . . . . . . . . . . . . . 17 |- ( r e. J |-> ( U. J \ r ) ) = ( r e. J |-> ( U. J \ r ) )
84	56, 83	opncldf1 18688	. . . . . . . . . . . . . . . 16 |- ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) : J -1-1-onto-> ( Clsd ` J ) /\ `' ( r e. J |-> ( U. J \ r ) ) = ( v e. ( Clsd ` J ) |-> ( U. J \ v ) ) ) )
85	84	simpld 459	. . . . . . . . . . . . . . 15 |- ( J e. Top -> ( r e. J |-> ( U. J \ r ) ) : J -1-1-onto-> ( Clsd ` J ) )
86		f1ofo 5648	. . . . . . . . . . . . . . 15 |- ( ( r e. J |-> ( U. J \ r ) ) : J -1-1-onto-> ( Clsd ` J ) -> ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) )
87	85, 86	syl 16	. . . . . . . . . . . . . 14 |- ( J e. Top -> ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) )
88		forn 5623	. . . . . . . . . . . . . 14 |- ( ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) -> ran ( r e. J |-> ( U. J \ r ) ) = ( Clsd ` J ) )
89	87, 88	syl 16	. . . . . . . . . . . . 13 |- ( J e. Top -> ran ( r e. J |-> ( U. J \ r ) ) = ( Clsd ` J ) )
90	82, 89	syl5sseq 3404	. . . . . . . . . . . 12 |- ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ( Clsd ` J ) )
91		fvex 5701	. . . . . . . . . . . . 13 |- ( Clsd ` J ) e. _V
92	91	elpw2 4456	. . . . . . . . . . . 12 |- ( ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) <-> ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ( Clsd ` J ) )
93	90, 92	sylibr 212	. . . . . . . . . . 11 |- ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) )
94	93	ad2antrr 725	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) )
95		elfi 7663	. . . . . . . . . 10 |- ( ( (/) e. _V /\ ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) ) -> ( (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) <-> E. w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) (/) = |^| w ) )
96	81, 94, 95	sylancr 663	. . . . . . . . 9 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) <-> E. w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) (/) = |^| w ) )
97		inundif 3757	. . . . . . . . . . . . . 14 |- ( ( ( ~P y i^i Fin ) i^i { (/) } ) u. ( ( ~P y i^i Fin ) \ { (/) } ) ) = ( ~P y i^i Fin )
98	97	rexeqi 2922	. . . . . . . . . . . . 13 |- ( E. z e. ( ( ( ~P y i^i Fin ) i^i { (/) } ) u. ( ( ~P y i^i Fin ) \ { (/) } ) ) U. J = U. z <-> E. z e. ( ~P y i^i Fin ) U. J = U. z )
99		rexun 3536	. . . . . . . . . . . . 13 |- ( E. z e. ( ( ( ~P y i^i Fin ) i^i { (/) } ) u. ( ( ~P y i^i Fin ) \ { (/) } ) ) U. J = U. z <-> ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z \/ E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
100	98, 99	bitr3i 251	. . . . . . . . . . . 12 |- ( E. z e. ( ~P y i^i Fin ) U. J = U. z <-> ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z \/ E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
101		inss2 3571	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ~P y i^i Fin ) i^i { (/) } ) C_ { (/) }
102	101	sseli 3352	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> z e. { (/) } )
103		elsni 3902	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. { (/) } -> z = (/) )
104	102, 103	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> z = (/) )
105	104	unieqd 4101	. . . . . . . . . . . . . . . . . . 19 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> U. z = U. (/) )
106		uni0 4118	. . . . . . . . . . . . . . . . . . 19 |- U. (/) = (/)
107	105, 106	syl6eq 2491	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> U. z = (/) )
108	107	eqeq2d 2454	. . . . . . . . . . . . . . . . 17 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> ( U. J = U. z <-> U. J = (/) ) )
109	108	biimpd 207	. . . . . . . . . . . . . . . 16 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> ( U. J = U. z -> U. J = (/) ) )
110	109	rexlimiv 2835	. . . . . . . . . . . . . . 15 |- ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z -> U. J = (/) )
111		ssid 3375	. . . . . . . . . . . . . . . . . . . 20 |- y C_ y
112	111	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y C_ y )
113		simprr 756	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J = (/) )
114		0ss 3666	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (/) C_ U. y
115	113, 114	syl6eqss 3406	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J C_ U. y )
116	25	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y C_ U. J )
117	115, 116	eqssd 3373	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J = U. y )
118	117, 113	eqtr3d 2477	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y = (/) )
119	118, 3	syl6eqel 2531	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y e. Fin )
120		pwfi 7606	. . . . . . . . . . . . . . . . . . . . 21 |- ( U. y e. Fin <-> ~P U. y e. Fin )
121	119, 120	sylib 196	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> ~P U. y e. Fin )
122		pwuni 4523	. . . . . . . . . . . . . . . . . . . 20 |- y C_ ~P U. y
123		ssfi 7533	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ~P U. y e. Fin /\ y C_ ~P U. y ) -> y e. Fin )
124	121, 122, 123	sylancl 662	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y e. Fin )
125		elfpw 7613	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( ~P y i^i Fin ) <-> ( y C_ y /\ y e. Fin ) )
126	112, 124, 125	sylanbrc 664	. . . . . . . . . . . . . . . . . 18 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y e. ( ~P y i^i Fin ) )
127		simprl 755	. . . . . . . . . . . . . . . . . 18 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y =/= (/) )
128		eldifsn 4000	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( ( ~P y i^i Fin ) \ { (/) } ) <-> ( y e. ( ~P y i^i Fin ) /\ y =/= (/) ) )
129	126, 127, 128	sylanbrc 664	. . . . . . . . . . . . . . . . 17 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y e. ( ( ~P y i^i Fin ) \ { (/) } ) )
130		unieq 4099	. . . . . . . . . . . . . . . . . . 19 |- ( z = y -> U. z = U. y )
131	130	eqeq2d 2454	. . . . . . . . . . . . . . . . . 18 |- ( z = y -> ( U. J = U. z <-> U. J = U. y ) )
132	131	rspcev 3073	. . . . . . . . . . . . . . . . 17 |- ( ( y e. ( ( ~P y i^i Fin ) \ { (/) } ) /\ U. J = U. y ) -> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z )
133	129, 117, 132	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z )
134	133	expr 615	. . . . . . . . . . . . . . 15 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( U. J = (/) -> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
135	110, 134	syl5 32	. . . . . . . . . . . . . 14 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z -> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
136		idd 24	. . . . . . . . . . . . . 14 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z -> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
137	135, 136	jaod 380	. . . . . . . . . . . . 13 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z \/ E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) -> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
138		olc 384	. . . . . . . . . . . . 13 |- ( E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z -> ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z \/ E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
139	137, 138	impbid1 203	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z \/ E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) <-> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
140	100, 139	syl5bb 257	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. z e. ( ~P y i^i Fin ) U. J = U. z <-> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
141		eldifi 3478	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) -> z e. ( ~P y i^i Fin ) )
142	141	adantl 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z e. ( ~P y i^i Fin ) )
143	142, 49	sylib 196	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( z C_ y /\ z e. Fin ) )
144	143	simpld 459	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z C_ y )
145		simpllr 758	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> y C_ J )
146	144, 145	sstrd 3366	. . . . . . . . . . . . . . . 16 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z C_ J )
147	146	unissd 4115	. . . . . . . . . . . . . . 15 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> U. z C_ U. J )
148		eqss 3371	. . . . . . . . . . . . . . . 16 |- ( U. z = U. J <-> ( U. z C_ U. J /\ U. J C_ U. z ) )
149	148	baib 896	. . . . . . . . . . . . . . 15 |- ( U. z C_ U. J -> ( U. z = U. J <-> U. J C_ U. z ) )
150	147, 149	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( U. z = U. J <-> U. J C_ U. z ) )
151		eqcom 2445	. . . . . . . . . . . . . 14 |- ( U. z = U. J <-> U. J = U. z )
152		ssdif0 3737	. . . . . . . . . . . . . . 15 |- ( U. J C_ U. z <-> ( U. J \ U. z ) = (/) )
153		eqcom 2445	. . . . . . . . . . . . . . 15 |- ( ( U. J \ U. z ) = (/) <-> (/) = ( U. J \ U. z ) )
154	152, 153	bitri 249	. . . . . . . . . . . . . 14 |- ( U. J C_ U. z <-> (/) = ( U. J \ U. z ) )
155	150, 151, 154	3bitr3g 287	. . . . . . . . . . . . 13 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( U. J = U. z <-> (/) = ( U. J \ U. z ) ) )
156		df-ima 4853	. . . . . . . . . . . . . . . . . 18 |- ( ( r e. y |-> ( U. J \ r ) ) " z ) = ran ( ( r e. y |-> ( U. J \ r ) ) |` z )
157		resmpt 5156	. . . . . . . . . . . . . . . . . . . 20 |- ( z C_ y -> ( ( r e. y |-> ( U. J \ r ) ) |` z ) = ( r e. z |-> ( U. J \ r ) ) )
158	144, 157	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( ( r e. y |-> ( U. J \ r ) ) |` z ) = ( r e. z |-> ( U. J \ r ) ) )
159	158	rneqd 5067	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ran ( ( r e. y |-> ( U. J \ r ) ) |` z ) = ran ( r e. z |-> ( U. J \ r ) ) )
160	156, 159	syl5eq 2487	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = ran ( r e. z |-> ( U. J \ r ) ) )
161	160	inteqd 4133	. . . . . . . . . . . . . . . 16 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = |^| ran ( r e. z |-> ( U. J \ r ) ) )
162	59	ralrimivw 2800	. . . . . . . . . . . . . . . . . 18 |- ( J e. Top -> A. r e. z ( U. J \ r ) e. _V )
163	162	ad3antrrr 729	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> A. r e. z ( U. J \ r ) e. _V )
164		dfiin3g 5093	. . . . . . . . . . . . . . . . 17 |- ( A. r e. z ( U. J \ r ) e. _V -> |^|_ r e. z ( U. J \ r ) = |^| ran ( r e. z |-> ( U. J \ r ) ) )
165	163, 164	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> |^|_ r e. z ( U. J \ r ) = |^| ran ( r e. z |-> ( U. J \ r ) ) )
166		eldifsn 4000	. . . . . . . . . . . . . . . . . . 19 |- ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) <-> ( z e. ( ~P y i^i Fin ) /\ z =/= (/) ) )
167	166	simprbi 464	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) -> z =/= (/) )
168	167	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z =/= (/) )
169		iindif2 4239	. . . . . . . . . . . . . . . . 17 |- ( z =/= (/) -> |^|_ r e. z ( U. J \ r ) = ( U. J \ U_ r e. z r ) )
170	168, 169	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> |^|_ r e. z ( U. J \ r ) = ( U. J \ U_ r e. z r ) )
171	161, 165, 170	3eqtr2d 2481	. . . . . . . . . . . . . . 15 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = ( U. J \ U_ r e. z r ) )
172		uniiun 4223	. . . . . . . . . . . . . . . 16 |- U. z = U_ r e. z r
173	172	difeq2i 3471	. . . . . . . . . . . . . . 15 |- ( U. J \ U. z ) = ( U. J \ U_ r e. z r )
174	171, 173	syl6eqr 2493	. . . . . . . . . . . . . 14 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = ( U. J \ U. z ) )
175	174	eqeq2d 2454	. . . . . . . . . . . . 13 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) <-> (/) = ( U. J \ U. z ) ) )
176	155, 175	bitr4d 256	. . . . . . . . . . . 12 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( U. J = U. z <-> (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) )
177	176	rexbidva 2732	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z <-> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) )
178	140, 177	bitrd 253	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. z e. ( ~P y i^i Fin ) U. J = U. z <-> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) )
179		imaeq2 5165	. . . . . . . . . . . . . . . . . . . 20 |- ( z = (/) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = ( ( r e. y |-> ( U. J \ r ) ) " (/) ) )
180		ima0 5184	. . . . . . . . . . . . . . . . . . . 20 |- ( ( r e. y |-> ( U. J \ r ) ) " (/) ) = (/)
181	179, 180	syl6eq 2491	. . . . . . . . . . . . . . . . . . 19 |- ( z = (/) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = (/) )
182	181	inteqd 4133	. . . . . . . . . . . . . . . . . 18 |- ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = |^| (/) )
183		int0 4142	. . . . . . . . . . . . . . . . . 18 |- |^| (/) = _V
184	182, 183	syl6eq 2491	. . . . . . . . . . . . . . . . 17 |- ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = _V )
185	184	neeq1d 2621	. . . . . . . . . . . . . . . 16 |- ( z = (/) -> ( |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) =/= (/) <-> _V =/= (/) ) )
186	15, 185	mpbiri 233	. . . . . . . . . . . . . . 15 |- ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) =/= (/) )
187	186	necomd 2695	. . . . . . . . . . . . . 14 |- ( z = (/) -> (/) =/= |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) )
188	187	necon2i 2658	. . . . . . . . . . . . 13 |- ( (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) -> z =/= (/) )
189	166	rbaibr 899	. . . . . . . . . . . . 13 |- ( z =/= (/) -> ( z e. ( ~P y i^i Fin ) <-> z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) )
190	188, 189	syl 16	. . . . . . . . . . . 12 |- ( (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) -> ( z e. ( ~P y i^i Fin ) <-> z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) )
191	190	pm5.32ri 638	. . . . . . . . . . 11 |- ( ( z e. ( ~P y i^i Fin ) /\ (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) <-> ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) /\ (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) )
192	191	rexbii2 2744	. . . . . . . . . 10 |- ( E. z e. ( ~P y i^i Fin ) (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) <-> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) )
193	178, 192	syl6bbr 263	. . . . . . . . 9 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. z e. ( ~P y i^i Fin ) U. J = U. z <-> E. z e. ( ~P y i^i Fin ) (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) )
194	80, 96, 193	3bitr4rd 286	. . . . . . . 8 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. z e. ( ~P y i^i Fin ) U. J = U. z <-> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) )
195	39, 194	imbi12d 320	. . . . . . 7 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) <-> ( |^|_ r e. y ( U. J \ r ) = (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) ) )
196	24, 195	pm2.61dane 2689	. . . . . 6 |- ( ( J e. Top /\ y C_ J ) -> ( ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) <-> ( |^|_ r e. y ( U. J \ r ) = (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) ) )
197	60	adantr 465	. . . . . . . . . . 11 |- ( ( J e. Top /\ y C_ J ) -> A. r e. y ( U. J \ r ) e. _V )
198		dfiin3g 5093	. . . . . . . . . . 11 |- ( A. r e. y ( U. J \ r ) e. _V -> |^|_ r e. y ( U. J \ r ) = |^| ran ( r e. y |-> ( U. J \ r ) ) )
199	197, 198	syl 16	. . . . . . . . . 10 |- ( ( J e. Top /\ y C_ J ) -> |^|_ r e. y ( U. J \ r ) = |^| ran ( r e. y |-> ( U. J \ r ) ) )
200	45	inteqd 4133	. . . . . . . . . 10 |- ( ( J e. Top /\ y C_ J ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = |^| ran ( r e. y |-> ( U. J \ r ) ) )
201	199, 200	eqtr4d 2478	. . . . . . . . 9 |- ( ( J e. Top /\ y C_ J ) -> |^|_ r e. y ( U. J \ r ) = |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) )
202	201	eqeq1d 2451	. . . . . . . 8 |- ( ( J e. Top /\ y C_ J ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = (/) ) )
203		nne 2612	. . . . . . . 8 |- ( -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = (/) )
204	202, 203	syl6bbr 263	. . . . . . 7 |- ( ( J e. Top /\ y C_ J ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) )
205	204	imbi1d 317	. . . . . 6 |- ( ( J e. Top /\ y C_ J ) -> ( ( |^|_ r e. y ( U. J \ r ) = (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) <-> ( -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) ) )
206	196, 205	bitrd 253	. . . . 5 |- ( ( J e. Top /\ y C_ J ) -> ( ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) <-> ( -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) ) )
207		con1b 333	. . . . 5 |- ( ( -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) <-> ( -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) )
208	206, 207	syl6bb 261	. . . 4 |- ( ( J e. Top /\ y C_ J ) -> ( ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) <-> ( -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) ) )
209	1, 208	sylan2 474	. . 3 |- ( ( J e. Top /\ y e. ~P J ) -> ( ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) <-> ( -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) ) )
210	209	ralbidva 2731	. 2 |- ( J e. Top -> ( A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) <-> A. y e. ~P J ( -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) ) )
211	56	iscmp 18991	. . 3 |- ( J e. Comp <-> ( J e. Top /\ A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) ) )
212	211	baib 896	. 2 |- ( J e. Top -> ( J e. Comp <-> A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) ) )
213	93	adantr 465	. . 3 |- ( ( J e. Top /\ y e. ~P J ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) )
214		simpl 457	. . . . 5 |- ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> J e. Top )
215		funmpt 5454	. . . . . 6 |- Fun ( r e. J |-> ( U. J \ r ) )
216	215	a1i 11	. . . . 5 |- ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> Fun ( r e. J |-> ( U. J \ r ) ) )
217		elpwi 3869	. . . . . . 7 |- ( x e. ~P ( Clsd ` J ) -> x C_ ( Clsd ` J ) )
218		foima 5625	. . . . . . . . 9 |- ( ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) -> ( ( r e. J |-> ( U. J \ r ) ) " J ) = ( Clsd ` J ) )
219	87, 218	syl 16	. . . . . . . 8 |- ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " J ) = ( Clsd ` J ) )
220	219	sseq2d 3384	. . . . . . 7 |- ( J e. Top -> ( x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) <-> x C_ ( Clsd ` J ) ) )
221	217, 220	syl5ibr 221	. . . . . 6 |- ( J e. Top -> ( x e. ~P ( Clsd ` J ) -> x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) ) )
222	221	imp 429	. . . . 5 |- ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) )
223		ssimaexg 5757	. . . . 5 |- ( ( J e. Top /\ Fun ( r e. J |-> ( U. J \ r ) ) /\ x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) ) -> E. y ( y C_ J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
224	214, 216, 222, 223	syl3anc 1218	. . . 4 |- ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> E. y ( y C_ J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
225		df-rex 2721	. . . . 5 |- ( E. y e. ~P J x = ( ( r e. J |-> ( U. J \ r ) ) " y ) <-> E. y ( y e. ~P J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
226		selpw 3867	. . . . . . 7 |- ( y e. ~P J <-> y C_ J )
227	226	anbi1i 695	. . . . . 6 |- ( ( y e. ~P J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) <-> ( y C_ J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
228	227	exbii 1634	. . . . 5 |- ( E. y ( y e. ~P J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) <-> E. y ( y C_ J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
229	225, 228	bitri 249	. . . 4 |- ( E. y e. ~P J x = ( ( r e. J |-> ( U. J \ r ) ) " y ) <-> E. y ( y C_ J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
230	224, 229	sylibr 212	. . 3 |- ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> E. y e. ~P J x = ( ( r e. J |-> ( U. J \ r ) ) " y ) )
231		simpr 461	. . . . . . 7 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> x = ( ( r e. J |-> ( U. J \ r ) ) " y ) )
232	231	fveq2d 5695	. . . . . 6 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( fi ` x ) = ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
233	232	eleq2d 2510	. . . . 5 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( (/) e. ( fi ` x ) <-> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) )
234	233	notbid 294	. . . 4 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( -. (/) e. ( fi ` x ) <-> -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) )
235	231	inteqd 4133	. . . . 5 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| x = |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) )
236	235	neeq1d 2621	. . . 4 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( |^| x =/= (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) )
237	234, 236	imbi12d 320	. . 3 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) <-> ( -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) ) )
238	213, 230, 237	ralxfrd 4506	. 2 |- ( J e. Top -> ( A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) <-> A. y e. ~P J ( -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) ) )
239	210, 212, 238	3bitr4d 285	1 |- ( J e. Top -> ( J e. Comp <-> A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   = wceq 1369   E.wex 1586   e. wcel 1756   =/= wne 2606   A.wral 2715   E.wrex 2716   _Vcvv 2972   \ cdif 3325   u. cun 3326   i^i cin 3327   C_ wss 3328   (/)c0 3637   ~Pcpw 3860   {csn 3877   U.cuni 4091   |^|cint 4128   U_ciun 4171   |^|_ciin 4172   e. cmpt 4350   `'ccnv 4839   ran crn 4841   |` cres 4842   "cima 4843   Fun wfun 5412   Fn wfn 5413   -onto->wfo 5416   -1-1-onto->wf1o 5417   ` cfv 5418   Fincfn 7310   ficfi 7660   Topctop 18498   Clsdccld 18620   Compccmp 18989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-tp 3882  df-op 3884  df-uni 4092  df-int 4129  df-iun 4173  df-iin 4174  df-br 4293  df-opab 4351  df-mpt 4352  df-tr 4386  df-eprel 4632  df-id 4636  df-po 4641  df-so 4642  df-fr 4679  df-we 4681  df-ord 4722  df-on 4723  df-lim 4724  df-suc 4725  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-om 6477  df-1st 6577  df-2nd 6578  df-recs 6832  df-rdg 6866  df-1o 6920  df-2o 6921  df-oadd 6924  df-er 7101  df-map 7216  df-en 7311  df-dom 7312  df-sdom 7313  df-fin 7314  df-fi 7661  df-top 18503  df-cld 18623  df-cmp 18990

This theorem is referenced by:  cmpfii  19012  fclscmp  19603  heibor1lem  28708