Theorem wessf1ornlem 39371

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 5485	. . . . . . . . 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 5990	. . . . . . . . . 10 |- ( F Fn A -> dom F = A )
5	3, 4	syl 17	. . . . . . . . 9 |- ( ph -> dom F = A )
6	5	adantr 481	. . . . . . . 8 |- ( ( ph /\ u e. ran F ) -> dom F = A )
7	2, 6	sseqtrd 3641	. . . . . . 7 |- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) C_ A )
8		wessf1ornlem.r	. . . . . . . . . 10 |- ( ph -> R We A )
9	8	adantr 481	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> R We A )
10	1, 5	syl5sseq 3653	. . . . . . . . . . 11 |- ( ph -> ( `' F " { u } ) C_ A )
11		wessf1ornlem.a	. . . . . . . . . . 11 |- ( ph -> A e. V )
12		ssexg 4804	. . . . . . . . . . 11 |- ( ( ( `' F " { u } ) C_ A /\ A e. V ) -> ( `' F " { u } ) e. _V )
13	10, 11, 12	syl2anc 693	. . . . . . . . . 10 |- ( ph -> ( `' F " { u } ) e. _V )
14	13	adantr 481	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) e. _V )
15		inisegn0 5497	. . . . . . . . . . 11 |- ( u e. ran F <-> ( `' F " { u } ) =/= (/) )
16	15	biimpi 206	. . . . . . . . . 10 |- ( u e. ran F -> ( `' F " { u } ) =/= (/) )
17	16	adantl 482	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) =/= (/) )
18		wereu 5110	. . . . . . . . 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 1328	. . . . . . . 8 |- ( ( ph /\ u e. ran F ) -> E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
20		riotacl 6625	. . . . . . . 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 3604	. . . . . 6 |- ( ( ph /\ u e. ran F ) -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. A )
23	22	ralrimiva 2966	. . . . 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 4187	. . . . . . . . . . 11 |- ( y = u -> { y } = { u } )
26	25	imaeq2d 5466	. . . . . . . . . 10 |- ( y = u -> ( `' F " { y } ) = ( `' F " { u } ) )
27	26	raleqdv 3144	. . . . . . . . . 10 |- ( y = u -> ( A. z e. ( `' F " { y } ) -. z R x <-> A. z e. ( `' F " { u } ) -. z R x ) )
28	26, 27	riotaeqbidv 6614	. . . . . . . . 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 4656	. . . . . . . . . . . . . . 15 |- ( z = t -> ( z R x <-> t R x ) )
30	29	notbid 308	. . . . . . . . . . . . . 14 |- ( z = t -> ( -. z R x <-> -. t R x ) )
31	30	cbvralv 3171	. . . . . . . . . . . . 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 4657	. . . . . . . . . . . . . 14 |- ( x = v -> ( t R x <-> t R v ) )
34	33	notbid 308	. . . . . . . . . . . . 13 |- ( x = v -> ( -. t R x <-> -. t R v ) )
35	34	ralbidv 2986	. . . . . . . . . . . 12 |- ( x = v -> ( A. t e. ( `' F " { u } ) -. t R x <-> A. t e. ( `' F " { u } ) -. t R v ) )
36	32, 35	bitrd 268	. . . . . . . . . . 11 |- ( x = v -> ( A. z e. ( `' F " { u } ) -. z R x <-> A. t e. ( `' F " { u } ) -. t R v ) )
37	36	cbvriotav 6622	. . . . . . . . . 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 2656	. . . . . . . 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 4750	. . . . . . 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 2644	. . . . . 6 |- G = ( u e. ran F |-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
42	41	rnmptss 6392	. . . . 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 4805	. . . . 5 |- ( ph -> ran G e. _V )
45		elpwg 4166	. . . . 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 247	. . 3 |- ( ph -> ran G e. ~P A )
48		dffn3 6054	. . . . . . . . . 10 |- ( F Fn A <-> F : A --> ran F )
49	48	biimpi 206	. . . . . . . . 9 |- ( F Fn A -> F : A --> ran F )
50	3, 49	syl 17	. . . . . . . 8 |- ( ph -> F : A --> ran F )
51	50, 43	fssresd 6071	. . . . . . 7 |- ( ph -> ( F |` ran G ) : ran G --> ran F )
52		simpl 473	. . . . . . . . 9 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> ph )
53		simprl 794	. . . . . . . . 9 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> w e. ran G )
54		simprr 796	. . . . . . . . 9 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> t e. ran G )
55		simpl 473	. . . . . . . . . . 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 6207	. . . . . . . . . . . . . . 15 |- ( w e. ran G -> ( ( F |` ran G ) ` w ) = ( F ` w ) )
57	56	eqcomd 2628	. . . . . . . . . . . . . 14 |- ( w e. ran G -> ( F ` w ) = ( ( F |` ran G ) ` w ) )
58	57	ad2antrr 762	. . . . . . . . . . . . 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 477	. . . . . . . . . . . . 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 6207	. . . . . . . . . . . . . 14 |- ( t e. ran G -> ( ( F |` ran G ) ` t ) = ( F ` t ) )
61	60	ad2antlr 763	. . . . . . . . . . . . 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 2660	. . . . . . . . . . . 12 |- ( ( ( w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( F ` w ) = ( F ` t ) )
63	62	3adantl1 1217	. . . . . . . . . . 11 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( F ` w ) = ( F ` t ) )
64		simpl1 1064	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ph )
65		simpl3 1066	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> t e. ran G )
66		vex 3203	. . . . . . . . . . . . . . . . . . 19 |- w e. _V
67	41	elrnmpt 5372	. . . . . . . . . . . . . . . . . . 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 206	. . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . 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 1224	. . . . . . . . . . . . . . 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 224	. . . . . . . . . . . . . 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 2628	. . . . . . . . . . . . . . 15 |- ( ( F ` w ) = ( F ` t ) -> ( F ` t ) = ( F ` w ) )
75	74	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( F ` t ) = ( F ` w ) )
76		eleq1 2689	. . . . . . . . . . . . . . . . . 18 |- ( b = w -> ( b e. ran G <-> w e. ran G ) )
77	76	3anbi3d 1405	. . . . . . . . . . . . . . . . 17 |- ( b = w -> ( ( ph /\ t e. ran G /\ b e. ran G ) <-> ( ph /\ t e. ran G /\ w e. ran G ) ) )
78		fveq2 6191	. . . . . . . . . . . . . . . . . 18 |- ( b = w -> ( F ` b ) = ( F ` w ) )
79	78	eqeq2d 2632	. . . . . . . . . . . . . . . . 17 |- ( b = w -> ( ( F ` t ) = ( F ` b ) <-> ( F ` t ) = ( F ` w ) ) )
80	77, 79	anbi12d 747	. . . . . . . . . . . . . . . 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 4656	. . . . . . . . . . . . . . . . 17 |- ( b = w -> ( b R t <-> w R t ) )
82	81	notbid 308	. . . . . . . . . . . . . . . 16 |- ( b = w -> ( -. b R t <-> -. w R t ) )
83	80, 82	imbi12d 334	. . . . . . . . . . . . . . 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 2689	. . . . . . . . . . . . . . . . . . 19 |- ( a = t -> ( a e. ran G <-> t e. ran G ) )
85	84	3anbi2d 1404	. . . . . . . . . . . . . . . . . 18 |- ( a = t -> ( ( ph /\ a e. ran G /\ b e. ran G ) <-> ( ph /\ t e. ran G /\ b e. ran G ) ) )
86		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 |- ( a = t -> ( F ` a ) = ( F ` t ) )
87	86	eqeq1d 2624	. . . . . . . . . . . . . . . . . 18 |- ( a = t -> ( ( F ` a ) = ( F ` b ) <-> ( F ` t ) = ( F ` b ) ) )
88	85, 87	anbi12d 747	. . . . . . . . . . . . . . . . 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 4657	. . . . . . . . . . . . . . . . . 18 |- ( a = t -> ( b R a <-> b R t ) )
90	89	notbid 308	. . . . . . . . . . . . . . . . 17 |- ( a = t -> ( -. b R a <-> -. b R t ) )
91	88, 90	imbi12d 334	. . . . . . . . . . . . . . . 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 2689	. . . . . . . . . . . . . . . . . . . 20 |- ( t = b -> ( t e. ran G <-> b e. ran G ) )
93	92	3anbi3d 1405	. . . . . . . . . . . . . . . . . . 19 |- ( t = b -> ( ( ph /\ a e. ran G /\ t e. ran G ) <-> ( ph /\ a e. ran G /\ b e. ran G ) ) )
94		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 |- ( t = b -> ( F ` t ) = ( F ` b ) )
95	94	eqeq2d 2632	. . . . . . . . . . . . . . . . . . 19 |- ( t = b -> ( ( F ` a ) = ( F ` t ) <-> ( F ` a ) = ( F ` b ) ) )
96	93, 95	anbi12d 747	. . . . . . . . . . . . . . . . . 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 4656	. . . . . . . . . . . . . . . . . . 19 |- ( t = b -> ( t R a <-> b R a ) )
98	97	notbid 308	. . . . . . . . . . . . . . . . . 18 |- ( t = b -> ( -. t R a <-> -. b R a ) )
99	96, 98	imbi12d 334	. . . . . . . . . . . . . . . . 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 2689	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = a -> ( w e. ran G <-> a e. ran G ) )
101	100	3anbi2d 1404	. . . . . . . . . . . . . . . . . . . 20 |- ( w = a -> ( ( ph /\ w e. ran G /\ t e. ran G ) <-> ( ph /\ a e. ran G /\ t e. ran G ) ) )
102		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = a -> ( F ` w ) = ( F ` a ) )
103	102	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . 20 |- ( w = a -> ( ( F ` w ) = ( F ` t ) <-> ( F ` a ) = ( F ` t ) ) )
104	101, 103	anbi12d 747	. . . . . . . . . . . . . . . . . . 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 4657	. . . . . . . . . . . . . . . . . . . 20 |- ( w = a -> ( t R w <-> t R a ) )
106	105	notbid 308	. . . . . . . . . . . . . . . . . . 19 |- ( w = a -> ( -. t R w <-> -. t R a ) )
107	104, 106	imbi12d 334	. . . . . . . . . . . . . . . . . 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 1843	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ u ph
109		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ u w
110		nfmpt1 4747	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/_ u ( u e. ran F |-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
111	41, 110	nfcxfr 2762	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ u G
112	111	nfrn 5368	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ u ran G
113	109, 112	nfel 2777	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ u w e. ran G
114	112	nfcri 2758	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ u t e. ran G
115	108, 113, 114	nf3an 1831	. . . . . . . . . . . . . . . . . . . . 21 |- F/ u ( ph /\ w e. ran G /\ t e. ran G )
116		nfv 1843	. . . . . . . . . . . . . . . . . . . . 21 |- F/ u ( F ` w ) = ( F ` t )
117	115, 116	nfan 1828	. . . . . . . . . . . . . . . . . . . 20 |- F/ u ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) )
118		nfv 1843	. . . . . . . . . . . . . . . . . . . 20 |- F/ u -. t R w
119		simp3 1063	. . . . . . . . . . . . . . . . . . . . . . . . 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 2628	. . . . . . . . . . . . . . . . . . . . . . . 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 1091	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1062	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( v = w -> ( t R v <-> t R w ) )
125	124	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( v = w -> ( -. t R v <-> -. t R w ) )
126	125	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( v = w -> ( A. t e. ( `' F " { u } ) -. t R v <-> A. t e. ( `' F " { u } ) -. t R w ) )
127	126	cbvriotav 6622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1084	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ u e. ran F ) -> E! w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w )
133		riota1 6629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1081	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 247	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 475	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1326	. . . . . . . . . . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . . . . . . . . . . . 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 6633	. . . . . . . . . . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . . . . . . . . . . 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 247	. . . . . . . . . . . . . . . . . . . . . . 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 1319	. . . . . . . . . . . . . . . . . . . . . 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 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ t e. ran G ) -> t e. A )
145	144	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ w e. ran G /\ t e. ran G ) -> t e. A )
146	145	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> t e. A )
147	146	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . . . 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 763	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1081	. . . . . . . . . . . . . . . . . . . . . . . . 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 6338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 222	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 479	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1319	. . . . . . . . . . . . . . . . . . . . . . . . 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 2656	. . . . . . . . . . . . . . . . . . . . . . . 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 554	. . . . . . . . . . . . . . . . . . . . . . 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 6338	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1082	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ w e. ran G /\ t e. ran G ) -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
160	159	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 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 1081	. . . . . . . . . . . . . . . . . . . . . . 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 247	. . . . . . . . . . . . . . . . . . . . . 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 2930	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A. t e. ( `' F " { u } ) -. t R w /\ t e. ( `' F " { u } ) ) -> -. t R w )
164	143, 162, 163	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 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 1264	. . . . . . . . . . . . . . . . . . . 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 3026	. . . . . . . . . . . . . . . . . . 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 2263	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ a e. ran G /\ t e. ran G ) /\ ( F ` a ) = ( F ` t ) ) -> -. t R a )
169	99, 168	chvarv 2263	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ a e. ran G /\ b e. ran G ) /\ ( F ` a ) = ( F ` b ) ) -> -. b R a )
170	91, 169	chvarv 2263	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ t e. ran G /\ b e. ran G ) /\ ( F ` t ) = ( F ` b ) ) -> -. b R t )
171	83, 170	chvarv 2263	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ t e. ran G /\ w e. ran G ) /\ ( F ` t ) = ( F ` w ) ) -> -. w R t )
172	64, 65, 72, 75, 171	syl31anc 1329	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> -. w R t )
173	172, 167	jca 554	. . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( -. w R t /\ -. t R w ) )
174		weso 5105	. . . . . . . . . . . . . . . 16 |- ( R We A -> R Or A )
175	8, 174	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> R Or A )
176	175	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( F ` w ) = ( F ` t ) ) -> R Or A )
177	176	3ad2antl1 1223	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> R Or A )
178	43	sselda 3603	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w e. ran G ) -> w e. A )
179	178	3adant3 1081	. . . . . . . . . . . . . 14 |- ( ( ph /\ w e. ran G /\ t e. ran G ) -> w e. A )
180	179	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w e. A )
181		sotrieq2 5063	. . . . . . . . . . . . 13 |- ( ( R Or A /\ ( w e. A /\ t e. A ) ) -> ( w = t <-> ( -. w R t /\ -. t R w ) ) )
182	177, 180, 146, 181	syl12anc 1324	. . . . . . . . . . . 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 247	. . . . . . . . . . 11 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w = t )
184	55, 63, 183	syl2anc 693	. . . . . . . . . 10 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> w = t )
185	184	ex 450	. . . . . . . . 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 1326	. . . . . . . 8 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> ( ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) -> w = t ) )
187	186	ralrimivva 2971	. . . . . . 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 554	. . . . . 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 6512	. . . . . 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 224	. . . . 5 |- ( ph -> ( F |` ran G ) : ran G -1-1-> ran F )
191		riotaex 6615	. . . . . . . . . . . . . 14 |- ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V
192	191	rgenw 2924	. . . . . . . . . . . . 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 6020	. . . . . . . . . . . 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 6054	. . . . . . . . . . . 12 |- ( G Fn ran F <-> G : ran F --> ran G )
197	196	biimpi 206	. . . . . . . . . . 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 6359	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> ( G ` u ) e. ran G )
200		fvres 6207	. . . . . . . . . . 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 224	. . . . . . . . . . . . . 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 6291	. . . . . . . . . . . . . 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 693	. . . . . . . . . . . . 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 2701	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ran F ) -> ( G ` u ) e. ( `' F " { u } ) )
207		fvex 6201	. . . . . . . . . . . . . 14 |- ( G ` u ) e. _V
208		eleq1 2689	. . . . . . . . . . . . . . . 16 |- ( w = ( G ` u ) -> ( w e. ( `' F " { u } ) <-> ( G ` u ) e. ( `' F " { u } ) ) )
209		eleq1 2689	. . . . . . . . . . . . . . . . 17 |- ( w = ( G ` u ) -> ( w e. A <-> ( G ` u ) e. A ) )
210		fveq2 6191	. . . . . . . . . . . . . . . . . 18 |- ( w = ( G ` u ) -> ( F ` w ) = ( F ` ( G ` u ) ) )
211	210	eqeq1d 2624	. . . . . . . . . . . . . . . . 17 |- ( w = ( G ` u ) -> ( ( F ` w ) = u <-> ( F ` ( G ` u ) ) = u ) )
212	209, 211	anbi12d 747	. . . . . . . . . . . . . . . 16 |- ( w = ( G ` u ) -> ( ( w e. A /\ ( F ` w ) = u ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
213	208, 212	bibi12d 335	. . . . . . . . . . . . . . 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 330	. . . . . . . . . . . . . 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 3259	. . . . . . . . . . . . 13 |- ( ph -> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
217	216	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ran F ) -> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
218	206, 217	mpbid 222	. . . . . . . . . . 11 |- ( ( ph /\ u e. ran F ) -> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) )
219	218	simprd 479	. . . . . . . . . 10 |- ( ( ph /\ u e. ran F ) -> ( F ` ( G ` u ) ) = u )
220	201, 219	eqtr2d 2657	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> u = ( ( F |` ran G ) ` ( G ` u ) ) )
221		fveq2 6191	. . . . . . . . . . 11 |- ( w = ( G ` u ) -> ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` ( G ` u ) ) )
222	221	eqeq2d 2632	. . . . . . . . . 10 |- ( w = ( G ` u ) -> ( u = ( ( F |` ran G ) ` w ) <-> u = ( ( F |` ran G ) ` ( G ` u ) ) ) )
223	222	rspcev 3309	. . . . . . . . 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 693	. . . . . . . 8 |- ( ( ph /\ u e. ran F ) -> E. w e. ran G u = ( ( F |` ran G ) ` w ) )
225	224	ralrimiva 2966	. . . . . . 7 |- ( ph -> A. u e. ran F E. w e. ran G u = ( ( F |` ran G ) ` w ) )
226	51, 225	jca 554	. . . . . 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 6374	. . . . . 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 224	. . . . 5 |- ( ph -> ( F |` ran G ) : ran G -onto-> ran F )
229	190, 228	jca 554	. . . 4 |- ( ph -> ( ( F |` ran G ) : ran G -1-1-> ran F /\ ( F |` ran G ) : ran G -onto-> ran F ) )
230		df-f1o 5895	. . . 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 224	. . 3 |- ( ph -> ( F |` ran G ) : ran G -1-1-onto-> ran F )
232		nfcv 2764	. . . . . 6 |- F/_ v F
233		nfcv 2764	. . . . . . . . 9 |- F/_ v ran F
234		nfriota1 6618	. . . . . . . . 9 |- F/_ v ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
235	233, 234	nfmpt 4746	. . . . . . . 8 |- F/_ v ( u e. ran F |-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
236	41, 235	nfcxfr 2762	. . . . . . 7 |- F/_ v G
237	236	nfrn 5368	. . . . . 6 |- F/_ v ran G
238	232, 237	nfres 5398	. . . . 5 |- F/_ v ( F |` ran G )
239	238, 237, 233	nff1o 6135	. . . 4 |- F/ v ( F |` ran G ) : ran G -1-1-onto-> ran F
240		reseq2 5391	. . . . 5 |- ( v = ran G -> ( F |` v ) = ( F |` ran G ) )
241		id 22	. . . . 5 |- ( v = ran G -> v = ran G )
242		eqidd 2623	. . . . 5 |- ( v = ran G -> ran F = ran F )
243	240, 241, 242	f1oeq123d 6133	. . . 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 3304	. . 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 693	. 2 |- ( ph -> E. v e. ~P A ( F |` v ) : v -1-1-onto-> ran F )
246		reseq2 5391	. . . 4 |- ( v = x -> ( F |` v ) = ( F |` x ) )
247		id 22	. . . 4 |- ( v = x -> v = x )
248		eqidd 2623	. . . 4 |- ( v = x -> ran F = ran F )
249	246, 247, 248	f1oeq123d 6133	. . 3 |- ( v = x -> ( ( F |` v ) : v -1-1-onto-> ran F <-> ( F |` x ) : x -1-1-onto-> ran F ) )
250	249	cbvrexv 3172	. 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 208	1 |- ( ph -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> ran F )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   E!wreu 2914   _Vcvv 3200   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   {csn 4177   class class class wbr 4653   |-> cmpt 4729   Or wor 5034   We wwe 5072   `'ccnv 5113   dom cdm 5114   ran crn 5115   |` cres 5116   "cima 5117   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   -onto->wfo 5886   -1-1-onto->wf1o 5887   ` cfv 5888   iota_crio 6610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611

This theorem is referenced by:  wessf1orn  39372