Theorem locfinreflem 28675

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 28674	. . . . 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 213	. . 3 |- ( ph -> ( U. U C_ U. V /\ E. g ( g : V --> U /\ A. v e. V v C_ ( g ` v ) ) ) )
6	5	simprd 464	. 2 |- ( ph -> E. g ( g : V --> U /\ A. v e. V v C_ ( g ` v ) ) )
7		funmpt 5637	. . . . . 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 2422	. . . . . . 7 |- ( u e. ran g |-> U. ( `' g " { u } ) ) = ( u e. ran g |-> U. ( `' g " { u } ) )
10	9	dmmptss 5350	. . . . . 6 |- dom ( u e. ran g |-> U. ( `' g " { u } ) ) C_ ran g
11		frn 5752	. . . . . . 7 |- ( g : V --> U -> ran g C_ U )
12	11	ad2antlr 731	. . . . . 6 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> ran g C_ U )
13	10, 12	syl5ss 3475	. . . . 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 20534	. . . . . . . . . 10 |- ( V e. ( LocFin ` J ) -> J e. Top )
15	2, 14	syl 17	. . . . . . . . 9 |- ( ph -> J e. Top )
16	15	ad3antrrr 734	. . . . . . . 8 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> J e. Top )
17		cnvimass 5207	. . . . . . . . . 10 |- ( `' g " { u } ) C_ dom g
18		fdm 5750	. . . . . . . . . . 11 |- ( g : V --> U -> dom g = V )
19	18	ad3antlr 735	. . . . . . . . . 10 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> dom g = V )
20	17, 19	syl5sseq 3512	. . . . . . . . 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 734	. . . . . . . . 9 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> V C_ J )
23	20, 22	sstrd 3474	. . . . . . . 8 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g ) -> ( `' g " { u } ) C_ J )
24		uniopn 19925	. . . . . . . 8 |- ( ( J e. Top /\ ( `' g " { u } ) C_ J ) -> U. ( `' g " { u } ) e. J )
25	16, 23, 24	syl2anc 665	. . . . . . 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 2836	. . . . . 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 6067	. . . . . 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 2422	. . . . . . . . . 10 |- U. V = U. V
30		eqid 2422	. . . . . . . . . 10 |- U. U = U. U
31	29, 30	refbas 20523	. . . . . . . . 9 |- ( V Ref U -> U. U = U. V )
32	1, 31	syl 17	. . . . . . . 8 |- ( ph -> U. U = U. V )
33	32	ad2antrr 730	. . . . . . 7 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> U. U = U. V )
34		nfv 1755	. . . . . . . . . . . . 13 |- F/ v ( ph /\ g : V --> U )
35		nfra1 2803	. . . . . . . . . . . . 13 |- F/ v A. v e. V v C_ ( g ` v )
36	34, 35	nfan 1988	. . . . . . . . . . . 12 |- F/ v ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) )
37		nfre1 2883	. . . . . . . . . . . 12 |- F/ v E. v e. V x e. v
38	36, 37	nfan 1988	. . . . . . . . . . 11 |- F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ E. v e. V x e. v )
39		ffn 5746	. . . . . . . . . . . . . . 15 |- ( g : V --> U -> g Fn V )
40	39	ad4antlr 737	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) /\ x e. v ) -> g Fn V )
41		simplr 760	. . . . . . . . . . . . . 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 665	. . . . . . . . . . . . 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 3483	. . . . . . . . . . . . . . 15 |- v C_ v
45	39	ad3antlr 735	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) -> g Fn V )
46		eqid 2422	. . . . . . . . . . . . . . . . 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 487	. . . . . . . . . . . . . . . . 17 |- ( ( g Fn V /\ ( v e. V /\ ( g ` v ) = ( g ` v ) ) ) -> v e. ( `' g " { ( g ` v ) } ) )
49	46, 48	mpanr2 688	. . . . . . . . . . . . . . . 16 |- ( ( g Fn V /\ v e. V ) -> v e. ( `' g " { ( g ` v ) } ) )
50	45, 49	sylancom 671	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ v e. V ) -> v e. ( `' g " { ( g ` v ) } ) )
51		ssuni 4241	. . . . . . . . . . . . . . 15 |- ( ( v C_ v /\ v e. ( `' g " { ( g ` v ) } ) ) -> v C_ U. ( `' g " { ( g ` v ) } ) )
52	44, 50, 51	sylancr 667	. . . . . . . . . . . . . 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 3464	. . . . . . . . . . . . 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 4008	. . . . . . . . . . . . . . . . 17 |- ( u = ( g ` v ) -> { u } = { ( g ` v ) } )
55	54	imaeq2d 5187	. . . . . . . . . . . . . . . 16 |- ( u = ( g ` v ) -> ( `' g " { u } ) = ( `' g " { ( g ` v ) } ) )
56	55	unieqd 4229	. . . . . . . . . . . . . . 15 |- ( u = ( g ` v ) -> U. ( `' g " { u } ) = U. ( `' g " { ( g ` v ) } ) )
57	56	eleq2d 2492	. . . . . . . . . . . . . 14 |- ( u = ( g ` v ) -> ( x e. U. ( `' g " { u } ) <-> x e. U. ( `' g " { ( g ` v ) } ) ) )
58	57	rspcev 3182	. . . . . . . . . . . . 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 665	. . . . . . . . . . . 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 723	. . . . . . . . . . 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 462	. . . . . . . . . . 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 2965	. . . . . . . . . 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 1755	. . . . . . . . . . . . . 14 |- F/ v u e. ran g
64	36, 63	nfan 1988	. . . . . . . . . . . . 13 |- F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ u e. ran g )
65		nfv 1755	. . . . . . . . . . . . 13 |- F/ v x e. U. ( `' g " { u } )
66	64, 65	nfan 1988	. . . . . . . . . . . 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 734	. . . . . . . . . . . . 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 760	. . . . . . . . . . . . 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 3465	. . . . . . . . . . . 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 462	. . . . . . . . . . . 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 462	. . . . . . . . . . . . 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 4223	. . . . . . . . . . . . 13 |- ( x e. U. ( `' g " { u } ) <-> E. v e. ( `' g " { u } ) x e. v )
73	71, 72	sylib 199	. . . . . . . . . . . 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 2892	. . . . . . . . . . 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 2966	. . . . . . . . . 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 840	. . . . . . . . 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 4223	. . . . . . . . 9 |- ( x e. U. V <-> E. v e. V x e. v )
78		eliun 4304	. . . . . . . . 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 291	. . . . . . . 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 2419	. . . . . . 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 5106	. . . . . . . 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 2467	. . . . . 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 735	. . . . . . . . 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 3083	. . . . . . . . . . 11 |- w e. _V
86	9	elrnmpt 5100	. . . . . . . . . . 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 486	. . . . . . . . 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 3526	. . . . . . . . 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 62	. . . . . . . 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 1755	. . . . . . . . . 10 |- F/ u ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) )
92		nfmpt1 4513	. . . . . . . . . . . 12 |- F/_ u ( u e. ran g |-> U. ( `' g " { u } ) )
93	92	nfrn 5096	. . . . . . . . . . 11 |- F/_ u ran ( u e. ran g |-> U. ( `' g " { u } ) )
94	93	nfcri 2573	. . . . . . . . . 10 |- F/ u w e. ran ( u e. ran g |-> U. ( `' g " { u } ) )
95	91, 94	nfan 1988	. . . . . . . . 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 462	. . . . . . . . . . 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 1755	. . . . . . . . . . . . . . . 16 |- F/ v w e. ran ( u e. ran g |-> U. ( `' g " { u } ) )
98	36, 97	nfan 1988	. . . . . . . . . . . . . . 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 1755	. . . . . . . . . . . . . . 15 |- F/ v u e. U
100	98, 99	nfan 1988	. . . . . . . . . . . . . 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 1755	. . . . . . . . . . . . . 14 |- F/ v w = U. ( `' g " { u } )
102	100, 101	nfan 1988	. . . . . . . . . . . . 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 777	. . . . . . . . . . . . . . . 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 739	. . . . . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . . . 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 460	. . . . . . . . . . . . . . . 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 2789	. . . . . . . . . . . . . . . 16 |- ( ( A. v e. V v C_ ( g ` v ) /\ v e. V ) -> v C_ ( g ` v ) )
110	103, 108, 109	syl2anc 665	. . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . 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 3500	. . . . . . . . . . . . . 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 435	. . . . . . . . . . . . 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 2822	. . . . . . . . . . . 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 4250	. . . . . . . . . . . 12 |- ( U. ( `' g " { u } ) C_ u <-> A. v e. ( `' g " { u } ) v C_ u )
116	114, 115	sylibr 215	. . . . . . . . . . 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 3498	. . . . . . . . . 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 607	. . . . . . . . 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 2891	. . . . . . . 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 2836	. . . . . 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 3083	. . . . . . . . . 10 |- g e. _V
123	122	rnex 6741	. . . . . . . . 9 |- ran g e. _V
124	123	mptex 6151	. . . . . . . 8 |- ( u e. ran g |-> U. ( `' g " { u } ) ) e. _V
125		rnexg 6739	. . . . . . . 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 2422	. . . . . . . 8 |- U. ran ( u e. ran g |-> U. ( `' g " { u } ) ) = U. ran ( u e. ran g |-> U. ( `' g " { u } ) )
128	127, 30	isref 20522	. . . . . . 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 930	. . . . 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 730	. . . . . 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 730	. . . . . . 7 |- ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) -> X = U. U )
134	133, 83	eqtrd 2463	. . . . . 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 1755	. . . . . . . . 9 |- F/ v x e. X
136	36, 135	nfan 1988	. . . . . . . 8 |- F/ v ( ( ( ph /\ g : V --> U ) /\ A. v e. V v C_ ( g ` v ) ) /\ x e. X )
137		simplr 760	. . . . . . . 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 5748	. . . . . . . . . . . . . 14 |- ( g : V --> U -> Fun g )
139	138	ad6antlr 741	. . . . . . . . . . . . 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 7876	. . . . . . . . . . . . 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 671	. . . . . . . . . . . 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 1007	. . . . . . . . . . . . . . . . . . 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 4008	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( u = k -> { u } = { k } )
144	143	imaeq2d 5187	. . . . . . . . . . . . . . . . . . . . . 22 |- ( u = k -> ( `' g " { u } ) = ( `' g " { k } ) )
145	144	unieqd 4229	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = k -> U. ( `' g " { u } ) = U. ( `' g " { k } ) )
146	122	cnvex 6754	. . . . . . . . . . . . . . . . . . . . . . 23 |- `' g e. _V
147		imaexg 6744	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( `' g e. _V -> ( `' g " { k } ) e. _V )
148	146, 147	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 |- ( `' g " { k } ) e. _V
149	148	uniex 6601	. . . . . . . . . . . . . . . . . . . . 21 |- U. ( `' g " { k } ) e. _V
150	145, 9, 149	fvmpt 5964	. . . . . . . . . . . . . . . . . . . 20 |- ( k e. ran g -> ( ( u e. ran g |-> U. ( `' g " { u } ) ) ` k ) = U. ( `' g " { k } ) )
151	150	3ad2ant2 1027	. . . . . . . . . . . . . . . . . . 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 2463	. . . . . . . . . . . . . . . . . 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 3663	. . . . . . . . . . . . . . . . 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 2697	. . . . . . . . . . . . . . . 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 6744	. . . . . . . . . . . . . . . . . . . . 21 |- ( `' g e. _V -> ( `' g " { u } ) e. _V )
157	146, 156	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- ( `' g " { u } ) e. _V
158	157	uniex 6601	. . . . . . . . . . . . . . . . . . 19 |- U. ( `' g " { u } ) e. _V
159	158, 9	fnmpti 5724	. . . . . . . . . . . . . . . . . 18 |- ( u e. ran g |-> U. ( `' g " { u } ) ) Fn ran g
160		dffn4 5816	. . . . . . . . . . . . . . . . . 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 211	. . . . . . . . . . . . . . . . 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 28139	. . . . . . . . . . . . . . 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 4008	. . . . . . . . . . . . . . . . . . . 20 |- ( k = u -> { k } = { u } )
165	164	imaeq2d 5187	. . . . . . . . . . . . . . . . . . 19 |- ( k = u -> ( `' g " { k } ) = ( `' g " { u } ) )
166	165	unieqd 4229	. . . . . . . . . . . . . . . . . 18 |- ( k = u -> U. ( `' g " { k } ) = U. ( `' g " { u } ) )
167	166	ineq1d 3663	. . . . . . . . . . . . . . . . 17 |- ( k = u -> ( U. ( `' g " { k } ) i^i v ) = ( U. ( `' g " { u } ) i^i v ) )
168	167	neeq1d 2697	. . . . . . . . . . . . . . . 16 |- ( k = u -> ( ( U. ( `' g " { k } ) i^i v ) =/= (/) <-> ( U. ( `' g " { u } ) i^i v ) =/= (/) ) )
169	168	cbvrabv 3079	. . . . . . . . . . . . . . 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 4463	. . . . . . . . . . . . . 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 4575	. . . . . . . . . . . . . . 15 |- { u e. ran g | E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u } e. _V
172		nfv 1755	. . . . . . . . . . . . . . . . . . . . 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 3006	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ j { j e. V | ( j i^i v ) =/= (/) }
174	173	nfel1 2596	. . . . . . . . . . . . . . . . . . . . 21 |- F/ j { j e. V | ( j i^i v ) =/= (/) } e. Fin
175	172, 174	nfan 1988	. . . . . . . . . . . . . . . . . . . 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 1755	. . . . . . . . . . . . . . . . . . . 20 |- F/ j u e. ran g
177	175, 176	nfan 1988	. . . . . . . . . . . . . . . . . . 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 1755	. . . . . . . . . . . . . . . . . . 19 |- F/ j ( U. ( `' g " { u } ) i^i v ) =/= (/)
179	177, 178	nfan 1988	. . . . . . . . . . . . . . . . . 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 1755	. . . . . . . . . . . . . . . . . . 19 |- F/ j ( g ` k ) = u
181	173, 180	nfrex 2885	. . . . . . . . . . . . . . . . . 18 |- F/ j E. k e. { j e. V | ( j i^i v ) =/= (/) } ( g ` k ) = u
182	39	ad5antlr 739	. . . . . . . . . . . . . . . . . . . . . . 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 738	. . . . . . . . . . . . . . . . . . . . . 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 760	. . . . . . . . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( g Fn V /\ j e. ( `' g " { u } ) ) -> ( j e. V /\ ( g ` j ) = u ) )
187	183, 184, 186	syl2anc 665	. . . . . . . . . . . . . . . . . . . . 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 460	. . . . . . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . . . . . 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 3002	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. { j e. V | ( j i^i v ) =/= (/) } <-> ( j e. V /\ ( j i^i v ) =/= (/) ) )
191	188, 189, 190	sylanbrc 668	. . . . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . . . . 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 5881	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = j -> ( g ` k ) = ( g ` j ) )
194	193	eqeq1d 2424	. . . . . . . . . . . . . . . . . . . 20 |- ( k = j -> ( ( g ` k ) = u <-> ( g ` j ) = u ) )
195	194	rspcev 3182	. . . . . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . . . . 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 28165	. . . . . . . . . . . . . . . . . . . 20 |- ( ( U. ( `' g " { u } ) i^i v ) =/= (/) <-> E. j e. ( `' g " { u } ) ( j i^i v ) =/= (/) )
198	197	biimpi 197	. . . . . . . . . . . . . . . . . . 19 |- ( ( U. ( `' g " { u } ) i^i v ) =/= (/) -> E. j e. ( `' g " { u } ) ( j i^i v ) =/= (/) )
199	198	adantl 467	. . . . . . . . . . . . . . . . . 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 2963	. . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . . 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 3542	. . . . . . . . . . . . . . 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 7625	. . . . . . . . . . . . . . 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 65	. . . . . . . . . . . . . 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 7632	. . . . . . . . . . . . . 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 665	. . . . . . . . . . . . 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 466	. . . . . . . . . . . . . 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 5753	. . . . . . . . . . . . . . 15 |- ( g Fn V <-> g : V --> ran g )
209	208	biimpi 197	. . . . . . . . . . . . . 14 |- ( g Fn V -> g : V --> ran g )
210		ssrab2 3546	. . . . . . . . . . . . . . 15 |- { j e. V | ( j i^i v ) =/= (/) } C_ V
211		fimarab 28246	. . . . . . . . . . . . . . 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 675	. . . . . . . . . . . . . 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 4450	. . . . . . . . . . . 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 7802	. . . . . . . . . . . 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 665	. . . . . . . . . . 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 435	. . . . . . . . . 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 697	. . . . . . . . 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 430	. . . . . . . 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 766	. . . . . . . . 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 20530	. . . . . . . . . . . 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 199	. . . . . . . . . . 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 1019	. . . . . . . . . 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 2791	. . . . . . . . 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 671	. . . . . . . 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 2892	. . . . . . 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 2836	. . . . . 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 20530	. . . . . 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 1189	. . . . 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 5620	. . . . . . . 8 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ( Fun f <-> Fun ( u e. ran g |-> U. ( `' g " { u } ) ) ) )
232		dmeq 5054	. . . . . . . . 9 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> dom f = dom ( u e. ran g |-> U. ( `' g " { u } ) ) )
233	232	sseq1d 3491	. . . . . . . 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 5079	. . . . . . . . 9 |- ( f = ( u e. ran g |-> U. ( `' g " { u } ) ) -> ran f = ran ( u e. ran g |-> U. ( `' g " { u } ) ) )
235	234	sseq1d 3491	. . . . . . . 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 1335	. . . . . . 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 4433	. . . . . . . 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 2491	. . . . . . . 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 715	. . . . . . 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 715	. . . . . 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 3173	. . . . 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 1272	. . . 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 622	. . 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 1772	. 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 187   /\ wa 370   /\ w3a 982   = wceq 1437   E.wex 1657   e. wcel 1872   =/= wne 2614   A.wral 2771   E.wrex 2772   {crab 2775   _Vcvv 3080   i^i cin 3435   C_ wss 3436   (/)c0 3761   {csn 3998   U.cuni 4219   U_ciun 4299   class class class wbr 4423   |-> cmpt 4482   `'ccnv 4852   dom cdm 4853   ran crn 4854   "cima 4856   Fun wfun 5595   Fn wfn 5596   -->wf 5597   -onto->wfo 5599   ` cfv 5601   ~<_ cdom 7578   Fincfn 7580   Topctop 19915   Refcref 20515   LocFinclocfin 20517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-reg 8116  ax-inf2 8155  ax-ac2 8900

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-iin 4302  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6267  df-om 6707  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-1o 7193  df-er 7374  df-en 7581  df-dom 7582  df-fin 7584  df-r1 8243  df-rank 8244  df-card 8381  df-ac 8554  df-top 19919  df-ref 20518  df-locfin 20520

This theorem is referenced by:  locfinref  28676