Theorem cmpfi 18911

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 3866	. . . 4 |- ( y e. ~P J -> y C_ J )
2		0ss 3663	. . . . . . . . . . 11 |- (/) C_ y
3		0fin 7536	. . . . . . . . . . 11 |- (/) e. Fin
4		elfpw 7609	. . . . . . . . . . 11 |- ( (/) e. ( ~P y i^i Fin ) <-> ( (/) C_ y /\ (/) e. Fin ) )
5	2, 3, 4	mpbir2an 906	. . . . . . . . . 10 |- (/) e. ( ~P y i^i Fin )
6		simprr 751	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. J = U. y )
7		simprl 750	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> y = (/) )
8	7	unieqd 4098	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. y = U. (/) )
9	6, 8	eqtrd 2473	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. J = U. (/) )
10		unieq 4096	. . . . . . . . . . . 12 |- ( z = (/) -> U. z = U. (/) )
11	10	eqeq2d 2452	. . . . . . . . . . 11 |- ( z = (/) -> ( U. J = U. z <-> U. J = U. (/) ) )
12	11	rspcev 3070	. . . . . . . . . 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 658	. . . . . . . . 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 612	. . . . . . . 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 3641	. . . . . . . . . 10 |- _V =/= (/)
16		iineq1 4182	. . . . . . . . . . . . . 14 |- ( y = (/) -> |^|_ r e. y ( U. J \ r ) = |^|_ r e. (/) ( U. J \ r ) )
17	16	adantl 463	. . . . . . . . . . . . 13 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> |^|_ r e. y ( U. J \ r ) = |^|_ r e. (/) ( U. J \ r ) )
18		0iin 4225	. . . . . . . . . . . . 13 |- |^|_ r e. (/) ( U. J \ r ) = _V
19	17, 18	syl6eq 2489	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> |^|_ r e. y ( U. J \ r ) = _V )
20	19	eqeq1d 2449	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> _V = (/) ) )
21	20	necon3bbid 2640	. . . . . . . . . 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 4109	. . . . . . . . . . . 12 |- ( y C_ J -> U. y C_ U. J )
26	25	ad2antlr 721	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> U. y C_ U. J )
27		eqss 3368	. . . . . . . . . . . 12 |- ( U. y = U. J <-> ( U. y C_ U. J /\ U. J C_ U. y ) )
28	27	baib 891	. . . . . . . . . . 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 2443	. . . . . . . . . 10 |- ( U. y = U. J <-> U. J = U. y )
31		ssdif0 3734	. . . . . . . . . 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 4236	. . . . . . . . . . . 12 |- ( y =/= (/) -> |^|_ r e. y ( U. J \ r ) = ( U. J \ U_ r e. y r ) )
34	33	adantl 463	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> |^|_ r e. y ( U. J \ r ) = ( U. J \ U_ r e. y r ) )
35		uniiun 4220	. . . . . . . . . . . 12 |- U. y = U_ r e. y r
36	35	difeq2i 3468	. . . . . . . . . . 11 |- ( U. J \ U. y ) = ( U. J \ U_ r e. y r )
37	34, 36	syl6eqr 2491	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> |^|_ r e. y ( U. J \ r ) = ( U. J \ U. y ) )
38	37	eqeq1d 2449	. . . . . . . . 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 5177	. . . . . . . . . . . 12 |- ( ( r e. y |-> ( U. J \ r ) ) " z ) C_ ran ( r e. y |-> ( U. J \ r ) )
41		df-ima 4849	. . . . . . . . . . . . . 14 |- ( ( r e. J |-> ( U. J \ r ) ) " y ) = ran ( ( r e. J |-> ( U. J \ r ) ) |` y )
42		resmpt 5153	. . . . . . . . . . . . . . . 16 |- ( y C_ J -> ( ( r e. J |-> ( U. J \ r ) ) |` y ) = ( r e. y |-> ( U. J \ r ) ) )
43	42	adantl 463	. . . . . . . . . . . . . . 15 |- ( ( J e. Top /\ y C_ J ) -> ( ( r e. J |-> ( U. J \ r ) ) |` y ) = ( r e. y |-> ( U. J \ r ) ) )
44	43	rneqd 5063	. . . . . . . . . . . . . 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 2485	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ y C_ J ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) = ran ( r e. y |-> ( U. J \ r ) ) )
46	45	ad2antrr 720	. . . . . . . . . . . 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 3402	. . . . . . . . . . 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 5451	. . . . . . . . . . . 12 |- Fun ( r e. y |-> ( U. J \ r ) )
49		elfpw 7609	. . . . . . . . . . . . . 14 |- ( z e. ( ~P y i^i Fin ) <-> ( z C_ y /\ z e. Fin ) )
50	49	simprbi 461	. . . . . . . . . . . . 13 |- ( z e. ( ~P y i^i Fin ) -> z e. Fin )
51	50	adantl 463	. . . . . . . . . . . 12 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ~P y i^i Fin ) ) -> z e. Fin )
52		imafi 7600	. . . . . . . . . . . 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 658	. . . . . . . . . . 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 7609	. . . . . . . . . . 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 659	. . . . . . . . . 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 2441	. . . . . . . . . . . . . . . . 17 |- U. J = U. J
57	56	topopn 18419	. . . . . . . . . . . . . . . 16 |- ( J e. Top -> U. J e. J )
58		difexg 4437	. . . . . . . . . . . . . . . 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 2798	. . . . . . . . . . . . . 14 |- ( J e. Top -> A. r e. y ( U. J \ r ) e. _V )
61		eqid 2441	. . . . . . . . . . . . . . 15 |- ( r e. y |-> ( U. J \ r ) ) = ( r e. y |-> ( U. J \ r ) )
62	61	fnmpt 5534	. . . . . . . . . . . . . 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 724	. . . . . . . . . . . 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 458	. . . . . . . . . . . . . . 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 7609	. . . . . . . . . . . . . . 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 456	. . . . . . . . . . . . 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 720	. . . . . . . . . . . . 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 3389	. . . . . . . . . . . 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 460	. . . . . . . . . . . 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 7613	. . . . . . . . . . . 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 1213	. . . . . . . . . . 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 2443	. . . . . . . . . . . 12 |- ( ( ( r e. y |-> ( U. J \ r ) ) " z ) = w <-> w = ( ( r e. y |-> ( U. J \ r ) ) " z ) )
75	74	rexbii 2738	. . . . . . . . . . 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 458	. . . . . . . . . . . 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 4130	. . . . . . . . . . 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 2452	. . . . . . . . . 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 4504	. . . . . . . . 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 4419	. . . . . . . . . 10 |- (/) e. _V
82		imassrn 5177	. . . . . . . . . . . . 13 |- ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ran ( r e. J |-> ( U. J \ r ) )
83		eqid 2441	. . . . . . . . . . . . . . . . 17 |- ( r e. J |-> ( U. J \ r ) ) = ( r e. J |-> ( U. J \ r ) )
84	56, 83	opncldf1 18588	. . . . . . . . . . . . . . . 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 456	. . . . . . . . . . . . . . 15 |- ( J e. Top -> ( r e. J |-> ( U. J \ r ) ) : J -1-1-onto-> ( Clsd ` J ) )
86		f1ofo 5645	. . . . . . . . . . . . . . 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 5620	. . . . . . . . . . . . . 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 3401	. . . . . . . . . . . 12 |- ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ( Clsd ` J ) )
91		fvex 5698	. . . . . . . . . . . . 13 |- ( Clsd ` J ) e. _V
92	91	elpw2 4453	. . . . . . . . . . . 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 720	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) )
95		elfi 7659	. . . . . . . . . 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 658	. . . . . . . . 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 3754	. . . . . . . . . . . . . 14 |- ( ( ( ~P y i^i Fin ) i^i { (/) } ) u. ( ( ~P y i^i Fin ) \ { (/) } ) ) = ( ~P y i^i Fin )
98	97	rexeqi 2920	. . . . . . . . . . . . 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 3533	. . . . . . . . . . . . 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 3568	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ~P y i^i Fin ) i^i { (/) } ) C_ { (/) }
102	101	sseli 3349	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> z e. { (/) } )
103		elsni 3899	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. { (/) } -> z = (/) )
104	102, 103	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> z = (/) )
105	104	unieqd 4098	. . . . . . . . . . . . . . . . . . 19 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> U. z = U. (/) )
106		uni0 4115	. . . . . . . . . . . . . . . . . . 19 |- U. (/) = (/)
107	105, 106	syl6eq 2489	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> U. z = (/) )
108	107	eqeq2d 2452	. . . . . . . . . . . . . . . . 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 2833	. . . . . . . . . . . . . . 15 |- ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z -> U. J = (/) )
111		ssid 3372	. . . . . . . . . . . . . . . . . . . 20 |- y C_ y
112	111	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y C_ y )
113		simprr 751	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J = (/) )
114		0ss 3663	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (/) C_ U. y
115	113, 114	syl6eqss 3403	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J C_ U. y )
116	25	ad2antlr 721	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y C_ U. J )
117	115, 116	eqssd 3370	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J = U. y )
118	117, 113	eqtr3d 2475	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y = (/) )
119	118, 3	syl6eqel 2529	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y e. Fin )
120		pwfi 7602	. . . . . . . . . . . . . . . . . . . . 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 4520	. . . . . . . . . . . . . . . . . . . 20 |- y C_ ~P U. y
123		ssfi 7529	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ~P U. y e. Fin /\ y C_ ~P U. y ) -> y e. Fin )
124	121, 122, 123	sylancl 657	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y e. Fin )
125		elfpw 7609	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( ~P y i^i Fin ) <-> ( y C_ y /\ y e. Fin ) )
126	112, 124, 125	sylanbrc 659	. . . . . . . . . . . . . . . . . 18 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y e. ( ~P y i^i Fin ) )
127		simprl 750	. . . . . . . . . . . . . . . . . 18 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y =/= (/) )
128		eldifsn 3997	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( ( ~P y i^i Fin ) \ { (/) } ) <-> ( y e. ( ~P y i^i Fin ) /\ y =/= (/) ) )
129	126, 127, 128	sylanbrc 659	. . . . . . . . . . . . . . . . 17 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y e. ( ( ~P y i^i Fin ) \ { (/) } ) )
130		unieq 4096	. . . . . . . . . . . . . . . . . . 19 |- ( z = y -> U. z = U. y )
131	130	eqeq2d 2452	. . . . . . . . . . . . . . . . . 18 |- ( z = y -> ( U. J = U. z <-> U. J = U. y ) )
132	131	rspcev 3070	. . . . . . . . . . . . . . . . 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 656	. . . . . . . . . . . . . . . 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 612	. . . . . . . . . . . . . . 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 3475	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) -> z e. ( ~P y i^i Fin ) )
142	141	adantl 463	. . . . . . . . . . . . . . . . . . 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 456	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z C_ y )
145		simpllr 753	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> y C_ J )
146	144, 145	sstrd 3363	. . . . . . . . . . . . . . . 16 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z C_ J )
147	146	unissd 4112	. . . . . . . . . . . . . . 15 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> U. z C_ U. J )
148		eqss 3368	. . . . . . . . . . . . . . . 16 |- ( U. z = U. J <-> ( U. z C_ U. J /\ U. J C_ U. z ) )
149	148	baib 891	. . . . . . . . . . . . . . 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 2443	. . . . . . . . . . . . . 14 |- ( U. z = U. J <-> U. J = U. z )
152		ssdif0 3734	. . . . . . . . . . . . . . 15 |- ( U. J C_ U. z <-> ( U. J \ U. z ) = (/) )
153		eqcom 2443	. . . . . . . . . . . . . . 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 4849	. . . . . . . . . . . . . . . . . 18 |- ( ( r e. y |-> ( U. J \ r ) ) " z ) = ran ( ( r e. y |-> ( U. J \ r ) ) |` z )
157		resmpt 5153	. . . . . . . . . . . . . . . . . . . 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 5063	. . . . . . . . . . . . . . . . . 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 2485	. . . . . . . . . . . . . . . . 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 4130	. . . . . . . . . . . . . . . 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 2798	. . . . . . . . . . . . . . . . . 18 |- ( J e. Top -> A. r e. z ( U. J \ r ) e. _V )
163	162	ad3antrrr 724	. . . . . . . . . . . . . . . . 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 5089	. . . . . . . . . . . . . . . . 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 3997	. . . . . . . . . . . . . . . . . . 19 |- ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) <-> ( z e. ( ~P y i^i Fin ) /\ z =/= (/) ) )
167	166	simprbi 461	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) -> z =/= (/) )
168	167	adantl 463	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z =/= (/) )
169		iindif2 4236	. . . . . . . . . . . . . . . . 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 2479	. . . . . . . . . . . . . . 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 4220	. . . . . . . . . . . . . . . 16 |- U. z = U_ r e. z r
173	172	difeq2i 3468	. . . . . . . . . . . . . . 15 |- ( U. J \ U. z ) = ( U. J \ U_ r e. z r )
174	171, 173	syl6eqr 2491	. . . . . . . . . . . . . 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 2452	. . . . . . . . . . . . 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 2730	. . . . . . . . . . 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 5162	. . . . . . . . . . . . . . . . . . . 20 |- ( z = (/) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = ( ( r e. y |-> ( U. J \ r ) ) " (/) ) )
180		ima0 5181	. . . . . . . . . . . . . . . . . . . 20 |- ( ( r e. y |-> ( U. J \ r ) ) " (/) ) = (/)
181	179, 180	syl6eq 2489	. . . . . . . . . . . . . . . . . . 19 |- ( z = (/) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = (/) )
182	181	inteqd 4130	. . . . . . . . . . . . . . . . . 18 |- ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = |^| (/) )
183		int0 4139	. . . . . . . . . . . . . . . . . 18 |- |^| (/) = _V
184	182, 183	syl6eq 2489	. . . . . . . . . . . . . . . . 17 |- ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = _V )
185	184	neeq1d 2619	. . . . . . . . . . . . . . . 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 2693	. . . . . . . . . . . . . 14 |- ( z = (/) -> (/) =/= |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) )
188	187	necon2i 2656	. . . . . . . . . . . . 13 |- ( (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) -> z =/= (/) )
189	166	rbaibr 894	. . . . . . . . . . . . 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 633	. . . . . . . . . . 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 2742	. . . . . . . . . 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 2687	. . . . . 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 462	. . . . . . . . . . 11 |- ( ( J e. Top /\ y C_ J ) -> A. r e. y ( U. J \ r ) e. _V )
198		dfiin3g 5089	. . . . . . . . . . 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 4130	. . . . . . . . . 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 2476	. . . . . . . . 9 |- ( ( J e. Top /\ y C_ J ) -> |^|_ r e. y ( U. J \ r ) = |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) )
202	201	eqeq1d 2449	. . . . . . . 8 |- ( ( J e. Top /\ y C_ J ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = (/) ) )
203		nne 2610	. . . . . . . 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 471	. . 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 2729	. 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 18891	. . 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 891	. 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 462	. . 3 |- ( ( J e. Top /\ y e. ~P J ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) )
214		simpl 454	. . . . 5 |- ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> J e. Top )
215		funmpt 5451	. . . . . 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 3866	. . . . . . 7 |- ( x e. ~P ( Clsd ` J ) -> x C_ ( Clsd ` J ) )
218		foima 5622	. . . . . . . . 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 3381	. . . . . . 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 5754	. . . . 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 1213	. . . 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 2719	. . . . 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 3864	. . . . . . 7 |- ( y e. ~P J <-> y C_ J )
227	226	anbi1i 690	. . . . . 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 1639	. . . . 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 458	. . . . . . 7 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> x = ( ( r e. J |-> ( U. J \ r ) ) " y ) )
232	231	fveq2d 5692	. . . . . 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 2508	. . . . 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 4130	. . . . 5 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| x = |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) )
236	235	neeq1d 2619	. . . 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 4503	. 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 1364   E.wex 1591   e. wcel 1761   =/= wne 2604   A.wral 2713   E.wrex 2714   _Vcvv 2970   \ cdif 3322   u. cun 3323   i^i cin 3324   C_ wss 3325   (/)c0 3634   ~Pcpw 3857   {csn 3874   U.cuni 4088   |^|cint 4125   U_ciun 4168   |^|_ciin 4169   e. cmpt 4347   `'ccnv 4835   ran crn 4837   |` cres 4838   "cima 4839   Fun wfun 5409   Fn wfn 5410   -onto->wfo 5413   -1-1-onto->wf1o 5414   ` cfv 5415   Fincfn 7306   ficfi 7656   Topctop 18398   Clsdccld 18520   Compccmp 18889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-iin 4171  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-1st 6576  df-2nd 6577  df-recs 6828  df-rdg 6862  df-1o 6916  df-2o 6917  df-oadd 6920  df-er 7097  df-map 7212  df-en 7307  df-dom 7308  df-sdom 7309  df-fin 7310  df-fi 7657  df-top 18403  df-cld 18523  df-cmp 18890

This theorem is referenced by:  cmpfii  18912  fclscmp  19503  heibor1lem  28617