Theorem wessf1ornlem 37453

Description: Given a function F on a well ordered domain A there exists a subset of A such that F restricted to such subset is injective and onto the range of F (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypotheses

Ref	Expression
wessf1ornlem.f	|- ( ph -> F Fn A )
wessf1ornlem.a	|- ( ph -> A e. V )
wessf1ornlem.r	|- ( ph -> R We A )
wessf1ornlem.g	|- G = ( y e. ran F |-> ( iota_ x e. ( `' F " { y } ) A. z e. ( `' F " { y } ) -. z R x ) )

Assertion

Ref	Expression
wessf1ornlem	|- ( ph -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> ran F )

Distinct variable groups:   x, A   x, F, y, z   x, R, y, z

Allowed substitution hints:   ph( x, y, z)   A( y, z)   G( x, y, z)   V( x, y, z)

Proof of Theorem wessf1ornlem

Dummy variables t u v w a b are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnvimass 5187	. . . . . . . . 9 |- ( `' F " { u } ) C_ dom F
2	1	a1i 11	. . . . . . . 8 |- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) C_ dom F )
3		wessf1ornlem.f	. . . . . . . . . 10 |- ( ph -> F Fn A )
4		fndm 5673	. . . . . . . . . 10 |- ( F Fn A -> dom F = A )
5	3, 4	syl 17	. . . . . . . . 9 |- ( ph -> dom F = A )
6	5	adantr 467	. . . . . . . 8 |- ( ( ph /\ u e. ran F ) -> dom F = A )
7	2, 6	sseqtrd 3467	. . . . . . 7 |- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) C_ A )
8		wessf1ornlem.r	. . . . . . . . . 10 |- ( ph -> R We A )
9	8	adantr 467	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> R We A )
10	1, 5	syl5sseq 3479	. . . . . . . . . . 11 |- ( ph -> ( `' F " { u } ) C_ A )
11		wessf1ornlem.a	. . . . . . . . . . 11 |- ( ph -> A e. V )
12		ssexg 4548	. . . . . . . . . . 11 |- ( ( ( `' F " { u } ) C_ A /\ A e. V ) -> ( `' F " { u } ) e. _V )
13	10, 11, 12	syl2anc 666	. . . . . . . . . 10 |- ( ph -> ( `' F " { u } ) e. _V )
14	13	adantr 467	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) e. _V )
15		inisegn0 5199	. . . . . . . . . . 11 |- ( u e. ran F <-> ( `' F " { u } ) =/= (/) )
16	15	biimpi 198	. . . . . . . . . 10 |- ( u e. ran F -> ( `' F " { u } ) =/= (/) )
17	16	adantl 468	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) =/= (/) )
18		wereu 4829	. . . . . . . . 9 |- ( ( R We A /\ ( ( `' F " { u } ) e. _V /\ ( `' F " { u } ) C_ A /\ ( `' F " { u } ) =/= (/) ) ) -> E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
19	9, 14, 7, 17, 18	syl13anc 1269	. . . . . . . 8 |- ( ( ph /\ u e. ran F ) -> E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
20		riotacl 6264	. . . . . . . 8 |- ( E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. ( `' F " { u } ) )
21	19, 20	syl 17	. . . . . . 7 |- ( ( ph /\ u e. ran F ) -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. ( `' F " { u } ) )
22	7, 21	sseldd 3432	. . . . . 6 |- ( ( ph /\ u e. ran F ) -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. A )
23	22	ralrimiva 2801	. . . . 5 |- ( ph -> A. u e. ran F ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. A )
24		wessf1ornlem.g	. . . . . . 7 |- G = ( y e. ran F |-> ( iota_ x e. ( `' F " { y } ) A. z e. ( `' F " { y } ) -. z R x ) )
25		sneq 3977	. . . . . . . . . . 11 |- ( y = u -> { y } = { u } )
26	25	imaeq2d 5167	. . . . . . . . . 10 |- ( y = u -> ( `' F " { y } ) = ( `' F " { u } ) )
27	26	raleqdv 2992	. . . . . . . . . 10 |- ( y = u -> ( A. z e. ( `' F " { y } ) -. z R x <-> A. z e. ( `' F " { u } ) -. z R x ) )
28	26, 27	riotaeqbidv 6253	. . . . . . . . 9 |- ( y = u -> ( iota_ x e. ( `' F " { y } ) A. z e. ( `' F " { y } ) -. z R x ) = ( iota_ x e. ( `' F " { u } ) A. z e. ( `' F " { u } ) -. z R x ) )
29		breq1 4404	. . . . . . . . . . . . . . 15 |- ( z = t -> ( z R x <-> t R x ) )
30	29	notbid 296	. . . . . . . . . . . . . 14 |- ( z = t -> ( -. z R x <-> -. t R x ) )
31	30	cbvralv 3018	. . . . . . . . . . . . 13 |- ( A. z e. ( `' F " { u } ) -. z R x <-> A. t e. ( `' F " { u } ) -. t R x )
32	31	a1i 11	. . . . . . . . . . . 12 |- ( x = v -> ( A. z e. ( `' F " { u } ) -. z R x <-> A. t e. ( `' F " { u } ) -. t R x ) )
33		breq2 4405	. . . . . . . . . . . . . 14 |- ( x = v -> ( t R x <-> t R v ) )
34	33	notbid 296	. . . . . . . . . . . . 13 |- ( x = v -> ( -. t R x <-> -. t R v ) )
35	34	ralbidv 2826	. . . . . . . . . . . 12 |- ( x = v -> ( A. t e. ( `' F " { u } ) -. t R x <-> A. t e. ( `' F " { u } ) -. t R v ) )
36	32, 35	bitrd 257	. . . . . . . . . . 11 |- ( x = v -> ( A. z e. ( `' F " { u } ) -. z R x <-> A. t e. ( `' F " { u } ) -. t R v ) )
37	36	cbvriotav 6261	. . . . . . . . . 10 |- ( iota_ x e. ( `' F " { u } ) A. z e. ( `' F " { u } ) -. z R x ) = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
38	37	a1i 11	. . . . . . . . 9 |- ( y = u -> ( iota_ x e. ( `' F " { u } ) A. z e. ( `' F " { u } ) -. z R x ) = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
39	28, 38	eqtrd 2484	. . . . . . . 8 |- ( y = u -> ( iota_ x e. ( `' F " { y } ) A. z e. ( `' F " { y } ) -. z R x ) = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
40	39	cbvmptv 4494	. . . . . . 7 |- ( y e. ran F |-> ( iota_ x e. ( `' F " { y } ) A. z e. ( `' F " { y } ) -. z R x ) ) = ( u e. ran F |-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
41	24, 40	eqtri 2472	. . . . . 6 |- G = ( u e. ran F |-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
42	41	rnmptss 6050	. . . . 5 |- ( A. u e. ran F ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. A -> ran G C_ A )
43	23, 42	syl 17	. . . 4 |- ( ph -> ran G C_ A )
44	11, 43	ssexd 4549	. . . . 5 |- ( ph -> ran G e. _V )
45		elpwg 3958	. . . . 5 |- ( ran G e. _V -> ( ran G e. ~P A <-> ran G C_ A ) )
46	44, 45	syl 17	. . . 4 |- ( ph -> ( ran G e. ~P A <-> ran G C_ A ) )
47	43, 46	mpbird 236	. . 3 |- ( ph -> ran G e. ~P A )
48		dffn3 5734	. . . . . . . . . 10 |- ( F Fn A <-> F : A --> ran F )
49	48	biimpi 198	. . . . . . . . 9 |- ( F Fn A -> F : A --> ran F )
50	3, 49	syl 17	. . . . . . . 8 |- ( ph -> F : A --> ran F )
51	50, 43	fssresd 5748	. . . . . . 7 |- ( ph -> ( F |` ran G ) : ran G --> ran F )
52		simpl 459	. . . . . . . . 9 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> ph )
53		simprl 763	. . . . . . . . 9 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> w e. ran G )
54		simprr 765	. . . . . . . . 9 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> t e. ran G )
55		simpl 459	. . . . . . . . . . 11 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( ph /\ w e. ran G /\ t e. ran G ) )
56		fvres 5877	. . . . . . . . . . . . . . 15 |- ( w e. ran G -> ( ( F |` ran G ) ` w ) = ( F ` w ) )
57	56	eqcomd 2456	. . . . . . . . . . . . . 14 |- ( w e. ran G -> ( F ` w ) = ( ( F |` ran G ) ` w ) )
58	57	ad2antrr 731	. . . . . . . . . . . . 13 |- ( ( ( w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( F ` w ) = ( ( F |` ran G ) ` w ) )
59		simpr 463	. . . . . . . . . . . . 13 |- ( ( ( w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) )
60		fvres 5877	. . . . . . . . . . . . . 14 |- ( t e. ran G -> ( ( F |` ran G ) ` t ) = ( F ` t ) )
61	60	ad2antlr 732	. . . . . . . . . . . . 13 |- ( ( ( w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( ( F |` ran G ) ` t ) = ( F ` t ) )
62	58, 59, 61	3eqtrd 2488	. . . . . . . . . . . 12 |- ( ( ( w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( F ` w ) = ( F ` t ) )
63	62	3adantl1 1163	. . . . . . . . . . 11 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( F ` w ) = ( F ` t ) )
64		simpl1 1010	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ph )
65		simpl3 1012	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> t e. ran G )
66		vex 3047	. . . . . . . . . . . . . . . . . . 19 |- w e. _V
67	41	elrnmpt 5080	. . . . . . . . . . . . . . . . . . 19 |- ( w e. _V -> ( w e. ran G <-> E. u e. ran F w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) )
68	66, 67	ax-mp 5	. . . . . . . . . . . . . . . . . 18 |- ( w e. ran G <-> E. u e. ran F w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
69	68	biimpi 198	. . . . . . . . . . . . . . . . 17 |- ( w e. ran G -> E. u e. ran F w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
70	69	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( w e. ran G /\ ( F ` w ) = ( F ` t ) ) -> E. u e. ran F w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
71	70	3ad2antl2 1170	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> E. u e. ran F w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
72	71, 68	sylibr 216	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w e. ran G )
73		id 22	. . . . . . . . . . . . . . . 16 |- ( ( F ` w ) = ( F ` t ) -> ( F ` w ) = ( F ` t ) )
74	73	eqcomd 2456	. . . . . . . . . . . . . . 15 |- ( ( F ` w ) = ( F ` t ) -> ( F ` t ) = ( F ` w ) )
75	74	adantl 468	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( F ` t ) = ( F ` w ) )
76		eleq1 2516	. . . . . . . . . . . . . . . . . 18 |- ( b = w -> ( b e. ran G <-> w e. ran G ) )
77	76	3anbi3d 1344	. . . . . . . . . . . . . . . . 17 |- ( b = w -> ( ( ph /\ t e. ran G /\ b e. ran G ) <-> ( ph /\ t e. ran G /\ w e. ran G ) ) )
78		fveq2 5863	. . . . . . . . . . . . . . . . . 18 |- ( b = w -> ( F ` b ) = ( F ` w ) )
79	78	eqeq2d 2460	. . . . . . . . . . . . . . . . 17 |- ( b = w -> ( ( F ` t ) = ( F ` b ) <-> ( F ` t ) = ( F ` w ) ) )
80	77, 79	anbi12d 716	. . . . . . . . . . . . . . . 16 |- ( b = w -> ( ( ( ph /\ t e. ran G /\ b e. ran G ) /\ ( F ` t ) = ( F ` b ) ) <-> ( ( ph /\ t e. ran G /\ w e. ran G ) /\ ( F ` t ) = ( F ` w ) ) ) )
81		breq1 4404	. . . . . . . . . . . . . . . . 17 |- ( b = w -> ( b R t <-> w R t ) )
82	81	notbid 296	. . . . . . . . . . . . . . . 16 |- ( b = w -> ( -. b R t <-> -. w R t ) )
83	80, 82	imbi12d 322	. . . . . . . . . . . . . . 15 |- ( b = w -> ( ( ( ( ph /\ t e. ran G /\ b e. ran G ) /\ ( F ` t ) = ( F ` b ) ) -> -. b R t ) <-> ( ( ( ph /\ t e. ran G /\ w e. ran G ) /\ ( F ` t ) = ( F ` w ) ) -> -. w R t ) ) )
84		eleq1 2516	. . . . . . . . . . . . . . . . . . 19 |- ( a = t -> ( a e. ran G <-> t e. ran G ) )
85	84	3anbi2d 1343	. . . . . . . . . . . . . . . . . 18 |- ( a = t -> ( ( ph /\ a e. ran G /\ b e. ran G ) <-> ( ph /\ t e. ran G /\ b e. ran G ) ) )
86		fveq2 5863	. . . . . . . . . . . . . . . . . . 19 |- ( a = t -> ( F ` a ) = ( F ` t ) )
87	86	eqeq1d 2452	. . . . . . . . . . . . . . . . . 18 |- ( a = t -> ( ( F ` a ) = ( F ` b ) <-> ( F ` t ) = ( F ` b ) ) )
88	85, 87	anbi12d 716	. . . . . . . . . . . . . . . . 17 |- ( a = t -> ( ( ( ph /\ a e. ran G /\ b e. ran G ) /\ ( F ` a ) = ( F ` b ) ) <-> ( ( ph /\ t e. ran G /\ b e. ran G ) /\ ( F ` t ) = ( F ` b ) ) ) )
89		breq2 4405	. . . . . . . . . . . . . . . . . 18 |- ( a = t -> ( b R a <-> b R t ) )
90	89	notbid 296	. . . . . . . . . . . . . . . . 17 |- ( a = t -> ( -. b R a <-> -. b R t ) )
91	88, 90	imbi12d 322	. . . . . . . . . . . . . . . 16 |- ( a = t -> ( ( ( ( ph /\ a e. ran G /\ b e. ran G ) /\ ( F ` a ) = ( F ` b ) ) -> -. b R a ) <-> ( ( ( ph /\ t e. ran G /\ b e. ran G ) /\ ( F ` t ) = ( F ` b ) ) -> -. b R t ) ) )
92		eleq1 2516	. . . . . . . . . . . . . . . . . . . 20 |- ( t = b -> ( t e. ran G <-> b e. ran G ) )
93	92	3anbi3d 1344	. . . . . . . . . . . . . . . . . . 19 |- ( t = b -> ( ( ph /\ a e. ran G /\ t e. ran G ) <-> ( ph /\ a e. ran G /\ b e. ran G ) ) )
94		fveq2 5863	. . . . . . . . . . . . . . . . . . . 20 |- ( t = b -> ( F ` t ) = ( F ` b ) )
95	94	eqeq2d 2460	. . . . . . . . . . . . . . . . . . 19 |- ( t = b -> ( ( F ` a ) = ( F ` t ) <-> ( F ` a ) = ( F ` b ) ) )
96	93, 95	anbi12d 716	. . . . . . . . . . . . . . . . . 18 |- ( t = b -> ( ( ( ph /\ a e. ran G /\ t e. ran G ) /\ ( F ` a ) = ( F ` t ) ) <-> ( ( ph /\ a e. ran G /\ b e. ran G ) /\ ( F ` a ) = ( F ` b ) ) ) )
97		breq1 4404	. . . . . . . . . . . . . . . . . . 19 |- ( t = b -> ( t R a <-> b R a ) )
98	97	notbid 296	. . . . . . . . . . . . . . . . . 18 |- ( t = b -> ( -. t R a <-> -. b R a ) )
99	96, 98	imbi12d 322	. . . . . . . . . . . . . . . . 17 |- ( t = b -> ( ( ( ( ph /\ a e. ran G /\ t e. ran G ) /\ ( F ` a ) = ( F ` t ) ) -> -. t R a ) <-> ( ( ( ph /\ a e. ran G /\ b e. ran G ) /\ ( F ` a ) = ( F ` b ) ) -> -. b R a ) ) )
100		eleq1 2516	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = a -> ( w e. ran G <-> a e. ran G ) )
101	100	3anbi2d 1343	. . . . . . . . . . . . . . . . . . . 20 |- ( w = a -> ( ( ph /\ w e. ran G /\ t e. ran G ) <-> ( ph /\ a e. ran G /\ t e. ran G ) ) )
102		fveq2 5863	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = a -> ( F ` w ) = ( F ` a ) )
103	102	eqeq1d 2452	. . . . . . . . . . . . . . . . . . . 20 |- ( w = a -> ( ( F ` w ) = ( F ` t ) <-> ( F ` a ) = ( F ` t ) ) )
104	101, 103	anbi12d 716	. . . . . . . . . . . . . . . . . . 19 |- ( w = a -> ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) <-> ( ( ph /\ a e. ran G /\ t e. ran G ) /\ ( F ` a ) = ( F ` t ) ) ) )
105		breq2 4405	. . . . . . . . . . . . . . . . . . . 20 |- ( w = a -> ( t R w <-> t R a ) )
106	105	notbid 296	. . . . . . . . . . . . . . . . . . 19 |- ( w = a -> ( -. t R w <-> -. t R a ) )
107	104, 106	imbi12d 322	. . . . . . . . . . . . . . . . . 18 |- ( w = a -> ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> -. t R w ) <-> ( ( ( ph /\ a e. ran G /\ t e. ran G ) /\ ( F ` a ) = ( F ` t ) ) -> -. t R a ) ) )
108		nfv 1760	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ u ph
109		nfcv 2591	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ u w
110		nfmpt1 4491	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/_ u ( u e. ran F |-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
111	41, 110	nfcxfr 2589	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ u G
112	111	nfrn 5076	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ u ran G
113	109, 112	nfel 2603	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ u w e. ran G
114	112	nfcri 2585	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ u t e. ran G
115	108, 113, 114	nf3an 2012	. . . . . . . . . . . . . . . . . . . . 21 |- F/ u ( ph /\ w e. ran G /\ t e. ran G )
116		nfv 1760	. . . . . . . . . . . . . . . . . . . . 21 |- F/ u ( F ` w ) = ( F ` t )
117	115, 116	nfan 2010	. . . . . . . . . . . . . . . . . . . 20 |- F/ u ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) )
118		nfv 1760	. . . . . . . . . . . . . . . . . . . 20 |- F/ u -. t R w
119		simp3 1009	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
120	119	eqcomd 2456	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) = w )
121		simp11 1037	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ph )
122		simp2 1008	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> u e. ran F )
123		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) -> w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
124		breq2 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( v = w -> ( t R v <-> t R w ) )
125	124	notbid 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( v = w -> ( -. t R v <-> -. t R w ) )
126	125	ralbidv 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( v = w -> ( A. t e. ( `' F " { u } ) -. t R v <-> A. t e. ( `' F " { u } ) -. t R w ) )
127	126	cbvriotav 6261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) = ( iota_ w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w )
128	127	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) = ( iota_ w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w ) )
129	123, 128	eqtr2d 2485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) -> ( iota_ w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w ) = w )
130	129	3ad2ant3 1030	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( iota_ w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w ) = w )
131	126	cbvreuv 3020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v <-> E! w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w )
132	19, 131	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ u e. ran F ) -> E! w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w )
133		riota1 6268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( E! w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w -> ( ( w e. ( `' F " { u } ) /\ A. t e. ( `' F " { u } ) -. t R w ) <-> ( iota_ w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w ) = w ) )
134	132, 133	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ u e. ran F ) -> ( ( w e. ( `' F " { u } ) /\ A. t e. ( `' F " { u } ) -. t R w ) <-> ( iota_ w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w ) = w ) )
135	134	3adant3 1027	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( ( w e. ( `' F " { u } ) /\ A. t e. ( `' F " { u } ) -. t R w ) <-> ( iota_ w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w ) = w ) )
136	130, 135	mpbird 236	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( w e. ( `' F " { u } ) /\ A. t e. ( `' F " { u } ) -. t R w ) )
137	136	simpld 461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> w e. ( `' F " { u } ) )
138	121, 122, 119, 137	syl3anc 1267	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> w e. ( `' F " { u } ) )
139	121, 122, 19	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
140	126	riota2 6272	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( w e. ( `' F " { u } ) /\ E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) -> ( A. t e. ( `' F " { u } ) -. t R w <-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) = w ) )
141	138, 139, 140	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( A. t e. ( `' F " { u } ) -. t R w <-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) = w ) )
142	120, 141	mpbird 236	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> A. t e. ( `' F " { u } ) -. t R w )
143	142	3adant1r 1260	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> A. t e. ( `' F " { u } ) -. t R w )
144	43	sselda 3431	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ t e. ran G ) -> t e. A )
145	144	3adant2 1026	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ w e. ran G /\ t e. ran G ) -> t e. A )
146	145	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> t e. A )
147	146	3ad2ant1 1028	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> t e. A )
148	74	ad2antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F ) -> ( F ` t ) = ( F ` w ) )
149	148	3adant3 1027	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( F ` t ) = ( F ` w ) )
150		fniniseg 6001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( F Fn A -> ( w e. ( `' F " { u } ) <-> ( w e. A /\ ( F ` w ) = u ) ) )
151	121, 3, 150	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( w e. ( `' F " { u } ) <-> ( w e. A /\ ( F ` w ) = u ) ) )
152	138, 151	mpbid 214	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( w e. A /\ ( F ` w ) = u ) )
153	152	simprd 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( F ` w ) = u )
154	153	3adant1r 1260	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( F ` w ) = u )
155	149, 154	eqtrd 2484	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( F ` t ) = u )
156	147, 155	jca 535	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( t e. A /\ ( F ` t ) = u ) )
157		fniniseg 6001	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( F Fn A -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
158	3, 157	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
159	158	3ad2ant1 1028	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ w e. ran G /\ t e. ran G ) -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
160	159	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F ) -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
161	160	3adant3 1027	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
162	156, 161	mpbird 236	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> t e. ( `' F " { u } ) )
163		rspa 2754	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A. t e. ( `' F " { u } ) -. t R w /\ t e. ( `' F " { u } ) ) -> -. t R w )
164	143, 162, 163	syl2anc 666	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> -. t R w )
165	164	3exp 1206	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( u e. ran F -> ( w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) -> -. t R w ) ) )
166	117, 118, 165	rexlimd 2870	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( E. u e. ran F w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) -> -. t R w ) )
167	71, 166	mpd 15	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> -. t R w )
168	107, 167	chvarv 2106	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ a e. ran G /\ t e. ran G ) /\ ( F ` a ) = ( F ` t ) ) -> -. t R a )
169	99, 168	chvarv 2106	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ a e. ran G /\ b e. ran G ) /\ ( F ` a ) = ( F ` b ) ) -> -. b R a )
170	91, 169	chvarv 2106	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ t e. ran G /\ b e. ran G ) /\ ( F ` t ) = ( F ` b ) ) -> -. b R t )
171	83, 170	chvarv 2106	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ t e. ran G /\ w e. ran G ) /\ ( F ` t ) = ( F ` w ) ) -> -. w R t )
172	64, 65, 72, 75, 171	syl31anc 1270	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> -. w R t )
173	172, 167	jca 535	. . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( -. w R t /\ -. t R w ) )
174		weso 4824	. . . . . . . . . . . . . . . 16 |- ( R We A -> R Or A )
175	8, 174	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> R Or A )
176	175	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( F ` w ) = ( F ` t ) ) -> R Or A )
177	176	3ad2antl1 1169	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> R Or A )
178	43	sselda 3431	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w e. ran G ) -> w e. A )
179	178	3adant3 1027	. . . . . . . . . . . . . 14 |- ( ( ph /\ w e. ran G /\ t e. ran G ) -> w e. A )
180	179	adantr 467	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w e. A )
181		sotrieq2 4782	. . . . . . . . . . . . 13 |- ( ( R Or A /\ ( w e. A /\ t e. A ) ) -> ( w = t <-> ( -. w R t /\ -. t R w ) ) )
182	177, 180, 146, 181	syl12anc 1265	. . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( w = t <-> ( -. w R t /\ -. t R w ) ) )
183	173, 182	mpbird 236	. . . . . . . . . . 11 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w = t )
184	55, 63, 183	syl2anc 666	. . . . . . . . . 10 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> w = t )
185	184	ex 436	. . . . . . . . 9 |- ( ( ph /\ w e. ran G /\ t e. ran G ) -> ( ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) -> w = t ) )
186	52, 53, 54, 185	syl3anc 1267	. . . . . . . 8 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> ( ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) -> w = t ) )
187	186	ralrimivva 2808	. . . . . . 7 |- ( ph -> A. w e. ran G A. t e. ran G ( ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) -> w = t ) )
188	51, 187	jca 535	. . . . . 6 |- ( ph -> ( ( F |` ran G ) : ran G --> ran F /\ A. w e. ran G A. t e. ran G ( ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) -> w = t ) ) )
189		dff13 6157	. . . . . 6 |- ( ( F |` ran G ) : ran G -1-1-> ran F <-> ( ( F |` ran G ) : ran G --> ran F /\ A. w e. ran G A. t e. ran G ( ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) -> w = t ) ) )
190	188, 189	sylibr 216	. . . . 5 |- ( ph -> ( F |` ran G ) : ran G -1-1-> ran F )
191		riotaex 6254	. . . . . . . . . . . . . 14 |- ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V
192	191	rgenw 2748	. . . . . . . . . . . . 13 |- A. u e. ran F ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V
193	192	a1i 11	. . . . . . . . . . . 12 |- ( ph -> A. u e. ran F ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V )
194	41	fnmpt 5702	. . . . . . . . . . . 12 |- ( A. u e. ran F ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V -> G Fn ran F )
195	193, 194	syl 17	. . . . . . . . . . 11 |- ( ph -> G Fn ran F )
196		dffn3 5734	. . . . . . . . . . . 12 |- ( G Fn ran F <-> G : ran F --> ran G )
197	196	biimpi 198	. . . . . . . . . . 11 |- ( G Fn ran F -> G : ran F --> ran G )
198	195, 197	syl 17	. . . . . . . . . 10 |- ( ph -> G : ran F --> ran G )
199	198	ffvelrnda 6020	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> ( G ` u ) e. ran G )
200		fvres 5877	. . . . . . . . . . 11 |- ( ( G ` u ) e. ran G -> ( ( F |` ran G ) ` ( G ` u ) ) = ( F ` ( G ` u ) ) )
201	199, 200	syl 17	. . . . . . . . . 10 |- ( ( ph /\ u e. ran F ) -> ( ( F |` ran G ) ` ( G ` u ) ) = ( F ` ( G ` u ) ) )
202	17, 15	sylibr 216	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ran F ) -> u e. ran F )
203	191	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ran F ) -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V )
204	41	fvmpt2 5955	. . . . . . . . . . . . . 14 |- ( ( u e. ran F /\ ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V ) -> ( G ` u ) = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
205	202, 203, 204	syl2anc 666	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ran F ) -> ( G ` u ) = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
206	205, 21	eqeltrd 2528	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ran F ) -> ( G ` u ) e. ( `' F " { u } ) )
207		fvex 5873	. . . . . . . . . . . . . 14 |- ( G ` u ) e. _V
208		eleq1 2516	. . . . . . . . . . . . . . . 16 |- ( w = ( G ` u ) -> ( w e. ( `' F " { u } ) <-> ( G ` u ) e. ( `' F " { u } ) ) )
209		eleq1 2516	. . . . . . . . . . . . . . . . 17 |- ( w = ( G ` u ) -> ( w e. A <-> ( G ` u ) e. A ) )
210		fveq2 5863	. . . . . . . . . . . . . . . . . 18 |- ( w = ( G ` u ) -> ( F ` w ) = ( F ` ( G ` u ) ) )
211	210	eqeq1d 2452	. . . . . . . . . . . . . . . . 17 |- ( w = ( G ` u ) -> ( ( F ` w ) = u <-> ( F ` ( G ` u ) ) = u ) )
212	209, 211	anbi12d 716	. . . . . . . . . . . . . . . 16 |- ( w = ( G ` u ) -> ( ( w e. A /\ ( F ` w ) = u ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
213	208, 212	bibi12d 323	. . . . . . . . . . . . . . 15 |- ( w = ( G ` u ) -> ( ( w e. ( `' F " { u } ) <-> ( w e. A /\ ( F ` w ) = u ) ) <-> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) ) )
214	213	imbi2d 318	. . . . . . . . . . . . . 14 |- ( w = ( G ` u ) -> ( ( ph -> ( w e. ( `' F " { u } ) <-> ( w e. A /\ ( F ` w ) = u ) ) ) <-> ( ph -> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) ) ) )
215	3, 150	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ( w e. ( `' F " { u } ) <-> ( w e. A /\ ( F ` w ) = u ) ) )
216	207, 214, 215	vtocl 3099	. . . . . . . . . . . . 13 |- ( ph -> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
217	216	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ran F ) -> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
218	206, 217	mpbid 214	. . . . . . . . . . 11 |- ( ( ph /\ u e. ran F ) -> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) )
219	218	simprd 465	. . . . . . . . . 10 |- ( ( ph /\ u e. ran F ) -> ( F ` ( G ` u ) ) = u )
220	201, 219	eqtr2d 2485	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> u = ( ( F |` ran G ) ` ( G ` u ) ) )
221		fveq2 5863	. . . . . . . . . . 11 |- ( w = ( G ` u ) -> ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` ( G ` u ) ) )
222	221	eqeq2d 2460	. . . . . . . . . 10 |- ( w = ( G ` u ) -> ( u = ( ( F |` ran G ) ` w ) <-> u = ( ( F |` ran G ) ` ( G ` u ) ) ) )
223	222	rspcev 3149	. . . . . . . . 9 |- ( ( ( G ` u ) e. ran G /\ u = ( ( F |` ran G ) ` ( G ` u ) ) ) -> E. w e. ran G u = ( ( F |` ran G ) ` w ) )
224	199, 220, 223	syl2anc 666	. . . . . . . 8 |- ( ( ph /\ u e. ran F ) -> E. w e. ran G u = ( ( F |` ran G ) ` w ) )
225	224	ralrimiva 2801	. . . . . . 7 |- ( ph -> A. u e. ran F E. w e. ran G u = ( ( F |` ran G ) ` w ) )
226	51, 225	jca 535	. . . . . 6 |- ( ph -> ( ( F |` ran G ) : ran G --> ran F /\ A. u e. ran F E. w e. ran G u = ( ( F |` ran G ) ` w ) ) )
227		dffo3 6035	. . . . . 6 |- ( ( F |` ran G ) : ran G -onto-> ran F <-> ( ( F |` ran G ) : ran G --> ran F /\ A. u e. ran F E. w e. ran G u = ( ( F |` ran G ) ` w ) ) )
228	226, 227	sylibr 216	. . . . 5 |- ( ph -> ( F |` ran G ) : ran G -onto-> ran F )
229	190, 228	jca 535	. . . 4 |- ( ph -> ( ( F |` ran G ) : ran G -1-1-> ran F /\ ( F |` ran G ) : ran G -onto-> ran F ) )
230		df-f1o 5588	. . . 4 |- ( ( F |` ran G ) : ran G -1-1-onto-> ran F <-> ( ( F |` ran G ) : ran G -1-1-> ran F /\ ( F |` ran G ) : ran G -onto-> ran F ) )
231	229, 230	sylibr 216	. . 3 |- ( ph -> ( F |` ran G ) : ran G -1-1-onto-> ran F )
232		nfcv 2591	. . . . . 6 |- F/_ v F
233		nfcv 2591	. . . . . . . . 9 |- F/_ v ran F
234		nfriota1 6257	. . . . . . . . 9 |- F/_ v ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
235	233, 234	nfmpt 4490	. . . . . . . 8 |- F/_ v ( u e. ran F |-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
236	41, 235	nfcxfr 2589	. . . . . . 7 |- F/_ v G
237	236	nfrn 5076	. . . . . 6 |- F/_ v ran G
238	232, 237	nfres 5106	. . . . 5 |- F/_ v ( F |` ran G )
239	238, 237, 233	nff1o 5810	. . . 4 |- F/ v ( F |` ran G ) : ran G -1-1-onto-> ran F
240		reseq2 5099	. . . . 5 |- ( v = ran G -> ( F |` v ) = ( F |` ran G ) )
241		id 22	. . . . 5 |- ( v = ran G -> v = ran G )
242		eqidd 2451	. . . . 5 |- ( v = ran G -> ran F = ran F )
243	240, 241, 242	f1oeq123d 5809	. . . 4 |- ( v = ran G -> ( ( F |` v ) : v -1-1-onto-> ran F <-> ( F |` ran G ) : ran G -1-1-onto-> ran F ) )
244	239, 243	rspce 3144	. . 3 |- ( ( ran G e. ~P A /\ ( F |` ran G ) : ran G -1-1-onto-> ran F ) -> E. v e. ~P A ( F |` v ) : v -1-1-onto-> ran F )
245	47, 231, 244	syl2anc 666	. 2 |- ( ph -> E. v e. ~P A ( F |` v ) : v -1-1-onto-> ran F )
246		reseq2 5099	. . . 4 |- ( v = x -> ( F |` v ) = ( F |` x ) )
247		id 22	. . . 4 |- ( v = x -> v = x )
248		eqidd 2451	. . . 4 |- ( v = x -> ran F = ran F )
249	246, 247, 248	f1oeq123d 5809	. . 3 |- ( v = x -> ( ( F |` v ) : v -1-1-onto-> ran F <-> ( F |` x ) : x -1-1-onto-> ran F ) )
250	249	cbvrexv 3019	. 2 |- ( E. v e. ~P A ( F |` v ) : v -1-1-onto-> ran F <-> E. x e. ~P A ( F |` x ) : x -1-1-onto-> ran F )
251	245, 250	sylib 200	1 |- ( ph -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> ran F )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   /\ wa 371   /\ w3a 984   = wceq 1443   e. wcel 1886   =/= wne 2621   A.wral 2736   E.wrex 2737   E!wreu 2738   _Vcvv 3044   C_ wss 3403   (/)c0 3730   ~Pcpw 3950   {csn 3967   class class class wbr 4401   |-> cmpt 4460   Or wor 4753   We wwe 4791   `'ccnv 4832   dom cdm 4833   ran crn 4834   |` cres 4835   "cima 4836   Fn wfn 5576   -->wf 5577   -1-1->wf1 5578   -onto->wfo 5579   -1-1-onto->wf1o 5580   ` cfv 5581   iota_crio 6249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250

This theorem is referenced by:  wessf1orn  37454