Theorem cmpfi 19886

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 4006	. . . 4 |- ( y e. ~P J -> y C_ J )
2		0ss 3800	. . . . . . . . . . 11 |- (/) C_ y
3		0fin 7749	. . . . . . . . . . 11 |- (/) e. Fin
4		elfpw 7824	. . . . . . . . . . 11 |- ( (/) e. ( ~P y i^i Fin ) <-> ( (/) C_ y /\ (/) e. Fin ) )
5	2, 3, 4	mpbir2an 920	. . . . . . . . . 10 |- (/) e. ( ~P y i^i Fin )
6		simprr 757	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. J = U. y )
7		simprl 756	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> y = (/) )
8	7	unieqd 4244	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. y = U. (/) )
9	6, 8	eqtrd 2484	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. J = U. (/) )
10		unieq 4242	. . . . . . . . . . . 12 |- ( z = (/) -> U. z = U. (/) )
11	10	eqeq2d 2457	. . . . . . . . . . 11 |- ( z = (/) -> ( U. J = U. z <-> U. J = U. (/) ) )
12	11	rspcev 3196	. . . . . . . . . 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 3778	. . . . . . . . . 10 |- _V =/= (/)
16		iineq1 4330	. . . . . . . . . . . . . 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 4373	. . . . . . . . . . . . 13 |- |^|_ r e. (/) ( U. J \ r ) = _V
19	17, 18	syl6eq 2500	. . . . . . . . . . . 12 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> |^|_ r e. y ( U. J \ r ) = _V )
20	19	eqeq1d 2445	. . . . . . . . . . 11 |- ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> _V = (/) ) )
21	20	necon3bbid 2690	. . . . . . . . . 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 4255	. . . . . . . . . . . 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 3504	. . . . . . . . . . . 12 |- ( U. y = U. J <-> ( U. y C_ U. J /\ U. J C_ U. y ) )
28	27	baib 903	. . . . . . . . . . 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 2452	. . . . . . . . . 10 |- ( U. y = U. J <-> U. J = U. y )
31		ssdif0 3871	. . . . . . . . . 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 4384	. . . . . . . . . . . 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 4368	. . . . . . . . . . . 12 |- U. y = U_ r e. y r
36	35	difeq2i 3604	. . . . . . . . . . 11 |- ( U. J \ U. y ) = ( U. J \ U_ r e. y r )
37	34, 36	syl6eqr 2502	. . . . . . . . . 10 |- ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> |^|_ r e. y ( U. J \ r ) = ( U. J \ U. y ) )
38	37	eqeq1d 2445	. . . . . . . . 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 5338	. . . . . . . . . . . 12 |- ( ( r e. y |-> ( U. J \ r ) ) " z ) C_ ran ( r e. y |-> ( U. J \ r ) )
41		df-ima 5002	. . . . . . . . . . . . . 14 |- ( ( r e. J |-> ( U. J \ r ) ) " y ) = ran ( ( r e. J |-> ( U. J \ r ) ) |` y )
42		resmpt 5313	. . . . . . . . . . . . . . . 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 5220	. . . . . . . . . . . . . 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 2496	. . . . . . . . . . . . 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 3538	. . . . . . . . . . 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 5614	. . . . . . . . . . . 12 |- Fun ( r e. y |-> ( U. J \ r ) )
49		elfpw 7824	. . . . . . . . . . . . . 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 7815	. . . . . . . . . . . 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 7824	. . . . . . . . . . 11 |- ( ( ( r e. y |-> ( U. J \ r ) ) " z ) e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) <-> ( ( ( r e. y |-> ( U. J \ r ) ) " z ) C_ ( ( r e. J |-> ( U. J \ r ) ) " y ) /\ ( ( r e. y |-> ( U. J \ r ) ) " z ) e. Fin ) )
55	47, 53, 54	sylanbrc 664	. . . . . . . . . 10 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ~P y i^i Fin ) ) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) )
56		eqid 2443	. . . . . . . . . . . . . . . . 17 |- U. J = U. J
57	56	topopn 19393	. . . . . . . . . . . . . . . 16 |- ( J e. Top -> U. J e. J )
58		difexg 4585	. . . . . . . . . . . . . . . 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 2858	. . . . . . . . . . . . . 14 |- ( J e. Top -> A. r e. y ( U. J \ r ) e. _V )
61		eqid 2443	. . . . . . . . . . . . . . 15 |- ( r e. y |-> ( U. J \ r ) ) = ( r e. y |-> ( U. J \ r ) )
62	61	fnmpt 5697	. . . . . . . . . . . . . 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 7824	. . . . . . . . . . . . . . 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 3525	. . . . . . . . . . . 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 7828	. . . . . . . . . . . 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 1229	. . . . . . . . . . 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 2452	. . . . . . . . . . . 12 |- ( ( ( r e. y |-> ( U. J \ r ) ) " z ) = w <-> w = ( ( r e. y |-> ( U. J \ r ) ) " z ) )
75	74	rexbii 2945	. . . . . . . . . . 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 4276	. . . . . . . . . . 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 2457	. . . . . . . . . 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 4652	. . . . . . . . 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 4567	. . . . . . . . . 10 |- (/) e. _V
82		imassrn 5338	. . . . . . . . . . . . 13 |- ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ran ( r e. J |-> ( U. J \ r ) )
83		eqid 2443	. . . . . . . . . . . . . . . . 17 |- ( r e. J |-> ( U. J \ r ) ) = ( r e. J |-> ( U. J \ r ) )
84	56, 83	opncldf1 19563	. . . . . . . . . . . . . . . 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 5813	. . . . . . . . . . . . . . 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 5788	. . . . . . . . . . . . . 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 3537	. . . . . . . . . . . 12 |- ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ( Clsd ` J ) )
91		fvex 5866	. . . . . . . . . . . . 13 |- ( Clsd ` J ) e. _V
92	91	elpw2 4601	. . . . . . . . . . . 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 7875	. . . . . . . . . 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 3892	. . . . . . . . . . . . . 14 |- ( ( ( ~P y i^i Fin ) i^i { (/) } ) u. ( ( ~P y i^i Fin ) \ { (/) } ) ) = ( ~P y i^i Fin )
98	97	rexeqi 3045	. . . . . . . . . . . . 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 3669	. . . . . . . . . . . . 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 3704	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ~P y i^i Fin ) i^i { (/) } ) C_ { (/) }
102	101	sseli 3485	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> z e. { (/) } )
103		elsni 4039	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. { (/) } -> z = (/) )
104	102, 103	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> z = (/) )
105	104	unieqd 4244	. . . . . . . . . . . . . . . . . . 19 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> U. z = U. (/) )
106		uni0 4261	. . . . . . . . . . . . . . . . . . 19 |- U. (/) = (/)
107	105, 106	syl6eq 2500	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> U. z = (/) )
108	107	eqeq2d 2457	. . . . . . . . . . . . . . . . 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 2929	. . . . . . . . . . . . . . 15 |- ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z -> U. J = (/) )
111		ssid 3508	. . . . . . . . . . . . . . . . . . . 20 |- y C_ y
112	111	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y C_ y )
113		simprr 757	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J = (/) )
114		0ss 3800	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (/) C_ U. y
115	113, 114	syl6eqss 3539	. . . . . . . . . . . . . . . . . . . . . . . 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 3506	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J = U. y )
118	117, 113	eqtr3d 2486	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y = (/) )
119	118, 3	syl6eqel 2539	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y e. Fin )
120		pwfi 7817	. . . . . . . . . . . . . . . . . . . . 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 4668	. . . . . . . . . . . . . . . . . . . 20 |- y C_ ~P U. y
123		ssfi 7742	. . . . . . . . . . . . . . . . . . . 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 7824	. . . . . . . . . . . . . . . . . . 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 756	. . . . . . . . . . . . . . . . . 18 |- ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y =/= (/) )
128		eldifsn 4140	. . . . . . . . . . . . . . . . . 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 4242	. . . . . . . . . . . . . . . . . . 19 |- ( z = y -> U. z = U. y )
131	130	eqeq2d 2457	. . . . . . . . . . . . . . . . . 18 |- ( z = y -> ( U. J = U. z <-> U. J = U. y ) )
132	131	rspcev 3196	. . . . . . . . . . . . . . . . 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 3611	. . . . . . . . . . . . . . . . . . . 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 760	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> y C_ J )
146	144, 145	sstrd 3499	. . . . . . . . . . . . . . . 16 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z C_ J )
147	146	unissd 4258	. . . . . . . . . . . . . . 15 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> U. z C_ U. J )
148		eqss 3504	. . . . . . . . . . . . . . . 16 |- ( U. z = U. J <-> ( U. z C_ U. J /\ U. J C_ U. z ) )
149	148	baib 903	. . . . . . . . . . . . . . 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 2452	. . . . . . . . . . . . . 14 |- ( U. z = U. J <-> U. J = U. z )
152		ssdif0 3871	. . . . . . . . . . . . . . 15 |- ( U. J C_ U. z <-> ( U. J \ U. z ) = (/) )
153		eqcom 2452	. . . . . . . . . . . . . . 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 5002	. . . . . . . . . . . . . . . . . 18 |- ( ( r e. y |-> ( U. J \ r ) ) " z ) = ran ( ( r e. y |-> ( U. J \ r ) ) |` z )
157	144	resmptd 5315	. . . . . . . . . . . . . . . . . . 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 5220	. . . . . . . . . . . . . . . . . 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 2496	. . . . . . . . . . . . . . . . 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 4276	. . . . . . . . . . . . . . . 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 2858	. . . . . . . . . . . . . . . . . 18 |- ( J e. Top -> A. r e. z ( U. J \ r ) e. _V )
162	161	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 )
163		dfiin3g 5246	. . . . . . . . . . . . . . . . 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 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 ) ) )
165		eldifsn 4140	. . . . . . . . . . . . . . . . . . 19 |- ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) <-> ( z e. ( ~P y i^i Fin ) /\ z =/= (/) ) )
166	165	simprbi 464	. . . . . . . . . . . . . . . . . 18 |- ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) -> z =/= (/) )
167	166	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z =/= (/) )
168		iindif2 4384	. . . . . . . . . . . . . . . . 17 |- ( z =/= (/) -> |^|_ r e. z ( U. J \ r ) = ( U. J \ U_ r e. z r ) )
169	167, 168	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 ) )
170	160, 164, 169	3eqtr2d 2490	. . . . . . . . . . . . . . 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 4368	. . . . . . . . . . . . . . . 16 |- U. z = U_ r e. z r
172	171	difeq2i 3604	. . . . . . . . . . . . . . 15 |- ( U. J \ U. z ) = ( U. J \ U_ r e. z r )
173	170, 172	syl6eqr 2502	. . . . . . . . . . . . . 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 2457	. . . . . . . . . . . . 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 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 ) ) )
176	175	rexbidva 2951	. . . . . . . . . . 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 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 ) ) )
178		imaeq2 5323	. . . . . . . . . . . . . . . . . . . 20 |- ( z = (/) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = ( ( r e. y |-> ( U. J \ r ) ) " (/) ) )
179		ima0 5342	. . . . . . . . . . . . . . . . . . . 20 |- ( ( r e. y |-> ( U. J \ r ) ) " (/) ) = (/)
180	178, 179	syl6eq 2500	. . . . . . . . . . . . . . . . . . 19 |- ( z = (/) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = (/) )
181	180	inteqd 4276	. . . . . . . . . . . . . . . . . 18 |- ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = |^| (/) )
182		int0 4285	. . . . . . . . . . . . . . . . . 18 |- |^| (/) = _V
183	181, 182	syl6eq 2500	. . . . . . . . . . . . . . . . 17 |- ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = _V )
184	183	neeq1d 2720	. . . . . . . . . . . . . . . 16 |- ( z = (/) -> ( |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) =/= (/) <-> _V =/= (/) ) )
185	15, 184	mpbiri 233	. . . . . . . . . . . . . . 15 |- ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) =/= (/) )
186	185	necomd 2714	. . . . . . . . . . . . . 14 |- ( z = (/) -> (/) =/= |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) )
187	186	necon2i 2686	. . . . . . . . . . . . 13 |- ( (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) -> z =/= (/) )
188	165	rbaibr 905	. . . . . . . . . . . . 13 |- ( z =/= (/) -> ( z e. ( ~P y i^i Fin ) <-> z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) )
189	187, 188	syl 16	. . . . . . . . . . . 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 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 ) ) )
191	190	rexbii2 2943	. . . . . . . . . 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 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 ) ) )
193	80, 96, 192	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 ) ) ) )
194	39, 193	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 ) ) ) ) )
195	24, 194	pm2.61dane 2761	. . . . . 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 465	. . . . . . . . . . 11 |- ( ( J e. Top /\ y C_ J ) -> A. r e. y ( U. J \ r ) e. _V )
197		dfiin3g 5246	. . . . . . . . . . 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 16	. . . . . . . . . 10 |- ( ( J e. Top /\ y C_ J ) -> |^|_ r e. y ( U. J \ r ) = |^| ran ( r e. y |-> ( U. J \ r ) ) )
199	45	inteqd 4276	. . . . . . . . . 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 2487	. . . . . . . . 9 |- ( ( J e. Top /\ y C_ J ) -> |^|_ r e. y ( U. J \ r ) = |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) )
201	200	eqeq1d 2445	. . . . . . . 8 |- ( ( J e. Top /\ y C_ J ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = (/) ) )
202		nne 2644	. . . . . . . 8 |- ( -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = (/) )
203	201, 202	syl6bbr 263	. . . . . . 7 |- ( ( J e. Top /\ y C_ J ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) )
204	203	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 ) ) ) ) )
205	195, 204	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 ) ) ) ) )
206		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 ) =/= (/) ) )
207	205, 206	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 ) =/= (/) ) ) )
208	1, 207	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 ) =/= (/) ) ) )
209	208	ralbidva 2879	. 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 19866	. . 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 903	. 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 465	. . 3 |- ( ( J e. Top /\ y e. ~P J ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) )
213		simpl 457	. . . . 5 |- ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> J e. Top )
214		funmpt 5614	. . . . . 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 4006	. . . . . . 7 |- ( x e. ~P ( Clsd ` J ) -> x C_ ( Clsd ` J ) )
217		foima 5790	. . . . . . . . 9 |- ( ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) -> ( ( r e. J |-> ( U. J \ r ) ) " J ) = ( Clsd ` J ) )
218	87, 217	syl 16	. . . . . . . 8 |- ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " J ) = ( Clsd ` J ) )
219	218	sseq2d 3517	. . . . . . 7 |- ( J e. Top -> ( x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) <-> x C_ ( Clsd ` J ) ) )
220	216, 219	syl5ibr 221	. . . . . 6 |- ( J e. Top -> ( x e. ~P ( Clsd ` J ) -> x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) ) )
221	220	imp 429	. . . . 5 |- ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) )
222		ssimaexg 5924	. . . . 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 1229	. . . 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 2799	. . . . 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 4004	. . . . . . 7 |- ( y e. ~P J <-> y C_ J )
226	225	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 ) ) )
227	226	exbii 1654	. . . . 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 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 ) ) )
229	223, 228	sylibr 212	. . 3 |- ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> E. y e. ~P J x = ( ( r e. J |-> ( U. J \ r ) ) " y ) )
230		simpr 461	. . . . . . 7 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> x = ( ( r e. J |-> ( U. J \ r ) ) " y ) )
231	230	fveq2d 5860	. . . . . 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 2513	. . . . 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 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 ) ) ) )
234	230	inteqd 4276	. . . . 5 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| x = |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) )
235	234	neeq1d 2720	. . . 4 |- ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( |^| x =/= (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) )
236	233, 235	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 ) =/= (/) ) ) )
237	212, 229, 236	ralxfrd 4651	. 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 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 1383   E.wex 1599   e. wcel 1804   =/= wne 2638   A.wral 2793   E.wrex 2794   _Vcvv 3095   \ cdif 3458   u. cun 3459   i^i cin 3460   C_ wss 3461   (/)c0 3770   ~Pcpw 3997   {csn 4014   U.cuni 4234   |^|cint 4271   U_ciun 4315   |^|_ciin 4316   |-> cmpt 4495   `'ccnv 4988   ran crn 4990   |` cres 4991   "cima 4992   Fun wfun 5572   Fn wfn 5573   -onto->wfo 5576   -1-1-onto->wf1o 5577   ` cfv 5578   Fincfn 7518   ficfi 7872   Topctop 19372   Clsdccld 19495   Compccmp 19864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-iin 4318  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-om 6686  df-1st 6785  df-2nd 6786  df-recs 7044  df-rdg 7078  df-1o 7132  df-2o 7133  df-oadd 7136  df-er 7313  df-map 7424  df-en 7519  df-dom 7520  df-sdom 7521  df-fin 7522  df-fi 7873  df-top 19377  df-cld 19498  df-cmp 19865

This theorem is referenced by:  cmpfii  19887  fclscmp  20509  heibor1lem  30281