Theorem wessf1ornlem 37297

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 5200	. . . . . . . . 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 466	. . . . . . . 8 |- ( ( ph /\ u e. ran F ) -> dom F = A )
7	2, 6	sseqtrd 3497	. . . . . . 7 |- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) C_ A )
8		wessf1ornlem.r	. . . . . . . . . 10 |- ( ph -> R We A )
9	8	adantr 466	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> R We A )
10	1, 5	syl5sseq 3509	. . . . . . . . . . 11 |- ( ph -> ( `' F " { u } ) C_ A )
11		wessf1ornlem.a	. . . . . . . . . . 11 |- ( ph -> A e. V )
12		ssexg 4563	. . . . . . . . . . 11 |- ( ( ( `' F " { u } ) C_ A /\ A e. V ) -> ( `' F " { u } ) e. _V )
13	10, 11, 12	syl2anc 665	. . . . . . . . . 10 |- ( ph -> ( `' F " { u } ) e. _V )
14	13	adantr 466	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) e. _V )
15		inisegn0 5212	. . . . . . . . . . 11 |- ( u e. ran F <-> ( `' F " { u } ) =/= (/) )
16	15	biimpi 197	. . . . . . . . . 10 |- ( u e. ran F -> ( `' F " { u } ) =/= (/) )
17	16	adantl 467	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) =/= (/) )
18		wereu 4842	. . . . . . . . 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 1266	. . . . . . . 8 |- ( ( ph /\ u e. ran F ) -> E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
20		riotacl 6273	. . . . . . . 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 3462	. . . . . 6 |- ( ( ph /\ u e. ran F ) -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. A )
23	22	ralrimiva 2837	. . . . 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 4003	. . . . . . . . . . 11 |- ( y = u -> { y } = { u } )
26	25	imaeq2d 5180	. . . . . . . . . 10 |- ( y = u -> ( `' F " { y } ) = ( `' F " { u } ) )
27	26	raleqdv 3029	. . . . . . . . . 10 |- ( y = u -> ( A. z e. ( `' F " { y } ) -. z R x <-> A. z e. ( `' F " { u } ) -. z R x ) )
28	26, 27	riotaeqbidv 6262	. . . . . . . . 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 4420	. . . . . . . . . . . . . . 15 |- ( z = t -> ( z R x <-> t R x ) )
30	29	notbid 295	. . . . . . . . . . . . . 14 |- ( z = t -> ( -. z R x <-> -. t R x ) )
31	30	cbvralv 3053	. . . . . . . . . . . . 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 4421	. . . . . . . . . . . . . 14 |- ( x = v -> ( t R x <-> t R v ) )
34	33	notbid 295	. . . . . . . . . . . . 13 |- ( x = v -> ( -. t R x <-> -. t R v ) )
35	34	ralbidv 2862	. . . . . . . . . . . 12 |- ( x = v -> ( A. t e. ( `' F " { u } ) -. t R x <-> A. t e. ( `' F " { u } ) -. t R v ) )
36	32, 35	bitrd 256	. . . . . . . . . . 11 |- ( x = v -> ( A. z e. ( `' F " { u } ) -. z R x <-> A. t e. ( `' F " { u } ) -. t R v ) )
37	36	cbvriotav 6270	. . . . . . . . . 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 2461	. . . . . . . 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 4510	. . . . . . 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 2449	. . . . . 6 |- G = ( u e. ran F |-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
42	41	rnmptss 6059	. . . . 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 4564	. . . . 5 |- ( ph -> ran G e. _V )
45		elpwg 3984	. . . . 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 235	. . 3 |- ( ph -> ran G e. ~P A )
48		dffn3 5745	. . . . . . . . . 10 |- ( F Fn A <-> F : A --> ran F )
49	48	biimpi 197	. . . . . . . . 9 |- ( F Fn A -> F : A --> ran F )
50	3, 49	syl 17	. . . . . . . 8 |- ( ph -> F : A --> ran F )
51	50, 43	fssresd 5759	. . . . . . 7 |- ( ph -> ( F |` ran G ) : ran G --> ran F )
52		simpl 458	. . . . . . . . 9 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> ph )
53		simprl 762	. . . . . . . . 9 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> w e. ran G )
54		simprr 764	. . . . . . . . 9 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> t e. ran G )
55		simpl 458	. . . . . . . . . . 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 5887	. . . . . . . . . . . . . . 15 |- ( w e. ran G -> ( ( F |` ran G ) ` w ) = ( F ` w ) )
57	56	eqcomd 2428	. . . . . . . . . . . . . 14 |- ( w e. ran G -> ( F ` w ) = ( ( F |` ran G ) ` w ) )
58	57	ad2antrr 730	. . . . . . . . . . . . 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 462	. . . . . . . . . . . . 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 5887	. . . . . . . . . . . . . 14 |- ( t e. ran G -> ( ( F |` ran G ) ` t ) = ( F ` t ) )
61	60	ad2antlr 731	. . . . . . . . . . . . 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 2465	. . . . . . . . . . . 12 |- ( ( ( w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( F ` w ) = ( F ` t ) )
63	62	3adantl1 1161	. . . . . . . . . . 11 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> ( F ` w ) = ( F ` t ) )
64		simpl1 1008	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ph )
65		simpl3 1010	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> t e. ran G )
66		vex 3081	. . . . . . . . . . . . . . . . . . 19 |- w e. _V
67	41	elrnmpt 5093	. . . . . . . . . . . . . . . . . . 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 197	. . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . 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 1168	. . . . . . . . . . . . . . 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 215	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w e. ran G )
73		id 23	. . . . . . . . . . . . . . . 16 |- ( ( F ` w ) = ( F ` t ) -> ( F ` w ) = ( F ` t ) )
74	73	eqcomd 2428	. . . . . . . . . . . . . . 15 |- ( ( F ` w ) = ( F ` t ) -> ( F ` t ) = ( F ` w ) )
75	74	adantl 467	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( F ` t ) = ( F ` w ) )
76		eleq1 2492	. . . . . . . . . . . . . . . . . 18 |- ( b = w -> ( b e. ran G <-> w e. ran G ) )
77	76	3anbi3d 1341	. . . . . . . . . . . . . . . . 17 |- ( b = w -> ( ( ph /\ t e. ran G /\ b e. ran G ) <-> ( ph /\ t e. ran G /\ w e. ran G ) ) )
78		fveq2 5873	. . . . . . . . . . . . . . . . . 18 |- ( b = w -> ( F ` b ) = ( F ` w ) )
79	78	eqeq2d 2434	. . . . . . . . . . . . . . . . 17 |- ( b = w -> ( ( F ` t ) = ( F ` b ) <-> ( F ` t ) = ( F ` w ) ) )
80	77, 79	anbi12d 715	. . . . . . . . . . . . . . . 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 4420	. . . . . . . . . . . . . . . . 17 |- ( b = w -> ( b R t <-> w R t ) )
82	81	notbid 295	. . . . . . . . . . . . . . . 16 |- ( b = w -> ( -. b R t <-> -. w R t ) )
83	80, 82	imbi12d 321	. . . . . . . . . . . . . . 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 2492	. . . . . . . . . . . . . . . . . . 19 |- ( a = t -> ( a e. ran G <-> t e. ran G ) )
85	84	3anbi2d 1340	. . . . . . . . . . . . . . . . . 18 |- ( a = t -> ( ( ph /\ a e. ran G /\ b e. ran G ) <-> ( ph /\ t e. ran G /\ b e. ran G ) ) )
86		fveq2 5873	. . . . . . . . . . . . . . . . . . 19 |- ( a = t -> ( F ` a ) = ( F ` t ) )
87	86	eqeq1d 2422	. . . . . . . . . . . . . . . . . 18 |- ( a = t -> ( ( F ` a ) = ( F ` b ) <-> ( F ` t ) = ( F ` b ) ) )
88	85, 87	anbi12d 715	. . . . . . . . . . . . . . . . 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 4421	. . . . . . . . . . . . . . . . . 18 |- ( a = t -> ( b R a <-> b R t ) )
90	89	notbid 295	. . . . . . . . . . . . . . . . 17 |- ( a = t -> ( -. b R a <-> -. b R t ) )
91	88, 90	imbi12d 321	. . . . . . . . . . . . . . . 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 2492	. . . . . . . . . . . . . . . . . . . 20 |- ( t = b -> ( t e. ran G <-> b e. ran G ) )
93	92	3anbi3d 1341	. . . . . . . . . . . . . . . . . . 19 |- ( t = b -> ( ( ph /\ a e. ran G /\ t e. ran G ) <-> ( ph /\ a e. ran G /\ b e. ran G ) ) )
94		fveq2 5873	. . . . . . . . . . . . . . . . . . . 20 |- ( t = b -> ( F ` t ) = ( F ` b ) )
95	94	eqeq2d 2434	. . . . . . . . . . . . . . . . . . 19 |- ( t = b -> ( ( F ` a ) = ( F ` t ) <-> ( F ` a ) = ( F ` b ) ) )
96	93, 95	anbi12d 715	. . . . . . . . . . . . . . . . . 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 4420	. . . . . . . . . . . . . . . . . . 19 |- ( t = b -> ( t R a <-> b R a ) )
98	97	notbid 295	. . . . . . . . . . . . . . . . . 18 |- ( t = b -> ( -. t R a <-> -. b R a ) )
99	96, 98	imbi12d 321	. . . . . . . . . . . . . . . . 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 2492	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = a -> ( w e. ran G <-> a e. ran G ) )
101	100	3anbi2d 1340	. . . . . . . . . . . . . . . . . . . 20 |- ( w = a -> ( ( ph /\ w e. ran G /\ t e. ran G ) <-> ( ph /\ a e. ran G /\ t e. ran G ) ) )
102		fveq2 5873	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = a -> ( F ` w ) = ( F ` a ) )
103	102	eqeq1d 2422	. . . . . . . . . . . . . . . . . . . 20 |- ( w = a -> ( ( F ` w ) = ( F ` t ) <-> ( F ` a ) = ( F ` t ) ) )
104	101, 103	anbi12d 715	. . . . . . . . . . . . . . . . . . 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 4421	. . . . . . . . . . . . . . . . . . . 20 |- ( w = a -> ( t R w <-> t R a ) )
106	105	notbid 295	. . . . . . . . . . . . . . . . . . 19 |- ( w = a -> ( -. t R w <-> -. t R a ) )
107	104, 106	imbi12d 321	. . . . . . . . . . . . . . . . . 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 1751	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ u ph
109		nfcv 2582	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ u w
110		nfmpt1 4507	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/_ u ( u e. ran F |-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
111	41, 110	nfcxfr 2580	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ u G
112	111	nfrn 5089	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ u ran G
113	109, 112	nfel 2595	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ u w e. ran G
114	112	nfcri 2575	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ u t e. ran G
115	108, 113, 114	nf3an 1985	. . . . . . . . . . . . . . . . . . . . 21 |- F/ u ( ph /\ w e. ran G /\ t e. ran G )
116		nfv 1751	. . . . . . . . . . . . . . . . . . . . 21 |- F/ u ( F ` w ) = ( F ` t )
117	115, 116	nfan 1983	. . . . . . . . . . . . . . . . . . . 20 |- F/ u ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) )
118		nfv 1751	. . . . . . . . . . . . . . . . . . . 20 |- F/ u -. t R w
119		simp3 1007	. . . . . . . . . . . . . . . . . . . . . . . . 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 2428	. . . . . . . . . . . . . . . . . . . . . . . 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 1035	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1006	. . . . . . . . . . . . . . . . . . . . . . . . . 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 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( v = w -> ( t R v <-> t R w ) )
125	124	notbid 295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( v = w -> ( -. t R v <-> -. t R w ) )
126	125	ralbidv 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( v = w -> ( A. t e. ( `' F " { u } ) -. t R v <-> A. t e. ( `' F " { u } ) -. t R w ) )
127	126	cbvriotav 6270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1028	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ u e. ran F ) -> E! w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w )
133		riota1 6277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1025	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 460	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1264	. . . . . . . . . . . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . . . . . . . . . . . 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 6281	. . . . . . . . . . . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . . . . . . . . . . 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 1257	. . . . . . . . . . . . . . . . . . . . . 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 3461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ t e. ran G ) -> t e. A )
145	144	3adant2 1024	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ w e. ran G /\ t e. ran G ) -> t e. A )
146	145	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> t e. A )
147	146	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . . . . . 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 731	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1025	. . . . . . . . . . . . . . . . . . . . . . . . 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 6010	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 213	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1257	. . . . . . . . . . . . . . . . . . . . . . . . 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 2461	. . . . . . . . . . . . . . . . . . . . . . . 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 534	. . . . . . . . . . . . . . . . . . . . . . 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 6010	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1026	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ w e. ran G /\ t e. ran G ) -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
160	159	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . 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 1025	. . . . . . . . . . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . . . . . . . . . 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 2790	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A. t e. ( `' F " { u } ) -. t R w /\ t e. ( `' F " { u } ) ) -> -. t R w )
164	143, 162, 163	syl2anc 665	. . . . . . . . . . . . . . . . . . . . 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 1204	. . . . . . . . . . . . . . . . . . . 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 2907	. . . . . . . . . . . . . . . . . . 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 2067	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ a e. ran G /\ t e. ran G ) /\ ( F ` a ) = ( F ` t ) ) -> -. t R a )
169	99, 168	chvarv 2067	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ a e. ran G /\ b e. ran G ) /\ ( F ` a ) = ( F ` b ) ) -> -. b R a )
170	91, 169	chvarv 2067	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ t e. ran G /\ b e. ran G ) /\ ( F ` t ) = ( F ` b ) ) -> -. b R t )
171	83, 170	chvarv 2067	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ t e. ran G /\ w e. ran G ) /\ ( F ` t ) = ( F ` w ) ) -> -. w R t )
172	64, 65, 72, 75, 171	syl31anc 1267	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> -. w R t )
173	172, 167	jca 534	. . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( -. w R t /\ -. t R w ) )
174		weso 4837	. . . . . . . . . . . . . . . 16 |- ( R We A -> R Or A )
175	8, 174	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> R Or A )
176	175	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( F ` w ) = ( F ` t ) ) -> R Or A )
177	176	3ad2antl1 1167	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> R Or A )
178	43	sselda 3461	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w e. ran G ) -> w e. A )
179	178	3adant3 1025	. . . . . . . . . . . . . 14 |- ( ( ph /\ w e. ran G /\ t e. ran G ) -> w e. A )
180	179	adantr 466	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w e. A )
181		sotrieq2 4795	. . . . . . . . . . . . 13 |- ( ( R Or A /\ ( w e. A /\ t e. A ) ) -> ( w = t <-> ( -. w R t /\ -. t R w ) ) )
182	177, 180, 146, 181	syl12anc 1262	. . . . . . . . . . . 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 235	. . . . . . . . . . 11 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w = t )
184	55, 63, 183	syl2anc 665	. . . . . . . . . 10 |- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) ) -> w = t )
185	184	ex 435	. . . . . . . . 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 1264	. . . . . . . 8 |- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> ( ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` t ) -> w = t ) )
187	186	ralrimivva 2844	. . . . . . 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 534	. . . . . 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 6166	. . . . . 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 215	. . . . 5 |- ( ph -> ( F |` ran G ) : ran G -1-1-> ran F )
191		riotaex 6263	. . . . . . . . . . . . . 14 |- ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V
192	191	rgenw 2784	. . . . . . . . . . . . 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 5745	. . . . . . . . . . . 12 |- ( G Fn ran F <-> G : ran F --> ran G )
197	196	biimpi 197	. . . . . . . . . . 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 6029	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> ( G ` u ) e. ran G )
200		fvres 5887	. . . . . . . . . . 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 215	. . . . . . . . . . . . . 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 5965	. . . . . . . . . . . . . 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 665	. . . . . . . . . . . . 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 2508	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ran F ) -> ( G ` u ) e. ( `' F " { u } ) )
207		fvex 5883	. . . . . . . . . . . . . 14 |- ( G ` u ) e. _V
208		eleq1 2492	. . . . . . . . . . . . . . . 16 |- ( w = ( G ` u ) -> ( w e. ( `' F " { u } ) <-> ( G ` u ) e. ( `' F " { u } ) ) )
209		eleq1 2492	. . . . . . . . . . . . . . . . 17 |- ( w = ( G ` u ) -> ( w e. A <-> ( G ` u ) e. A ) )
210		fveq2 5873	. . . . . . . . . . . . . . . . . 18 |- ( w = ( G ` u ) -> ( F ` w ) = ( F ` ( G ` u ) ) )
211	210	eqeq1d 2422	. . . . . . . . . . . . . . . . 17 |- ( w = ( G ` u ) -> ( ( F ` w ) = u <-> ( F ` ( G ` u ) ) = u ) )
212	209, 211	anbi12d 715	. . . . . . . . . . . . . . . 16 |- ( w = ( G ` u ) -> ( ( w e. A /\ ( F ` w ) = u ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
213	208, 212	bibi12d 322	. . . . . . . . . . . . . . 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 317	. . . . . . . . . . . . . 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 3130	. . . . . . . . . . . . 13 |- ( ph -> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
217	216	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ran F ) -> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
218	206, 217	mpbid 213	. . . . . . . . . . 11 |- ( ( ph /\ u e. ran F ) -> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) )
219	218	simprd 464	. . . . . . . . . 10 |- ( ( ph /\ u e. ran F ) -> ( F ` ( G ` u ) ) = u )
220	201, 219	eqtr2d 2462	. . . . . . . . 9 |- ( ( ph /\ u e. ran F ) -> u = ( ( F |` ran G ) ` ( G ` u ) ) )
221		fveq2 5873	. . . . . . . . . . 11 |- ( w = ( G ` u ) -> ( ( F |` ran G ) ` w ) = ( ( F |` ran G ) ` ( G ` u ) ) )
222	221	eqeq2d 2434	. . . . . . . . . 10 |- ( w = ( G ` u ) -> ( u = ( ( F |` ran G ) ` w ) <-> u = ( ( F |` ran G ) ` ( G ` u ) ) ) )
223	222	rspcev 3179	. . . . . . . . 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 665	. . . . . . . 8 |- ( ( ph /\ u e. ran F ) -> E. w e. ran G u = ( ( F |` ran G ) ` w ) )
225	224	ralrimiva 2837	. . . . . . 7 |- ( ph -> A. u e. ran F E. w e. ran G u = ( ( F |` ran G ) ` w ) )
226	51, 225	jca 534	. . . . . 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 6044	. . . . . 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 215	. . . . 5 |- ( ph -> ( F |` ran G ) : ran G -onto-> ran F )
229	190, 228	jca 534	. . . 4 |- ( ph -> ( ( F |` ran G ) : ran G -1-1-> ran F /\ ( F |` ran G ) : ran G -onto-> ran F ) )
230		df-f1o 5600	. . . 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 215	. . 3 |- ( ph -> ( F |` ran G ) : ran G -1-1-onto-> ran F )
232		nfcv 2582	. . . . . 6 |- F/_ v F
233		nfcv 2582	. . . . . . . . 9 |- F/_ v ran F
234		nfriota1 6266	. . . . . . . . 9 |- F/_ v ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
235	233, 234	nfmpt 4506	. . . . . . . 8 |- F/_ v ( u e. ran F |-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
236	41, 235	nfcxfr 2580	. . . . . . 7 |- F/_ v G
237	236	nfrn 5089	. . . . . 6 |- F/_ v ran G
238	232, 237	nfres 5119	. . . . 5 |- F/_ v ( F |` ran G )
239	238, 237, 233	nff1o 5821	. . . 4 |- F/ v ( F |` ran G ) : ran G -1-1-onto-> ran F
240		reseq2 5112	. . . . 5 |- ( v = ran G -> ( F |` v ) = ( F |` ran G ) )
241		id 23	. . . . 5 |- ( v = ran G -> v = ran G )
242		eqidd 2421	. . . . 5 |- ( v = ran G -> ran F = ran F )
243	240, 241, 242	f1oeq123d 5820	. . . 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 3174	. . 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 665	. 2 |- ( ph -> E. v e. ~P A ( F |` v ) : v -1-1-onto-> ran F )
246		reseq2 5112	. . . 4 |- ( v = x -> ( F |` v ) = ( F |` x ) )
247		id 23	. . . 4 |- ( v = x -> v = x )
248		eqidd 2421	. . . 4 |- ( v = x -> ran F = ran F )
249	246, 247, 248	f1oeq123d 5820	. . 3 |- ( v = x -> ( ( F |` v ) : v -1-1-onto-> ran F <-> ( F |` x ) : x -1-1-onto-> ran F ) )
250	249	cbvrexv 3054	. 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 199	1 |- ( ph -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> ran F )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1867   =/= wne 2616   A.wral 2773   E.wrex 2774   E!wreu 2775   _Vcvv 3078   C_ wss 3433   (/)c0 3758   ~Pcpw 3976   {csn 3993   class class class wbr 4417   |-> cmpt 4476   Or wor 4766   We wwe 4804   `'ccnv 4845   dom cdm 4846   ran crn 4847   |` cres 4848   "cima 4849   Fn wfn 5588   -->wf 5589   -1-1->wf1 5590   -onto->wfo 5591   -1-1-onto->wf1o 5592   ` cfv 5593   iota_crio 6258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4540  ax-nul 4548  ax-pow 4595  ax-pr 4653

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-reu 2780  df-rmo 2781  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4477  df-mpt 4478  df-id 4761  df-po 4767  df-so 4768  df-fr 4805  df-we 4807  df-xp 4852  df-rel 4853  df-cnv 4854  df-co 4855  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859  df-iota 5557  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6259

This theorem is referenced by:  wessf1orn  37298