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

Metamath Proof Explorer

Theorem wessf1ornlem

Proof