Theorem wessf1ornlem 37530

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 5194	. . . . . . . . 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 5685	. . . . . . . . . 10 |- ( F Fn A -> dom F = A )
5	3, 4	syl 17	. . . . . . . . 9 |- ( ph -> dom F = A )
6	5	adantr 472	. . . . . . . 8 |- ( ( ph /\ u e. ran F ) -> dom F = A )
7	2, 6	sseqtrd 3454	. . . . . . 7 |- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) C_ A )
8		wessf1ornlem.r	. . . . . . . . . 10 |- ( ph -> R We A )
9	8	adantr 472	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> R We A )
10	1, 5	syl5sseq 3466	. . . . . . . . . . 11 |- ( ph -> ( `' F " { u } ) C_ A )
11		wessf1ornlem.a	. . . . . . . . . . 11 |- ( ph -> A e. V )
12		ssexg 4542	. . . . . . . . . . 11 |- ( ( ( `' F " { u } ) C_ A /\ A e. V ) -> ( `' F " { u } ) e. _V )
13	10, 11, 12	syl2anc 673	. . . . . . . . . 10 |- ( ph -> ( `' F " { u } ) e. _V )
14	13	adantr 472	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) e. _V )
15		inisegn0 5206	. . . . . . . . . . 11 |- ( u e. ran F <-> ( `' F " { u } ) =/= (/) )
16	15	biimpi 199	. . . . . . . . . 10 |- ( u e. ran F -> ( `' F " { u } ) =/= (/) )
17	16	adantl 473	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) =/= (/) )
18		wereu 4835	. . . . . . . . 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 1294	. . . . . . . 8 |- ( ( ph /\ u e. ran F ) -> E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
20		riotacl 6284	. . . . . . . 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 3419	. . . . . 6 |- ( ( ph /\ u e. ran F ) -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. A )
23	22	ralrimiva 2809	. . . . 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 3969	. . . . . . . . . . 11 |- ( y = u -> { y } = { u } )
26	25	imaeq2d 5174	. . . . . . . . . 10 |- ( y = u -> ( `' F " { y } ) = ( `' F " { u } ) )
27	26	raleqdv 2979	. . . . . . . . . 10 |- ( y = u -> ( A. z e. ( `' F " { y } ) -. z R x <-> A. z e. ( `' F " { u } ) -. z R x ) )
28	26, 27	riotaeqbidv 6273	. . . . . . . . 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 4398	. . . . . . . . . . . . . . 15 |- ( z = t -> ( z R x <-> t R x ) )
30	29	notbid 301	. . . . . . . . . . . . . 14 |- ( z = t -> ( -. z R x <-> -. t R x ) )
31	30	cbvralv 3005	. . . . . . . . . . . . 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 4399	. . . . . . . . . . . . . 14 |- ( x = v -> ( t R x <-> t R v ) )
34	33	notbid 301	. . . . . . . . . . . . 13 |- ( x = v -> ( -. t R x <-> -. t R v ) )
35	34	ralbidv 2829	. . . . . . . . . . . 12 |- ( x = v -> ( A. t e. ( `' F " { u } ) -. t R x <-> A. t e. ( `' F " { u } ) -. t R v ) )
36	32, 35	bitrd 261	. . . . . . . . . . 11 |- ( x = v -> ( A. z e. ( `' F " { u } ) -. z R x <-> A. t e. ( `' F " { u } ) -. t R v ) )
37	36	cbvriotav 6281	. . . . . . . . . 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 2505	. . . . . . . 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 4488	. . . . . . 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 2493	. . . . . 6 |- G = ( u e. ran F |-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
42	41	rnmptss 6068	. . . . 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 4543	. . . . 5 |- ( ph -> ran G e. _V )
45		elpwg 3950	. . . . 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 240	. . 3 |- ( ph -> ran G e. ~P A )
48		dffn3 5748	. . . . . . . . . 10 |- ( F Fn A <-> F : A --> ran F )
49	48	biimpi 199	. . . . . . . . 9 |- ( F Fn A -> F : A --> ran F )
50	3, 49	syl 17	. . . . . . . 8 |- ( ph -> F : A --> ran F )
51	50, 43	fssresd 5762	. . . . . . 7 |- ( ph -> ( F |` ran G ) : ran G --> ran F )
52		simpl 464	. . . . . . . . 9 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> ph )
53		simprl 772	. . . . . . . . 9 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> w e. ran G )
54		simprr 774	. . . . . . . . 9 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> t e. ran G )
55		simpl 464	. . . . . . . . . . 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 5893	. . . . . . . . . . . . . . 15 |- ( w e. ran G -> ( ( F |` ran G ) ` w ) = ( F ` w ) )
57	56	eqcomd 2477	. . . . . . . . . . . . . 14 |- ( w e. ran G -> ( F ` w ) = ( ( F |` ran G ) ` w ) )
58	57	ad2antrr 740	. . . . . . . . . . . . 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 468	. . . . . . . . . . . . 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 5893	. . . . . . . . . . . . . 14 |- ( t e. ran G -> ( ( F |` ran G ) ` t ) = ( F ` t ) )
61	60	ad2antlr 741	. . . . . . . . . . . . 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 2509	. . . . . . . . . . . 12 |- ( ( ( w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( F ` w ) = ( F ` t ) )
63	62	3adantl1 1186	. . . . . . . . . . 11 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( F ` w ) = ( F ` t ) )
64		simpl1 1033	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ph )
65		simpl3 1035	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> t e. ran G )
66		vex 3034	. . . . . . . . . . . . . . . . . . 19 |- w e. _V
67	41	elrnmpt 5087	. . . . . . . . . . . . . . . . . . 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 199	. . . . . . . . . . . . . . . . 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 472	. . . . . . . . . . . . . . . 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 1193	. . . . . . . . . . . . . . 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 217	. . . . . . . . . . . . . 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 2477	. . . . . . . . . . . . . . 15 |- ( ( F ` w ) = ( F ` t ) -> ( F ` t ) = ( F ` w ) )
75	74	adantl 473	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( F ` t ) = ( F ` w ) )
76		eleq1 2537	. . . . . . . . . . . . . . . . . 18 |- ( b = w -> ( b e. ran G <-> w e. ran G ) )
77	76	3anbi3d 1371	. . . . . . . . . . . . . . . . 17 |- ( b = w -> ( ( ph /\ t e. ran G /\ b e. ran G ) <-> ( ph /\ t e. ran G /\ w e. ran G ) ) )
78		fveq2 5879	. . . . . . . . . . . . . . . . . 18 |- ( b = w -> ( F ` b ) = ( F ` w ) )
79	78	eqeq2d 2481	. . . . . . . . . . . . . . . . 17 |- ( b = w -> ( ( F ` t ) = ( F ` b ) <-> ( F ` t ) = ( F ` w ) ) )
80	77, 79	anbi12d 725	. . . . . . . . . . . . . . . 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 4398	. . . . . . . . . . . . . . . . 17 |- ( b = w -> ( b R t <-> w R t ) )
82	81	notbid 301	. . . . . . . . . . . . . . . 16 |- ( b = w -> ( -. b R t <-> -. w R t ) )
83	80, 82	imbi12d 327	. . . . . . . . . . . . . . 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 2537	. . . . . . . . . . . . . . . . . . 19 |- ( a = t -> ( a e. ran G <-> t e. ran G ) )
85	84	3anbi2d 1370	. . . . . . . . . . . . . . . . . 18 |- ( a = t -> ( ( ph /\ a e. ran G /\ b e. ran G ) <-> ( ph /\ t e. ran G /\ b e. ran G ) ) )
86		fveq2 5879	. . . . . . . . . . . . . . . . . . 19 |- ( a = t -> ( F ` a ) = ( F ` t ) )
87	86	eqeq1d 2473	. . . . . . . . . . . . . . . . . 18 |- ( a = t -> ( ( F ` a ) = ( F ` b ) <-> ( F ` t ) = ( F ` b ) ) )
88	85, 87	anbi12d 725	. . . . . . . . . . . . . . . . 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 4399	. . . . . . . . . . . . . . . . . 18 |- ( a = t -> ( b R a <-> b R t ) )
90	89	notbid 301	. . . . . . . . . . . . . . . . 17 |- ( a = t -> ( -. b R a <-> -. b R t ) )
91	88, 90	imbi12d 327	. . . . . . . . . . . . . . . 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 2537	. . . . . . . . . . . . . . . . . . . 20 |- ( t = b -> ( t e. ran G <-> b e. ran G ) )
93	92	3anbi3d 1371	. . . . . . . . . . . . . . . . . . 19 |- ( t = b -> ( ( ph /\ a e. ran G /\ t e. ran G ) <-> ( ph /\ a e. ran G /\ b e. ran G ) ) )
94		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20 |- ( t = b -> ( F ` t ) = ( F ` b ) )
95	94	eqeq2d 2481	. . . . . . . . . . . . . . . . . . 19 |- ( t = b -> ( ( F ` a ) = ( F ` t ) <-> ( F ` a ) = ( F ` b ) ) )
96	93, 95	anbi12d 725	. . . . . . . . . . . . . . . . . 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 4398	. . . . . . . . . . . . . . . . . . 19 |- ( t = b -> ( t R a <-> b R a ) )
98	97	notbid 301	. . . . . . . . . . . . . . . . . 18 |- ( t = b -> ( -. t R a <-> -. b R a ) )
99	96, 98	imbi12d 327	. . . . . . . . . . . . . . . . 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 2537	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = a -> ( w e. ran G <-> a e. ran G ) )
101	100	3anbi2d 1370	. . . . . . . . . . . . . . . . . . . 20 |- ( w = a -> ( ( ph /\ w e. ran G /\ t e. ran G ) <-> ( ph /\ a e. ran G /\ t e. ran G ) ) )
102		fveq2 5879	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = a -> ( F ` w ) = ( F ` a ) )
103	102	eqeq1d 2473	. . . . . . . . . . . . . . . . . . . 20 |- ( w = a -> ( ( F ` w ) = ( F ` t ) <-> ( F ` a ) = ( F ` t ) ) )
104	101, 103	anbi12d 725	. . . . . . . . . . . . . . . . . . 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 4399	. . . . . . . . . . . . . . . . . . . 20 |- ( w = a -> ( t R w <-> t R a ) )
106	105	notbid 301	. . . . . . . . . . . . . . . . . . 19 |- ( w = a -> ( -. t R w <-> -. t R a ) )
107	104, 106	imbi12d 327	. . . . . . . . . . . . . . . . . 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 1769	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ u ph
109		nfcv 2612	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ u w
110		nfmpt1 4485	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/_ u ( u e. ran F |-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
111	41, 110	nfcxfr 2610	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ u G
112	111	nfrn 5083	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ u ran G
113	109, 112	nfel 2624	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ u w e. ran G
114	112	nfcri 2606	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ u t e. ran G
115	108, 113, 114	nf3an 2033	. . . . . . . . . . . . . . . . . . . . 21 |- F/ u ( ph /\ w e. ran G /\ t e. ran G )
116		nfv 1769	. . . . . . . . . . . . . . . . . . . . 21 |- F/ u ( F ` w ) = ( F ` t )
117	115, 116	nfan 2031	. . . . . . . . . . . . . . . . . . . 20 |- F/ u ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) )
118		nfv 1769	. . . . . . . . . . . . . . . . . . . 20 |- F/ u -. t R w
119		simp3 1032	. . . . . . . . . . . . . . . . . . . . . . . . 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 2477	. . . . . . . . . . . . . . . . . . . . . . . 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 1060	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1031	. . . . . . . . . . . . . . . . . . . . . . . . . 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 4399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( v = w -> ( t R v <-> t R w ) )
125	124	notbid 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( v = w -> ( -. t R v <-> -. t R w ) )
126	125	ralbidv 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( v = w -> ( A. t e. ( `' F " { u } ) -. t R v <-> A. t e. ( `' F " { u } ) -. t R w ) )
127	126	cbvriotav 6281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1053	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ u e. ran F ) -> E! w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w )
133		riota1 6288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1050	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1292	. . . . . . . . . . . . . . . . . . . . . . . . 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 673	. . . . . . . . . . . . . . . . . . . . . . . . 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 6292	. . . . . . . . . . . . . . . . . . . . . . . . 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 673	. . . . . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . . . . . . 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 1285	. . . . . . . . . . . . . . . . . . . . . 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 3418	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ t e. ran G ) -> t e. A )
145	144	3adant2 1049	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ w e. ran G /\ t e. ran G ) -> t e. A )
146	145	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> t e. A )
147	146	3ad2ant1 1051	. . . . . . . . . . . . . . . . . . . . . . . 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 741	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1050	. . . . . . . . . . . . . . . . . . . . . . . . 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 6018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 215	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 470	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1285	. . . . . . . . . . . . . . . . . . . . . . . . 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 2505	. . . . . . . . . . . . . . . . . . . . . . . 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 541	. . . . . . . . . . . . . . . . . . . . . . 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 6018	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1051	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ w e. ran G /\ t e. ran G ) -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
160	159	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . 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 1050	. . . . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . . . . . 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 2774	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A. t e. ( `' F " { u } ) -. t R w /\ t e. ( `' F " { u } ) ) -> -. t R w )
164	143, 162, 163	syl2anc 673	. . . . . . . . . . . . . . . . . . . . 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 1230	. . . . . . . . . . . . . . . . . . . 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 2866	. . . . . . . . . . . . . . . . . . 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 2120	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ a e. ran G /\ t e. ran G ) /\ ( F ` a ) = ( F ` t ) ) -> -. t R a )
169	99, 168	chvarv 2120	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ a e. ran G /\ b e. ran G ) /\ ( F ` a ) = ( F ` b ) ) -> -. b R a )
170	91, 169	chvarv 2120	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ t e. ran G /\ b e. ran G ) /\ ( F ` t ) = ( F ` b ) ) -> -. b R t )
171	83, 170	chvarv 2120	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ t e. ran G /\ w e. ran G ) /\ ( F ` t ) = ( F ` w ) ) -> -. w R t )
172	64, 65, 72, 75, 171	syl31anc 1295	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> -. w R t )
173	172, 167	jca 541	. . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( -. w R t /\ -. t R w ) )
174		weso 4830	. . . . . . . . . . . . . . . 16 |- ( R We A -> R Or A )
175	8, 174	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> R Or A )
176	175	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( F ` w ) = ( F ` t ) ) -> R Or A )
177	176	3ad2antl1 1192	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> R Or A )
178	43	sselda 3418	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w e. ran G ) -> w e. A )
179	178	3adant3 1050	. . . . . . . . . . . . . 14 |- ( ( ph /\ w e. ran G /\ t e. ran G ) -> w e. A )
180	179	adantr 472	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w e. A )
181		sotrieq2 4788	. . . . . . . . . . . . 13 |- ( ( R Or A /\ ( w e. A /\ t e. A ) ) -> ( w = t <-> ( -. w R t /\ -. t R w ) ) )
182	177, 180, 146, 181	syl12anc 1290	. . . . . . . . . . . 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 240	. . . . . . . . . . 11 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w = t )
184	55, 63, 183	syl2anc 673	. . . . . . . . . 10 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> w = t )
185	184	ex 441	. . . . . . . . 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 1292	. . . . . . . 8 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> ( ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) -> w = t ) )
187	186	ralrimivva 2814	. . . . . . 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 541	. . . . . 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 6177	. . . . . 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 217	. . . . 5 |- ( ph -> ( F |` ran G ) : ran G -1-1-> ran F )
191		riotaex 6274	. . . . . . . . . . . . . 14 |- ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V
192	191	rgenw 2768	. . . . . . . . . . . . 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 5714	. . . . . . . . . . . 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 5748	. . . . . . . . . . . 12 |- ( G Fn ran F <-> G : ran F --> ran G )
197	196	biimpi 199	. . . . . . . . . . 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 6037	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> ( G ` u ) e. ran G )
200		fvres 5893	. . . . . . . . . . 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 217	. . . . . . . . . . . . . 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 5972	. . . . . . . . . . . . . 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 673	. . . . . . . . . . . . 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 2549	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ran F ) -> ( G ` u ) e. ( `' F " { u } ) )
207		fvex 5889	. . . . . . . . . . . . . 14 |- ( G ` u ) e. _V
208		eleq1 2537	. . . . . . . . . . . . . . . 16 |- ( w = ( G ` u ) -> ( w e. ( `' F " { u } ) <-> ( G ` u ) e. ( `' F " { u } ) ) )
209		eleq1 2537	. . . . . . . . . . . . . . . . 17 |- ( w = ( G ` u ) -> ( w e. A <-> ( G ` u ) e. A ) )
210		fveq2 5879	. . . . . . . . . . . . . . . . . 18 |- ( w = ( G ` u ) -> ( F ` w ) = ( F ` ( G ` u ) ) )
211	210	eqeq1d 2473	. . . . . . . . . . . . . . . . 17 |- ( w = ( G ` u ) -> ( ( F ` w ) = u <-> ( F ` ( G ` u ) ) = u ) )
212	209, 211	anbi12d 725	. . . . . . . . . . . . . . . 16 |- ( w = ( G ` u ) -> ( ( w e. A /\ ( F ` w ) = u ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
213	208, 212	bibi12d 328	. . . . . . . . . . . . . . 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 323	. . . . . . . . . . . . . 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 3086	. . . . . . . . . . . . 13 |- ( ph -> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
217	216	adantr 472	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ran F ) -> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
218	206, 217	mpbid 215	. . . . . . . . . . 11 |- ( ( ph /\ u e. ran F ) -> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) )
219	218	simprd 470	. . . . . . . . . 10 |- ( ( ph /\ u e. ran F ) -> ( F ` ( G ` u ) ) = u )
220	201, 219	eqtr2d 2506	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> u = ( ( F |` ran G ) ` ( G ` u ) ) )
221		fveq2 5879	. . . . . . . . . . 11 |- ( w = ( G ` u ) -> ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` ( G ` u ) ) )
222	221	eqeq2d 2481	. . . . . . . . . 10 |- ( w = ( G ` u ) -> ( u = ( ( F |` ran G ) ` w ) <-> u = ( ( F |` ran G ) ` ( G ` u ) ) ) )
223	222	rspcev 3136	. . . . . . . . 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 673	. . . . . . . 8 |- ( ( ph /\ u e. ran F ) -> E. w e. ran G u = ( ( F |` ran G ) ` w ) )
225	224	ralrimiva 2809	. . . . . . 7 |- ( ph -> A. u e. ran F E. w e. ran G u = ( ( F |` ran G ) ` w ) )
226	51, 225	jca 541	. . . . . 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 6052	. . . . . 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 217	. . . . 5 |- ( ph -> ( F |` ran G ) : ran G -onto-> ran F )
229	190, 228	jca 541	. . . 4 |- ( ph -> ( ( F |` ran G ) : ran G -1-1-> ran F /\ ( F |` ran G ) : ran G -onto-> ran F ) )
230		df-f1o 5596	. . . 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 217	. . 3 |- ( ph -> ( F |` ran G ) : ran G -1-1-onto-> ran F )
232		nfcv 2612	. . . . . 6 |- F/_ v F
233		nfcv 2612	. . . . . . . . 9 |- F/_ v ran F
234		nfriota1 6277	. . . . . . . . 9 |- F/_ v ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
235	233, 234	nfmpt 4484	. . . . . . . 8 |- F/_ v ( u e. ran F |-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
236	41, 235	nfcxfr 2610	. . . . . . 7 |- F/_ v G
237	236	nfrn 5083	. . . . . 6 |- F/_ v ran G
238	232, 237	nfres 5113	. . . . 5 |- F/_ v ( F |` ran G )
239	238, 237, 233	nff1o 5826	. . . 4 |- F/ v ( F |` ran G ) : ran G -1-1-onto-> ran F
240		reseq2 5106	. . . . 5 |- ( v = ran G -> ( F |` v ) = ( F |` ran G ) )
241		id 22	. . . . 5 |- ( v = ran G -> v = ran G )
242		eqidd 2472	. . . . 5 |- ( v = ran G -> ran F = ran F )
243	240, 241, 242	f1oeq123d 5824	. . . 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 3131	. . 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 673	. 2 |- ( ph -> E. v e. ~P A ( F |` v ) : v -1-1-onto-> ran F )
246		reseq2 5106	. . . 4 |- ( v = x -> ( F |` v ) = ( F |` x ) )
247		id 22	. . . 4 |- ( v = x -> v = x )
248		eqidd 2472	. . . 4 |- ( v = x -> ran F = ran F )
249	246, 247, 248	f1oeq123d 5824	. . 3 |- ( v = x -> ( ( F |` v ) : v -1-1-onto-> ran F <-> ( F |` x ) : x -1-1-onto-> ran F ) )
250	249	cbvrexv 3006	. 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 201	1 |- ( ph -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> ran F )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 376   /\ w3a 1007   = wceq 1452   e. wcel 1904   =/= wne 2641   A.wral 2756   E.wrex 2757   E!wreu 2758   _Vcvv 3031   C_ wss 3390   (/)c0 3722   ~Pcpw 3942   {csn 3959   class class class wbr 4395   |-> cmpt 4454   Or wor 4759   We wwe 4797   `'ccnv 4838   dom cdm 4839   ran crn 4840   |` cres 4841   "cima 4842   Fn wfn 5584   -->wf 5585   -1-1->wf1 5586   -onto->wfo 5587   -1-1-onto->wf1o 5588   ` cfv 5589   iota_crio 6269

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

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270

This theorem is referenced by:  wessf1orn  37531