Theorem locfinreflem 27821

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 27820	. . . . 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 463	. 2 |- ( ph -> E. g ( g : V --> U /\ A. v e. V v C_ ( g ` v ) ) )
7		funmpt 5614	. . . . . 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 2443	. . . . . . 7 |- ( u e. ran g |-> U. ( `' g " { u } ) ) = ( u e. ran g |-> U. ( `' g " { u } ) )
10	9	dmmptss 5493	. . . . . 6 |- dom ( u e. ran g |-> U. ( `' g " { u } ) ) C_ ran g
11		frn 5727	. . . . . . 7 |- ( g : V --> U -> ran g C_ U )
12	11	ad2antlr 726	. . . . . 6 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ran g C_ U )
13	10, 12	syl5ss 3500	. . . . 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 20000	. . . . . . . . . 10 |- ( V e. ( LocFin ` J ) -> J e. Top )
15	2, 14	syl 16	. . . . . . . . 9 |- ( ph -> J e. Top )
16	15	ad3antrrr 729	. . . . . . . 8 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> J e. Top )
17		cnvimass 5347	. . . . . . . . . 10 |- ( `' g " { u } ) C_ dom g
18		fdm 5725	. . . . . . . . . . 11 |- ( g : V --> U -> dom g = V )
19	18	ad3antlr 730	. . . . . . . . . 10 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> dom g = V )
20	17, 19	syl5sseq 3537	. . . . . . . . 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 729	. . . . . . . . 9 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> V C_ J )
23	20, 22	sstrd 3499	. . . . . . . 8 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> ( `' g " { u } ) C_ J )
24		uniopn 19384	. . . . . . . 8 |- ( ( J e. Top /\ ( `' g " { u } ) C_ J ) -> U. ( `' g " { u } ) e. J )
25	16, 23, 24	syl2anc 661	. . . . . . 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 2857	. . . . . 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 6045	. . . . . 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 2443	. . . . . . . . . 10 |- U. V = U. V
30		eqid 2443	. . . . . . . . . 10 |- U. U = U. U
31	29, 30	refbas 19989	. . . . . . . . 9 |- ( V Ref U -> U. U = U. V )
32	1, 31	syl 16	. . . . . . . 8 |- ( ph -> U. U = U. V )
33	32	ad2antrr 725	. . . . . . 7 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> U. U = U. V )
34		nfv 1694	. . . . . . . . . . . . 13 |- F/ v ( ph /\ g : V --> U )
35		nfra1 2824	. . . . . . . . . . . . 13 |- F/ v A. v e. V v C_ ( g ` v )
36	34, 35	nfan 1914	. . . . . . . . . . . 12 |- F/ v ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) )
37		nfre1 2904	. . . . . . . . . . . 12 |- F/ v E. v e. V x e. v
38	36, 37	nfan 1914	. . . . . . . . . . 11 |- F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ E. v e. V x e. v )
39		ffn 5721	. . . . . . . . . . . . . . 15 |- ( g : V --> U -> g Fn V )
40	39	ad4antlr 732	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) /\ x e. v ) -> g Fn V )
41		simplr 755	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) /\ x e. v ) -> v e. V )
42		fnfvelrn 6013	. . . . . . . . . . . . . 14 |- ( ( g Fn V /\ v e. V ) -> ( g ` v ) e. ran g )
43	40, 41, 42	syl2anc 661	. . . . . . . . . . . . 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 3508	. . . . . . . . . . . . . . 15 |- v C_ v
45	39	ad3antlr 730	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) -> g Fn V )
46		eqid 2443	. . . . . . . . . . . . . . . . 17 |- ( g ` v ) = ( g ` v )
47		fniniseg 5993	. . . . . . . . . . . . . . . . . 18 |- ( g Fn V -> ( v e. ( `' g " { ( g ` v ) } ) <-> ( v e. V /\ ( g ` v ) = ( g ` v ) ) ) )
48	47	biimpar 485	. . . . . . . . . . . . . . . . 17 |- ( ( g Fn V /\ ( v e. V /\ ( g ` v ) = ( g ` v ) ) ) -> v e. ( `' g " { ( g ` v ) } ) )
49	46, 48	mpanr2 684	. . . . . . . . . . . . . . . 16 |- ( ( g Fn V /\ v e. V ) -> v e. ( `' g " { ( g ` v ) } ) )
50	45, 49	sylancom 667	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) -> v e. ( `' g " { ( g ` v ) } ) )
51		ssuni 4256	. . . . . . . . . . . . . . 15 |- ( ( v C_ v /\ v e. ( `' g " { ( g ` v ) } ) ) -> v C_ U. ( `' g " { ( g ` v ) } ) )
52	44, 50, 51	sylancr 663	. . . . . . . . . . . . . 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 3489	. . . . . . . . . . . . 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 4024	. . . . . . . . . . . . . . . . 17 |- ( u = ( g ` v ) -> { u } = { ( g ` v ) } )
55	54	imaeq2d 5327	. . . . . . . . . . . . . . . 16 |- ( u = ( g ` v ) -> ( `' g " { u } ) = ( `' g " { ( g ` v ) } ) )
56	55	unieqd 4244	. . . . . . . . . . . . . . 15 |- ( u = ( g ` v ) -> U. ( `' g " { u } ) = U. ( `' g " { ( g ` v ) } ) )
57	56	eleq2d 2513	. . . . . . . . . . . . . 14 |- ( u = ( g ` v ) -> ( x e. U. ( `' g " { u } ) <-> x e. U. ( `' g " { ( g ` v ) } ) ) )
58	57	rspcev 3196	. . . . . . . . . . . . 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 661	. . . . . . . . . . . 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 718	. . . . . . . . . . 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 461	. . . . . . . . . . 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 2983	. . . . . . . . . 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 1694	. . . . . . . . . . . . . 14 |- F/ v u e. ran g
64	36, 63	nfan 1914	. . . . . . . . . . . . 13 |- F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g )
65		nfv 1694	. . . . . . . . . . . . 13 |- F/ v x e. U. ( `' g " { u } )
66	64, 65	nfan 1914	. . . . . . . . . . . 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 729	. . . . . . . . . . . . 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 755	. . . . . . . . . . . . 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 3490	. . . . . . . . . . . 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 461	. . . . . . . . . . . 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 461	. . . . . . . . . . . . 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 4238	. . . . . . . . . . . . 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 2913	. . . . . . . . . . 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 2984	. . . . . . . . . 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 832	. . . . . . . . 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 4238	. . . . . . . . 9 |- ( x e. U. V <-> E. v e. V x e. v )
78		eliun 4320	. . . . . . . . 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 2440	. . . . . . 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 5245	. . . . . . . 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 2488	. . . . . 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 730	. . . . . . . . 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 3098	. . . . . . . . . . 11 |- w e. _V
86	9	elrnmpt 5239	. . . . . . . . . . 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 484	. . . . . . . . 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 3550	. . . . . . . . 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 1694	. . . . . . . . . 10 |- F/ u ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) )
92		nfmpt1 4526	. . . . . . . . . . . 12 |- F/_ u ( u e. ran g |-> U. ( `' g " { u } ) )
93	92	nfrn 5235	. . . . . . . . . . 11 |- F/_ u ran ( u e. ran g |-> U. ( `' g " { u } ) )
94	93	nfcri 2598	. . . . . . . . . 10 |- F/ u w e. ran ( u e. ran g |-> U. ( `' g " { u } ) )
95	91, 94	nfan 1914	. . . . . . . . 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 461	. . . . . . . . . . 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 1694	. . . . . . . . . . . . . . . 16 |- F/ v w e. ran ( u e. ran g |-> U. ( `' g " { u } ) )
98	36, 97	nfan 1914	. . . . . . . . . . . . . . 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 1694	. . . . . . . . . . . . . . 15 |- F/ v u e. U
100	98, 99	nfan 1914	. . . . . . . . . . . . . 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 1694	. . . . . . . . . . . . . 14 |- F/ v w = U. ( `' g " { u } )
102	100, 101	nfan 1914	. . . . . . . . . . . . 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 770	. . . . . . . . . . . . . . . 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 734	. . . . . . . . . . . . . . . . . . 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 5993	. . . . . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . . . 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 459	. . . . . . . . . . . . . . . 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 2810	. . . . . . . . . . . . . . . 16 |- ( ( A. v e. V v C_ ( g ` v ) /\ v e. V ) -> v C_ ( g ` v ) )
110	103, 108, 109	syl2anc 661	. . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . 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 3525	. . . . . . . . . . . . . 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 434	. . . . . . . . . . . . 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 2843	. . . . . . . . . . . 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 4266	. . . . . . . . . . . 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 3523	. . . . . . . . . 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 604	. . . . . . . . 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 2912	. . . . . . . 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 2857	. . . . . 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 3098	. . . . . . . . . 10 |- g e. _V
123	122	rnex 6719	. . . . . . . . 9 |- ran g e. _V
124	123	mptex 6128	. . . . . . . 8 |- ( u e. ran g |-> U. ( `' g " { u } ) ) e. _V
125		rnexg 6717	. . . . . . . 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 2443	. . . . . . . 8 |- U. ran ( u e. ran g |-> U. ( `' g " { u } ) ) = U. ran ( u e. ran g |-> U. ( `' g " { u } ) )
128	127, 30	isref 19988	. . . . . . 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 922	. . . . 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 725	. . . . . 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 725	. . . . . . 7 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> X = U. U )
134	133, 83	eqtrd 2484	. . . . . 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 1694	. . . . . . . . 9 |- F/ v x e. X
136	36, 135	nfan 1914	. . . . . . . 8 |- F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X )
137		simplr 755	. . . . . . . 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 5723	. . . . . . . . . . . . . 14 |- ( g : V --> U -> Fun g )
139	138	ad6antlr 736	. . . . . . . . . . . . 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 7815	. . . . . . . . . . . . 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 667	. . . . . . . . . . . 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 999	. . . . . . . . . . . . . . . . . . 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 4024	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( u = k -> { u } = { k } )
144	143	imaeq2d 5327	. . . . . . . . . . . . . . . . . . . . . 22 |- ( u = k -> ( `' g " { u } ) = ( `' g " { k } ) )
145	144	unieqd 4244	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = k -> U. ( `' g " { u } ) = U. ( `' g " { k } ) )
146	122	cnvex 6732	. . . . . . . . . . . . . . . . . . . . . . 23 |- `' g e. _V
147		imaexg 6722	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( `' g e. _V -> ( `' g " { k } ) e. _V )
148	146, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 |- ( `' g " { k } ) e. _V
149	148	uniex 6581	. . . . . . . . . . . . . . . . . . . . 21 |- U. ( `' g " { k } ) e. _V
150	145, 9, 149	fvmpt 5941	. . . . . . . . . . . . . . . . . . . 20 |- ( k e. ran g -> ( ( u e. ran g |-> U. ( `' g " { u } ) ) ` k ) = U. ( `' g " { k } ) )
151	150	3ad2ant2 1019	. . . . . . . . . . . . . . . . . . 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 2484	. . . . . . . . . . . . . . . . . 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 3684	. . . . . . . . . . . . . . . . 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 2720	. . . . . . . . . . . . . . . 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 6722	. . . . . . . . . . . . . . . . . . . . 21 |- ( `' g e. _V -> ( `' g " { u } ) e. _V )
157	146, 156	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- ( `' g " { u } ) e. _V
158	157	uniex 6581	. . . . . . . . . . . . . . . . . . 19 |- U. ( `' g " { u } ) e. _V
159	158, 9	fnmpti 5699	. . . . . . . . . . . . . . . . . 18 |- ( u e. ran g |-> U. ( `' g " { u } ) ) Fn ran g
160		dffn4 5791	. . . . . . . . . . . . . . . . . 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 27382	. . . . . . . . . . . . . . 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 4024	. . . . . . . . . . . . . . . . . . . 20 |- ( k = u -> { k } = { u } )
165	164	imaeq2d 5327	. . . . . . . . . . . . . . . . . . 19 |- ( k = u -> ( `' g " { k } ) = ( `' g " { u } ) )
166	165	unieqd 4244	. . . . . . . . . . . . . . . . . 18 |- ( k = u -> U. ( `' g " { k } ) = U. ( `' g " { u } ) )
167	166	ineq1d 3684	. . . . . . . . . . . . . . . . 17 |- ( k = u -> ( U. ( `' g " { k } ) i^i v ) = ( U. ( `' g " { u } ) i^i v ) )
168	167	neeq1d 2720	. . . . . . . . . . . . . . . 16 |- ( k = u -> ( ( U. ( `' g " { k } ) i^i v ) =/= (/) <-> ( U. ( `' g " { u } ) i^i v ) =/= (/) ) )
169	168	cbvrabv 3094	. . . . . . . . . . . . . . 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 4476	. . . . . . . . . . . . . 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 4588	. . . . . . . . . . . . . . 15 |- { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } e. _V
172		nfv 1694	. . . . . . . . . . . . . . . . . . . . 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 3024	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ j { j e. V | ( j i^i v ) =/= (/) }
174	173	nfel1 2621	. . . . . . . . . . . . . . . . . . . . 21 |- F/ j { j e. V | ( j i^i v ) =/= (/) } e. Fin
175	172, 174	nfan 1914	. . . . . . . . . . . . . . . . . . . 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 1694	. . . . . . . . . . . . . . . . . . . 20 |- F/ j u e. ran g
177	175, 176	nfan 1914	. . . . . . . . . . . . . . . . . . 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 1694	. . . . . . . . . . . . . . . . . . 19 |- F/ j ( U. ( `' g " { u } ) i^i v ) =/= (/)
179	177, 178	nfan 1914	. . . . . . . . . . . . . . . . . 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 1694	. . . . . . . . . . . . . . . . . . 19 |- F/ j ( g ` k ) = u
181	173, 180	nfrex 2906	. . . . . . . . . . . . . . . . . 18 |- F/ j E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u
182	39	ad5antlr 734	. . . . . . . . . . . . . . . . . . . . . . 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 733	. . . . . . . . . . . . . . . . . . . . . 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 755	. . . . . . . . . . . . . . . . . . . . . 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 5993	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g Fn V -> ( j e. ( `' g " { u } ) <-> ( j e. V /\ ( g ` j ) = u ) ) )
186	185	biimpa 484	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( g Fn V /\ j e. ( `' g " { u } ) ) -> ( j e. V /\ ( g ` j ) = u ) )
187	183, 184, 186	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 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 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 e. V )
189		simpr 461	. . . . . . . . . . . . . . . . . . . 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 3020	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. { j e. V | ( j i^i v ) =/= (/) } <-> ( j e. V /\ ( j i^i v ) =/= (/) ) )
191	188, 189, 190	sylanbrc 664	. . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . 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 5856	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = j -> ( g ` k ) = ( g ` j ) )
194	193	eqeq1d 2445	. . . . . . . . . . . . . . . . . . . 20 |- ( k = j -> ( ( g ` k ) = u <-> ( g ` j ) = u ) )
195	194	rspcev 3196	. . . . . . . . . . . . . . . . . . 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 661	. . . . . . . . . . . . . . . . . 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 27402	. . . . . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . 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 2981	. . . . . . . . . . . . . . . . 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 434	. . . . . . . . . . . . . . . 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 3566	. . . . . . . . . . . . . . 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 7563	. . . . . . . . . . . . . . 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 7570	. . . . . . . . . . . . . 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 661	. . . . . . . . . . . . 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 465	. . . . . . . . . . . . . 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 5728	. . . . . . . . . . . . . . 15 |- ( g Fn V <-> g : V --> ran g )
209	208	biimpi 194	. . . . . . . . . . . . . 14 |- ( g Fn V -> g : V --> ran g )
210		ssrab2 3570	. . . . . . . . . . . . . . 15 |- { j e. V | ( j i^i v ) =/= (/) } C_ V
211		fimarab 27461	. . . . . . . . . . . . . . 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 671	. . . . . . . . . . . . . 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 4463	. . . . . . . . . . . 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 7743	. . . . . . . . . . . 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 661	. . . . . . . . . . 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 434	. . . . . . . . . 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 693	. . . . . . . . 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 429	. . . . . . . 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 759	. . . . . . . . 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 19996	. . . . . . . . . . . 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 1011	. . . . . . . . . 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 2812	. . . . . . . . 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 667	. . . . . . . 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 2913	. . . . . . 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 2857	. . . . . 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 19996	. . . . . 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 1181	. . . . 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 5597	. . . . . . . 8 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( Fun f <-> Fun ( u e. ran g |-> U. ( `' g " { u } ) ) ) )
232		dmeq 5193	. . . . . . . . 9 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> dom f = dom ( u e. ran g |-> U. ( `' g " { u } ) ) )
233	232	sseq1d 3516	. . . . . . . 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 5218	. . . . . . . . 9 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ran f = ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
235	234	sseq1d 3516	. . . . . . . 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 1300	. . . . . . 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 4447	. . . . . . . 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 2512	. . . . . . . 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 710	. . . . . . 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 710	. . . . . 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 3187	. . . . 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 1237	. . . 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 618	. . 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 1711	. 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 369   /\ w3a 974   = wceq 1383   E.wex 1599   e. wcel 1804   =/= wne 2638   A.wral 2793   E.wrex 2794   {crab 2797   _Vcvv 3095   i^i cin 3460   C_ wss 3461   (/)c0 3770   {csn 4014   U.cuni 4234   U_ciun 4315   class class class wbr 4437   |-> cmpt 4495   `'ccnv 4988   dom cdm 4989   ran crn 4990   "cima 4992   Fun wfun 5572   Fn wfn 5573   -->wf 5574   -onto->wfo 5576   ` cfv 5578   ~<_ cdom 7516   Fincfn 7518   Topctop 19372   Refcref 19981   LocFinclocfin 19983

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-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-reg 8021  ax-inf2 8061  ax-ac2 8846

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-rmo 2801  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-se 4829  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-isom 5587  df-riota 6242  df-om 6686  df-recs 7044  df-rdg 7078  df-1o 7132  df-er 7313  df-en 7519  df-dom 7520  df-fin 7522  df-r1 8185  df-rank 8186  df-card 8323  df-ac 8500  df-top 19377  df-ref 19984  df-locfin 19986

This theorem is referenced by:  locfinref  27822