wessf1ornlem

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)

	Ref	Expression
Hypotheses	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	wessf1ornlem	\|- ( ph -> E. x e. ~P A ( F \|` x ) : x -1-1-onto-> ran F )

Proof

Step	Hyp	Ref	Expression
1		wessf1ornlem.f	\|- ( ph -> F Fn A )
2		wessf1ornlem.a	\|- ( ph -> A e. V )
3		wessf1ornlem.r	\|- ( ph -> R We A )
4		wessf1ornlem.g	\|- G = ( y e. ran F \|-> ( iota_ x e. ( `' F " { y } ) A. z e. ( `' F " { y } ) -. z R x ) )
5		cnvimass	\|- ( `' F " { u } ) C_ dom F
6	1	fndmd	\|- ( ph -> dom F = A )
7	6	adantr	\|- ( ( ph /\ u e. ran F ) -> dom F = A )
8	5 7	sseqtrid	\|- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) C_ A )
9	3	adantr	\|- ( ( ph /\ u e. ran F ) -> R We A )
10	5 6	sseqtrid	\|- ( ph -> ( `' F " { u } ) C_ A )
11	2 10	ssexd	\|- ( ph -> ( `' F " { u } ) e. _V )
12	11	adantr	\|- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) e. _V )
13		inisegn0	\|- ( u e. ran F <-> ( `' F " { u } ) =/= (/) )
14	13	bilani	\|- ( ( ph /\ u e. ran F ) -> ( `' F " { u } ) =/= (/) )
15		wereu	\|- ( ( 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 )
16	9 12 8 14 15	syl13anc	\|- ( ( ph /\ u e. ran F ) -> E! v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v )
17		riotacl	\|- ( 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 } ) )
18	16 17	syl	\|- ( ( ph /\ u e. ran F ) -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. ( `' F " { u } ) )
19	8 18	sseldd	\|- ( ( ph /\ u e. ran F ) -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. A )
20	19	ralrimiva	\|- ( ph -> A. u e. ran F ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. A )
21		sneq	\|- ( y = u -> { y } = { u } )
22	21	imaeq2d	\|- ( y = u -> ( `' F " { y } ) = ( `' F " { u } ) )
23	22	raleqdv	\|- ( y = u -> ( A. z e. ( `' F " { y } ) -. z R x <-> A. z e. ( `' F " { u } ) -. z R x ) )
24	22 23	riotaeqbidv	\|- ( 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 ) )
25		breq1	\|- ( z = t -> ( z R x <-> t R x ) )
26	25	notbid	\|- ( z = t -> ( -. z R x <-> -. t R x ) )
27	26	cbvralvw	\|- ( A. z e. ( `' F " { u } ) -. z R x <-> A. t e. ( `' F " { u } ) -. t R x )
28		breq2	\|- ( x = v -> ( t R x <-> t R v ) )
29	28	notbid	\|- ( x = v -> ( -. t R x <-> -. t R v ) )
30	29	ralbidv	\|- ( x = v -> ( A. t e. ( `' F " { u } ) -. t R x <-> A. t e. ( `' F " { u } ) -. t R v ) )
31	27 30	bitrid	\|- ( x = v -> ( A. z e. ( `' F " { u } ) -. z R x <-> A. t e. ( `' F " { u } ) -. t R v ) )
32	31	cbvriotavw	\|- ( 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 )
33	24 32	eqtrdi	\|- ( 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 ) )
34	33	cbvmptv	\|- ( 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 ) )
35	4 34	eqtri	\|- G = ( u e. ran F \|-> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
36	35	rnmptss	\|- ( A. u e. ran F ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. A -> ran G C_ A )
37	20 36	syl	\|- ( ph -> ran G C_ A )
38	2 37	sselpwd	\|- ( ph -> ran G e. ~P A )
39		dffn3	\|- ( F Fn A <-> F : A --> ran F )
40	1 39	sylib	\|- ( ph -> F : A --> ran F )
41	40 37	fssresd	\|- ( ph -> ( F \|` ran G ) : ran G --> ran F )
42		fvres	\|- ( w e. ran G -> ( ( F \|` ran G ) ` w ) = ( F ` w ) )
43	42	eqcomd	\|- ( w e. ran G -> ( F ` w ) = ( ( F \|` ran G ) ` w ) )
44	43	ad2antrr	\|- ( ( ( w e. ran G /\ t e. ran G ) /\ ( ( F \|` ran G ) ` w ) = ( ( F \|` ran G ) ` t ) ) -> ( F ` w ) = ( ( F \|` ran G ) ` w ) )
45		simpr	\|- ( ( ( w e. ran G /\ t e. ran G ) /\ ( ( F \|` ran G ) ` w ) = ( ( F \|` ran G ) ` t ) ) -> ( ( F \|` ran G ) ` w ) = ( ( F \|` ran G ) ` t ) )
46		fvres	\|- ( t e. ran G -> ( ( F \|` ran G ) ` t ) = ( F ` t ) )
47	46	ad2antlr	\|- ( ( ( w e. ran G /\ t e. ran G ) /\ ( ( F \|` ran G ) ` w ) = ( ( F \|` ran G ) ` t ) ) -> ( ( F \|` ran G ) ` t ) = ( F ` t ) )
48	44 45 47	3eqtrd	\|- ( ( ( w e. ran G /\ t e. ran G ) /\ ( ( F \|` ran G ) ` w ) = ( ( F \|` ran G ) ` t ) ) -> ( F ` w ) = ( F ` t ) )
49	48	3adantl1	\|- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( ( F \|` ran G ) ` w ) = ( ( F \|` ran G ) ` t ) ) -> ( F ` w ) = ( F ` t ) )
50		simpl1	\|- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ph )
51		simpl3	\|- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> t e. ran G )
52		simpl2	\|- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w e. ran G )
53		id	\|- ( ( F ` w ) = ( F ` t ) -> ( F ` w ) = ( F ` t ) )
54	53	eqcomd	\|- ( ( F ` w ) = ( F ` t ) -> ( F ` t ) = ( F ` w ) )
55	54	adantl	\|- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( F ` t ) = ( F ` w ) )
56		eleq1w	\|- ( b = w -> ( b e. ran G <-> w e. ran G ) )
57	56	3anbi3d	\|- ( b = w -> ( ( ph /\ t e. ran G /\ b e. ran G ) <-> ( ph /\ t e. ran G /\ w e. ran G ) ) )
58		fveq2	\|- ( b = w -> ( F ` b ) = ( F ` w ) )
59	58	eqeq2d	\|- ( b = w -> ( ( F ` t ) = ( F ` b ) <-> ( F ` t ) = ( F ` w ) ) )
60	57 59	anbi12d	\|- ( 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 ) ) ) )
61		breq1	\|- ( b = w -> ( b R t <-> w R t ) )
62	61	notbid	\|- ( b = w -> ( -. b R t <-> -. w R t ) )
63	60 62	imbi12d	\|- ( 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 ) ) )
64		eleq1w	\|- ( a = t -> ( a e. ran G <-> t e. ran G ) )
65	64	3anbi2d	\|- ( a = t -> ( ( ph /\ a e. ran G /\ b e. ran G ) <-> ( ph /\ t e. ran G /\ b e. ran G ) ) )
66		fveqeq2	\|- ( a = t -> ( ( F ` a ) = ( F ` b ) <-> ( F ` t ) = ( F ` b ) ) )
67	65 66	anbi12d	\|- ( 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 ) ) ) )
68		breq2	\|- ( a = t -> ( b R a <-> b R t ) )
69	68	notbid	\|- ( a = t -> ( -. b R a <-> -. b R t ) )
70	67 69	imbi12d	\|- ( 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 ) ) )
71		eleq1w	\|- ( t = b -> ( t e. ran G <-> b e. ran G ) )
72	71	3anbi3d	\|- ( t = b -> ( ( ph /\ a e. ran G /\ t e. ran G ) <-> ( ph /\ a e. ran G /\ b e. ran G ) ) )
73		fveq2	\|- ( t = b -> ( F ` t ) = ( F ` b ) )
74	73	eqeq2d	\|- ( t = b -> ( ( F ` a ) = ( F ` t ) <-> ( F ` a ) = ( F ` b ) ) )
75	72 74	anbi12d	\|- ( 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 ) ) ) )
76		breq1	\|- ( t = b -> ( t R a <-> b R a ) )
77	76	notbid	\|- ( t = b -> ( -. t R a <-> -. b R a ) )
78	75 77	imbi12d	\|- ( 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 ) ) )
79		eleq1w	\|- ( w = a -> ( w e. ran G <-> a e. ran G ) )
80	79	3anbi2d	\|- ( w = a -> ( ( ph /\ w e. ran G /\ t e. ran G ) <-> ( ph /\ a e. ran G /\ t e. ran G ) ) )
81		fveqeq2	\|- ( w = a -> ( ( F ` w ) = ( F ` t ) <-> ( F ` a ) = ( F ` t ) ) )
82	80 81	anbi12d	\|- ( 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 ) ) ) )
83		breq2	\|- ( w = a -> ( t R w <-> t R a ) )
84	83	notbid	\|- ( w = a -> ( -. t R w <-> -. t R a ) )
85	82 84	imbi12d	\|- ( 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 ) ) )
86	35	elrnmpt	\|- ( 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 ) ) )
87	86	elv	\|- ( w e. ran G <-> E. u e. ran F w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
88	87	birani	\|- ( ( 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 ) )
89	88	3ad2antl2	\|- ( ( ( 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 ) )
90		simp3	\|- ( ( ( 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 ) )
91	90	eqcomd	\|- ( ( ( 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 )
92		simp11	\|- ( ( ( 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 )
93		id	\|- ( 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 ) )
94		breq2	\|- ( v = w -> ( t R v <-> t R w ) )
95	94	notbid	\|- ( v = w -> ( -. t R v <-> -. t R w ) )
96	95	ralbidv	\|- ( v = w -> ( A. t e. ( `' F " { u } ) -. t R v <-> A. t e. ( `' F " { u } ) -. t R w ) )
97	96	cbvriotavw	\|- ( 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 )
98	93 97	eqtr2di	\|- ( 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 )
99	98	3ad2ant3	\|- ( ( 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 )
100	96	cbvreuvw	\|- ( 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 )
101	16 100	sylib	\|- ( ( ph /\ u e. ran F ) -> E! w e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R w )
102		riota1	\|- ( 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 ) )
103	101 102	syl	\|- ( ( 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 ) )
104	103	3adant3	\|- ( ( 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 ) )
105	99 104	mpbird	\|- ( ( 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 ) )
106	105	simpld	\|- ( ( ph /\ u e. ran F /\ w = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) ) -> w e. ( `' F " { u } ) )
107	92 106	syld3an1	\|- ( ( ( 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 } ) )
108		simp2	\|- ( ( ( 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 )
109	92 108 16	syl2anc	\|- ( ( ( 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 )
110	96	riota2	\|- ( ( 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 ) )
111	107 109 110	syl2anc	\|- ( ( ( 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 ) )
112	91 111	mpbird	\|- ( ( ( 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 )
113	112	3adant1r	\|- ( ( ( ( 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 )
114	37	sselda	\|- ( ( ph /\ t e. ran G ) -> t e. A )
115	114	3adant2	\|- ( ( ph /\ w e. ran G /\ t e. ran G ) -> t e. A )
116	115	adantr	\|- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> t e. A )
117	116	3ad2ant1	\|- ( ( ( ( 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 )
118	54	ad2antlr	\|- ( ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) /\ u e. ran F ) -> ( F ` t ) = ( F ` w ) )
119	118	3adant3	\|- ( ( ( ( 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 ) )
120		fniniseg	\|- ( F Fn A -> ( w e. ( `' F " { u } ) <-> ( w e. A /\ ( F ` w ) = u ) ) )
121	92 1 120	3syl	\|- ( ( ( 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 ) ) )
122	107 121	mpbid	\|- ( ( ( 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 ) )
123	122	simprd	\|- ( ( ( 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 )
124	123	3adant1r	\|- ( ( ( ( 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 )
125	119 124	eqtrd	\|- ( ( ( ( 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 )
126		fniniseg	\|- ( F Fn A -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
127	1 126	syl	\|- ( ph -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
128	127	3ad2ant1	\|- ( ( ph /\ w e. ran G /\ t e. ran G ) -> ( t e. ( `' F " { u } ) <-> ( t e. A /\ ( F ` t ) = u ) ) )
129	128	ad2antrr	\|- ( ( ( ( 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 ) ) )
130	129	3adant3	\|- ( ( ( ( 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 ) ) )
131	117 125 130	mpbir2and	\|- ( ( ( ( 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 } ) )
132		rspa	\|- ( ( A. t e. ( `' F " { u } ) -. t R w /\ t e. ( `' F " { u } ) ) -> -. t R w )
133	113 131 132	syl2anc	\|- ( ( ( ( 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 )
134	133	rexlimdv3a	\|- ( ( ( 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 ) )
135	89 134	mpd	\|- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> -. t R w )
136	85 135	chvarvv	\|- ( ( ( ph /\ a e. ran G /\ t e. ran G ) /\ ( F ` a ) = ( F ` t ) ) -> -. t R a )
137	78 136	chvarvv	\|- ( ( ( ph /\ a e. ran G /\ b e. ran G ) /\ ( F ` a ) = ( F ` b ) ) -> -. b R a )
138	70 137	chvarvv	\|- ( ( ( ph /\ t e. ran G /\ b e. ran G ) /\ ( F ` t ) = ( F ` b ) ) -> -. b R t )
139	63 138	chvarvv	\|- ( ( ( ph /\ t e. ran G /\ w e. ran G ) /\ ( F ` t ) = ( F ` w ) ) -> -. w R t )
140	50 51 52 55 139	syl31anc	\|- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> -. w R t )
141		weso	\|- ( R We A -> R Or A )
142	3 141	syl	\|- ( ph -> R Or A )
143	142	adantr	\|- ( ( ph /\ ( F ` w ) = ( F ` t ) ) -> R Or A )
144	143	3ad2antl1	\|- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> R Or A )
145	37	sselda	\|- ( ( ph /\ w e. ran G ) -> w e. A )
146	145	3adant3	\|- ( ( ph /\ w e. ran G /\ t e. ran G ) -> w e. A )
147	146	adantr	\|- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w e. A )
148		sotrieq2	\|- ( ( R Or A /\ ( w e. A /\ t e. A ) ) -> ( w = t <-> ( -. w R t /\ -. t R w ) ) )
149	144 147 116 148	syl12anc	\|- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> ( w = t <-> ( -. w R t /\ -. t R w ) ) )
150	140 135 149	mpbir2and	\|- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( F ` w ) = ( F ` t ) ) -> w = t )
151	49 150	syldan	\|- ( ( ( ph /\ w e. ran G /\ t e. ran G ) /\ ( ( F \|` ran G ) ` w ) = ( ( F \|` ran G ) ` t ) ) -> w = t )
152	151	ex	\|- ( ( ph /\ w e. ran G /\ t e. ran G ) -> ( ( ( F \|` ran G ) ` w ) = ( ( F \|` ran G ) ` t ) -> w = t ) )
153	152	3expb	\|- ( ( ph /\ ( w e. ran G /\ t e. ran G ) ) -> ( ( ( F \|` ran G ) ` w ) = ( ( F \|` ran G ) ` t ) -> w = t ) )
154	153	ralrimivva	\|- ( ph -> A. w e. ran G A. t e. ran G ( ( ( F \|` ran G ) ` w ) = ( ( F \|` ran G ) ` t ) -> w = t ) )
155		dff13	\|- ( ( 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 ) ) )
156	41 154 155	sylanbrc	\|- ( ph -> ( F \|` ran G ) : ran G -1-1-> ran F )
157		riotaex	\|- ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V
158	157	rgenw	\|- A. u e. ran F ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V
159	35	fnmpt	\|- ( A. u e. ran F ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V -> G Fn ran F )
160	158 159	mp1i	\|- ( ph -> G Fn ran F )
161		dffn3	\|- ( G Fn ran F <-> G : ran F --> ran G )
162	160 161	sylib	\|- ( ph -> G : ran F --> ran G )
163	162	ffvelcdmda	\|- ( ( ph /\ u e. ran F ) -> ( G ` u ) e. ran G )
164	163	fvresd	\|- ( ( ph /\ u e. ran F ) -> ( ( F \|` ran G ) ` ( G ` u ) ) = ( F ` ( G ` u ) ) )
165		simpr	\|- ( ( ph /\ u e. ran F ) -> u e. ran F )
166	157	a1i	\|- ( ( ph /\ u e. ran F ) -> ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) e. _V )
167	4 33 165 166	fvmptd3	\|- ( ( ph /\ u e. ran F ) -> ( G ` u ) = ( iota_ v e. ( `' F " { u } ) A. t e. ( `' F " { u } ) -. t R v ) )
168	167 18	eqeltrd	\|- ( ( ph /\ u e. ran F ) -> ( G ` u ) e. ( `' F " { u } ) )
169		fvex	\|- ( G ` u ) e. _V
170		eleq1	\|- ( w = ( G ` u ) -> ( w e. ( `' F " { u } ) <-> ( G ` u ) e. ( `' F " { u } ) ) )
171		eleq1	\|- ( w = ( G ` u ) -> ( w e. A <-> ( G ` u ) e. A ) )
172		fveqeq2	\|- ( w = ( G ` u ) -> ( ( F ` w ) = u <-> ( F ` ( G ` u ) ) = u ) )
173	171 172	anbi12d	\|- ( w = ( G ` u ) -> ( ( w e. A /\ ( F ` w ) = u ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
174	170 173	bibi12d	\|- ( 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 ) ) ) )
175	174	imbi2d	\|- ( 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 ) ) ) ) )
176	1 120	syl	\|- ( ph -> ( w e. ( `' F " { u } ) <-> ( w e. A /\ ( F ` w ) = u ) ) )
177	169 175 176	vtocl	\|- ( ph -> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
178	177	adantr	\|- ( ( ph /\ u e. ran F ) -> ( ( G ` u ) e. ( `' F " { u } ) <-> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) ) )
179	168 178	mpbid	\|- ( ( ph /\ u e. ran F ) -> ( ( G ` u ) e. A /\ ( F ` ( G ` u ) ) = u ) )
180	179	simprd	\|- ( ( ph /\ u e. ran F ) -> ( F ` ( G ` u ) ) = u )
181	164 180	eqtr2d	\|- ( ( ph /\ u e. ran F ) -> u = ( ( F \|` ran G ) ` ( G ` u ) ) )
182		fveq2	\|- ( w = ( G ` u ) -> ( ( F \|` ran G ) ` w ) = ( ( F \|` ran G ) ` ( G ` u ) ) )
183	182	rspceeqv	\|- ( ( ( G ` u ) e. ran G /\ u = ( ( F \|` ran G ) ` ( G ` u ) ) ) -> E. w e. ran G u = ( ( F \|` ran G ) ` w ) )
184	163 181 183	syl2anc	\|- ( ( ph /\ u e. ran F ) -> E. w e. ran G u = ( ( F \|` ran G ) ` w ) )
185	184	ralrimiva	\|- ( ph -> A. u e. ran F E. w e. ran G u = ( ( F \|` ran G ) ` w ) )
186		dffo3	\|- ( ( 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 ) ) )
187	41 185 186	sylanbrc	\|- ( ph -> ( F \|` ran G ) : ran G -onto-> ran F )
188		df-f1o	\|- ( ( 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 ) )
189	156 187 188	sylanbrc	\|- ( ph -> ( F \|` ran G ) : ran G -1-1-onto-> ran F )
190		reseq2	\|- ( v = ran G -> ( F \|` v ) = ( F \|` ran G ) )
191		id	\|- ( v = ran G -> v = ran G )
192		eqidd	\|- ( v = ran G -> ran F = ran F )
193	190 191 192	f1oeq123d	\|- ( v = ran G -> ( ( F \|` v ) : v -1-1-onto-> ran F <-> ( F \|` ran G ) : ran G -1-1-onto-> ran F ) )
194	193	rspcev	\|- ( ( 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 )
195	38 189 194	syl2anc	\|- ( ph -> E. v e. ~P A ( F \|` v ) : v -1-1-onto-> ran F )
196		reseq2	\|- ( v = x -> ( F \|` v ) = ( F \|` x ) )
197		id	\|- ( v = x -> v = x )
198		eqidd	\|- ( v = x -> ran F = ran F )
199	196 197 198	f1oeq123d	\|- ( v = x -> ( ( F \|` v ) : v -1-1-onto-> ran F <-> ( F \|` x ) : x -1-1-onto-> ran F ) )
200	199	cbvrexvw	\|- ( 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 )
201	195 200	sylib	\|- ( ph -> E. x e. ~P A ( F \|` x ) : x -1-1-onto-> ran F )

Metamath Proof Explorer

Theorem wessf1ornlem

Proof