Theorem locfinreflem 27997

Description: A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf , it is expressed by exposing a function f from the original cover U, which is taken as the index set. The solution is constructed by building unions, so the same method can be used to prove a similar theorem about closed covers. (Contributed by Thierry Arnoux, 29-Jan-2020.)

Hypotheses

Ref	Expression
locfinref.x	|- X = U. J
locfinref.1	|- ( ph -> U C_ J )
locfinref.2	|- ( ph -> X = U. U )
locfinref.3	|- ( ph -> V C_ J )
locfinref.4	|- ( ph -> V Ref U )
locfinref.5	|- ( ph -> V e. ( LocFin ` J ) )

Assertion

Ref	Expression
locfinreflem	|- ( ph -> E. f ( ( Fun f /\ dom f C_ U /\ ran f C_ J ) /\ ( ran f Ref U /\ ran f e. ( LocFin ` J ) ) ) )

Distinct variable groups:   f, J   U, f   f, V   ph, f

Allowed substitution hint:   X( f)

Proof of Theorem locfinreflem

Dummy variables g j k u v w x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		locfinref.4	. . . 4 |- ( ph -> V Ref U )
2		locfinref.5	. . . . 5 |- ( ph -> V e. ( LocFin ` J ) )
3		reff 27996	. . . . 5 |- ( V e. ( LocFin ` J ) -> ( V Ref U <-> ( U. U C_ U. V /\ E. g ( g : V --> U /\ A. v e. V v C_ ( g ` v ) ) ) ) )
4	2, 3	syl 16	. . . 4 |- ( ph -> ( V Ref U <-> ( U. U C_ U. V /\ E. g ( g : V --> U /\ A. v e. V v C_ ( g ` v ) ) ) ) )
5	1, 4	mpbid 210	. . 3 |- ( ph -> ( U. U C_ U. V /\ E. g ( g : V --> U /\ A. v e. V v C_ ( g ` v ) ) ) )
6	5	simprd 461	. 2 |- ( ph -> E. g ( g : V --> U /\ A. v e. V v C_ ( g ` v ) ) )
7		funmpt 5532	. . . . . 6 |- Fun ( u e. ran g |-> U. ( `' g " { u } ) )
8	7	a1i 11	. . . . 5 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> Fun ( u e. ran g |-> U. ( `' g " { u } ) ) )
9		eqid 2382	. . . . . . 7 |- ( u e. ran g |-> U. ( `' g " { u } ) ) = ( u e. ran g |-> U. ( `' g " { u } ) )
10	9	dmmptss 5411	. . . . . 6 |- dom ( u e. ran g |-> U. ( `' g " { u } ) ) C_ ran g
11		frn 5645	. . . . . . 7 |- ( g : V --> U -> ran g C_ U )
12	11	ad2antlr 724	. . . . . 6 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ran g C_ U )
13	10, 12	syl5ss 3428	. . . . 5 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> dom ( u e. ran g |-> U. ( `' g " { u } ) ) C_ U )
14		locfintop 20107	. . . . . . . . . 10 |- ( V e. ( LocFin ` J ) -> J e. Top )
15	2, 14	syl 16	. . . . . . . . 9 |- ( ph -> J e. Top )
16	15	ad3antrrr 727	. . . . . . . 8 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> J e. Top )
17		cnvimass 5269	. . . . . . . . . 10 |- ( `' g " { u } ) C_ dom g
18		fdm 5643	. . . . . . . . . . 11 |- ( g : V --> U -> dom g = V )
19	18	ad3antlr 728	. . . . . . . . . 10 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> dom g = V )
20	17, 19	syl5sseq 3465	. . . . . . . . 9 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> ( `' g " { u } ) C_ V )
21		locfinref.3	. . . . . . . . . 10 |- ( ph -> V C_ J )
22	21	ad3antrrr 727	. . . . . . . . 9 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> V C_ J )
23	20, 22	sstrd 3427	. . . . . . . 8 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> ( `' g " { u } ) C_ J )
24		uniopn 19491	. . . . . . . 8 |- ( ( J e. Top /\ ( `' g " { u } ) C_ J ) -> U. ( `' g " { u } ) e. J )
25	16, 23, 24	syl2anc 659	. . . . . . 7 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> U. ( `' g " { u } ) e. J )
26	25	ralrimiva 2796	. . . . . 6 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> A. u e. ran g U. ( `' g " { u } ) e. J )
27	9	rnmptss 5962	. . . . . 6 |- ( A. u e. ran g U. ( `' g " { u } ) e. J -> ran ( u e. ran g |-> U. ( `' g " { u } ) ) C_ J )
28	26, 27	syl 16	. . . . 5 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ran ( u e. ran g |-> U. ( `' g " { u } ) ) C_ J )
29		eqid 2382	. . . . . . . . . 10 |- U. V = U. V
30		eqid 2382	. . . . . . . . . 10 |- U. U = U. U
31	29, 30	refbas 20096	. . . . . . . . 9 |- ( V Ref U -> U. U = U. V )
32	1, 31	syl 16	. . . . . . . 8 |- ( ph -> U. U = U. V )
33	32	ad2antrr 723	. . . . . . 7 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> U. U = U. V )
34		nfv 1715	. . . . . . . . . . . . 13 |- F/ v ( ph /\ g : V --> U )
35		nfra1 2763	. . . . . . . . . . . . 13 |- F/ v A. v e. V v C_ ( g ` v )
36	34, 35	nfan 1936	. . . . . . . . . . . 12 |- F/ v ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) )
37		nfre1 2843	. . . . . . . . . . . 12 |- F/ v E. v e. V x e. v
38	36, 37	nfan 1936	. . . . . . . . . . 11 |- F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ E. v e. V x e. v )
39		ffn 5639	. . . . . . . . . . . . . . 15 |- ( g : V --> U -> g Fn V )
40	39	ad4antlr 730	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) /\ x e. v ) -> g Fn V )
41		simplr 753	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) /\ x e. v ) -> v e. V )
42		fnfvelrn 5930	. . . . . . . . . . . . . 14 |- ( ( g Fn V /\ v e. V ) -> ( g ` v ) e. ran g )
43	40, 41, 42	syl2anc 659	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) /\ x e. v ) -> ( g ` v ) e. ran g )
44		ssid 3436	. . . . . . . . . . . . . . 15 |- v C_ v
45	39	ad3antlr 728	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) -> g Fn V )
46		eqid 2382	. . . . . . . . . . . . . . . . 17 |- ( g ` v ) = ( g ` v )
47		fniniseg 5910	. . . . . . . . . . . . . . . . . 18 |- ( g Fn V -> ( v e. ( `' g " { ( g ` v ) } ) <-> ( v e. V /\ ( g ` v ) = ( g ` v ) ) ) )
48	47	biimpar 483	. . . . . . . . . . . . . . . . 17 |- ( ( g Fn V /\ ( v e. V /\ ( g ` v ) = ( g ` v ) ) ) -> v e. ( `' g " { ( g ` v ) } ) )
49	46, 48	mpanr2 682	. . . . . . . . . . . . . . . 16 |- ( ( g Fn V /\ v e. V ) -> v e. ( `' g " { ( g ` v ) } ) )
50	45, 49	sylancom 665	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) -> v e. ( `' g " { ( g ` v ) } ) )
51		ssuni 4185	. . . . . . . . . . . . . . 15 |- ( ( v C_ v /\ v e. ( `' g " { ( g ` v ) } ) ) -> v C_ U. ( `' g " { ( g ` v ) } ) )
52	44, 50, 51	sylancr 661	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) -> v C_ U. ( `' g " { ( g ` v ) } ) )
53	52	sselda 3417	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) /\ x e. v ) -> x e. U. ( `' g " { ( g ` v ) } ) )
54		sneq 3954	. . . . . . . . . . . . . . . . 17 |- ( u = ( g ` v ) -> { u } = { ( g ` v ) } )
55	54	imaeq2d 5249	. . . . . . . . . . . . . . . 16 |- ( u = ( g ` v ) -> ( `' g " { u } ) = ( `' g " { ( g ` v ) } ) )
56	55	unieqd 4173	. . . . . . . . . . . . . . 15 |- ( u = ( g ` v ) -> U. ( `' g " { u } ) = U. ( `' g " { ( g ` v ) } ) )
57	56	eleq2d 2452	. . . . . . . . . . . . . 14 |- ( u = ( g ` v ) -> ( x e. U. ( `' g " { u } ) <-> x e. U. ( `' g " { ( g ` v ) } ) ) )
58	57	rspcev 3135	. . . . . . . . . . . . 13 |- ( ( ( g ` v ) e. ran g /\ x e. U. ( `' g " { ( g ` v ) } ) ) -> E. u e. ran g x e. U. ( `' g " { u } ) )
59	43, 53, 58	syl2anc 659	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) /\ x e. v ) -> E. u e. ran g x e. U. ( `' g " { u } ) )
60	59	adantllr 716	. . . . . . . . . . 11 |- ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ E. v e. V x e. v ) /\ v e. V ) /\ x e. v ) -> E. u e. ran g x e. U. ( `' g " { u } ) )
61		simpr 459	. . . . . . . . . . 11 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ E. v e. V x e. v ) -> E. v e. V x e. v )
62	38, 60, 61	r19.29af 2922	. . . . . . . . . 10 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ E. v e. V x e. v ) -> E. u e. ran g x e. U. ( `' g " { u } ) )
63		nfv 1715	. . . . . . . . . . . . . 14 |- F/ v u e. ran g
64	36, 63	nfan 1936	. . . . . . . . . . . . 13 |- F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g )
65		nfv 1715	. . . . . . . . . . . . 13 |- F/ v x e. U. ( `' g " { u } )
66	64, 65	nfan 1936	. . . . . . . . . . . 12 |- F/ v ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) /\ x e. U. ( `' g " { u } ) )
67	20	ad3antrrr 727	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) /\ x e. U. ( `' g " { u } ) ) /\ v e. ( `' g " { u } ) ) /\ x e. v ) -> ( `' g " { u } ) C_ V )
68		simplr 753	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) /\ x e. U. ( `' g " { u } ) ) /\ v e. ( `' g " { u } ) ) /\ x e. v ) -> v e. ( `' g " { u } ) )
69	67, 68	sseldd 3418	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) /\ x e. U. ( `' g " { u } ) ) /\ v e. ( `' g " { u } ) ) /\ x e. v ) -> v e. V )
70		simpr 459	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) /\ x e. U. ( `' g " { u } ) ) /\ v e. ( `' g " { u } ) ) /\ x e. v ) -> x e. v )
71		simpr 459	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) /\ x e. U. ( `' g " { u } ) ) -> x e. U. ( `' g " { u } ) )
72		eluni2 4167	. . . . . . . . . . . . 13 |- ( x e. U. ( `' g " { u } ) <-> E. v e. ( `' g " { u } ) x e. v )
73	71, 72	sylib 196	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) /\ x e. U. ( `' g " { u } ) ) -> E. v e. ( `' g " { u } ) x e. v )
74	66, 69, 70, 73	reximd2a 2852	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) /\ x e. U. ( `' g " { u } ) ) -> E. v e. V x e. v )
75	74	r19.29an 2923	. . . . . . . . . 10 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ E. u e. ran g x e. U. ( `' g " { u } ) ) -> E. v e. V x e. v )
76	62, 75	impbida 830	. . . . . . . . 9 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ( E. v e. V x e. v <-> E. u e. ran g x e. U. ( `' g " { u } ) ) )
77		eluni2 4167	. . . . . . . . 9 |- ( x e. U. V <-> E. v e. V x e. v )
78		eliun 4248	. . . . . . . . 9 |- ( x e. U_ u e. ran g U. ( `' g " { u } ) <-> E. u e. ran g x e. U. ( `' g " { u } ) )
79	76, 77, 78	3bitr4g 288	. . . . . . . 8 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ( x e. U. V <-> x e. U_ u e. ran g U. ( `' g " { u } ) ) )
80	79	eqrdv 2379	. . . . . . 7 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> U. V = U_ u e. ran g U. ( `' g " { u } ) )
81		dfiun3g 5168	. . . . . . . 8 |- ( A. u e. ran g U. ( `' g " { u } ) e. J -> U_ u e. ran g U. ( `' g " { u } ) = U. ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
82	26, 81	syl 16	. . . . . . 7 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> U_ u e. ran g U. ( `' g " { u } ) = U. ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
83	33, 80, 82	3eqtrd 2427	. . . . . 6 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> U. U = U. ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
84	11	ad3antlr 728	. . . . . . . . 9 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) -> ran g C_ U )
85		vex 3037	. . . . . . . . . . 11 |- w e. _V
86	9	elrnmpt 5162	. . . . . . . . . . 11 |- ( w e. _V -> ( w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) <-> E. u e. ran g w = U. ( `' g " { u } ) ) )
87	85, 86	mp1i 12	. . . . . . . . . 10 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ( w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) <-> E. u e. ran g w = U. ( `' g " { u } ) ) )
88	87	biimpa 482	. . . . . . . . 9 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) -> E. u e. ran g w = U. ( `' g " { u } ) )
89		ssrexv 3479	. . . . . . . . 9 |- ( ran g C_ U -> ( E. u e. ran g w = U. ( `' g " { u } ) -> E. u e. U w = U. ( `' g " { u } ) ) )
90	84, 88, 89	sylc 60	. . . . . . . 8 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) -> E. u e. U w = U. ( `' g " { u } ) )
91		nfv 1715	. . . . . . . . . 10 |- F/ u ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) )
92		nfmpt1 4456	. . . . . . . . . . . 12 |- F/_ u ( u e. ran g |-> U. ( `' g " { u } ) )
93	92	nfrn 5158	. . . . . . . . . . 11 |- F/_ u ran ( u e. ran g |-> U. ( `' g " { u } ) )
94	93	nfcri 2537	. . . . . . . . . 10 |- F/ u w e. ran ( u e. ran g |-> U. ( `' g " { u } ) )
95	91, 94	nfan 1936	. . . . . . . . 9 |- F/ u ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
96		simpr 459	. . . . . . . . . . 11 |- ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) /\ u e. U ) /\ w = U. ( `' g " { u } ) ) -> w = U. ( `' g " { u } ) )
97		nfv 1715	. . . . . . . . . . . . . . . 16 |- F/ v w e. ran ( u e. ran g |-> U. ( `' g " { u } ) )
98	36, 97	nfan 1936	. . . . . . . . . . . . . . 15 |- F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
99		nfv 1715	. . . . . . . . . . . . . . 15 |- F/ v u e. U
100	98, 99	nfan 1936	. . . . . . . . . . . . . 14 |- F/ v ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) /\ u e. U )
101		nfv 1715	. . . . . . . . . . . . . 14 |- F/ v w = U. ( `' g " { u } )
102	100, 101	nfan 1936	. . . . . . . . . . . . 13 |- F/ v ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) /\ u e. U ) /\ w = U. ( `' g " { u } ) )
103		simp-5r 768	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) /\ u e. U ) /\ w = U. ( `' g " { u } ) ) /\ v e. ( `' g " { u } ) ) -> A. v e. V v C_ ( g ` v ) )
104	39	ad5antlr 732	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) /\ u e. U ) /\ w = U. ( `' g " { u } ) ) -> g Fn V )
105		fniniseg 5910	. . . . . . . . . . . . . . . . . . 19 |- ( g Fn V -> ( v e. ( `' g " { u } ) <-> ( v e. V /\ ( g ` v ) = u ) ) )
106	104, 105	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) /\ u e. U ) /\ w = U. ( `' g " { u } ) ) -> ( v e. ( `' g " { u } ) <-> ( v e. V /\ ( g ` v ) = u ) ) )
107	106	biimpa 482	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) /\ u e. U ) /\ w = U. ( `' g " { u } ) ) /\ v e. ( `' g " { u } ) ) -> ( v e. V /\ ( g ` v ) = u ) )
108	107	simpld 457	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) /\ u e. U ) /\ w = U. ( `' g " { u } ) ) /\ v e. ( `' g " { u } ) ) -> v e. V )
109		rspa 2749	. . . . . . . . . . . . . . . 16 |- ( ( A. v e. V v C_ ( g ` v ) /\ v e. V ) -> v C_ ( g ` v ) )
110	103, 108, 109	syl2anc 659	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) /\ u e. U ) /\ w = U. ( `' g " { u } ) ) /\ v e. ( `' g " { u } ) ) -> v C_ ( g ` v ) )
111	107	simprd 461	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) /\ u e. U ) /\ w = U. ( `' g " { u } ) ) /\ v e. ( `' g " { u } ) ) -> ( g ` v ) = u )
112	110, 111	sseqtrd 3453	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) /\ u e. U ) /\ w = U. ( `' g " { u } ) ) /\ v e. ( `' g " { u } ) ) -> v C_ u )
113	112	ex 432	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) /\ u e. U ) /\ w = U. ( `' g " { u } ) ) -> ( v e. ( `' g " { u } ) -> v C_ u ) )
114	102, 113	ralrimi 2782	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) /\ u e. U ) /\ w = U. ( `' g " { u } ) ) -> A. v e. ( `' g " { u } ) v C_ u )
115		unissb 4194	. . . . . . . . . . . 12 |- ( U. ( `' g " { u } ) C_ u <-> A. v e. ( `' g " { u } ) v C_ u )
116	114, 115	sylibr 212	. . . . . . . . . . 11 |- ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) /\ u e. U ) /\ w = U. ( `' g " { u } ) ) -> U. ( `' g " { u } ) C_ u )
117	96, 116	eqsstrd 3451	. . . . . . . . . 10 |- ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) /\ u e. U ) /\ w = U. ( `' g " { u } ) ) -> w C_ u )
118	117	exp31 602	. . . . . . . . 9 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) -> ( u e. U -> ( w = U. ( `' g " { u } ) -> w C_ u ) ) )
119	95, 118	reximdai 2851	. . . . . . . 8 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) -> ( E. u e. U w = U. ( `' g " { u } ) -> E. u e. U w C_ u ) )
120	90, 119	mpd 15	. . . . . . 7 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) ) -> E. u e. U w C_ u )
121	120	ralrimiva 2796	. . . . . 6 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> A. w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) E. u e. U w C_ u )
122		vex 3037	. . . . . . . . . 10 |- g e. _V
123	122	rnex 6633	. . . . . . . . 9 |- ran g e. _V
124	123	mptex 6044	. . . . . . . 8 |- ( u e. ran g |-> U. ( `' g " { u } ) ) e. _V
125		rnexg 6631	. . . . . . . 8 |- ( ( u e. ran g |-> U. ( `' g " { u } ) ) e. _V -> ran ( u e. ran g |-> U. ( `' g " { u } ) ) e. _V )
126	124, 125	mp1i 12	. . . . . . 7 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ran ( u e. ran g |-> U. ( `' g " { u } ) ) e. _V )
127		eqid 2382	. . . . . . . 8 |- U. ran ( u e. ran g |-> U. ( `' g " { u } ) ) = U. ran ( u e. ran g |-> U. ( `' g " { u } ) )
128	127, 30	isref 20095	. . . . . . 7 |- ( ran ( u e. ran g |-> U. ( `' g " { u } ) ) e. _V -> ( ran ( u e. ran g |-> U. ( `' g " { u } ) ) Ref U <-> ( U. U = U. ran ( u e. ran g |-> U. ( `' g " { u } ) ) /\ A. w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) E. u e. U w C_ u ) ) )
129	126, 128	syl 16	. . . . . 6 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ( ran ( u e. ran g |-> U. ( `' g " { u } ) ) Ref U <-> ( U. U = U. ran ( u e. ran g |-> U. ( `' g " { u } ) ) /\ A. w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) E. u e. U w C_ u ) ) )
130	83, 121, 129	mpbir2and 920	. . . . 5 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ran ( u e. ran g |-> U. ( `' g " { u } ) ) Ref U )
131	15	ad2antrr 723	. . . . . 6 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> J e. Top )
132		locfinref.2	. . . . . . . 8 |- ( ph -> X = U. U )
133	132	ad2antrr 723	. . . . . . 7 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> X = U. U )
134	133, 83	eqtrd 2423	. . . . . 6 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> X = U. ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
135		nfv 1715	. . . . . . . . 9 |- F/ v x e. X
136	36, 135	nfan 1936	. . . . . . . 8 |- F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X )
137		simplr 753	. . . . . . . 8 |- ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ ( x e. v /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) ) -> v e. J )
138		ffun 5641	. . . . . . . . . . . . . 14 |- ( g : V --> U -> Fun g )
139	138	ad6antlr 734	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> Fun g )
140		imafi 7728	. . . . . . . . . . . . 13 |- ( ( Fun g /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> ( g " { j e. V | ( j i^i v ) =/= (/) } ) e. Fin )
141	139, 140	sylancom 665	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> ( g " { j e. V | ( j i^i v ) =/= (/) } ) e. Fin )
142		simp3 996	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ k e. ran g /\ w = ( ( u e. ran g |-> U. ( `' g " { u } ) ) ` k ) ) -> w = ( ( u e. ran g |-> U. ( `' g " { u } ) ) ` k ) )
143		sneq 3954	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( u = k -> { u } = { k } )
144	143	imaeq2d 5249	. . . . . . . . . . . . . . . . . . . . . 22 |- ( u = k -> ( `' g " { u } ) = ( `' g " { k } ) )
145	144	unieqd 4173	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = k -> U. ( `' g " { u } ) = U. ( `' g " { k } ) )
146	122	cnvex 6646	. . . . . . . . . . . . . . . . . . . . . . 23 |- `' g e. _V
147		imaexg 6636	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( `' g e. _V -> ( `' g " { k } ) e. _V )
148	146, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 |- ( `' g " { k } ) e. _V
149	148	uniex 6495	. . . . . . . . . . . . . . . . . . . . 21 |- U. ( `' g " { k } ) e. _V
150	145, 9, 149	fvmpt 5857	. . . . . . . . . . . . . . . . . . . 20 |- ( k e. ran g -> ( ( u e. ran g |-> U. ( `' g " { u } ) ) ` k ) = U. ( `' g " { k } ) )
151	150	3ad2ant2 1016	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ k e. ran g /\ w = ( ( u e. ran g |-> U. ( `' g " { u } ) ) ` k ) ) -> ( ( u e. ran g |-> U. ( `' g " { u } ) ) ` k ) = U. ( `' g " { k } ) )
152	142, 151	eqtrd 2423	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ k e. ran g /\ w = ( ( u e. ran g |-> U. ( `' g " { u } ) ) ` k ) ) -> w = U. ( `' g " { k } ) )
153	152	ineq1d 3613	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ k e. ran g /\ w = ( ( u e. ran g |-> U. ( `' g " { u } ) ) ` k ) ) -> ( w i^i v ) = ( U. ( `' g " { k } ) i^i v ) )
154	153	neeq1d 2659	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ k e. ran g /\ w = ( ( u e. ran g |-> U. ( `' g " { u } ) ) ` k ) ) -> ( ( w i^i v ) =/= (/) <-> ( U. ( `' g " { k } ) i^i v ) =/= (/) ) )
155	123	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> ran g e. _V )
156		imaexg 6636	. . . . . . . . . . . . . . . . . . . . 21 |- ( `' g e. _V -> ( `' g " { u } ) e. _V )
157	146, 156	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- ( `' g " { u } ) e. _V
158	157	uniex 6495	. . . . . . . . . . . . . . . . . . 19 |- U. ( `' g " { u } ) e. _V
159	158, 9	fnmpti 5617	. . . . . . . . . . . . . . . . . 18 |- ( u e. ran g |-> U. ( `' g " { u } ) ) Fn ran g
160		dffn4 5709	. . . . . . . . . . . . . . . . . 18 |- ( ( u e. ran g |-> U. ( `' g " { u } ) ) Fn ran g <-> ( u e. ran g |-> U. ( `' g " { u } ) ) : ran g -onto-> ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
161	159, 160	mpbi 208	. . . . . . . . . . . . . . . . 17 |- ( u e. ran g |-> U. ( `' g " { u } ) ) : ran g -onto-> ran ( u e. ran g |-> U. ( `' g " { u } ) )
162	161	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> ( u e. ran g |-> U. ( `' g " { u } ) ) : ran g -onto-> ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
163	154, 155, 162	rabfodom 27522	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> { w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) | ( w i^i v ) =/= (/) } ~<_ { k e. ran g | ( U. ( `' g " { k } ) i^i v ) =/= (/) } )
164		sneq 3954	. . . . . . . . . . . . . . . . . . . 20 |- ( k = u -> { k } = { u } )
165	164	imaeq2d 5249	. . . . . . . . . . . . . . . . . . 19 |- ( k = u -> ( `' g " { k } ) = ( `' g " { u } ) )
166	165	unieqd 4173	. . . . . . . . . . . . . . . . . 18 |- ( k = u -> U. ( `' g " { k } ) = U. ( `' g " { u } ) )
167	166	ineq1d 3613	. . . . . . . . . . . . . . . . 17 |- ( k = u -> ( U. ( `' g " { k } ) i^i v ) = ( U. ( `' g " { u } ) i^i v ) )
168	167	neeq1d 2659	. . . . . . . . . . . . . . . 16 |- ( k = u -> ( ( U. ( `' g " { k } ) i^i v ) =/= (/) <-> ( U. ( `' g " { u } ) i^i v ) =/= (/) ) )
169	168	cbvrabv 3033	. . . . . . . . . . . . . . 15 |- { k e. ran g | ( U. ( `' g " { k } ) i^i v ) =/= (/) } = { u e. ran g | ( U. ( `' g " { u } ) i^i v ) =/= (/) }
170	163, 169	syl6breq 4406	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> { w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) | ( w i^i v ) =/= (/) } ~<_ { u e. ran g | ( U. ( `' g " { u } ) i^i v ) =/= (/) } )
171	123	rabex 4516	. . . . . . . . . . . . . . 15 |- { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } e. _V
172		nfv 1715	. . . . . . . . . . . . . . . . . . . . 21 |- F/ j ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v )
173		nfrab1 2963	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ j { j e. V | ( j i^i v ) =/= (/) }
174	173	nfel1 2560	. . . . . . . . . . . . . . . . . . . . 21 |- F/ j { j e. V | ( j i^i v ) =/= (/) } e. Fin
175	172, 174	nfan 1936	. . . . . . . . . . . . . . . . . . . 20 |- F/ j ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin )
176		nfv 1715	. . . . . . . . . . . . . . . . . . . 20 |- F/ j u e. ran g
177	175, 176	nfan 1936	. . . . . . . . . . . . . . . . . . 19 |- F/ j ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ u e. ran g )
178		nfv 1715	. . . . . . . . . . . . . . . . . . 19 |- F/ j ( U. ( `' g " { u } ) i^i v ) =/= (/)
179	177, 178	nfan 1936	. . . . . . . . . . . . . . . . . 18 |- F/ j ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ u e. ran g ) /\ ( U. ( `' g " { u } ) i^i v ) =/= (/) )
180		nfv 1715	. . . . . . . . . . . . . . . . . . 19 |- F/ j ( g ` k ) = u
181	173, 180	nfrex 2845	. . . . . . . . . . . . . . . . . 18 |- F/ j E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u
182	39	ad5antlr 732	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) -> g Fn V )
183	182	ad5antr 731	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ u e. ran g ) /\ ( U. ( `' g " { u } ) i^i v ) =/= (/) ) /\ j e. ( `' g " { u } ) ) /\ ( j i^i v ) =/= (/) ) -> g Fn V )
184		simplr 753	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ u e. ran g ) /\ ( U. ( `' g " { u } ) i^i v ) =/= (/) ) /\ j e. ( `' g " { u } ) ) /\ ( j i^i v ) =/= (/) ) -> j e. ( `' g " { u } ) )
185		fniniseg 5910	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g Fn V -> ( j e. ( `' g " { u } ) <-> ( j e. V /\ ( g ` j ) = u ) ) )
186	185	biimpa 482	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( g Fn V /\ j e. ( `' g " { u } ) ) -> ( j e. V /\ ( g ` j ) = u ) )
187	183, 184, 186	syl2anc 659	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ u e. ran g ) /\ ( U. ( `' g " { u } ) i^i v ) =/= (/) ) /\ j e. ( `' g " { u } ) ) /\ ( j i^i v ) =/= (/) ) -> ( j e. V /\ ( g ` j ) = u ) )
188	187	simpld 457	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ u e. ran g ) /\ ( U. ( `' g " { u } ) i^i v ) =/= (/) ) /\ j e. ( `' g " { u } ) ) /\ ( j i^i v ) =/= (/) ) -> j e. V )
189		simpr 459	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ u e. ran g ) /\ ( U. ( `' g " { u } ) i^i v ) =/= (/) ) /\ j e. ( `' g " { u } ) ) /\ ( j i^i v ) =/= (/) ) -> ( j i^i v ) =/= (/) )
190		rabid 2959	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. { j e. V | ( j i^i v ) =/= (/) } <-> ( j e. V /\ ( j i^i v ) =/= (/) ) )
191	188, 189, 190	sylanbrc 662	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ u e. ran g ) /\ ( U. ( `' g " { u } ) i^i v ) =/= (/) ) /\ j e. ( `' g " { u } ) ) /\ ( j i^i v ) =/= (/) ) -> j e. { j e. V | ( j i^i v ) =/= (/) } )
192	187	simprd 461	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ u e. ran g ) /\ ( U. ( `' g " { u } ) i^i v ) =/= (/) ) /\ j e. ( `' g " { u } ) ) /\ ( j i^i v ) =/= (/) ) -> ( g ` j ) = u )
193		fveq2 5774	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = j -> ( g ` k ) = ( g ` j ) )
194	193	eqeq1d 2384	. . . . . . . . . . . . . . . . . . . 20 |- ( k = j -> ( ( g ` k ) = u <-> ( g ` j ) = u ) )
195	194	rspcev 3135	. . . . . . . . . . . . . . . . . . 19 |- ( ( j e. { j e. V | ( j i^i v ) =/= (/) } /\ ( g ` j ) = u ) -> E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u )
196	191, 192, 195	syl2anc 659	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ u e. ran g ) /\ ( U. ( `' g " { u } ) i^i v ) =/= (/) ) /\ j e. ( `' g " { u } ) ) /\ ( j i^i v ) =/= (/) ) -> E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u )
197		uniinn0 27549	. . . . . . . . . . . . . . . . . . . 20 |- ( ( U. ( `' g " { u } ) i^i v ) =/= (/) <-> E. j e. ( `' g " { u } ) ( j i^i v ) =/= (/) )
198	197	biimpi 194	. . . . . . . . . . . . . . . . . . 19 |- ( ( U. ( `' g " { u } ) i^i v ) =/= (/) -> E. j e. ( `' g " { u } ) ( j i^i v ) =/= (/) )
199	198	adantl 464	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ u e. ran g ) /\ ( U. ( `' g " { u } ) i^i v ) =/= (/) ) -> E. j e. ( `' g " { u } ) ( j i^i v ) =/= (/) )
200	179, 181, 196, 199	r19.29af2 2920	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ u e. ran g ) /\ ( U. ( `' g " { u } ) i^i v ) =/= (/) ) -> E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u )
201	200	ex 432	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) /\ u e. ran g ) -> ( ( U. ( `' g " { u } ) i^i v ) =/= (/) -> E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u ) )
202	201	ss2rabdv 3495	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> { u e. ran g | ( U. ( `' g " { u } ) i^i v ) =/= (/) } C_ { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } )
203		ssdomg 7480	. . . . . . . . . . . . . . 15 |- ( { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } e. _V -> ( { u e. ran g | ( U. ( `' g " { u } ) i^i v ) =/= (/) } C_ { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } -> { u e. ran g | ( U. ( `' g " { u } ) i^i v ) =/= (/) } ~<_ { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } ) )
204	171, 202, 203	mpsyl 63	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> { u e. ran g | ( U. ( `' g " { u } ) i^i v ) =/= (/) } ~<_ { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } )
205		domtr 7487	. . . . . . . . . . . . . 14 |- ( ( { w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) | ( w i^i v ) =/= (/) } ~<_ { u e. ran g | ( U. ( `' g " { u } ) i^i v ) =/= (/) } /\ { u e. ran g | ( U. ( `' g " { u } ) i^i v ) =/= (/) } ~<_ { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } ) -> { w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) | ( w i^i v ) =/= (/) } ~<_ { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } )
206	170, 204, 205	syl2anc 659	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> { w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) | ( w i^i v ) =/= (/) } ~<_ { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } )
207	182	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> g Fn V )
208		dffn3 5646	. . . . . . . . . . . . . . 15 |- ( g Fn V <-> g : V --> ran g )
209	208	biimpi 194	. . . . . . . . . . . . . 14 |- ( g Fn V -> g : V --> ran g )
210		ssrab2 3499	. . . . . . . . . . . . . . 15 |- { j e. V | ( j i^i v ) =/= (/) } C_ V
211		fimarab 27623	. . . . . . . . . . . . . . 15 |- ( ( g : V --> ran g /\ { j e. V | ( j i^i v ) =/= (/) } C_ V ) -> ( g " { j e. V | ( j i^i v ) =/= (/) } ) = { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } )
212	210, 211	mpan2 669	. . . . . . . . . . . . . 14 |- ( g : V --> ran g -> ( g " { j e. V | ( j i^i v ) =/= (/) } ) = { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } )
213	207, 209, 212	3syl 20	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> ( g " { j e. V | ( j i^i v ) =/= (/) } ) = { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } )
214	206, 213	breqtrrd 4393	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> { w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) | ( w i^i v ) =/= (/) } ~<_ ( g " { j e. V | ( j i^i v ) =/= (/) } ) )
215		domfi 7657	. . . . . . . . . . . 12 |- ( ( ( g " { j e. V | ( j i^i v ) =/= (/) } ) e. Fin /\ { w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) | ( w i^i v ) =/= (/) } ~<_ ( g " { j e. V | ( j i^i v ) =/= (/) } ) ) -> { w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) | ( w i^i v ) =/= (/) } e. Fin )
216	141, 214, 215	syl2anc 659	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> { w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) | ( w i^i v ) =/= (/) } e. Fin )
217	216	ex 432	. . . . . . . . . 10 |- ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ x e. v ) -> ( { j e. V | ( j i^i v ) =/= (/) } e. Fin -> { w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) | ( w i^i v ) =/= (/) } e. Fin ) )
218	217	imdistanda 691	. . . . . . . . 9 |- ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) -> ( ( x e. v /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) -> ( x e. v /\ { w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) | ( w i^i v ) =/= (/) } e. Fin ) ) )
219	218	imp 427	. . . . . . . 8 |- ( ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) /\ v e. J ) /\ ( x e. v /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) ) -> ( x e. v /\ { w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) | ( w i^i v ) =/= (/) } e. Fin ) )
220		simplll 757	. . . . . . . . 9 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) -> ph )
221		locfinref.x	. . . . . . . . . . . . 13 |- X = U. J
222	221, 29	islocfin 20103	. . . . . . . . . . . 12 |- ( V e. ( LocFin ` J ) <-> ( J e. Top /\ X = U. V /\ A. x e. X E. v e. J ( x e. v /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) ) )
223	2, 222	sylib 196	. . . . . . . . . . 11 |- ( ph -> ( J e. Top /\ X = U. V /\ A. x e. X E. v e. J ( x e. v /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) ) )
224	223	simp3d 1008	. . . . . . . . . 10 |- ( ph -> A. x e. X E. v e. J ( x e. v /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) )
225	224	r19.21bi 2751	. . . . . . . . 9 |- ( ( ph /\ x e. X ) -> E. v e. J ( x e. v /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) )
226	220, 225	sylancom 665	. . . . . . . 8 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) -> E. v e. J ( x e. v /\ { j e. V | ( j i^i v ) =/= (/) } e. Fin ) )
227	136, 137, 219, 226	reximd2a 2852	. . . . . . 7 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X ) -> E. v e. J ( x e. v /\ { w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) | ( w i^i v ) =/= (/) } e. Fin ) )
228	227	ralrimiva 2796	. . . . . 6 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> A. x e. X E. v e. J ( x e. v /\ { w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) | ( w i^i v ) =/= (/) } e. Fin ) )
229	221, 127	islocfin 20103	. . . . . 6 |- ( ran ( u e. ran g |-> U. ( `' g " { u } ) ) e. ( LocFin ` J ) <-> ( J e. Top /\ X = U. ran ( u e. ran g |-> U. ( `' g " { u } ) ) /\ A. x e. X E. v e. J ( x e. v /\ { w e. ran ( u e. ran g |-> U. ( `' g " { u } ) ) | ( w i^i v ) =/= (/) } e. Fin ) ) )
230	131, 134, 228, 229	syl3anbrc 1178	. . . . 5 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ran ( u e. ran g |-> U. ( `' g " { u } ) ) e. ( LocFin ` J ) )
231		funeq 5515	. . . . . . . 8 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( Fun f <-> Fun ( u e. ran g |-> U. ( `' g " { u } ) ) ) )
232		dmeq 5116	. . . . . . . . 9 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> dom f = dom ( u e. ran g |-> U. ( `' g " { u } ) ) )
233	232	sseq1d 3444	. . . . . . . 8 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( dom f C_ U <-> dom ( u e. ran g |-> U. ( `' g " { u } ) ) C_ U ) )
234		rneq 5141	. . . . . . . . 9 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ran f = ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
235	234	sseq1d 3444	. . . . . . . 8 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( ran f C_ J <-> ran ( u e. ran g |-> U. ( `' g " { u } ) ) C_ J ) )
236	231, 233, 235	3anbi123d 1297	. . . . . . 7 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( ( Fun f /\ dom f C_ U /\ ran f C_ J ) <-> ( Fun ( u e. ran g |-> U. ( `' g " { u } ) ) /\ dom ( u e. ran g |-> U. ( `' g " { u } ) ) C_ U /\ ran ( u e. ran g |-> U. ( `' g " { u } ) ) C_ J ) ) )
237	234	breq1d 4377	. . . . . . . 8 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( ran f Ref U <-> ran ( u e. ran g |-> U. ( `' g " { u } ) ) Ref U ) )
238	234	eleq1d 2451	. . . . . . . 8 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( ran f e. ( LocFin ` J ) <-> ran ( u e. ran g |-> U. ( `' g " { u } ) ) e. ( LocFin ` J ) ) )
239	237, 238	anbi12d 708	. . . . . . 7 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( ( ran f Ref U /\ ran f e. ( LocFin ` J ) ) <-> ( ran ( u e. ran g |-> U. ( `' g " { u } ) ) Ref U /\ ran ( u e. ran g |-> U. ( `' g " { u } ) ) e. ( LocFin ` J ) ) ) )
240	236, 239	anbi12d 708	. . . . . 6 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( ( ( Fun f /\ dom f C_ U /\ ran f C_ J ) /\ ( ran f Ref U /\ ran f e. ( LocFin ` J ) ) ) <-> ( ( Fun ( u e. ran g |-> U. ( `' g " { u } ) ) /\ dom ( u e. ran g |-> U. ( `' g " { u } ) ) C_ U /\ ran ( u e. ran g |-> U. ( `' g " { u } ) ) C_ J ) /\ ( ran ( u e. ran g |-> U. ( `' g " { u } ) ) Ref U /\ ran ( u e. ran g |-> U. ( `' g " { u } ) ) e. ( LocFin ` J ) ) ) ) )
241	124, 240	spcev 3126	. . . . 5 |- ( ( ( Fun ( u e. ran g |-> U. ( `' g " { u } ) ) /\ dom ( u e. ran g |-> U. ( `' g " { u } ) ) C_ U /\ ran ( u e. ran g |-> U. ( `' g " { u } ) ) C_ J ) /\ ( ran ( u e. ran g |-> U. ( `' g " { u } ) ) Ref U /\ ran ( u e. ran g |-> U. ( `' g " { u } ) ) e. ( LocFin ` J ) ) ) -> E. f ( ( Fun f /\ dom f C_ U /\ ran f C_ J ) /\ ( ran f Ref U /\ ran f e. ( LocFin ` J ) ) ) )
242	8, 13, 28, 130, 230, 241	syl32anc 1234	. . . 4 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> E. f ( ( Fun f /\ dom f C_ U /\ ran f C_ J ) /\ ( ran f Ref U /\ ran f e. ( LocFin ` J ) ) ) )
243	242	expl 616	. . 3 |- ( ph -> ( ( g : V --> U /\ A. v e. V v C_ ( g ` v ) ) -> E. f ( ( Fun f /\ dom f C_ U /\ ran f C_ J ) /\ ( ran f Ref U /\ ran f e. ( LocFin ` J ) ) ) ) )
244	243	exlimdv 1732	. 2 |- ( ph -> ( E. g ( g : V --> U /\ A. v e. V v C_ ( g ` v ) ) -> E. f ( ( Fun f /\ dom f C_ U /\ ran f C_ J ) /\ ( ran f Ref U /\ ran f e. ( LocFin ` J ) ) ) ) )
245	6, 244	mpd 15	1 |- ( ph -> E. f ( ( Fun f /\ dom f C_ U /\ ran f C_ J ) /\ ( ran f Ref U /\ ran f e. ( LocFin ` J ) ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   /\ w3a 971   = wceq 1399   E.wex 1620   e. wcel 1826   =/= wne 2577   A.wral 2732   E.wrex 2733   {crab 2736   _Vcvv 3034   i^i cin 3388   C_ wss 3389   (/)c0 3711   {csn 3944   U.cuni 4163   U_ciun 4243   class class class wbr 4367   |-> cmpt 4425   `'ccnv 4912   dom cdm 4913   ran crn 4914   "cima 4916   Fun wfun 5490   Fn wfn 5491   -->wf 5492   -onto->wfo 5494   ` cfv 5496   ~<_ cdom 7433   Fincfn 7435   Topctop 19479   Refcref 20088   LocFinclocfin 20090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-rep 4478  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-reg 7933  ax-inf2 7972  ax-ac2 8756

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-reu 2739  df-rmo 2740  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-int 4200  df-iun 4245  df-iin 4246  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-se 4753  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-isom 5505  df-riota 6158  df-om 6600  df-recs 6960  df-rdg 6994  df-1o 7048  df-er 7229  df-en 7436  df-dom 7437  df-fin 7439  df-r1 8095  df-rank 8096  df-card 8233  df-ac 8410  df-top 19484  df-ref 20091  df-locfin 20093

This theorem is referenced by:  locfinref  27998