Theorem ac6sfilem3 4590

Description: Lemma for ac6sfi 4591.

Hypothesis

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

Assertion

Ref	Expression
ac6sfilem3	|- (((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))

Distinct variable groups:   f,h,x,z,g,w,y,B   ph,f,g,h,w,z   ps,g,h,w,y,z

Proof of Theorem ac6sfilem3

Step	Hyp	Ref	Expression
1		fun 3748	. . . . 5 |- (((g:(`'h"w)-->B /\ {<.(`'h` w), y>.}:{(`'h` w)}-->B) /\ ((`'h"w) i^i {(`'h` w)}) = (/)) -> (g u. {<.(`'h` w), y>.}):((`'h"w) u. {(`'h` w)})-->(B u. B))
2		simprl 414	. . . . . 6 |- (((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:(`'h"w)-->B)
3		fvex 3843	. . . . . . . 8 |- (`'h` w) e. V
4		visset 1859	. . . . . . . 8 |- y e. V
5	3, 4	f1osn 3830	. . . . . . 7 |- {<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y}
6		3simp1 794	. . . . . . . . . . 11 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> y e. B)
7	6	adantr 389	. . . . . . . . . 10 |- (((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)) -> y e. B)
8	4	snss 2525	. . . . . . . . . 10 |- (y e. B <-> {y} (_ B)
9	7, 8	sylib 196	. . . . . . . . 9 |- (((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)) -> {y} (_ B)
10		fss 3742	. . . . . . . . . 10 |- (({<.(`'h` w), y>.}:{(`'h` w)}-->{y} /\ {y} (_ B) -> {<.(`'h` w), y>.}:{(`'h` w)}-->B)
11	10	expcom 372	. . . . . . . . 9 |- ({y} (_ B -> ({<.(`'h` w), y>.}:{(`'h` w)}-->{y} -> {<.(`'h` w), y>.}:{(`'h` w)}-->B))
12	9, 11	syl 10	. . . . . . . 8 |- (((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)) -> ({<.(`'h` w), y>.}:{(`'h` w)}-->{y} -> {<.(`'h` w), y>.}:{(`'h` w)}-->B))
13		f1of 3797	. . . . . . . 8 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> {<.(`'h` w), y>.}:{(`'h` w)}-->{y})
14	12, 13	syl5 21	. . . . . . 7 |- (((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)) -> ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> {<.(`'h` w), y>.}:{(`'h` w)}-->B))
15	5, 14	mpi 44	. . . . . 6 |- (((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)) -> {<.(`'h` w), y>.}:{(`'h` w)}-->B)
16	2, 15	jca 286	. . . . 5 |- (((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:(`'h"w)-->B /\ {<.(`'h` w), y>.}:{(`'h` w)}-->B))
17		nnord 3227	. . . . . . . . . . . . . 14 |- (w e. om -> Ord w)
18		nordeq 2994	. . . . . . . . . . . . . . . 16 |- ((Ord w /\ t e. w) -> w =/= t)
19		necom 1682	. . . . . . . . . . . . . . . . 17 |- (w =/= t <-> t =/= w)
20		df-ne 1630	. . . . . . . . . . . . . . . . 17 |- (t =/= w <-> -. t = w)
21	19, 20	bitri 171	. . . . . . . . . . . . . . . 16 |- (w =/= t <-> -. t = w)
22	18, 21	sylib 196	. . . . . . . . . . . . . . 15 |- ((Ord w /\ t e. w) -> -. t = w)
23	22	ex 371	. . . . . . . . . . . . . 14 |- (Ord w -> (t e. w -> -. t = w))
24	17, 23	syl 10	. . . . . . . . . . . . 13 |- (w e. om -> (t e. w -> -. t = w))
25	24	ad2antrl 406	. . . . . . . . . . . 12 |- (([(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> (t e. w -> -. t = w))
26	25	3adant1 803	. . . . . . . . . . 11 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> (t e. w -> -. t = w))
27	26	adantr 389	. . . . . . . . . 10 |- (((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)) -> (t e. w -> -. t = w))
28	27	imp 348	. . . . . . . . 9 |- ((((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)) /\ t e. w) -> -. t = w)
29		f1fveq 3990	. . . . . . . . . 10 |- ((`'h:suc w-1-1->z /\ (t e. suc w /\ w e. suc w)) -> ((`'h` t) = (`'h` w) <-> t = w))
30		f1of1 3796	. . . . . . . . . . . . 13 |- (`'h:suc w-1-1-onto->z -> `'h:suc w-1-1->z)
31	30	ad2antll 407	. . . . . . . . . . . 12 |- (([(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> `'h:suc w-1-1->z)
32	31	3adant1 803	. . . . . . . . . . 11 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> `'h:suc w-1-1->z)
33	32	ad2antrr 404	. . . . . . . . . 10 |- ((((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)) /\ t e. w) -> `'h:suc w-1-1->z)
34		elelsuc 3045	. . . . . . . . . . . 12 |- (t e. w -> t e. suc w)
35	34	adantl 388	. . . . . . . . . . 11 |- ((((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)) /\ t e. w) -> t e. suc w)
36		visset 1859	. . . . . . . . . . . 12 |- w e. V
37	36	sucid 3051	. . . . . . . . . . 11 |- w e. suc w
38	35, 37	jctir 291	. . . . . . . . . 10 |- ((((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)) /\ t e. w) -> (t e. suc w /\ w e. suc w))
39	29, 33, 38	sylanc 473	. . . . . . . . 9 |- ((((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)) /\ t e. w) -> ((`'h` t) = (`'h` w) <-> t = w))
40	28, 39	mtbird 720	. . . . . . . 8 |- ((((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)) /\ t e. w) -> -. (`'h` t) = (`'h` w))
41	40	nrexdv 1776	. . . . . . 7 |- (((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.t e. w (`'h` t) = (`'h` w))
42		fvelimab 3876	. . . . . . . 8 |- ((`'h Fn suc w /\ w (_ suc w) -> ((`'h` w) e. (`'h"w) <-> E.t e. w (`'h` t) = (`'h` w)))
43		f1ofn 3798	. . . . . . . . . . 11 |- (`'h:suc w-1-1-onto->z -> `'h Fn suc w)
44	43	ad2antll 407	. . . . . . . . . 10 |- (([(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> `'h Fn suc w)
45	44	3adant1 803	. . . . . . . . 9 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> `'h Fn suc w)
46	45	adantr 389	. . . . . . . 8 |- (((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)) -> `'h Fn suc w)
47		sssucid 3050	. . . . . . . . 9 |- w (_ suc w
48	47	a1i 8	. . . . . . . 8 |- (((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)) -> w (_ suc w)
49	42, 46, 48	sylanc 473	. . . . . . 7 |- (((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)) -> ((`'h` w) e. (`'h"w) <-> E.t e. w (`'h` t) = (`'h` w)))
50	41, 49	mtbird 720	. . . . . 6 |- (((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)) -> -. (`'h` w) e. (`'h"w))
51		disjsn 2502	. . . . . 6 |- (((`'h"w) i^i {(`'h` w)}) = (/) <-> -. (`'h` w) e. (`'h"w))
52	50, 51	sylibr 198	. . . . 5 |- (((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)) -> ((`'h"w) i^i {(`'h` w)}) = (/))
53	1, 16, 52	sylanc 473	. . . 4 |- (((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>.}):((`'h"w) u. {(`'h` w)})-->(B u. B))
54		unidm 2227	. . . . . 6 |- (B u. B) = B
55	54	a1i 8	. . . . 5 |- (((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)) -> (B u. B) = B)
56		feq3 3729	. . . . 5 |- ((B u. B) = B -> ((g u. {<.(`'h` w), y>.}):((`'h"w) u. {(`'h` w)})-->(B u. B) <-> (g u. {<.(`'h` w), y>.}):((`'h"w) u. {(`'h` w)})-->B))
57	55, 56	syl 10	. . . 4 |- (((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>.}):((`'h"w) u. {(`'h` w)})-->(B u. B) <-> (g u. {<.(`'h` w), y>.}):((`'h"w) u. {(`'h` w)})-->B))
58	53, 57	mpbid 193	. . 3 |- (((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>.}):((`'h"w) u. {(`'h` w)})-->B)
59	36	ac6sfilem2 4589	. . . . . . 7 |- (`'h:suc w-1-1-onto->z -> ((`'h"w) u. {(`'h` w)}) = z)
60	59	ad2antll 407	. . . . . 6 |- (([(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> ((`'h"w) u. {(`'h` w)}) = z)
61	60	3adant1 803	. . . . 5 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> ((`'h"w) u. {(`'h` w)}) = z)
62	61	adantr 389	. . . 4 |- (((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)) -> ((`'h"w) u. {(`'h` w)}) = z)
63		feq2 3728	. . . 4 |- (((`'h"w) u. {(`'h` w)}) = z -> ((g u. {<.(`'h` w), y>.}):((`'h"w) u. {(`'h` w)})-->B <-> (g u. {<.(`'h` w), y>.}):z-->B))
64	62, 63	syl 10	. . 3 |- (((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>.}):((`'h"w) u. {(`'h` w)})-->B <-> (g u. {<.(`'h` w), y>.}):z-->B))
65	58, 64	mpbid 193	. 2 |- (((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)
66		ax-17 1007	. . . . . . 7 |- (y e. B -> A.x y e. B)
67	3	hbsbc1v 1995	. . . . . . 7 |- ([(`'h` w) / x]ph -> A.x[(`'h` w) / x]ph)
68		ax-17 1007	. . . . . . 7 |- ((w e. om /\ `'h:suc w-1-1-onto->z) -> A.x(w e. om /\ `'h:suc w-1-1-onto->z))
69	66, 67, 68	hb3an 1048	. . . . . 6 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> A.x(y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)))
70		ax-17 1007	. . . . . . 7 |- (g:(`'h"w)-->B -> A.x g:(`'h"w)-->B)
71		hbra1 1733	. . . . . . 7 |- (A.x e. (`'h"w)[g / f]ps -> A.xA.x e. (`'h"w)[g / f]ps)
72	70, 71	hban 1045	. . . . . 6 |- ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> A.x(g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps))
73	69, 72	hban 1045	. . . . 5 |- (((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)) -> A.x((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)))
74		ax-17 1007	. . . . 5 |- ((g u. {<.(`'h` w), y>.}):z-->B -> A.x(g u. {<.(`'h` w), y>.}):z-->B)
75	73, 74	hban 1045	. . . 4 |- ((((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(((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))
76	59	eqcomd 1523	. . . . . . . . . 10 |- (`'h:suc w-1-1-onto->z -> z = ((`'h"w) u. {(`'h` w)}))
77	76	ad2antll 407	. . . . . . . . 9 |- (([(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> z = ((`'h"w) u. {(`'h` w)}))
78	77	3adant1 803	. . . . . . . 8 |- ((y e. B /\ [(`'h` w) / x]ph /\ (w e. om /\ `'h:suc w-1-1-onto->z)) -> z = ((`'h"w) u. {(`'h` w)}))
79	78	ad2antrr 404	. . . . . . 7 |- ((((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) -> z = ((`'h"w) u. {(`'h` w)}))
80	79	eleq2d 1584	. . . . . 6 |- ((((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) -> (x e. z <-> x e. ((`'h"w) u. {(`'h` w)})))
81		elun 2225	. . . . . 6 |- (x e. ((`'h"w) u. {(`'h` w)}) <-> (x e. (`'h"w) \/ x e. {(`'h` w)}))
82	80, 81	syl6bb 539	. . . . 5 |- ((((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) -> (x e. z <-> (x e. (`'h"w) \/ x e. {(`'h` w)})))
83		pm2.27 62	. . . . . . . . . . . 12 |- (x e. (`'h"w) -> ((x e. (`'h"w) -> [g / f]ps) -> [g / f]ps))
84		3simp2 795	. . . . . . . . . . . . . . 15 |- ((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) -> [g / f]ps)
85	84	adantr 389	. . . . . . . . . . . . . 14 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> [g / f]ps)
86		funssfv 3846	. . . . . . . . . . . . . . . 16 |- ((Fun (g u. {<.(`'h` w), y>.}) /\ g (_ (g u. {<.(`'h` w), y>.}) /\ x e. dom g) -> ((g u. {<.(`'h` w), y>.})` x) = (g` x))
87		ffun 3736	. . . . . . . . . . . . . . . . 17 |- ((g u. {<.(`'h` w), y>.}):z-->B -> Fun (g u. {<.(`'h` w), y>.}))
88	87	adantl 388	. . . . . . . . . . . . . . . 16 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> Fun (g u. {<.(`'h` w), y>.}))
89		ssun1 2245	. . . . . . . . . . . . . . . . 17 |- g (_ (g u. {<.(`'h` w), y>.})
90	89	a1i 8	. . . . . . . . . . . . . . . 16 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> g (_ (g u. {<.(`'h` w), y>.}))
91		3simp1 794	. . . . . . . . . . . . . . . . . 18 |- ((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) -> x e. (`'h"w))
92	91	adantr 389	. . . . . . . . . . . . . . . . 17 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> x e. (`'h"w))
93		fdm 3738	. . . . . . . . . . . . . . . . . . 19 |- (g:(`'h"w)-->B -> dom g = (`'h"w))
94	93	3ad2ant3 808	. . . . . . . . . . . . . . . . . 18 |- ((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) -> dom g = (`'h"w))
95	94	adantr 389	. . . . . . . . . . . . . . . . 17 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> dom g = (`'h"w))
96	92, 95	eleqtrrd 1594	. . . . . . . . . . . . . . . 16 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> x e. dom g)
97	86, 88, 90, 96	syl3anc 864	. . . . . . . . . . . . . . 15 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> ((g u. {<.(`'h` w), y>.})` x) = (g` x))
98		visset 1859	. . . . . . . . . . . . . . . . . . 19 |- g e. V
99		snex 2826	. . . . . . . . . . . . . . . . . . 19 |- {<.(`'h` w), y>.} e. V
100	98, 99	unex 3095	. . . . . . . . . . . . . . . . . 18 |- (g u. {<.(`'h` w), y>.}) e. V
101		fvex 3843	. . . . . . . . . . . . . . . . . . 19 |- (g` x) e. V
102		ac6sfi.1	. . . . . . . . . . . . . . . . . . . 20 |- (y = (f` x) -> (ph <-> ps))
103	102	ax-gen 999	. . . . . . . . . . . . . . . . . . 19 |- A.y(y = (f` x) -> (ph <-> ps))
104		ax-17 1007	. . . . . . . . . . . . . . . . . . . 20 |- (m e. (g` x) -> A.y m e. (g` x))
105		ax-17 1007	. . . . . . . . . . . . . . . . . . . . 21 |- ((g` x) = (f` x) -> A.y(g` x) = (f` x))
106	101	hbsbc1v 1995	. . . . . . . . . . . . . . . . . . . . . 22 |- ([(g` x) / y]ph -> A.y[(g` x) / y]ph)
107		ax-17 1007	. . . . . . . . . . . . . . . . . . . . . 22 |- (ps -> A.yps)
108	106, 107	hbbi 1046	. . . . . . . . . . . . . . . . . . . . 21 |- (([(g` x) / y]ph <-> ps) -> A.y([(g` x) / y]ph <-> ps))
109	105, 108	hbim 1043	. . . . . . . . . . . . . . . . . . . 20 |- (((g` x) = (f` x) -> ([(g` x) / y]ph <-> ps)) -> A.y((g` x) = (f` x) -> ([(g` x) / y]ph <-> ps)))
110		eqeq1 1524	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (g` x) -> (y = (f` x) <-> (g` x) = (f` x)))
111		sbceq1a 1989	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = (g` x) -> (ph <-> [(g` x) / y]ph))
112	111	bibi1d 622	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (g` x) -> ((ph <-> ps) <-> ([(g` x) / y]ph <-> ps)))
113	110, 112	imbi12d 629	. . . . . . . . . . . . . . . . . . . 20 |- (y = (g` x) -> ((y = (f` x) -> (ph <-> ps)) <-> ((g` x) = (f` x) -> ([(g` x) / y]ph <-> ps))))
114	104, 109, 113	cla4gf 1906	. . . . . . . . . . . . . . . . . . 19 |- ((g` x) e. V -> (A.y(y = (f` x) -> (ph <-> ps)) -> ((g` x) = (f` x) -> ([(g` x) / y]ph <-> ps))))
115	101, 103, 114	mp2 43	. . . . . . . . . . . . . . . . . 18 |- ((g` x) = (f` x) -> ([(g` x) / y]ph <-> ps))
116	100, 115	ac6sfilem1 4588	. . . . . . . . . . . . . . . . 17 |- ((g` x) = ((g u. {<.(`'h` w), y>.})` x) -> ([(g` x) / y]ph <-> [(g u. {<.(`'h` w), y>.}) / f]ps))
117	116	eqcoms 1521	. . . . . . . . . . . . . . . 16 |- (((g u. {<.(`'h` w), y>.})` x) = (g` x) -> ([(g` x) / y]ph <-> [(g u. {<.(`'h` w), y>.}) / f]ps))
118		eqid 1518	. . . . . . . . . . . . . . . . 17 |- (g` x) = (g` x)
119	98, 115	ac6sfilem1 4588	. . . . . . . . . . . . . . . . 17 |- ((g` x) = (g` x) -> ([(g` x) / y]ph <-> [g / f]ps))
120	118, 119	ax-mp 7	. . . . . . . . . . . . . . . 16 |- ([(g` x) / y]ph <-> [g / f]ps)
121	117, 120	syl5rbbr 538	. . . . . . . . . . . . . . 15 |- (((g u. {<.(`'h` w), y>.})` x) = (g` x) -> ([(g u. {<.(`'h` w), y>.}) / f]ps <-> [g / f]ps))
122	97, 121	syl 10	. . . . . . . . . . . . . 14 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> ([(g u. {<.(`'h` w), y>.}) / f]ps <-> [g / f]ps))
123	85, 122	mpbird 194	. . . . . . . . . . . . 13 |- (((x e. (`'h"w) /\ [g / f]ps /\ g:(`'h"w)-->B) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> [(g u. {<.(`'h` w), y>.}) / f]ps)
124	123	3exp1 855	. . . . . . . . . . . 12 |- (x e. (`'h"w) -> ([g / f]ps -> (g:(`'h"w)-->B -> ((g u. {<.(`'h` w), y>.}):z-->B -> [(g u. {<.(`'h` w), y>.}) / f]ps))))
125	83, 124	syld 27	. . . . . . . . . . 11 |- (x e. (`'h"w) -> ((x e. (`'h"w) -> [g / f]ps) -> (g:(`'h"w)-->B -> ((g u. {<.(`'h` w), y>.}):z-->B -> [(g u. {<.(`'h` w), y>.}) / f]ps))))
126	125	com4l 39	. . . . . . . . . 10 |- ((x e. (`'h"w) -> [g / f]ps) -> (g:(`'h"w)-->B -> ((g u. {<.(`'h` w), y>.}):z-->B -> (x e. (`'h"w) -> [(g u. {<.(`'h` w), y>.}) / f]ps))))
127	126	impcom 349	. . . . . . . . 9 |- ((g:(`'h"w)-->B /\ (x e. (`'h"w) -> [g / f]ps)) -> ((g u. {<.(`'h` w), y>.}):z-->B -> (x e. (`'h"w) -> [(g u. {<.(`'h` w), y>.}) / f]ps)))
128		ra4 1740	. . . . . . . . 9 |- (A.x e. (`'h"w)[g / f]ps -> (x e. (`'h"w) -> [g / f]ps))
129	127, 128	sylan2 453	. . . . . . . 8 |- ((g:(`'h"w)-->B /\ A.x e. (`'h"w)[g / f]ps) -> ((g u. {<.(`'h` w), y>.}):z-->B -> (x e. (`'h"w) -> [(g u. {<.(`'h` w), y>.}) / f]ps)))
130	129	adantl 388	. . . . . . 7 |- (((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 -> (x e. (`'h"w) -> [(g u. {<.(`'h` w), y>.}) / f]ps)))
131	130	imp 348	. . . . . 6 |- ((((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) -> (x e. (`'h"w) -> [(g u. {<.(`'h` w), y>.}) / f]ps))
132		f1ofn 3798	. . . . . . . . . . 11 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> {<.(`'h` w), y>.} Fn {(`'h` w)})
133		fndm 3693	. . . . . . . . . . 11 |- ({<.(`'h` w), y>.} Fn {(`'h` w)} -> dom {<.(`'h` w), y>.} = {(`'h` w)})
134	132, 133	syl 10	. . . . . . . . . 10 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> dom {<.(`'h` w), y>.} = {(`'h` w)})
135		opex 2858	. . . . . . . . . . . 12 |- <.(`'h` w), y>. e. V
136	135	snid 2496	. . . . . . . . . . 11 |- <.(`'h` w), y>. e. {<.(`'h` w), y>.}
137		f1ofun 3799	. . . . . . . . . . . 12 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> Fun {<.(`'h` w), y>.})
138	4	funopfv 3862	. . . . . . . . . . . 12 |- (Fun {<.(`'h` w), y>.} -> (<.(`'h` w), y>. e. {<.(`'h` w), y>.} -> ({<.(`'h` w), y>.}` (`'h` w)) = y))
139	137, 138	syl 10	. . . . . . . . . . 11 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> (<.(`'h` w), y>. e. {<.(`'h` w), y>.} -> ({<.(`'h` w), y>.}` (`'h` w)) = y))
140	136, 139	mpi 44	. . . . . . . . . 10 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> ({<.(`'h` w), y>.}` (`'h` w)) = y)
141	134, 140	jca 286	. . . . . . . . 9 |- ({<.(`'h` w), y>.}:{(`'h` w)}-1-1-onto->{y} -> (dom {<.(`'h` w), y>.} = {(`'h` w)} /\ ({<.(`'h` w), y>.}` (`'h` w)) = y))
142	5, 141	ax-mp 7	. . . . . . . 8 |- (dom {<.(`'h` w), y>.} = {(`'h` w)} /\ ({<.(`'h` w), y>.}` (`'h` w)) = y)
143		fveq2 3835	. . . . . . . . . . . . 13 |- (x = (`'h` w) -> ({<.(`'h` w), y>.}` x) = ({<.(`'h` w), y>.}` (`'h` w)))
144	143	eqcomd 1523	. . . . . . . . . . . 12 |- (x = (`'h` w) -> ({<.(`'h` w), y>.}` (`'h` w)) = ({<.(`'h` w), y>.}` x))
145	144	eqeq1d 1526	. . . . . . . . . . 11 |- (x = (`'h` w) -> (({<.(`'h` w), y>.}` (`'h` w)) = y <-> ({<.(`'h` w), y>.}` x) = y))
146		sbceq1a 1989	. . . . . . . . . . . . . . . . . . 19 |- (x = (`'h` w) -> (ph <-> [(`'h` w) / x]ph))
147		funssfv 3846	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((Fun (g u. {<.(`'h` w), y>.}) /\ {<.(`'h` w), y>.} (_ (g u. {<.(`'h` w), y>.}) /\ x e. dom {<.(`'h` w), y>.}) -> ((g u. {<.(`'h` w), y>.})` x) = ({<.(`'h` w), y>.}` x))
148	87	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) -> Fun (g u. {<.(`'h` w), y>.}))
149	148	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) /\ ({<.(`'h` w), y>.}` x) = y) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> Fun (g u. {<.(`'h` w), y>.}))
150		ssun2 2246	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {<.(`'h` w), y>.} (_ (g u. {<.(`'h` w), y>.})
151	150	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((x = (`'h` w) /\ (g u. {<.(`'h` w), y>.}):z-->B) /\ ({<.(`'h` w), y>.}` x) = y) /\ dom {<.(`'h` w), y>.} = {(`'h` w)}) -> {<.(`'h` w)