Theorem cmpfi 21211

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 v r w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpwi 4168	. . . 4 |- ( y e. ~P J -> y C_ J )
2		0ss 3972	. . . . . . . . . . 11 |- (/) C_ y
3		0fin 8188	. . . . . . . . . . 11 |- (/) e. Fin
4		elfpw 8268	. . . . . . . . . . 11 |- ( (/) e. ( ~P y i^i Fin ) <-> ( (/) C_ y /\ (/) e. Fin ) )
5	2, 3, 4	mpbir2an 955	. . . . . . . . . 10 |- (/) e. ( ~P y i^i Fin )
6		simprr 796	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. J = U. y )
7		simprl 794	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> y = (/) )
8	7	unieqd 4446	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. y = U. (/) )
9	6, 8	eqtrd 2656	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. J = U. (/) )
10		unieq 4444	. . . . . . . . . . . 12 |- ( z = (/) -> U. z = U. (/) )
11	10	eqeq2d 2632	. . . . . . . . . . 11 |- ( z = (/) -> ( U. J = U. z <-> U. J = U. (/) ) )
12	11	rspcev 3309	. . . . . . . . . 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 695	. . . . . . . . 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 643	. . . . . . . 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 3924	. . . . . . . . . 10 |- _V =/= (/)
16		iineq1 4535	. . . . . . . . . . . . . 14 |- ( y = (/) -> |^|_ r e. y ( U. J \ r ) = |^|_ r e. (/) ( U. J \ r ) )
17	16	adantl 482	. . . . . . . . . . . . 13 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> |^|_ r e. y ( U. J \ r ) = |^|_ r e. (/) ( U. J \ r ) )
18		0iin 4578	. . . . . . . . . . . . 13 |- |^|_ r e. (/) ( U. J \ r ) = _V
19	17, 18	syl6eq 2672	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> |^|_ r e. y ( U. J \ r ) = _V )
20	19	eqeq1d 2624	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> _V = (/) ) )
21	20	necon3bbid 2831	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> ( -. |^|_ r e. y ( U. J \ r ) = (/) <-> _V =/= (/) ) )
22	15, 21	mpbiri 248	. . . . . . . . 9 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> -. |^|_ r e. y ( U. J \ r ) = (/) )
23	22	pm2.21d 118	. . . . . . . 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 255	. . . . . . 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 4458	. . . . . . . . . . . 12 |- ( y C_ J -> U. y C_ U. J )
26	25	ad2antlr 763	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> U. y C_ U. J )
27		eqss 3618	. . . . . . . . . . . 12 |- ( U. y = U. J <-> ( U. y C_ U. J /\ U. J C_ U. y ) )
28	27	baib 944	. . . . . . . . . . 11 |- ( U. y C_ U. J -> ( U. y = U. J <-> U. J C_ U. y ) )
29	26, 28	syl 17	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( U. y = U. J <-> U. J C_ U. y ) )
30		eqcom 2629	. . . . . . . . . 10 |- ( U. y = U. J <-> U. J = U. y )
31		ssdif0 3942	. . . . . . . . . 10 |- ( U. J C_ U. y <-> ( U. J \ U. y ) = (/) )
32	29, 30, 31	3bitr3g 302	. . . . . . . . 9 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( U. J = U. y <-> ( U. J \ U. y ) = (/) ) )
33		iindif2 4589	. . . . . . . . . . . 12 |- ( y =/= (/) -> |^|_ r e. y ( U. J \ r ) = ( U. J \ U_ r e. y r ) )
34	33	adantl 482	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> |^|_ r e. y ( U. J \ r ) = ( U. J \ U_ r e. y r ) )
35		uniiun 4573	. . . . . . . . . . . 12 |- U. y = U_ r e. y r
36	35	difeq2i 3725	. . . . . . . . . . 11 |- ( U. J \ U. y ) = ( U. J \ U_ r e. y r )
37	34, 36	syl6eqr 2674	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> |^|_ r e. y ( U. J \ r ) = ( U. J \ U. y ) )
38	37	eqeq1d 2624	. . . . . . . . 9 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> ( U. J \ U. y ) = (/) ) )
39	32, 38	bitr4d 271	. . . . . . . 8 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( U. J = U. y <-> |^|_ r e. y ( U. J \ r ) = (/) ) )
40		imassrn 5477	. . . . . . . . . . . 12 |- ( ( r e. y |-> ( U. J \ r ) ) " z ) C_ ran ( r e. y |-> ( U. J \ r ) )
41		df-ima 5127	. . . . . . . . . . . . . 14 |- ( ( r e. J |-> ( U. J \ r ) ) " y ) = ran ( ( r e. J |-> ( U. J \ r ) ) |` y )
42		resmpt 5449	. . . . . . . . . . . . . . . 16 |- ( y C_ J -> ( ( r e. J |-> ( U. J \ r ) ) |` y ) = ( r e. y |-> ( U. J \ r ) ) )
43	42	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( J e. Top /\ y C_ J ) -> ( ( r e. J |-> ( U. J \ r ) ) |` y ) = ( r e. y |-> ( U. J \ r ) ) )
44	43	rneqd 5353	. . . . . . . . . . . . . 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 2668	. . . . . . . . . . . . 13 |- ( ( J e. Top /\ y C_ J ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) = ran ( r e. y |-> ( U. J \ r ) ) )
46	45	ad2antrr 762	. . . . . . . . . . . 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 3654	. . . . . . . . . . 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 5926	. . . . . . . . . . . 12 |- Fun ( r e. y |-> ( U. J \ r ) )
49		elfpw 8268	. . . . . . . . . . . . . 14 |- ( z e. ( ~P y i^i Fin ) <-> ( z C_ y /\ z e. Fin ) )
50	49	simprbi 480	. . . . . . . . . . . . 13 |- ( z e. ( ~P y i^i Fin ) -> z e. Fin )
51	50	adantl 482	. . . . . . . . . . . 12 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ~P y i^i Fin ) ) -> z e. Fin )
52		imafi 8259	. . . . . . . . . . . 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 695	. . . . . . . . . . 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 8268	. . . . . . . . . . 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 698	. . . . . . . . . 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 2622	. . . . . . . . . . . . . . . . 17 |- U. J = U. J
57	56	topopn 20711	. . . . . . . . . . . . . . . 16 |- ( J e. Top -> U. J e. J )
58		difexg 4808	. . . . . . . . . . . . . . . 16 |- ( U. J e. J -> ( U. J \ r ) e. _V )
59	57, 58	syl 17	. . . . . . . . . . . . . . 15 |- ( J e. Top -> ( U. J \ r ) e. _V )
60	59	ralrimivw 2967	. . . . . . . . . . . . . 14 |- ( J e. Top -> A. r e. y ( U. J \ r ) e. _V )
61		eqid 2622	. . . . . . . . . . . . . . 15 |- ( r e. y |-> ( U. J \ r ) ) = ( r e. y |-> ( U. J \ r ) )
62	61	fnmpt 6020	. . . . . . . . . . . . . 14 |- ( A. r e. y ( U. J \ r ) e. _V -> ( r e. y |-> ( U. J \ r ) ) Fn y )
63	60, 62	syl 17	. . . . . . . . . . . . 13 |- ( J e. Top -> ( r e. y |-> ( U. J \ r ) ) Fn y )
64	63	ad3antrrr 766	. . . . . . . . . . . 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 477	. . . . . . . . . . . . . . 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 8268	. . . . . . . . . . . . . . 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 208	. . . . . . . . . . . . . 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 475	. . . . . . . . . . . . 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 762	. . . . . . . . . . . . 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 3641	. . . . . . . . . . . 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 479	. . . . . . . . . . . 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 8272	. . . . . . . . . . . 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 1326	. . . . . . . . . . 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 2629	. . . . . . . . . . . 12 |- ( ( ( r e. y |-> ( U. J \ r ) ) " z ) = w <-> w = ( ( r e. y |-> ( U. J \ r ) ) " z ) )
75	74	rexbii 3041	. . . . . . . . . . 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 208	. . . . . . . . . 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 477	. . . . . . . . . . . 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 4480	. . . . . . . . . . 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 2632	. . . . . . . . . 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 4881	. . . . . . . . 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 4790	. . . . . . . . . 10 |- (/) e. _V
82		imassrn 5477	. . . . . . . . . . . . 13 |- ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ran ( r e. J |-> ( U. J \ r ) )
83		eqid 2622	. . . . . . . . . . . . . . . . 17 |- ( r e. J |-> ( U. J \ r ) ) = ( r e. J |-> ( U. J \ r ) )
84	56, 83	opncldf1 20888	. . . . . . . . . . . . . . . 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 475	. . . . . . . . . . . . . . 15 |- ( J e. Top -> ( r e. J |-> ( U. J \ r ) ) : J -1-1-onto-> ( Clsd ` J ) )
86		f1ofo 6144	. . . . . . . . . . . . . . 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 17	. . . . . . . . . . . . . 14 |- ( J e. Top -> ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) )
88		forn 6118	. . . . . . . . . . . . . 14 |- ( ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) -> ran ( r e. J |-> ( U. J \ r ) ) = ( Clsd ` J ) )
89	87, 88	syl 17	. . . . . . . . . . . . 13 |- ( J e. Top -> ran ( r e. J |-> ( U. J \ r ) ) = ( Clsd ` J ) )
90	82, 89	syl5sseq 3653	. . . . . . . . . . . 12 |- ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ( Clsd ` J ) )
91		fvex 6201	. . . . . . . . . . . . 13 |- ( Clsd ` J ) e. _V
92	91	elpw2 4828	. . . . . . . . . . . 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 224	. . . . . . . . . . 11 |- ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) )
94	93	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) )
95		elfi 8319	. . . . . . . . . 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 695	. . . . . . . . 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 4046	. . . . . . . . . . . . . 14 |- ( ( ( ~P y i^i Fin ) i^i { (/) } ) u. ( ( ~P y i^i Fin ) \ { (/) } ) ) = ( ~P y i^i Fin )
98	97	rexeqi 3143	. . . . . . . . . . . . 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 3793	. . . . . . . . . . . . 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 266	. . . . . . . . . . . 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 3834	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ~P y i^i Fin ) i^i { (/) } ) C_ { (/) }
102	101	sseli 3599	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> z e. { (/) } )
103		elsni 4194	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. { (/) } -> z = (/) )
104	102, 103	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> z = (/) )
105	104	unieqd 4446	. . . . . . . . . . . . . . . . . . 19 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> U. z = U. (/) )
106		uni0 4465	. . . . . . . . . . . . . . . . . . 19 |- U. (/) = (/)
107	105, 106	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> U. z = (/) )
108	107	eqeq2d 2632	. . . . . . . . . . . . . . . . 17 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> ( U. J = U. z <-> U. J = (/) ) )
109	108	biimpd 219	. . . . . . . . . . . . . . . 16 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> ( U. J = U. z -> U. J = (/) ) )
110	109	rexlimiv 3027	. . . . . . . . . . . . . . 15 |- ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z -> U. J = (/) )
111		ssid 3624	. . . . . . . . . . . . . . . . . . . 20 |- y C_ y
112	111	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y C_ y )
113		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J = (/) )
114		0ss 3972	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (/) C_ U. y
115	113, 114	syl6eqss 3655	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J C_ U. y )
116	25	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y C_ U. J )
117	115, 116	eqssd 3620	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J = U. y )
118	117, 113	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y = (/) )
119	118, 3	syl6eqel 2709	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y e. Fin )
120		pwfi 8261	. . . . . . . . . . . . . . . . . . . . 21 |- ( U. y e. Fin <-> ~P U. y e. Fin )
121	119, 120	sylib 208	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> ~P U. y e. Fin )
122		pwuni 4474	. . . . . . . . . . . . . . . . . . . 20 |- y C_ ~P U. y
123		ssfi 8180	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ~P U. y e. Fin /\ y C_ ~P U. y ) -> y e. Fin )
124	121, 122, 123	sylancl 694	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y e. Fin )
125		elfpw 8268	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( ~P y i^i Fin ) <-> ( y C_ y /\ y e. Fin ) )
126	112, 124, 125	sylanbrc 698	. . . . . . . . . . . . . . . . . 18 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y e. ( ~P y i^i Fin ) )
127		simprl 794	. . . . . . . . . . . . . . . . . 18 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y =/= (/) )
128		eldifsn 4317	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( ( ~P y i^i Fin ) \ { (/) } ) <-> ( y e. ( ~P y i^i Fin ) /\ y =/= (/) ) )
129	126, 127, 128	sylanbrc 698	. . . . . . . . . . . . . . . . 17 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y e. ( ( ~P y i^i Fin ) \ { (/) } ) )
130		unieq 4444	. . . . . . . . . . . . . . . . . . 19 |- ( z = y -> U. z = U. y )
131	130	eqeq2d 2632	. . . . . . . . . . . . . . . . . 18 |- ( z = y -> ( U. J = U. z <-> U. J = U. y ) )
132	131	rspcev 3309	. . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . . 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 643	. . . . . . . . . . . . . . 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 34	. . . . . . . . . . . . . 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 395	. . . . . . . . . . . . 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 399	. . . . . . . . . . . . 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 215	. . . . . . . . . . . 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 272	. . . . . . . . . . 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 3732	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) -> z e. ( ~P y i^i Fin ) )
142	141	adantl 482	. . . . . . . . . . . . . . . . . . 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 208	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( z C_ y /\ z e. Fin ) )
144	143	simpld 475	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z C_ y )
145		simpllr 799	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> y C_ J )
146	144, 145	sstrd 3613	. . . . . . . . . . . . . . . 16 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z C_ J )
147	146	unissd 4462	. . . . . . . . . . . . . . 15 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> U. z C_ U. J )
148		eqss 3618	. . . . . . . . . . . . . . . 16 |- ( U. z = U. J <-> ( U. z C_ U. J /\ U. J C_ U. z ) )
149	148	baib 944	. . . . . . . . . . . . . . 15 |- ( U. z C_ U. J -> ( U. z = U. J <-> U. J C_ U. z ) )
150	147, 149	syl 17	. . . . . . . . . . . . . 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 2629	. . . . . . . . . . . . . 14 |- ( U. z = U. J <-> U. J = U. z )
152		ssdif0 3942	. . . . . . . . . . . . . . 15 |- ( U. J C_ U. z <-> ( U. J \ U. z ) = (/) )
153		eqcom 2629	. . . . . . . . . . . . . . 15 |- ( ( U. J \ U. z ) = (/) <-> (/) = ( U. J \ U. z ) )
154	152, 153	bitri 264	. . . . . . . . . . . . . 14 |- ( U. J C_ U. z <-> (/) = ( U. J \ U. z ) )
155	150, 151, 154	3bitr3g 302	. . . . . . . . . . . . 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 5127	. . . . . . . . . . . . . . . . . 18 |- ( ( r e. y |-> ( U. J \ r ) ) " z ) = ran ( ( r e. y |-> ( U. J \ r ) ) |` z )
157	144	resmptd 5452	. . . . . . . . . . . . . . . . . . 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 ) ) )
158	157	rneqd 5353	. . . . . . . . . . . . . . . . . 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 ) ) )
159	156, 158	syl5eq 2668	. . . . . . . . . . . . . . . . 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 ) ) )
160	159	inteqd 4480	. . . . . . . . . . . . . . . 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 ) ) )
161	59	ralrimivw 2967	. . . . . . . . . . . . . . . . . 18 |- ( J e. Top -> A. r e. z ( U. J \ r ) e. _V )
162	161	ad3antrrr 766	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> A. r e. z ( U. J \ r ) e. _V )
163		dfiin3g 5379	. . . . . . . . . . . . . . . . 17 |- ( A. r e. z ( U. J \ r ) e. _V -> |^|_ r e. z ( U. J \ r ) = |^| ran ( r e. z |-> ( U. J \ r ) ) )
164	162, 163	syl 17	. . . . . . . . . . . . . . . 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 ) ) )
165		eldifsn 4317	. . . . . . . . . . . . . . . . . . 19 |- ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) <-> ( z e. ( ~P y i^i Fin ) /\ z =/= (/) ) )
166	165	simprbi 480	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) -> z =/= (/) )
167	166	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z =/= (/) )
168		iindif2 4589	. . . . . . . . . . . . . . . . 17 |- ( z =/= (/) -> |^|_ r e. z ( U. J \ r ) = ( U. J \ U_ r e. z r ) )
169	167, 168	syl 17	. . . . . . . . . . . . . . . 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 ) )
170	160, 164, 169	3eqtr2d 2662	. . . . . . . . . . . . . . 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 ) )
171		uniiun 4573	. . . . . . . . . . . . . . . 16 |- U. z = U_ r e. z r
172	171	difeq2i 3725	. . . . . . . . . . . . . . 15 |- ( U. J \ U. z ) = ( U. J \ U_ r e. z r )
173	170, 172	syl6eqr 2674	. . . . . . . . . . . . . 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 ) )
174	173	eqeq2d 2632	. . . . . . . . . . . . 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 ) ) )
175	155, 174	bitr4d 271	. . . . . . . . . . . 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 ) ) )
176	175	rexbidva 3049	. . . . . . . . . . 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 ) ) )
177	140, 176	bitrd 268	. . . . . . . . . 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 ) ) )
178		imaeq2 5462	. . . . . . . . . . . . . . . . . . . 20 |- ( z = (/) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = ( ( r e. y |-> ( U. J \ r ) ) " (/) ) )
179		ima0 5481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( r e. y |-> ( U. J \ r ) ) " (/) ) = (/)
180	178, 179	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19 |- ( z = (/) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = (/) )
181	180	inteqd 4480	. . . . . . . . . . . . . . . . . 18 |- ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = |^| (/) )
182		int0 4490	. . . . . . . . . . . . . . . . . 18 |- |^| (/) = _V
183	181, 182	syl6eq 2672	. . . . . . . . . . . . . . . . 17 |- ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = _V )
184	183	neeq1d 2853	. . . . . . . . . . . . . . . 16 |- ( z = (/) -> ( |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) =/= (/) <-> _V =/= (/) ) )
185	15, 184	mpbiri 248	. . . . . . . . . . . . . . 15 |- ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) =/= (/) )
186	185	necomd 2849	. . . . . . . . . . . . . 14 |- ( z = (/) -> (/) =/= |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) )
187	186	necon2i 2828	. . . . . . . . . . . . 13 |- ( (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) -> z =/= (/) )
188	165	rbaibr 946	. . . . . . . . . . . . 13 |- ( z =/= (/) -> ( z e. ( ~P y i^i Fin ) <-> z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) )
189	187, 188	syl 17	. . . . . . . . . . . 12 |- ( (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) -> ( z e. ( ~P y i^i Fin ) <-> z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) )
190	189	pm5.32ri 670	. . . . . . . . . . 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 ) ) )
191	190	rexbii2 3039	. . . . . . . . . 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 ) )
192	177, 191	syl6bbr 278	. . . . . . . . 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 ) ) )
193	80, 96, 192	3bitr4rd 301	. . . . . . . 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 ) ) ) )
194	39, 193	imbi12d 334	. . . . . . 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 ) ) ) ) )
195	24, 194	pm2.61dane 2881	. . . . . 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 ) ) ) ) )
196	60	adantr 481	. . . . . . . . . . 11 |- ( ( J e. Top /\ y C_ J ) -> A. r e. y ( U. J \ r ) e. _V )
197		dfiin3g 5379	. . . . . . . . . . 11 |- ( A. r e. y ( U. J \ r ) e. _V -> |^|_ r e. y ( U. J \ r ) = |^| ran ( r e. y |-> ( U. J \ r ) ) )
198	196, 197	syl 17	. . . . . . . . . 10 |- ( ( J e. Top /\ y C_ J ) -> |^|_ r e. y ( U. J \ r ) = |^| ran ( r e. y |-> ( U. J \ r ) ) )
199	45	inteqd 4480	. . . . . . . . . 10 |- ( ( J e. Top /\ y C_ J ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = |^| ran ( r e. y |-> ( U. J \ r ) ) )
200	198, 199	eqtr4d 2659	. . . . . . . . 9 |- ( ( J e. Top /\ y C_ J ) -> |^|_ r e. y ( U. J \ r ) = |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) )
201	200	eqeq1d 2624	. . . . . . . 8 |- ( ( J e. Top /\ y C_ J ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = (/) ) )
202		nne 2798	. . . . . . . 8 |- ( -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = (/) )
203	201, 202	syl6bbr 278	. . . . . . 7 |- ( ( J e. Top /\ y C_ J ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) )
204	203	imbi1d 331	. . . . . 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 ) ) ) ) )
205	195, 204	bitrd 268	. . . . 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 ) ) ) ) )
206		con1b 348	. . . . 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 ) =/= (/) ) )
207	205, 206	syl6bb 276	. . . 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 ) =/= (/) ) ) )
208	1, 207	sylan2 491	. . 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 ) =/= (/) ) ) )
209	208	ralbidva 2985	. 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 ) =/= (/) ) ) )
210	56	iscmp 21191	. . 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 ) ) )
211	210	baib 944	. 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 ) ) )
212	93	adantr 481	. . 3 |- ( ( J e. Top /\ y e. ~P J ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) )
213		simpl 473	. . . . 5 |- ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> J e. Top )
214		funmpt 5926	. . . . . 6 |- Fun ( r e. J |-> ( U. J \ r ) )
215	214	a1i 11	. . . . 5 |- ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> Fun ( r e. J |-> ( U. J \ r ) ) )
216		elpwi 4168	. . . . . . 7 |- ( x e. ~P ( Clsd ` J ) -> x C_ ( Clsd ` J ) )
217		foima 6120	. . . . . . . . 9 |- ( ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) -> ( ( r e. J |-> ( U. J \ r ) ) " J ) = ( Clsd ` J ) )
218	87, 217	syl 17	. . . . . . . 8 |- ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " J ) = ( Clsd ` J ) )
219	218	sseq2d 3633	. . . . . . 7 |- ( J e. Top -> ( x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) <-> x C_ ( Clsd ` J ) ) )
220	216, 219	syl5ibr 236	. . . . . 6 |- ( J e. Top -> ( x e. ~P ( Clsd ` J ) -> x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) ) )
221	220	imp 445	. . . . 5 |- ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) )
222		ssimaexg 6264	. . . . 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 ) ) )
223	213, 215, 221, 222	syl3anc 1326	. . . 4 |- ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> E. y ( y C_ J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
224		df-rex 2918	. . . . 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 ) ) )
225		selpw 4165	. . . . . . 7 |- ( y e. ~P J <-> y C_ J )
226	225	anbi1i 731	. . . . . 6 |- ( ( y e. ~P J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) <-> ( y C_ J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
227	226	exbii 1774	. . . . 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 ) ) )
228	224, 227	bitri 264	. . . 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 ) ) )
229	223, 228	sylibr 224	. . 3 |- ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> E. y e. ~P J x = ( ( r e. J |-> ( U. J \ r ) ) " y ) )
230		simpr 477	. . . . . . 7 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> x = ( ( r e. J |-> ( U. J \ r ) ) " y ) )
231	230	fveq2d 6195	. . . . . 6 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( fi ` x ) = ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
232	231	eleq2d 2687	. . . . 5 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( (/) e. ( fi ` x ) <-> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) )
233	232	notbid 308	. . . 4 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( -. (/) e. ( fi ` x ) <-> -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) )
234	230	inteqd 4480	. . . . 5 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| x = |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) )
235	234	neeq1d 2853	. . . 4 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( |^| x =/= (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) )
236	233, 235	imbi12d 334	. . 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 ) =/= (/) ) ) )
237	212, 229, 236	ralxfrd 4879	. 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 ) =/= (/) ) ) )
238	209, 211, 237	3bitr4d 300	1 |- ( J e. Top -> ( J e. Comp <-> A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   {csn 4177   U.cuni 4436   |^|cint 4475   U_ciun 4520   |^|_ciin 4521   |-> cmpt 4729   `'ccnv 5113   ran crn 5115   |` cres 5116   "cima 5117   Fun wfun 5882   Fn wfn 5883   -onto->wfo 5886   -1-1-onto->wf1o 5887   ` cfv 5888   Fincfn 7955   ficfi 8316   Topctop 20698   Clsdccld 20820   Compccmp 21189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fi 8317  df-top 20699  df-cld 20823  df-cmp 21190

This theorem is referenced by:  cmpfii  21212  fclscmp  21834  heibor1lem  33608