Theorem compfipin0lem 15435

Description: Lemma for compfipin0 15436.

Assertion

Ref	Expression
compfipin0lem	|- (J e. Top -> (A.x e. ~P (Clsd` J)(A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x) -> A.y e. ~P J(A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y)))

Distinct variable group:   x,w,y,z,J

Proof of Theorem compfipin0lem

Step	Hyp	Ref	Expression
1		imassrn 4278	. . . . . . 7 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) C_ ran {<.r, s>. | (r e. J /\ s = (U.J \ r))}
2		eqid 1884	. . . . . . . . . 10 |- U.J = U.J
3		eqid 1884	. . . . . . . . . 10 |- {<.r, s>. | (r e. J /\ s = (U.J \ r))} = {<.r, s>. | (r e. J /\ s = (U.J \ r))}
4	2, 3	opncldf1 15402	. . . . . . . . 9 |- (J e. Top -> {<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1-onto->(Clsd` J))
5		f1ofo 4643	. . . . . . . . 9 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1-onto->(Clsd` J) -> {<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-onto->(Clsd` J))
6		forn 4620	. . . . . . . . 9 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-onto->(Clsd` J) -> ran {<.r, s>. | (r e. J /\ s = (U.J \ r))} = (Clsd` J))
7	4, 5, 6	3syl 24	. . . . . . . 8 |- (J e. Top -> ran {<.r, s>. | (r e. J /\ s = (U.J \ r))} = (Clsd` J))
8	7	sseq2d 2645	. . . . . . 7 |- (J e. Top -> (({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) C_ ran {<.r, s>. | (r e. J /\ s = (U.J \ r))} <-> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) C_ (Clsd` J)))
9	1, 8	mpbii 210	. . . . . 6 |- (J e. Top -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) C_ (Clsd` J))
10		fvex 4689	. . . . . . 7 |- (Clsd` J) e. _V
11	10	elpw2 3464	. . . . . 6 |- (({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) e. ~P(Clsd` J) <-> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) C_ (Clsd` J))
12	9, 11	sylibr 217	. . . . 5 |- (J e. Top -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) e. ~P(Clsd` J))
13	12	adantr 425	. . . 4 |- ((J e. Top /\ y e. ~PJ) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) e. ~P(Clsd` J))
14		pweq 3036	. . . . . . . 8 |- (x = ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) -> ~Px = ~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y))
15	14	ineq1d 2795	. . . . . . 7 |- (x = ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) -> (~Px i^i Fin) = (~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) i^i Fin))
16	15	raleqdv 2269	. . . . . 6 |- (x = ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) -> (A.w e. (~Px i^i Fin) -. (/) = |^|w <-> A.w e. (~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) i^i Fin) -. (/) = |^|w))
17		inteq 3217	. . . . . . . 8 |- (x = ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) -> |^|x = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y))
18	17	eqeq2d 1895	. . . . . . 7 |- (x = ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) -> ((/) = |^|x <-> (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)))
19	18	notbid 673	. . . . . 6 |- (x = ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) -> (-. (/) = |^|x <-> -. (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)))
20	16, 19	imbi12d 688	. . . . 5 |- (x = ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) -> ((A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x) <-> (A.w e. (~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) i^i Fin) -. (/) = |^|w -> -. (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y))))
21	20	rcla4v 2376	. . . 4 |- (({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) e. ~P(Clsd` J) -> (A.x e. ~P (Clsd` J)(A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x) -> (A.w e. (~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) i^i Fin) -. (/) = |^|w -> -. (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y))))
22	13, 21	syl 12	. . 3 |- ((J e. Top /\ y e. ~PJ) -> (A.x e. ~P (Clsd` J)(A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x) -> (A.w e. (~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) i^i Fin) -. (/) = |^|w -> -. (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y))))
23		elin 2786	. . . . . . . . . 10 |- ((/) e. (~Py i^i Fin) <-> ((/) e. ~Py /\ (/) e. Fin))
24		0elpw 3473	. . . . . . . . . 10 |- (/) e. ~Py
25		emfin 10165	. . . . . . . . . 10 |- (/) e. Fin
26	23, 24, 25	mpbir2an 800	. . . . . . . . 9 |- (/) e. (~Py i^i Fin)
27		uni0 3205	. . . . . . . . . 10 |- U.(/) = (/)
28	27	eqcomi 1888	. . . . . . . . 9 |- (/) = U.(/)
29		unieq 3185	. . . . . . . . . . 11 |- (z = (/) -> U.z = U.(/))
30	29	eqeq2d 1895	. . . . . . . . . 10 |- (z = (/) -> ((/) = U.z <-> (/) = U.(/)))
31	30	rcla4ev 2381	. . . . . . . . 9 |- (((/) e. (~Py i^i Fin) /\ (/) = U.(/)) -> E.z e. (~Py i^i Fin)(/) = U.z)
32	26, 28, 31	mp2an 761	. . . . . . . 8 |- E.z e. (~Py i^i Fin)(/) = U.z
33		eqeq1 1890	. . . . . . . . 9 |- (U.J = (/) -> (U.J = U.z <-> (/) = U.z))
34	33	rexbidv 2124	. . . . . . . 8 |- (U.J = (/) -> (E.z e. (~Py i^i Fin)U.J = U.z <-> E.z e. (~Py i^i Fin)(/) = U.z))
35	32, 34	mpbiri 211	. . . . . . 7 |- (U.J = (/) -> E.z e. (~Py i^i Fin)U.J = U.z)
36		dfrex2 2116	. . . . . . 7 |- (E.z e. (~Py i^i Fin)U.J = U.z <-> -. A.z e. (~Py i^i Fin) -. U.J = U.z)
37	35, 36	sylib 215	. . . . . 6 |- (U.J = (/) -> -. A.z e. (~Py i^i Fin) -. U.J = U.z)
38	37	pm2.21d 94	. . . . 5 |- (U.J = (/) -> (A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y))
39	38	a1i13 15326	. . . 4 |- ((J e. Top /\ y e. ~PJ) -> (U.J = (/) -> ((A.w e. (~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) i^i Fin) -. (/) = |^|w -> -. (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) -> (A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y))))
40		elin 2786	. . . . . . . . . . . . 13 |- ((`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. (~Py i^i Fin) <-> ((`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. ~Py /\ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. Fin))
41		imass2 4299	. . . . . . . . . . . . . . . . . 18 |- (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)))
42	41	adantl 424	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ y e. ~PJ) /\ w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)))
43		f1imacnv 4656	. . . . . . . . . . . . . . . . . . . 20 |- (({<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1->(Clsd` J) /\ y C_ J) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) = y)
44		f1of1 4634	. . . . . . . . . . . . . . . . . . . . 21 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1-onto->(Clsd` J) -> {<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1->(Clsd` J))
45	4, 44	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (J e. Top -> {<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1->(Clsd` J))
46	43, 45	sylan 497	. . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ y C_ J) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) = y)
47		visset 2295	. . . . . . . . . . . . . . . . . . . 20 |- y e. _V
48	47	elpw 3037	. . . . . . . . . . . . . . . . . . 19 |- (y e. ~PJ <-> y C_ J)
49	46, 48	sylan2b 501	. . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ y e. ~PJ) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) = y)
50	49	adantr 425	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ y e. ~PJ) /\ w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) = y)
51	42, 50	sseqtrd 2653	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ y e. ~PJ) /\ w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) C_ y)
52	51	3adantl3 1034	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) C_ y)
53	52	adantrr 431	. . . . . . . . . . . . . 14 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) C_ y)
54		f1ocnv 4651	. . . . . . . . . . . . . . . . . 18 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1-onto->(Clsd` J) -> `'{<.r, s>. | (r e. J /\ s = (U.J \ r))}:(Clsd` J)-1-1-onto->J)
55		f1ofun 4637	. . . . . . . . . . . . . . . . . . 19 |- (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}:(Clsd` J)-1-1-onto->J -> Fun `'{<.r, s>. | (r e. J /\ s = (U.J \ r))})
56		visset 2295	. . . . . . . . . . . . . . . . . . . 20 |- w e. _V
57	56	funimaex 4496	. . . . . . . . . . . . . . . . . . 19 |- (Fun `'{<.r, s>. | (r e. J /\ s = (U.J \ r))} -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. _V)
58	55, 57	syl 12	. . . . . . . . . . . . . . . . . 18 |- (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}:(Clsd` J)-1-1-onto->J -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. _V)
59	4, 54, 58	3syl 24	. . . . . . . . . . . . . . . . 17 |- (J e. Top -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. _V)
60	59	3ad2ant1 897	. . . . . . . . . . . . . . . 16 |- ((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. _V)
61	60	adantr 425	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. _V)
62		elpwg 3038	. . . . . . . . . . . . . . 15 |- ((`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. _V -> ((`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. ~Py <-> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) C_ y))
63	61, 62	syl 12	. . . . . . . . . . . . . 14 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin)) -> ((`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. ~Py <-> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) C_ y))
64	53, 63	mpbird 213	. . . . . . . . . . . . 13 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. ~Py)
65		simprr 451	. . . . . . . . . . . . . 14 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin)) -> w e. Fin)
66		f1of1 4634	. . . . . . . . . . . . . . . . . . . 20 |- (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}:(Clsd` J)-1-1-onto->J -> `'{<.r, s>. | (r e. J /\ s = (U.J \ r))}:(Clsd` J)-1-1->J)
67	4, 54, 66	3syl 24	. . . . . . . . . . . . . . . . . . 19 |- (J e. Top -> `'{<.r, s>. | (r e. J /\ s = (U.J \ r))}:(Clsd` J)-1-1->J)
68	67	3ad2ant1 897	. . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) -> `'{<.r, s>. | (r e. J /\ s = (U.J \ r))}:(Clsd` J)-1-1->J)
69	68	adantr 425	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin)) -> `'{<.r, s>. | (r e. J /\ s = (U.J \ r))}:(Clsd` J)-1-1->J)
70	7	sseq2d 2645	. . . . . . . . . . . . . . . . . . . . 21 |- (J e. Top -> (w C_ ran {<.r, s>. | (r e. J /\ s = (U.J \ r))} <-> w C_ (Clsd` J)))
71	70	biimpa 460	. . . . . . . . . . . . . . . . . . . 20 |- ((J e. Top /\ w C_ ran {<.r, s>. | (r e. J /\ s = (U.J \ r))}) -> w C_ (Clsd` J))
72		sstr 2625	. . . . . . . . . . . . . . . . . . . . 21 |- ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) C_ ran {<.r, s>. | (r e. J /\ s = (U.J \ r))}) -> w C_ ran {<.r, s>. | (r e. J /\ s = (U.J \ r))})
73	1, 72	mpan2 760	. . . . . . . . . . . . . . . . . . . 20 |- (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) -> w C_ ran {<.r, s>. | (r e. J /\ s = (U.J \ r))})
74	71, 73	sylan2 500	. . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) -> w C_ (Clsd` J))
75	74	3ad2antl1 1038	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) -> w C_ (Clsd` J))
76	75	adantrr 431	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin)) -> w C_ (Clsd` J))
77		f1ores 4654	. . . . . . . . . . . . . . . . 17 |- ((`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}:(Clsd` J)-1-1->J /\ w C_ (Clsd` J)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))} |` w):w-1-1-onto->(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w))
78	69, 76, 77	syl11anc 524	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))} |` w):w-1-1-onto->(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w))
79	56	f1oen 5457	. . . . . . . . . . . . . . . 16 |- ((`'{<.r, s>. | (r e. J /\ s = (U.J \ r))} |` w):w-1-1-onto->(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) -> w ~~ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w))
80	78, 79	syl 12	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin)) -> w ~~ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w))
81		enfi 5627	. . . . . . . . . . . . . . 15 |- (((`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. _V /\ w ~~ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w)) -> (w e. Fin <-> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. Fin))
82	61, 80, 81	syl11anc 524	. . . . . . . . . . . . . 14 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin)) -> (w e. Fin <-> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. Fin))
83	65, 82	mpbid 212	. . . . . . . . . . . . 13 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. Fin)
84	40, 64, 83	sylanbrc 527	. . . . . . . . . . . 12 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. (~Py i^i Fin))
85		unieq 3185	. . . . . . . . . . . . . . 15 |- (z = (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) -> U.z = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w))
86	85	eqeq2d 1895	. . . . . . . . . . . . . 14 |- (z = (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) -> (U.J = U.z <-> U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w)))
87	86	notbid 673	. . . . . . . . . . . . 13 |- (z = (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) -> (-. U.J = U.z <-> -. U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w)))
88	87	rcla4v 2376	. . . . . . . . . . . 12 |- ((`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) e. (~Py i^i Fin) -> (A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w)))
89	84, 88	syl 12	. . . . . . . . . . 11 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin)) -> (A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w)))
90		difeq2 2719	. . . . . . . . . . . . . . 15 |- ((/) = |^|w -> (U.J \ (/)) = (U.J \ |^|w))
91	90	ad2antll 443	. . . . . . . . . . . . . 14 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> (U.J \ (/)) = (U.J \ |^|w))
92		dif0 2943	. . . . . . . . . . . . . 14 |- (U.J \ (/)) = U.J
93		intiin 3307	. . . . . . . . . . . . . . . 16 |- |^|w = |^|_v e. w v
94	93	difeq2i 2723	. . . . . . . . . . . . . . 15 |- (U.J \ |^|w) = (U.J \ |^|_v e. w v)
95		iundif2 3322	. . . . . . . . . . . . . . 15 |- U_v e. w (U.J \ v) = (U.J \ |^|_v e. w v)
96	94, 95	eqtr4i 1911	. . . . . . . . . . . . . 14 |- (U.J \ |^|w) = U_v e. w (U.J \ v)
97	91, 92, 96	3eqtr3g 1952	. . . . . . . . . . . . 13 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> U.J = U_v e. w (U.J \ v))
98		uniexg 3795	. . . . . . . . . . . . . . . . . . 19 |- (J e. Top -> U.J e. _V)
99		difexg 3458	. . . . . . . . . . . . . . . . . . 19 |- (U.J e. _V -> (U.J \ v) e. _V)
100	98, 99	syl 12	. . . . . . . . . . . . . . . . . 18 |- (J e. Top -> (U.J \ v) e. _V)
101	100	3ad2ant1 897	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) -> (U.J \ v) e. _V)
102	101	adantr 425	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> (U.J \ v) e. _V)
103	102	a1d 15	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> (v e. w -> (U.J \ v) e. _V))
104	103	r19.21aiv 2175	. . . . . . . . . . . . . 14 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> A.v e. w (U.J \ v) e. _V)
105		dfiun2g 3283	. . . . . . . . . . . . . 14 |- (A.v e. w (U.J \ v) e. _V -> U_v e. w (U.J \ v) = U.{u | E.v e. w u = (U.J \ v)})
106	104, 105	syl 12	. . . . . . . . . . . . 13 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> U_v e. w (U.J \ v) = U.{u | E.v e. w u = (U.J \ v)})
107		simp1 876	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) -> J e. Top)
108	107	adantr 425	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w) /\ v e. w)) -> J e. Top)
109		sstr 2625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) C_ (Clsd` J)) -> w C_ (Clsd` J))
110	109	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) C_ (Clsd` J) /\ w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) -> w C_ (Clsd` J))
111	1	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (J e. Top -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) C_ ran {<.r, s>. | (r e. J /\ s = (U.J \ r))})
112	111, 7	sseqtrd 2653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (J e. Top -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) C_ (Clsd` J))
113	110, 112	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((J e. Top /\ w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) -> w C_ (Clsd` J))
114	113	sseld 2619	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((J e. Top /\ w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) -> (v e. w -> v e. (Clsd` J)))
115	114	impr 422	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((J e. Top /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ v e. w)) -> v e. (Clsd` J))
116	115	adantrlr 437	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((J e. Top /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ v e. w)) -> v e. (Clsd` J))
117	116	adantrlr 437	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((J e. Top /\ (((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w) /\ v e. w)) -> v e. (Clsd` J))
118	117	3ad2antl1 1038	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w) /\ v e. w)) -> v e. (Clsd` J))
119	2, 3	opncldf3 15404	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ v e. (Clsd` J)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = (U.J \ v))
120	108, 118, 119	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w) /\ v e. w)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = (U.J \ v))
121	120	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w) /\ v e. w)) -> (U.J \ v) = (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v))
122	121	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w) /\ v e. w)) -> ((U.J \ v) = u <-> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u))
123		eqcom 1886	. . . . . . . . . . . . . . . . . . . 20 |- (u = (U.J \ v) <-> (U.J \ v) = u)
124	122, 123	syl5bb 591	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w) /\ v e. w)) -> (u = (U.J \ v) <-> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u))
125	124	expr 418	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> (v e. w -> (u = (U.J \ v) <-> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u)))
126	125	pm5.32d 709	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> ((v e. w /\ u = (U.J \ v)) <-> (v e. w /\ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u)))
127	126	rexbidv2 2126	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> (E.v e. w u = (U.J \ v) <-> E.v e. w (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u))
128	127	abbidv 2008	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> {u | E.v e. w u = (U.J \ v)} = {u | E.v e. w (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u})
129	4, 54, 55	3syl 24	. . . . . . . . . . . . . . . . . 18 |- (J e. Top -> Fun `'{<.r, s>. | (r e. J /\ s = (U.J \ r))})
130	129	3ad2ant1 897	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) -> Fun `'{<.r, s>. | (r e. J /\ s = (U.J \ r))})
131	130	adantr 425	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> Fun `'{<.r, s>. | (r e. J /\ s = (U.J \ r))})
132		df-rn 4005	. . . . . . . . . . . . . . . . . . 19 |- ran {<.r, s>. | (r e. J /\ s = (U.J \ r))} = dom `'{<.r, s>. | (r e. J /\ s = (U.J \ r))}
133	73, 132	syl6ss 2663	. . . . . . . . . . . . . . . . . 18 |- (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) -> w C_ dom `'{<.r, s>. | (r e. J /\ s = (U.J \ r))})
134	133	adantr 425	. . . . . . . . . . . . . . . . 17 |- ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) -> w C_ dom `'{<.r, s>. | (r e. J /\ s = (U.J \ r))})
135	134	ad2antrl 442	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> w C_ dom `'{<.r, s>. | (r e. J /\ s = (U.J \ r))})
136		dfimafn 4720	. . . . . . . . . . . . . . . 16 |- ((Fun `'{<.r, s>. | (r e. J /\ s = (U.J \ r))} /\ w C_ dom `'{<.r, s>. | (r e. J /\ s = (U.J \ r))}) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) = {u | E.v e. w (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u})
137	131, 135, 136	syl11anc 524	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w) = {u | E.v e. w (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u})
138	128, 137	eqtr4d 1928	. . . . . . . . . . . . . 14 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> {u | E.v e. w u = (U.J \ v)} = (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w))
139	138	unieqd 3188	. . . . . . . . . . . . 13 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> U.{u | E.v e. w u = (U.J \ v)} = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w))
140	97, 106, 139	3eqtrd 1929	. . . . . . . . . . . 12 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) /\ (/) = |^|w)) -> U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w))
141	140	expr 418	. . . . . . . . . . 11 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin)) -> ((/) = |^|w -> U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"w)))
142	89, 141	nsyld 132	. . . . . . . . . 10 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin)) -> (A.z e. (~Py i^i Fin) -. U.J = U.z -> -. (/) = |^|w))
143	142	ex 402	. . . . . . . . 9 |- ((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) -> ((w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) -> (A.z e. (~Py i^i Fin) -. U.J = U.z -> -. (/) = |^|w)))
144		elin 2786	. . . . . . . . . 10 |- (w e. (~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) i^i Fin) <-> (w e. ~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin))
145	56	elpw 3037	. . . . . . . . . . 11 |- (w e. ~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) <-> w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y))
146	145	anbi1i 539	. . . . . . . . . 10 |- ((w e. ~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin) <-> (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin))
147	144, 146	bitri 190	. . . . . . . . 9 |- (w e. (~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) i^i Fin) <-> (w C_ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) /\ w e. Fin))
148	143, 147	syl5ib 223	. . . . . . . 8 |- ((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) -> (w e. (~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) i^i Fin) -> (A.z e. (~Py i^i Fin) -. U.J = U.z -> -. (/) = |^|w)))
149	148	com23 36	. . . . . . 7 |- ((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) -> (A.z e. (~Py i^i Fin) -. U.J = U.z -> (w e. (~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) i^i Fin) -> -. (/) = |^|w)))
150	149	r19.21adv 2181	. . . . . 6 |- ((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) -> (A.z e. (~Py i^i Fin) -. U.J = U.z -> A.w e. (~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) i^i Fin) -. (/) = |^|w))
151		difeq2 2719	. . . . . . . . . . . 12 |- (U.J = U.y -> (U.J \ U.J) = (U.J \ U.y))
152	151	adantl 424	. . . . . . . . . . 11 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> (U.J \ U.J) = (U.J \ U.y))
153		difid 2942	. . . . . . . . . . 11 |- (U.J \ U.J) = (/)
154		uniiun 3306	. . . . . . . . . . . 12 |- U.y = U_v e. y v
155	154	difeq2i 2723	. . . . . . . . . . 11 |- (U.J \ U.y) = (U.J \ U_v e. y v)
156	152, 153, 155	3eqtr3g 1952	. . . . . . . . . 10 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> (/) = (U.J \ U_v e. y v))
157		eqtr 1904	. . . . . . . . . . . . . . . . . . . 20 |- ((U.J = U.y /\ U.y = (/)) -> U.J = (/))
158	157	ex 402	. . . . . . . . . . . . . . . . . . 19 |- (U.J = U.y -> (U.y = (/) -> U.J = (/)))
159	158	adantl 424	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ y e. ~PJ) /\ U.J = U.y) -> (U.y = (/) -> U.J = (/)))
160		unieq 3185	. . . . . . . . . . . . . . . . . . 19 |- (y = (/) -> U.y = U.(/))
161	160, 27	syl6eq 1944	. . . . . . . . . . . . . . . . . 18 |- (y = (/) -> U.y = (/))
162	159, 161	syl5 20	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ y e. ~PJ) /\ U.J = U.y) -> (y = (/) -> U.J = (/)))
163	162	con3d 111	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ y e. ~PJ) /\ U.J = U.y) -> (-. U.J = (/) -> -. y = (/)))
164	163	ex 402	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ y e. ~PJ) -> (U.J = U.y -> (-. U.J = (/) -> -. y = (/))))
165	164	com23 36	. . . . . . . . . . . . . 14 |- ((J e. Top /\ y e. ~PJ) -> (-. U.J = (/) -> (U.J = U.y -> -. y = (/))))
166	165	3impia 1064	. . . . . . . . . . . . 13 |- ((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) -> (U.J = U.y -> -. y = (/)))
167	166	imp 377	. . . . . . . . . . . 12 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> -. y = (/))
168		df-ne 2019	. . . . . . . . . . . 12 |- (y =/= (/) <-> -. y = (/))
169	167, 168	sylibr 217	. . . . . . . . . . 11 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> y =/= (/))
170		iindif2 3324	. . . . . . . . . . 11 |- (y =/= (/) -> |^|_v e. y (U.J \ v) = (U.J \ U_v e. y v))
171	169, 170	syl 12	. . . . . . . . . 10 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> |^|_v e. y (U.J \ v) = (U.J \ U_v e. y v))
172	156, 171	eqtr4d 1928	. . . . . . . . 9 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> (/) = |^|_v e. y (U.J \ v))
173	101	adantr 425	. . . . . . . . . . . 12 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> (U.J \ v) e. _V)
174	173	a1d 15	. . . . . . . . . . 11 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> (v e. y -> (U.J \ v) e. _V))
175	174	r19.21aiv 2175	. . . . . . . . . 10 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> A.v e. y (U.J \ v) e. _V)
176		dfiin2g 3286	. . . . . . . . . 10 |- (A.v e. y (U.J \ v) e. _V -> |^|_v e. y (U.J \ v) = |^|{u | E.v e. y u = (U.J \ v)})
177	175, 176	syl 12	. . . . . . . . 9 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> |^|_v e. y (U.J \ v) = |^|{u | E.v e. y u = (U.J \ v)})
178	107	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (U.J = U.y /\ v e. y)) -> J e. Top)
179		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y C_ J /\ v e. y) -> v e. J)
180	179, 48	sylanb 498	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. ~PJ /\ v e. y) -> v e. J)
181	180	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ v e. y) -> v e. J)
182	181	adantrl 430	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (U.J = U.y /\ v e. y)) -> v e. J)
183	2, 3	opncldf2 15403	. . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ v e. J) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = (U.J \ v))
184	178, 182, 183	syl11anc 524	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (U.J = U.y /\ v e. y)) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = (U.J \ v))
185	184	eqcomd 1889	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (U.J = U.y /\ v e. y)) -> (U.J \ v) = ({<.r, s>. | (r e. J /\ s = (U.J \ r))}` v))
186	185	eqeq1d 1892	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (U.J = U.y /\ v e. y)) -> ((U.J \ v) = u <-> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u))
187	186, 123	syl5bb 591	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ (U.J = U.y /\ v e. y)) -> (u = (U.J \ v) <-> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u))
188	187	expr 418	. . . . . . . . . . . . . 14 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> (v e. y -> (u = (U.J \ v) <-> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u)))
189	188	pm5.32d 709	. . . . . . . . . . . . 13 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> ((v e. y /\ u = (U.J \ v)) <-> (v e. y /\ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u)))
190	189	rexbidv2 2126	. . . . . . . . . . . 12 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> (E.v e. y u = (U.J \ v) <-> E.v e. y ({<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u))
191	190	abbidv 2008	. . . . . . . . . . 11 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> {u | E.v e. y u = (U.J \ v)} = {u | E.v e. y ({<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u})
192		f1ofun 4637	. . . . . . . . . . . . . . 15 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1-onto->(Clsd` J) -> Fun {<.r, s>. | (r e. J /\ s = (U.J \ r))})
193	4, 192	syl 12	. . . . . . . . . . . . . 14 |- (J e. Top -> Fun {<.r, s>. | (r e. J /\ s = (U.J \ r))})
194	193	3ad2ant1 897	. . . . . . . . . . . . 13 |- ((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) -> Fun {<.r, s>. | (r e. J /\ s = (U.J \ r))})
195	194	adantr 425	. . . . . . . . . . . 12 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> Fun {<.r, s>. | (r e. J /\ s = (U.J \ r))})
196		f1ofn 4636	. . . . . . . . . . . . . . . . . 18 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1-onto->(Clsd` J) -> {<.r, s>. | (r e. J /\ s = (U.J \ r))} Fn J)
197		fndm 4512	. . . . . . . . . . . . . . . . . 18 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))} Fn J -> dom {<.r, s>. | (r e. J /\ s = (U.J \ r))} = J)
198	4, 196, 197	3syl 24	. . . . . . . . . . . . . . . . 17 |- (J e. Top -> dom {<.r, s>. | (r e. J /\ s = (U.J \ r))} = J)
199	198	sseq2d 2645	. . . . . . . . . . . . . . . 16 |- (J e. Top -> (y C_ dom {<.r, s>. | (r e. J /\ s = (U.J \ r))} <-> y C_ J))
200	199	biimpar 461	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ y C_ J) -> y C_ dom {<.r, s>. | (r e. J /\ s = (U.J \ r))})
201	200, 48	sylan2b 501	. . . . . . . . . . . . . 14 |- ((J e. Top /\ y e. ~PJ) -> y C_ dom {<.r, s>. | (r e. J /\ s = (U.J \ r))})
202	201	3adant3 896	. . . . . . . . . . . . 13 |- ((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) -> y C_ dom {<.r, s>. | (r e. J /\ s = (U.J \ r))})
203	202	adantr 425	. . . . . . . . . . . 12 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> y C_ dom {<.r, s>. | (r e. J /\ s = (U.J \ r))})
204		dfimafn 4720	. . . . . . . . . . . 12 |- ((Fun {<.r, s>. | (r e. J /\ s = (U.J \ r))} /\ y C_ dom {<.r, s>. | (r e. J /\ s = (U.J \ r))}) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) = {u | E.v e. y ({<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u})
205	195, 203, 204	syl11anc 524	. . . . . . . . . . 11 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) = {u | E.v e. y ({<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u})
206	191, 205	eqtr4d 1928	. . . . . . . . . 10 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> {u | E.v e. y u = (U.J \ v)} = ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y))
207	206	inteqd 3219	. . . . . . . . 9 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> |^|{u | E.v e. y u = (U.J \ v)} = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y))
208	172, 177, 207	3eqtrd 1929	. . . . . . . 8 |- (((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) /\ U.J = U.y) -> (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y))
209	208	ex 402	. . . . . . 7 |- ((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) -> (U.J = U.y -> (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)))
210	209	con3d 111	. . . . . 6 |- ((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) -> (-. (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) -> -. U.J = U.y))
211	150, 210	imim12d 69	. . . . 5 |- ((J e. Top /\ y e. ~PJ /\ -. U.J = (/)) -> ((A.w e. (~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) i^i Fin) -. (/) = |^|w -> -. (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) -> (A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y)))
212	211	3expia 1069	. . . 4 |- ((J e. Top /\ y e. ~PJ) -> (-. U.J = (/) -> ((A.w e. (~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) i^i Fin) -. (/) = |^|w -> -. (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) -> (A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y))))
213	39, 212	pm2.61d 141	. . 3 |- ((J e. Top /\ y e. ~PJ) -> ((A.w e. (~P({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y) i^i Fin) -. (/) = |^|w -> -. (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"y)) -> (A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y)))
214	22, 213	syld 30	. 2 |- ((J e. Top /\ y e. ~PJ) -> (A.x e. ~P (Clsd` J)(A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x) -> (A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y)))
215	214	r19.21adva 2182	1 |- (J e. Top -> (A.x e. ~P (Clsd` J)(A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x) -> A.y e. ~P J(A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   \ cdif 2590   i^i cin 2592   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  U.cuni 3177  |^|cint 3214  U_ciun 3255  |^|_ciin 3256   class class class wbr 3338  {copab 3395  `'ccnv 3985  dom cdm 3986  ran crn 3987   |` cres 3988  "cima 3989  Fun wfun 3992   Fn wfn 3993  -1-1->wf1 3995  -onto->wfo 3996  -1-1-onto->wf1o 3997  ` cfv 3998   ~~ cen 5423  Fincfn 5426  Topctop 8857  Clsdccld 8936

This theorem is referenced by:  compfipin0 15436

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-iin 3258  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-er 5318  df-en 5427  df-fin 5430  df-cld 8939

Copyright terms: Public domain