Theorem cmpfi 19702

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 4019	. . . 4 |- ( y e. ~P J -> y C_ J )
2		0ss 3814	. . . . . . . . . . 11 |- (/) C_ y
3		0fin 7747	. . . . . . . . . . 11 |- (/) e. Fin
4		elfpw 7822	. . . . . . . . . . 11 |- ( (/) e. ( ~P y i^i Fin ) <-> ( (/) C_ y /\ (/) e. Fin ) )
5	2, 3, 4	mpbir2an 918	. . . . . . . . . 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 4255	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. y = U. (/) )
9	6, 8	eqtrd 2508	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. J = U. (/) )
10		unieq 4253	. . . . . . . . . . . 12 |- ( z = (/) -> U. z = U. (/) )
11	10	eqeq2d 2481	. . . . . . . . . . 11 |- ( z = (/) -> ( U. J = U. z <-> U. J = U. (/) ) )
12	11	rspcev 3214	. . . . . . . . . 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 3792	. . . . . . . . . 10 |- _V =/= (/)
16		iineq1 4340	. . . . . . . . . . . . . 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 4383	. . . . . . . . . . . . 13 |- |^|_ r e. (/) ( U. J \ r ) = _V
19	17, 18	syl6eq 2524	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> |^|_ r e. y ( U. J \ r ) = _V )
20	19	eqeq1d 2469	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> _V = (/) ) )
21	20	necon3bbid 2714	. . . . . . . . . 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 4266	. . . . . . . . . . . 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 3519	. . . . . . . . . . . 12 |- ( U. y = U. J <-> ( U. y C_ U. J /\ U. J C_ U. y ) )
28	27	baib 901	. . . . . . . . . . 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 2476	. . . . . . . . . 10 |- ( U. y = U. J <-> U. J = U. y )
31		ssdif0 3885	. . . . . . . . . 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 4394	. . . . . . . . . . . 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 4378	. . . . . . . . . . . 12 |- U. y = U_ r e. y r
36	35	difeq2i 3619	. . . . . . . . . . 11 |- ( U. J \ U. y ) = ( U. J \ U_ r e. y r )
37	34, 36	syl6eqr 2526	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> |^|_ r e. y ( U. J \ r ) = ( U. J \ U. y ) )
38	37	eqeq1d 2469	. . . . . . . . 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 5348	. . . . . . . . . . . 12 |- ( ( r e. y |-> ( U. J \ r ) ) " z ) C_ ran ( r e. y |-> ( U. J \ r ) )
41		df-ima 5012	. . . . . . . . . . . . . 14 |- ( ( r e. J |-> ( U. J \ r ) ) " y ) = ran ( ( r e. J |-> ( U. J \ r ) ) |` y )
42		resmpt 5323	. . . . . . . . . . . . . . . 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 5230	. . . . . . . . . . . . . 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 2520	. . . . . . . . . . . . 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 3553	. . . . . . . . . . 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 5624	. . . . . . . . . . . 12 |- Fun ( r e. y |-> ( U. J \ r ) )
49		elfpw 7822	. . . . . . . . . . . . . 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 7813	. . . . . . . . . . . 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 7822	. . . . . . . . . . 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 2467	. . . . . . . . . . . . . . . . 17 |- U. J = U. J
57	56	topopn 19210	. . . . . . . . . . . . . . . 16 |- ( J e. Top -> U. J e. J )
58		difexg 4595	. . . . . . . . . . . . . . . 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 2879	. . . . . . . . . . . . . 14 |- ( J e. Top -> A. r e. y ( U. J \ r ) e. _V )
61		eqid 2467	. . . . . . . . . . . . . . 15 |- ( r e. y |-> ( U. J \ r ) ) = ( r e. y |-> ( U. J \ r ) )
62	61	fnmpt 5707	. . . . . . . . . . . . . 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 7822	. . . . . . . . . . . . . . 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 3540	. . . . . . . . . . . 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 7826	. . . . . . . . . . . 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 1228	. . . . . . . . . . 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 2476	. . . . . . . . . . . 12 |- ( ( ( r e. y |-> ( U. J \ r ) ) " z ) = w <-> w = ( ( r e. y |-> ( U. J \ r ) ) " z ) )
75	74	rexbii 2965	. . . . . . . . . . 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 4287	. . . . . . . . . . 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 2481	. . . . . . . . . 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 4662	. . . . . . . . 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 4577	. . . . . . . . . 10 |- (/) e. _V
82		imassrn 5348	. . . . . . . . . . . . 13 |- ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ran ( r e. J |-> ( U. J \ r ) )
83		eqid 2467	. . . . . . . . . . . . . . . . 17 |- ( r e. J |-> ( U. J \ r ) ) = ( r e. J |-> ( U. J \ r ) )
84	56, 83	opncldf1 19379	. . . . . . . . . . . . . . . 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 5823	. . . . . . . . . . . . . . 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 5798	. . . . . . . . . . . . . 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 3552	. . . . . . . . . . . 12 |- ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ( Clsd ` J ) )
91		fvex 5876	. . . . . . . . . . . . 13 |- ( Clsd ` J ) e. _V
92	91	elpw2 4611	. . . . . . . . . . . 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 7873	. . . . . . . . . 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 3905	. . . . . . . . . . . . . 14 |- ( ( ( ~P y i^i Fin ) i^i { (/) } ) u. ( ( ~P y i^i Fin ) \ { (/) } ) ) = ( ~P y i^i Fin )
98	97	rexeqi 3063	. . . . . . . . . . . . 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 3684	. . . . . . . . . . . . 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 3719	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ~P y i^i Fin ) i^i { (/) } ) C_ { (/) }
102	101	sseli 3500	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> z e. { (/) } )
103		elsni 4052	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. { (/) } -> z = (/) )
104	102, 103	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> z = (/) )
105	104	unieqd 4255	. . . . . . . . . . . . . . . . . . 19 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> U. z = U. (/) )
106		uni0 4272	. . . . . . . . . . . . . . . . . . 19 |- U. (/) = (/)
107	105, 106	syl6eq 2524	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> U. z = (/) )
108	107	eqeq2d 2481	. . . . . . . . . . . . . . . . 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 2949	. . . . . . . . . . . . . . 15 |- ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z -> U. J = (/) )
111		ssid 3523	. . . . . . . . . . . . . . . . . . . 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 3814	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (/) C_ U. y
115	113, 114	syl6eqss 3554	. . . . . . . . . . . . . . . . . . . . . . . 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 3521	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J = U. y )
118	117, 113	eqtr3d 2510	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y = (/) )
119	118, 3	syl6eqel 2563	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y e. Fin )
120		pwfi 7815	. . . . . . . . . . . . . . . . . . . . 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 4678	. . . . . . . . . . . . . . . . . . . 20 |- y C_ ~P U. y
123		ssfi 7740	. . . . . . . . . . . . . . . . . . . 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 7822	. . . . . . . . . . . . . . . . . . 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 4152	. . . . . . . . . . . . . . . . . 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 4253	. . . . . . . . . . . . . . . . . . 19 |- ( z = y -> U. z = U. y )
131	130	eqeq2d 2481	. . . . . . . . . . . . . . . . . 18 |- ( z = y -> ( U. J = U. z <-> U. J = U. y ) )
132	131	rspcev 3214	. . . . . . . . . . . . . . . . 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 3626	. . . . . . . . . . . . . . . . . . . 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 3514	. . . . . . . . . . . . . . . 16 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z C_ J )
147	146	unissd 4269	. . . . . . . . . . . . . . 15 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> U. z C_ U. J )
148		eqss 3519	. . . . . . . . . . . . . . . 16 |- ( U. z = U. J <-> ( U. z C_ U. J /\ U. J C_ U. z ) )
149	148	baib 901	. . . . . . . . . . . . . . 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 2476	. . . . . . . . . . . . . 14 |- ( U. z = U. J <-> U. J = U. z )
152		ssdif0 3885	. . . . . . . . . . . . . . 15 |- ( U. J C_ U. z <-> ( U. J \ U. z ) = (/) )
153		eqcom 2476	. . . . . . . . . . . . . . 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 5012	. . . . . . . . . . . . . . . . . 18 |- ( ( r e. y |-> ( U. J \ r ) ) " z ) = ran ( ( r e. y |-> ( U. J \ r ) ) |` z )
157		resmpt 5323	. . . . . . . . . . . . . . . . . . . 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 5230	. . . . . . . . . . . . . . . . . 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 2520	. . . . . . . . . . . . . . . . 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 4287	. . . . . . . . . . . . . . . 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 2879	. . . . . . . . . . . . . . . . . 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 5256	. . . . . . . . . . . . . . . . 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 4152	. . . . . . . . . . . . . . . . . . 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 4394	. . . . . . . . . . . . . . . . 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 2514	. . . . . . . . . . . . . . 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 4378	. . . . . . . . . . . . . . . 16 |- U. z = U_ r e. z r
173	172	difeq2i 3619	. . . . . . . . . . . . . . 15 |- ( U. J \ U. z ) = ( U. J \ U_ r e. z r )
174	171, 173	syl6eqr 2526	. . . . . . . . . . . . . 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 2481	. . . . . . . . . . . . 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 2970	. . . . . . . . . . 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 5333	. . . . . . . . . . . . . . . . . . . 20 |- ( z = (/) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = ( ( r e. y |-> ( U. J \ r ) ) " (/) ) )
180		ima0 5352	. . . . . . . . . . . . . . . . . . . 20 |- ( ( r e. y |-> ( U. J \ r ) ) " (/) ) = (/)
181	179, 180	syl6eq 2524	. . . . . . . . . . . . . . . . . . 19 |- ( z = (/) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = (/) )
182	181	inteqd 4287	. . . . . . . . . . . . . . . . . 18 |- ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = |^| (/) )
183		int0 4296	. . . . . . . . . . . . . . . . . 18 |- |^| (/) = _V
184	182, 183	syl6eq 2524	. . . . . . . . . . . . . . . . 17 |- ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = _V )
185	184	neeq1d 2744	. . . . . . . . . . . . . . . 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 2738	. . . . . . . . . . . . . 14 |- ( z = (/) -> (/) =/= |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) )
188	187	necon2i 2710	. . . . . . . . . . . . 13 |- ( (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) -> z =/= (/) )
189	166	rbaibr 903	. . . . . . . . . . . . 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 2963	. . . . . . . . . 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 2785	. . . . . 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 5256	. . . . . . . . . . 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 4287	. . . . . . . . . 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 2511	. . . . . . . . 9 |- ( ( J e. Top /\ y C_ J ) -> |^|_ r e. y ( U. J \ r ) = |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) )
202	201	eqeq1d 2469	. . . . . . . 8 |- ( ( J e. Top /\ y C_ J ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = (/) ) )
203		nne 2668	. . . . . . . 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 2900	. 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 19682	. . 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 901	. 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 5624	. . . . . 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 4019	. . . . . . 7 |- ( x e. ~P ( Clsd ` J ) -> x C_ ( Clsd ` J ) )
218		foima 5800	. . . . . . . . 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 3532	. . . . . . 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 5933	. . . . 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 1228	. . . 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 2820	. . . . 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 4017	. . . . . . 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 1644	. . . . 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 5870	. . . . . 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 2537	. . . . 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 4287	. . . . 5 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| x = |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) )
236	235	neeq1d 2744	. . . 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 4661	. 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 1379   E.wex 1596   e. wcel 1767   =/= wne 2662   A.wral 2814   E.wrex 2815   _Vcvv 3113   \ cdif 3473   u. cun 3474   i^i cin 3475   C_ wss 3476   (/)c0 3785   ~Pcpw 4010   {csn 4027   U.cuni 4245   |^|cint 4282   U_ciun 4325   |^|_ciin 4326   |-> cmpt 4505   `'ccnv 4998   ran crn 5000   |` cres 5001   "cima 5002   Fun wfun 5582   Fn wfn 5583   -onto->wfo 5586   -1-1-onto->wf1o 5587   ` cfv 5588   Fincfn 7516   ficfi 7870   Topctop 19189   Clsdccld 19311   Compccmp 19680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-iin 4328  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-om 6685  df-1st 6784  df-2nd 6785  df-recs 7042  df-rdg 7076  df-1o 7130  df-2o 7131  df-oadd 7134  df-er 7311  df-map 7422  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-fi 7871  df-top 19194  df-cld 19314  df-cmp 19681

This theorem is referenced by:  cmpfii  19703  fclscmp  20294  heibor1lem  29936