Theorem ac6sfi 4591

Description: A version of ac6s 4902 for finite sets. (Contributed by Jeffrey Hankins, 26-Jun-2009.)

Hypothesis

Ref	Expression
ac6sfi.1	|- (y = (f` x) -> (ph <-> ps))

Assertion

Ref	Expression
ac6sfi	|- ((A e. Fin /\ A.x e. A E.y e. B ph) -> E.f(f:A-->B /\ A.x e. A ps))

Distinct variable groups:   x,f,A   y,f,B,x   ph,f   ps,y

Proof of Theorem ac6sfi

Step	Hyp	Ref	Expression
1		isfi 4523	. . 3 |- (A e. Fin <-> E.m e. om A ~~ m)
2		relen 4513	. . . . . . 7 |- Rel ~~
3	2	brrelexi 3291	. . . . . 6 |- (A ~~ m -> A e. V)
4		visset 1859	. . . . . . . 8 |- m e. V
5	4	bren 4518	. . . . . . 7 |- (A ~~ m <-> E.h h:A-1-1-onto->m)
6		f1oeq2 3793	. . . . . . . . . . . 12 |- (z = A -> (h:z-1-1-onto->m <-> h:A-1-1-onto->m))
7	6	exbidv 1317	. . . . . . . . . . 11 |- (z = A -> (E.h h:z-1-1-onto->m <-> E.h h:A-1-1-onto->m))
8		raleq1 1832	. . . . . . . . . . . 12 |- (z = A -> (A.x e. z E.y e. B ph <-> A.x e. A E.y e. B ph))
9		feq2 3728	. . . . . . . . . . . . . 14 |- (z = A -> (f:z-->B <-> f:A-->B))
10		raleq1 1832	. . . . . . . . . . . . . 14 |- (z = A -> (A.x e. z ps <-> A.x e. A ps))
11	9, 10	anbi12d 631	. . . . . . . . . . . . 13 |- (z = A -> ((f:z-->B /\ A.x e. z ps) <-> (f:A-->B /\ A.x e. A ps)))
12	11	exbidv 1317	. . . . . . . . . . . 12 |- (z = A -> (E.f(f:z-->B /\ A.x e. z ps) <-> E.f(f:A-->B /\ A.x e. A ps)))
13	8, 12	imbi12d 629	. . . . . . . . . . 11 |- (z = A -> ((A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)) <-> (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps))))
14	7, 13	imbi12d 629	. . . . . . . . . 10 |- (z = A -> ((E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> (E.h h:A-1-1-onto->m -> (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps)))))
15	14	cla4gv 1908	. . . . . . . . 9 |- (A e. V -> (A.z(E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) -> (E.h h:A-1-1-onto->m -> (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps)))))
16		f1oeq3 3794	. . . . . . . . . . . . 13 |- (m = (/) -> (h:z-1-1-onto->m <-> h:z-1-1-onto->(/)))
17	16	exbidv 1317	. . . . . . . . . . . 12 |- (m = (/) -> (E.h h:z-1-1-onto->m <-> E.h h:z-1-1-onto->(/)))
18	17	imbi1d 616	. . . . . . . . . . 11 |- (m = (/) -> ((E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> (E.h h:z-1-1-onto->(/) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
19	18	albidv 1316	. . . . . . . . . 10 |- (m = (/) -> (A.z(E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> A.z(E.h h:z-1-1-onto->(/) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
20		f1oeq3 3794	. . . . . . . . . . . . 13 |- (m = w -> (h:z-1-1-onto->m <-> h:z-1-1-onto->w))
21	20	exbidv 1317	. . . . . . . . . . . 12 |- (m = w -> (E.h h:z-1-1-onto->m <-> E.h h:z-1-1-onto->w))
22	21	imbi1d 616	. . . . . . . . . . 11 |- (m = w -> ((E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> (E.h h:z-1-1-onto->w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
23	22	albidv 1316	. . . . . . . . . 10 |- (m = w -> (A.z(E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> A.z(E.h h:z-1-1-onto->w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
24		f1oeq3 3794	. . . . . . . . . . . . 13 |- (m = suc w -> (h:z-1-1-onto->m <-> h:z-1-1-onto->suc w))
25	24	exbidv 1317	. . . . . . . . . . . 12 |- (m = suc w -> (E.h h:z-1-1-onto->m <-> E.h h:z-1-1-onto->suc w))
26	25	imbi1d 616	. . . . . . . . . . 11 |- (m = suc w -> ((E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> (E.h h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
27	26	albidv 1316	. . . . . . . . . 10 |- (m = suc w -> (A.z(E.h h:z-1-1-onto->m -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))) <-> A.z(E.h h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
28		f1ocnv 3809	. . . . . . . . . . . . . 14 |- (h:z-1-1-onto->(/) -> `'h:(/)-1-1-onto->z)
29		f1o00 3825	. . . . . . . . . . . . . . 15 |- (`'h:(/)-1-1-onto->z <-> (`'h = (/) /\ z = (/)))
30	29	biimpi 149	. . . . . . . . . . . . . 14 |- (`'h:(/)-1-1-onto->z -> (`'h = (/) /\ z = (/)))
31		ax-17 1007	. . . . . . . . . . . . . . . 16 |- (x e. (/) -> A.f x e. (/))
32		ax-17 1007	. . . . . . . . . . . . . . . . 17 |- ((/):z-->B -> A.f(/):z-->B)
33		ax-17 1007	. . . . . . . . . . . . . . . . . 18 |- (x e. z -> A.f x e. z)
34		0ex 2785	. . . . . . . . . . . . . . . . . . 19 |- (/) e. V
35	34	hbsbc1v 1995	. . . . . . . . . . . . . . . . . 18 |- ([(/) / f]ps -> A.f[(/) / f]ps)
36	33, 35	hbral 1732	. . . . . . . . . . . . . . . . 17 |- (A.x e. z [(/) / f]ps -> A.fA.x e. z [(/) / f]ps)
37	32, 36	hban 1045	. . . . . . . . . . . . . . . 16 |- (((/):z-->B /\ A.x e. z [(/) / f]ps) -> A.f((/):z-->B /\ A.x e. z [(/) / f]ps))
38		feq1 3727	. . . . . . . . . . . . . . . . 17 |- (f = (/) -> (f:z-->B <-> (/):z-->B))
39		sbceq1a 1989	. . . . . . . . . . . . . . . . . 18 |- (f = (/) -> (ps <-> [(/) / f]ps))
40	39	ralbidv 1709	. . . . . . . . . . . . . . . . 17 |- (f = (/) -> (A.x e. z ps <-> A.x e. z [(/) / f]ps))
41	38, 40	anbi12d 631	. . . . . . . . . . . . . . . 16 |- (f = (/) -> ((f:z-->B /\ A.x e. z ps) <-> ((/):z-->B /\ A.x e. z [(/) / f]ps)))
42	31, 37, 41	cla4egf 1907	. . . . . . . . . . . . . . 15 |- ((/) e. V -> (((/):z-->B /\ A.x e. z [(/) / f]ps) -> E.f(f:z-->B /\ A.x e. z ps)))
43	34	a1i 8	. . . . . . . . . . . . . . 15 |- ((`'h = (/) /\ z = (/)) -> (/) e. V)
44		f0 3763	. . . . . . . . . . . . . . . . . 18 |- (/):(/)-->B
45		ral0 2412	. . . . . . . . . . . . . . . . . 18 |- A.x e. (/) [(/) / f]ps
46	44, 45	pm3.2i 283	. . . . . . . . . . . . . . . . 17 |- ((/):(/)-->B /\ A.x e. (/) [(/) / f]ps)
47		feq2 3728	. . . . . . . . . . . . . . . . . 18 |- (z = (/) -> ((/):z-->B <-> (/):(/)-->B))
48		raleq1 1832	. . . . . . . . . . . . . . . . . 18 |- (z = (/) -> (A.x e. z [(/) / f]ps <-> A.x e. (/) [(/) / f]ps))
49	47, 48	anbi12d 631	. . . . . . . . . . . . . . . . 17 |- (z = (/) -> (((/):z-->B /\ A.x e. z [(/) / f]ps) <-> ((/):(/)-->B /\ A.x e. (/) [(/) / f]ps)))
50	46, 49	mpbiri 192	. . . . . . . . . . . . . . . 16 |- (z = (/) -> ((/):z-->B /\ A.x e. z [(/) / f]ps))
51	50	adantl 388	. . . . . . . . . . . . . . 15 |- ((`'h = (/) /\ z = (/)) -> ((/):z-->B /\ A.x e. z [(/) / f]ps))
52	42, 43, 51	sylc 68	. . . . . . . . . . . . . 14 |- ((`'h = (/) /\ z = (/)) -> E.f(f:z-->B /\ A.x e. z ps))
53	28, 30, 52	3syl 20	. . . . . . . . . . . . 13 |- (h:z-1-1-onto->(/) -> E.f(f:z-->B /\ A.x e. z ps))
54	53	a1d 12	. . . . . . . . . . . 12 |- (h:z-1-1-onto->(/) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))
55	54	19.23aiv 1333	. . . . . . . . . . 11 |- (E.h h:z-1-1-onto->(/) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))
56	55	ax-gen 999	. . . . . . . . . 10 |- A.z(E.h h:z-1-1-onto->(/) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))
57		f1ores 3811	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((`'h:suc w-1-1->z /\ w (_ suc w) -> (`'h |` w):w-1-1-onto->(`'h"w))
58		f1of1 3796	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (`'h:suc w-1-1-onto->z -> `'h:suc w-1-1->z)
59		sssucid 3050	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- w (_ suc w
60	59	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (`'h:suc w-1-1-onto->z -> w (_ suc w)
61	57, 58, 60	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . 23 |- (`'h:suc w-1-1-onto->z -> (`'h |` w):w-1-1-onto->(`'h"w))
62	61	adantl 388	. . . . . . . . . . . . . . . . . . . . . 22 |- ((w e. om /\ `'h:suc w-1-1-onto->z) -> (`'h |` w):w-1-1-onto->(`'h"w))
63		f1ocnv 3809	. . . . . . . . . . . . . . . . . . . . . 22 |- (h:z-1-1-onto->suc w -> `'h:suc w-1-1-onto->z)
64	62, 63	sylan2 453	. . . . . . . . . . . . . . . . . . . . 21 |- ((w e. om /\ h:z-1-1-onto->suc w) -> (`'h |` w):w-1-1-onto->(`'h"w))
65		f1ocnv 3809	. . . . . . . . . . . . . . . . . . . . 21 |- ((`'h |` w):w-1-1-onto->(`'h"w) -> `'(`'h |` w):(`'h"w)-1-1-onto->w)
66		visset 1859	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- h e. V
67	66	cnvex 3625	. . . . . . . . . . . . . . . . . . . . . . . 24 |- `'h e. V
68		resexg 3484	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (`'h e. V -> (`'h |` w) e. V)
69	67, 68	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . 23 |- (`'h |` w) e. V
70	69	cnvex 3625	. . . . . . . . . . . . . . . . . . . . . 22 |- `'(`'h |` w) e. V
71		f1oeq1 3792	. . . . . . . . . . . . . . . . . . . . . 22 |- (k = `'(`'h |` w) -> (k:(`'h"w)-1-1-onto->w <-> `'(`'h |` w):(`'h"w)-1-1-onto->w))
72	70, 71	cla4ev 1915	. . . . . . . . . . . . . . . . . . . . 21 |- (`'(`'h |` w):(`'h"w)-1-1-onto->w -> E.k k:(`'h"w)-1-1-onto->w)
73	64, 65, 72	3syl 20	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. om /\ h:z-1-1-onto->suc w) -> E.k k:(`'h"w)-1-1-onto->w)
74		pm2.27 62	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.k k:(`'h"w)-1-1-onto->w -> ((E.k k:(`'h"w)-1-1-onto->w -> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))) -> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))))
75		dff1o5 3805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (`'h:suc w-1-1-onto->z <-> (`'h:suc w-1-1->z /\ ran `' h = z))
76	75	biimpi 149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (`'h:suc w-1-1-onto->z -> (`'h:suc w-1-1->z /\ ran `' h = z))
77		pm3.27 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((`'h:suc w-1-1->z /\ ran `' h = z) -> ran `' h = z)
78		imassrn 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (`'h"w) (_ ran `' h
79		sseq2 2135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (ran `' h = z -> ((`'h"w) (_ ran `' h <-> (`'h"w) (_ z))
80	78, 79	mpbii 191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (ran `' h = z -> (`'h"w) (_ z)
81	76, 77, 80	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (`'h:suc w-1-1-onto->z -> (`'h"w) (_ z)
82		ssralv 2166	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((`'h"w) (_ z -> (A.x e. z E.y e. B ph -> A.x e. (`'h"w)E.y e. B ph))
83	63, 81, 82	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> A.x e. (`'h"w)E.y e. B ph))
84	83	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. om /\ h:z-1-1-onto->suc w) -> (A.x e. z E.y e. B ph -> A.x e. (`'h"w)E.y e. B ph))
85	84	imp 348	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> A.x e. (`'h"w)E.y e. B ph)
86		pm2.27 62	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (A.x e. (`'h"w)E.y e. B ph -> ((A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)) -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)))
87		ax-17 1007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f:(`'h"w)-->B /\ A.x e. (`'h"w)ps) -> A.g(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))
88		ax-17 1007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (g:(`'h"w)-->B -> A.f g:(`'h"w)-->B)
89		ax-17 1007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (x e. (`'h"w) -> A.f x e. (`'h"w))
90		visset 1859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- g e. V
91	90	hbsbc1v 1995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ([g / f]ps -> A.f[g / f]ps)
92	89, 91	hbral 1732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (A.x e. (`'h"w)[g / f]ps -> A.fA.x e. (`'h"w)[g / f]ps)
93	88, 92	hban 1045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> A.f(g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps))
94		feq1 3727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f = g -> (f:(`'h"w)-->B <-> g:(`'h"w)-->B))
95		sbequ12 1218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f = g -> (ps <-> [g / f]ps))
96	95	ralbidv 1709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f = g -> (A.x e. (`'h"w)ps <-> A.x e. (`'h"w)[g / f]ps))
97	94, 96	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f = g -> ((f:(`'h"w)-->B /\ A.x e. (`'h"w)ps) <-> (g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps)))
98	87, 93, 97	cbvex 1203	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps) <-> E.g(g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps))
99		ssralv 2166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ({(`'h` w)} (_ z -> (A.x e. z E.y e. B ph -> A.x e. {(`'h` w)}E.y e. B ph))
100	99	imp 348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (({(`'h` w)} (_ z /\ A.x e. z E.y e. B ph) -> A.x e. {(`'h` w)}E.y e. B ph)
101		visset 1859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- w e. V
102	101	sucid 3051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- w e. suc w
103		fnsnfv 3878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((`'h Fn suc w /\ w e. suc w) -> {(`'h` w)} = (`'h"{w}))
104	102, 103	mpan2 700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (`'h Fn suc w -> {(`'h` w)} = (`'h"{w}))
105	104	eqcomd 1523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (`'h Fn suc w -> (`'h"{w}) = {(`'h` w)})
106	105	sseq1d 2140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (`'h Fn suc w -> ((`'h"{w}) (_ z <-> {(`'h` w)} (_ z))
107	106	biimpa 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((`'h Fn suc w /\ (`'h"{w}) (_ z) -> {(`'h` w)} (_ z)
108	100, 107	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((`'h Fn suc w /\ (`'h"{w}) (_ z) /\ A.x e. z E.y e. B ph) -> A.x e. {(`'h` w)}E.y e. B ph)
109		f1ofo 3803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (`'h:suc w-1-1-onto->z -> `'h:suc w-onto->z)
110		fofn 3781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (`'h:suc w-onto->z -> `'h Fn suc w)
111	63, 109, 110	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (h:z-1-1-onto->suc w -> `'h Fn suc w)
112		foima 3784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (`'h:suc w-onto->z -> (`'h"suc w) = z)
113	63, 109, 112	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (h:z-1-1-onto->suc w -> (`'h"suc w) = z)
114		df-suc 2981	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- suc w = (w u. {w})
115	114	imaeq2i 3494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (`'h"suc w) = (`'h"(w u. {w}))
116		imaundi 3545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (`'h"(w u. {w})) = ((`'h"w) u. (`'h"{w}))
117	115, 116	eqtri 1538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (`'h"suc w) = ((`'h"w) u. (`'h"{w}))
118	117	eqeq1i 1525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((`'h"suc w) = z <-> ((`'h"w) u. (`'h"{w})) = z)
119	118	biimpi 149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((`'h"suc w) = z -> ((`'h"w) u. (`'h"{w})) = z)
120		ssun2 2246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (`'h"{w}) (_ ((`'h"w) u. (`'h"{w}))
121		sseq2 2135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((`'h"w) u. (`'h"{w})) = z -> ((`'h"{w}) (_ ((`'h"w) u. (`'h"{w})) <-> (`'h"{w}) (_ z))
122	120, 121	mpbii 191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((`'h"w) u. (`'h"{w})) = z -> (`'h"{w}) (_ z)
123	113, 119, 122	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (h:z-1-1-onto->suc w -> (`'h"{w}) (_ z)
124	111, 123	jca 286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (h:z-1-1-onto->suc w -> (`'h Fn suc w /\ (`'h"{w}) (_ z))
125	108, 124	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((h:z-1-1-onto->suc w /\ A.x e. z E.y e. B ph) -> A.x e. {(`'h` w)}E.y e. B ph)
126	125	adantll 392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> A.x e. {(`'h` w)}E.y e. B ph)
127		ac6sfi.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (y = (f` x) -> (ph <-> ps))
128	127	ac6sfilem3 4590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) /\ (g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps)) -> ((g u. {<.(`'h` w), y>.}):z-->B /\ A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps))
129		snex 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- {<.(`'h` w), y>.} e. V
130	90, 129	unex 3095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (g u. {<.(`'h` w), y>.}) e. V
131		ax-17 1007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (t e. (g u. {<.(`'h` w), y>.}) -> A.f t e. (g u. {<.(`'h` w), y>.}))
132		ax-17 1007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((g u. {<.(`'h` w), y>.}):z-->B -> A.f(g u. {<.(`'h` w), y>.}):z-->B)
133	130	hbsbc1v 1995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ([(g u. {<.(`'h` w), y>.}) / f]ps -> A.f[(g u. {<.(`'h` w), y>.}) / f]ps)
134	33, 133	hbral 1732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps -> A.fA.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps)
135	132, 134	hban 1045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((g u. {<.(`'h` w), y>.}):z-->B /\ A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps) -> A.f((g u. {<.(`'h` w), y>.}):z-->B /\ A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps))
136		feq1 3727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (f = (g u. {<.(`'h` w), y>.}) -> (f:z-->B <-> (g u. {<.(`'h` w), y>.}):z-->B))
137		sbceq1a 1989	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (f = (g u. {<.(`'h` w), y>.}) -> (ps <-> [(g u. {<.(`'h` w), y>.}) / f]ps))
138	137	ralbidv 1709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (f = (g u. {<.(`'h` w), y>.}) -> (A.x e. z ps <-> A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps))
139	136, 138	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (f = (g u. {<.(`'h` w), y>.}) -> ((f:z-->B /\ A.x e. z ps) <-> ((g u. {<.(`'h` w), y>.}):z-->B /\ A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps)))
140	131, 135, 139	cla4egf 1907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((g u. {<.(`'h` w), y>.}) e. V -> (((g u. {<.(`'h` w), y>.}):z-->B /\ A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps) -> E.f(f:z-->B /\ A.x e. z ps)))
141	130, 140	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((g u. {<.(`'h` w), y>.}):z-->B /\ A.x e. z [(g u. {<.(`'h` w), y>.}) / f]ps) -> E.f(f:z-->B /\ A.x e. z ps))
142	128, 141	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) /\ (g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps)) -> E.f(f:z-->B /\ A.x e. z ps))
143	142	3exp1 855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (y e. B -> ([(`'h` w) / x]ph -> ((w e. om /\ `'h:suc w-1-1-onto->z) -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps)))))
144	143	r19.23aiv 1789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (E.y e. B [(`'h` w) / x]ph -> ((w e. om /\ `'h:suc w-1-1-onto->z) -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps))))
145	144	com12 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((w e. om /\ `'h:suc w-1-1-onto->z) -> (E.y e. B [(`'h` w) / x]ph -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps))))
146	145, 63	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((w e. om /\ h:z-1-1-onto->suc w) -> (E.y e. B [(`'h` w) / x]ph -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps))))
147	146	imp 348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ E.y e. B [(`'h` w) / x]ph) -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps)))
148		fvex 3843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (`'h` w) e. V
149		sbcrexg 2045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((`'h` w) e. V -> ([(`'h` w) / x]E.y e. B ph <-> E.y e. B [(`'h` w) / x]ph))
150	148, 149	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ([(`'h` w) / x]E.y e. B ph <-> E.y e. B [(`'h` w) / x]ph)
151	147, 150	sylan2b 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ [(`'h` w) / x]E.y e. B ph) -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps)))
152	148	ralsn 2488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (A.x e. {(`'h` w)}E.y e. B ph <-> [(`'h` w) / x]E.y e. B ph)
153	151, 152	sylan2b 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. {(`'h` w)}E.y e. B ph) -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps)))
154	126, 153	syldan 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> E.f(f:z-->B /\ A.x e. z ps)))
155	154	com12 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> E.f(f:z-->B /\ A.x e. z ps)))
156	155	19.23aiv 1333	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.g(g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> E.f(f:z-->B /\ A.x e. z ps)))
157	98, 156	sylbi 197	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps) -> (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> E.f(f:z-->B /\ A.x e. z ps)))
158	86, 157	syl6 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.x e. (`'h"w)E.y e. B ph -> ((A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)) -> (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> E.f(f:z-->B /\ A.x e. z ps))))
159	158	com3r 35	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> (A.x e. (`'h"w)E.y e. B ph -> ((A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)) -> E.f(f:z-->B /\ A.x e. z ps))))
160	85, 159	mpd 26	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((w e. om /\ h:z-1-1-onto->suc w) /\ A.x e. z E.y e. B ph) -> ((A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)) -> E.f(f:z-->B /\ A.x e. z ps)))
161	160	ex 371	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((w e. om /\ h:z-1-1-onto->suc w) -> (A.x e. z E.y e. B ph -> ((A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)) -> E.f(f:z-->B /\ A.x e. z ps))))
162	161	com3r 35	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)) -> ((w e. om /\ h:z-1-1-onto->suc w) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))))
163	74, 162	syl6 22	. . . . . . . . . . . . . . . . . . . . 21 |- (E.k k:(`'h"w)-1-1-onto->w -> ((E.k k:(`'h"w)-1-1-onto->w -> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))) -> ((w e. om /\ h:z-1-1-onto->suc w) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
164	163	com3r 35	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. om /\ h:z-1-1-onto->suc w) -> (E.k k:(`'h"w)-1-1-onto->w -> ((E.k k:(`'h"w)-1-1-onto->w -> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
165	73, 164	mpd 26	. . . . . . . . . . . . . . . . . . 19 |- ((w e. om /\ h:z-1-1-onto->suc w) -> ((E.k k:(`'h"w)-1-1-onto->w -> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))))
166		imaexg 3508	. . . . . . . . . . . . . . . . . . . . 21 |- (`'h e. V -> (`'h"w) e. V)
167	67, 166	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 |- (`'h"w) e. V
168		f1oeq2 3793	. . . . . . . . . . . . . . . . . . . . . 22 |- (t = (`'h"w) -> (k:t-1-1-onto->w <-> k:(`'h"w)-1-1-onto->w))
169	168	exbidv 1317	. . . . . . . . . . . . . . . . . . . . 21 |- (t = (`'h"w) -> (E.k k:t-1-1-onto->w <-> E.k k:(`'h"w)-1-1-onto->w))
170		raleq1 1832	. . . . . . . . . . . . . . . . . . . . . 22 |- (t = (`'h"w) -> (A.x e. t E.y e. B ph <-> A.x e. (`'h"w)E.y e. B ph))
171		feq2 3728	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (t = (`'h"w) -> (f:t-->B <-> f:(`'h"w)-->B))
172		raleq1 1832	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (t = (`'h"w) -> (A.x e. t ps <-> A.x e. (`'h"w)ps))
173	171, 172	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . 23 |- (t = (`'h"w) -> ((f:t-->B /\ A.x e. t ps) <-> (f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)))
174	173	exbidv 1317	. . . . . . . . . . . . . . . . . . . . . 22 |- (t = (`'h"w) -> (E.f(f:t-->B /\ A.x e. t ps) <-> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)))
175	170, 174	imbi12d 629	. . . . . . . . . . . . . . . . . . . . 21 |- (t = (`'h"w) -> ((A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps)) <-> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))))
176	169, 175	imbi12d 629	. . . . . . . . . . . . . . . . . . . 20 |- (t = (`'h"w) -> ((E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))) <-> (E.k k:(`'h"w)-1-1-onto->w -> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps)))))
177	167, 176	cla4v 1914	. . . . . . . . . . . . . . . . . . 19 |- (A.t(E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))) -> (E.k k:(`'h"w)-1-1-onto->w -> (A.x e. (`'h"w)E.y e. B ph -> E.f(f:(`'h"w)-->B /\ A.x e. (`'h"w)ps))))
178	165, 177	syl5 21	. . . . . . . . . . . . . . . . . 18 |- ((w e. om /\ h:z-1-1-onto->suc w) -> (A.t(E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))))
179	178	ex 371	. . . . . . . . . . . . . . . . 17 |- (w e. om -> (h:z-1-1-onto->suc w -> (A.t(E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))) -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
180	179	com23 32	. . . . . . . . . . . . . . . 16 |- (w e. om -> (A.t(E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))) -> (h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps)))))
181	180	imp 348	. . . . . . . . . . . . . . 15 |- ((w e. om /\ A.t(E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps)))) -> (h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))))
182	181	19.23adv 1251	. . . . . . . . . . . . . 14 |- ((w e. om /\ A.t(E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps)))) -> (E.h h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))))
183		f1oeq1 3792	. . . . . . . . . . . . . . . . 17 |- (h = k -> (h:t-1-1-onto->w <-> k:t-1-1-onto->w))
184	183	cbvexv 1353	. . . . . . . . . . . . . . . 16 |- (E.h h:t-1-1-onto->w <-> E.k k:t-1-1-onto->w)
185	184	imbi1i 184	. . . . . . . . . . . . . . 15 |- ((E.h h:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))) <-> (E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))))
186	185	albii 1035	. . . . . . . . . . . . . 14 |- (A.t(E.h h:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))) <-> A.t(E.k k:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps))))
187	182, 186	sylan2b 454	. . . . . . . . . . . . 13 |- ((w e. om /\ A.t(E.h h:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps)))) -> (E.h h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))))
188	187	19.21aiv 1324	. . . . . . . . . . . 12 |- ((w e. om /\ A.t(E.h h:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.f(f:t-->B /\ A.x e. t ps)))) -> A.z(E.h h:z-1-1-onto->suc w -> (A.x e. z E.y e. B ph -> E.f(f:z-->B /\ A.x e. z ps))))
189	188	ex 371	. . . . . . . . . . 11 |- (w e. om -> (A.t(E.h h:t-1-1-onto->w -> (A.x e. t E.y e. B ph -> E.