Theorem locfinreflem 28741

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 28740	. . . . 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 17	. . . 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 215	. . 3 |- ( ph -> ( U. U C_ U. V /\ E. g ( g : V --> U /\ A. v e. V v C_ ( g ` v ) ) ) )
6	5	simprd 470	. 2 |- ( ph -> E. g ( g : V --> U /\ A. v e. V v C_ ( g ` v ) ) )
7		funmpt 5625	. . . . . 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 2471	. . . . . . 7 |- ( u e. ran g |-> U. ( `' g " { u } ) ) = ( u e. ran g |-> U. ( `' g " { u } ) )
10	9	dmmptss 5338	. . . . . 6 |- dom ( u e. ran g |-> U. ( `' g " { u } ) ) C_ ran g
11		frn 5747	. . . . . . 7 |- ( g : V --> U -> ran g C_ U )
12	11	ad2antlr 741	. . . . . 6 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ran g C_ U )
13	10, 12	syl5ss 3429	. . . . 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 20613	. . . . . . . . . 10 |- ( V e. ( LocFin ` J ) -> J e. Top )
15	2, 14	syl 17	. . . . . . . . 9 |- ( ph -> J e. Top )
16	15	ad3antrrr 744	. . . . . . . 8 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> J e. Top )
17		cnvimass 5194	. . . . . . . . . 10 |- ( `' g " { u } ) C_ dom g
18		fdm 5745	. . . . . . . . . . 11 |- ( g : V --> U -> dom g = V )
19	18	ad3antlr 745	. . . . . . . . . 10 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> dom g = V )
20	17, 19	syl5sseq 3466	. . . . . . . . 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 744	. . . . . . . . 9 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> V C_ J )
23	20, 22	sstrd 3428	. . . . . . . 8 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> ( `' g " { u } ) C_ J )
24		uniopn 20004	. . . . . . . 8 |- ( ( J e. Top /\ ( `' g " { u } ) C_ J ) -> U. ( `' g " { u } ) e. J )
25	16, 23, 24	syl2anc 673	. . . . . . 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 2809	. . . . . 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 6068	. . . . . 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 17	. . . . 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 2471	. . . . . . . . . 10 |- U. V = U. V
30		eqid 2471	. . . . . . . . . 10 |- U. U = U. U
31	29, 30	refbas 20602	. . . . . . . . 9 |- ( V Ref U -> U. U = U. V )
32	1, 31	syl 17	. . . . . . . 8 |- ( ph -> U. U = U. V )
33	32	ad2antrr 740	. . . . . . 7 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> U. U = U. V )
34		nfv 1769	. . . . . . . . . . . . 13 |- F/ v ( ph /\ g : V --> U )
35		nfra1 2785	. . . . . . . . . . . . 13 |- F/ v A. v e. V v C_ ( g ` v )
36	34, 35	nfan 2031	. . . . . . . . . . . 12 |- F/ v ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) )
37		nfre1 2846	. . . . . . . . . . . 12 |- F/ v E. v e. V x e. v
38	36, 37	nfan 2031	. . . . . . . . . . 11 |- F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ E. v e. V x e. v )
39		ffn 5739	. . . . . . . . . . . . . . 15 |- ( g : V --> U -> g Fn V )
40	39	ad4antlr 747	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) /\ x e. v ) -> g Fn V )
41		simplr 770	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) /\ x e. v ) -> v e. V )
42		fnfvelrn 6034	. . . . . . . . . . . . . 14 |- ( ( g Fn V /\ v e. V ) -> ( g ` v ) e. ran g )
43	40, 41, 42	syl2anc 673	. . . . . . . . . . . . 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 3437	. . . . . . . . . . . . . . 15 |- v C_ v
45	39	ad3antlr 745	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) -> g Fn V )
46		eqid 2471	. . . . . . . . . . . . . . . . 17 |- ( g ` v ) = ( g ` v )
47		fniniseg 6018	. . . . . . . . . . . . . . . . . 18 |- ( g Fn V -> ( v e. ( `' g " { ( g ` v ) } ) <-> ( v e. V /\ ( g ` v ) = ( g ` v ) ) ) )
48	47	biimpar 493	. . . . . . . . . . . . . . . . 17 |- ( ( g Fn V /\ ( v e. V /\ ( g ` v ) = ( g ` v ) ) ) -> v e. ( `' g " { ( g ` v ) } ) )
49	46, 48	mpanr2 698	. . . . . . . . . . . . . . . 16 |- ( ( g Fn V /\ v e. V ) -> v e. ( `' g " { ( g ` v ) } ) )
50	45, 49	sylancom 680	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) -> v e. ( `' g " { ( g ` v ) } ) )
51		ssuni 4212	. . . . . . . . . . . . . . 15 |- ( ( v C_ v /\ v e. ( `' g " { ( g ` v ) } ) ) -> v C_ U. ( `' g " { ( g ` v ) } ) )
52	44, 50, 51	sylancr 676	. . . . . . . . . . . . . 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 3418	. . . . . . . . . . . . 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 3969	. . . . . . . . . . . . . . . . 17 |- ( u = ( g ` v ) -> { u } = { ( g ` v ) } )
55	54	imaeq2d 5174	. . . . . . . . . . . . . . . 16 |- ( u = ( g ` v ) -> ( `' g " { u } ) = ( `' g " { ( g ` v ) } ) )
56	55	unieqd 4200	. . . . . . . . . . . . . . 15 |- ( u = ( g ` v ) -> U. ( `' g " { u } ) = U. ( `' g " { ( g ` v ) } ) )
57	56	eleq2d 2534	. . . . . . . . . . . . . 14 |- ( u = ( g ` v ) -> ( x e. U. ( `' g " { u } ) <-> x e. U. ( `' g " { ( g ` v ) } ) ) )
58	57	rspcev 3136	. . . . . . . . . . . . 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 673	. . . . . . . . . . . 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 733	. . . . . . . . . . 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 468	. . . . . . . . . . 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 2916	. . . . . . . . . 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 1769	. . . . . . . . . . . . . 14 |- F/ v u e. ran g
64	36, 63	nfan 2031	. . . . . . . . . . . . 13 |- F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g )
65		nfv 1769	. . . . . . . . . . . . 13 |- F/ v x e. U. ( `' g " { u } )
66	64, 65	nfan 2031	. . . . . . . . . . . 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 744	. . . . . . . . . . . . 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 770	. . . . . . . . . . . . 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 3419	. . . . . . . . . . . 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 468	. . . . . . . . . . . 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 468	. . . . . . . . . . . . 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 4194	. . . . . . . . . . . . 13 |- ( x e. U. ( `' g " { u } ) <-> E. v e. ( `' g " { u } ) x e. v )
73	71, 72	sylib 201	. . . . . . . . . . . 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 2854	. . . . . . . . . . 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 2917	. . . . . . . . . 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 850	. . . . . . . . 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 4194	. . . . . . . . 9 |- ( x e. U. V <-> E. v e. V x e. v )
78		eliun 4274	. . . . . . . . 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 296	. . . . . . . 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 2469	. . . . . . 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 5093	. . . . . . . 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 17	. . . . . . 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 2509	. . . . . 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 745	. . . . . . . . 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 3034	. . . . . . . . . . 11 |- w e. _V
86	9	elrnmpt 5087	. . . . . . . . . . 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 13	. . . . . . . . . 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 492	. . . . . . . . 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 3480	. . . . . . . . 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 61	. . . . . . . 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 1769	. . . . . . . . . 10 |- F/ u ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) )
92		nfmpt1 4485	. . . . . . . . . . . 12 |- F/_ u ( u e. ran g |-> U. ( `' g " { u } ) )
93	92	nfrn 5083	. . . . . . . . . . 11 |- F/_ u ran ( u e. ran g |-> U. ( `' g " { u } ) )
94	93	nfcri 2606	. . . . . . . . . 10 |- F/ u w e. ran ( u e. ran g |-> U. ( `' g " { u } ) )
95	91, 94	nfan 2031	. . . . . . . . 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 468	. . . . . . . . . . 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 1769	. . . . . . . . . . . . . . . 16 |- F/ v w e. ran ( u e. ran g |-> U. ( `' g " { u } ) )
98	36, 97	nfan 2031	. . . . . . . . . . . . . . 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 1769	. . . . . . . . . . . . . . 15 |- F/ v u e. U
100	98, 99	nfan 2031	. . . . . . . . . . . . . 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 1769	. . . . . . . . . . . . . 14 |- F/ v w = U. ( `' g " { u } )
102	100, 101	nfan 2031	. . . . . . . . . . . . 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 787	. . . . . . . . . . . . . . . 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 749	. . . . . . . . . . . . . . . . . . 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 6018	. . . . . . . . . . . . . . . . . . 19 |- ( g Fn V -> ( v e. ( `' g " { u } ) <-> ( v e. V /\ ( g ` v ) = u ) ) )
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . 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 492	. . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . 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 2774	. . . . . . . . . . . . . . . 16 |- ( ( A. v e. V v C_ ( g ` v ) /\ v e. V ) -> v C_ ( g ` v ) )
110	103, 108, 109	syl2anc 673	. . . . . . . . . . . . . . 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 470	. . . . . . . . . . . . . . 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 3454	. . . . . . . . . . . . . 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 441	. . . . . . . . . . . . 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 2800	. . . . . . . . . . . 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 4221	. . . . . . . . . . . 12 |- ( U. ( `' g " { u } ) C_ u <-> A. v e. ( `' g " { u } ) v C_ u )
116	114, 115	sylibr 217	. . . . . . . . . . 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 3452	. . . . . . . . . 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 615	. . . . . . . . 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 2853	. . . . . . . 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 2809	. . . . . 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 3034	. . . . . . . . . 10 |- g e. _V
123	122	rnex 6746	. . . . . . . . 9 |- ran g e. _V
124	123	mptex 6152	. . . . . . . 8 |- ( u e. ran g |-> U. ( `' g " { u } ) ) e. _V
125		rnexg 6744	. . . . . . . 8 |- ( ( u e. ran g |-> U. ( `' g " { u } ) ) e. _V -> ran ( u e. ran g |-> U. ( `' g " { u } ) ) e. _V )
126	124, 125	mp1i 13	. . . . . . 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 2471	. . . . . . . 8 |- U. ran ( u e. ran g |-> U. ( `' g " { u } ) ) = U. ran ( u e. ran g |-> U. ( `' g " { u } ) )
128	127, 30	isref 20601	. . . . . . 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 17	. . . . . 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 936	. . . . 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 740	. . . . . 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 740	. . . . . . 7 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> X = U. U )
134	133, 83	eqtrd 2505	. . . . . 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 1769	. . . . . . . . 9 |- F/ v x e. X
136	36, 135	nfan 2031	. . . . . . . 8 |- F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X )
137		simplr 770	. . . . . . . 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 5742	. . . . . . . . . . . . . 14 |- ( g : V --> U -> Fun g )
139	138	ad6antlr 751	. . . . . . . . . . . . 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 7885	. . . . . . . . . . . . 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 680	. . . . . . . . . . . 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 1032	. . . . . . . . . . . . . . . . . . 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 3969	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( u = k -> { u } = { k } )
144	143	imaeq2d 5174	. . . . . . . . . . . . . . . . . . . . . 22 |- ( u = k -> ( `' g " { u } ) = ( `' g " { k } ) )
145	144	unieqd 4200	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = k -> U. ( `' g " { u } ) = U. ( `' g " { k } ) )
146	122	cnvex 6759	. . . . . . . . . . . . . . . . . . . . . . 23 |- `' g e. _V
147		imaexg 6749	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( `' g e. _V -> ( `' g " { k } ) e. _V )
148	146, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 |- ( `' g " { k } ) e. _V
149	148	uniex 6606	. . . . . . . . . . . . . . . . . . . . 21 |- U. ( `' g " { k } ) e. _V
150	145, 9, 149	fvmpt 5963	. . . . . . . . . . . . . . . . . . . 20 |- ( k e. ran g -> ( ( u e. ran g |-> U. ( `' g " { u } ) ) ` k ) = U. ( `' g " { k } ) )
151	150	3ad2ant2 1052	. . . . . . . . . . . . . . . . . . 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 2505	. . . . . . . . . . . . . . . . . 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 3624	. . . . . . . . . . . . . . . . 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 2702	. . . . . . . . . . . . . . . 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 6749	. . . . . . . . . . . . . . . . . . . . 21 |- ( `' g e. _V -> ( `' g " { u } ) e. _V )
157	146, 156	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- ( `' g " { u } ) e. _V
158	157	uniex 6606	. . . . . . . . . . . . . . . . . . 19 |- U. ( `' g " { u } ) e. _V
159	158, 9	fnmpti 5716	. . . . . . . . . . . . . . . . . 18 |- ( u e. ran g |-> U. ( `' g " { u } ) ) Fn ran g
160		dffn4 5812	. . . . . . . . . . . . . . . . . 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 213	. . . . . . . . . . . . . . . . 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 28219	. . . . . . . . . . . . . . 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 3969	. . . . . . . . . . . . . . . . . . . 20 |- ( k = u -> { k } = { u } )
165	164	imaeq2d 5174	. . . . . . . . . . . . . . . . . . 19 |- ( k = u -> ( `' g " { k } ) = ( `' g " { u } ) )
166	165	unieqd 4200	. . . . . . . . . . . . . . . . . 18 |- ( k = u -> U. ( `' g " { k } ) = U. ( `' g " { u } ) )
167	166	ineq1d 3624	. . . . . . . . . . . . . . . . 17 |- ( k = u -> ( U. ( `' g " { k } ) i^i v ) = ( U. ( `' g " { u } ) i^i v ) )
168	167	neeq1d 2702	. . . . . . . . . . . . . . . 16 |- ( k = u -> ( ( U. ( `' g " { k } ) i^i v ) =/= (/) <-> ( U. ( `' g " { u } ) i^i v ) =/= (/) ) )
169	168	cbvrabv 3030	. . . . . . . . . . . . . . 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 4435	. . . . . . . . . . . . . 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 4550	. . . . . . . . . . . . . . 15 |- { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } e. _V
172		nfv 1769	. . . . . . . . . . . . . . . . . . . . 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 2957	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ j { j e. V | ( j i^i v ) =/= (/) }
174	173	nfel1 2626	. . . . . . . . . . . . . . . . . . . . 21 |- F/ j { j e. V | ( j i^i v ) =/= (/) } e. Fin
175	172, 174	nfan 2031	. . . . . . . . . . . . . . . . . . . 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 1769	. . . . . . . . . . . . . . . . . . . 20 |- F/ j u e. ran g
177	175, 176	nfan 2031	. . . . . . . . . . . . . . . . . . 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 1769	. . . . . . . . . . . . . . . . . . 19 |- F/ j ( U. ( `' g " { u } ) i^i v ) =/= (/)
179	177, 178	nfan 2031	. . . . . . . . . . . . . . . . . 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 1769	. . . . . . . . . . . . . . . . . . 19 |- F/ j ( g ` k ) = u
181	173, 180	nfrex 2848	. . . . . . . . . . . . . . . . . 18 |- F/ j E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u
182	39	ad5antlr 749	. . . . . . . . . . . . . . . . . . . . . . 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 748	. . . . . . . . . . . . . . . . . . . . . 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 770	. . . . . . . . . . . . . . . . . . . . . 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 6018	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g Fn V -> ( j e. ( `' g " { u } ) <-> ( j e. V /\ ( g ` j ) = u ) ) )
186	185	biimpa 492	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( g Fn V /\ j e. ( `' g " { u } ) ) -> ( j e. V /\ ( g ` j ) = u ) )
187	183, 184, 186	syl2anc 673	. . . . . . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . . . . . . 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 2953	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. { j e. V | ( j i^i v ) =/= (/) } <-> ( j e. V /\ ( j i^i v ) =/= (/) ) )
191	188, 189, 190	sylanbrc 677	. . . . . . . . . . . . . . . . . . 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 470	. . . . . . . . . . . . . . . . . . 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 5879	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = j -> ( g ` k ) = ( g ` j ) )
194	193	eqeq1d 2473	. . . . . . . . . . . . . . . . . . . 20 |- ( k = j -> ( ( g ` k ) = u <-> ( g ` j ) = u ) )
195	194	rspcev 3136	. . . . . . . . . . . . . . . . . . 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 673	. . . . . . . . . . . . . . . . . 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 28241	. . . . . . . . . . . . . . . . . . . 20 |- ( ( U. ( `' g " { u } ) i^i v ) =/= (/) <-> E. j e. ( `' g " { u } ) ( j i^i v ) =/= (/) )
198	197	biimpi 199	. . . . . . . . . . . . . . . . . . 19 |- ( ( U. ( `' g " { u } ) i^i v ) =/= (/) -> E. j e. ( `' g " { u } ) ( j i^i v ) =/= (/) )
199	198	adantl 473	. . . . . . . . . . . . . . . . . 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 2915	. . . . . . . . . . . . . . . . 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 441	. . . . . . . . . . . . . . . 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 3496	. . . . . . . . . . . . . . 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 7633	. . . . . . . . . . . . . . 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 64	. . . . . . . . . . . . . 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 7640	. . . . . . . . . . . . . 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 673	. . . . . . . . . . . . 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 472	. . . . . . . . . . . . . 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 5748	. . . . . . . . . . . . . . 15 |- ( g Fn V <-> g : V --> ran g )
209	208	biimpi 199	. . . . . . . . . . . . . 14 |- ( g Fn V -> g : V --> ran g )
210		ssrab2 3500	. . . . . . . . . . . . . . 15 |- { j e. V | ( j i^i v ) =/= (/) } C_ V
211		fimarab 28320	. . . . . . . . . . . . . . 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 685	. . . . . . . . . . . . . 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 18	. . . . . . . . . . . . 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 4422	. . . . . . . . . . . 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 7811	. . . . . . . . . . . 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 673	. . . . . . . . . . 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 441	. . . . . . . . . 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 707	. . . . . . . . 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 436	. . . . . . . 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 776	. . . . . . . . 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 20609	. . . . . . . . . . . 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 201	. . . . . . . . . . 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 1044	. . . . . . . . . 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 2776	. . . . . . . . 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 680	. . . . . . . 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 2854	. . . . . . 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 2809	. . . . . 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 20609	. . . . . 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 1214	. . . . 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 5608	. . . . . . . 8 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( Fun f <-> Fun ( u e. ran g |-> U. ( `' g " { u } ) ) ) )
232		dmeq 5040	. . . . . . . . 9 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> dom f = dom ( u e. ran g |-> U. ( `' g " { u } ) ) )
233	232	sseq1d 3445	. . . . . . . 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 5066	. . . . . . . . 9 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ran f = ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
235	234	sseq1d 3445	. . . . . . . 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 1365	. . . . . . 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 4405	. . . . . . . 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 2533	. . . . . . . 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 725	. . . . . . 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 725	. . . . . 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 3127	. . . . 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 1300	. . . 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 630	. . 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 1787	. 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 189   /\ wa 376   /\ w3a 1007   = wceq 1452   E.wex 1671   e. wcel 1904   =/= wne 2641   A.wral 2756   E.wrex 2757   {crab 2760   _Vcvv 3031   i^i cin 3389   C_ wss 3390   (/)c0 3722   {csn 3959   U.cuni 4190   U_ciun 4269   class class class wbr 4395   |-> cmpt 4454   `'ccnv 4838   dom cdm 4839   ran crn 4840   "cima 4842   Fun wfun 5583   Fn wfn 5584   -->wf 5585   -onto->wfo 5587   ` cfv 5589   ~<_ cdom 7585   Fincfn 7587   Topctop 19994   Refcref 20594   LocFinclocfin 20596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-reg 8125  ax-inf2 8164  ax-ac2 8911

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-om 6712  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-er 7381  df-en 7588  df-dom 7589  df-fin 7591  df-r1 8253  df-rank 8254  df-card 8391  df-ac 8565  df-top 19998  df-ref 20597  df-locfin 20599

This theorem is referenced by:  locfinref  28742