Theorem sdclem2 11876

Description: Lemma for sdc 11877. A consequence of acdc5g 11844 that will be used multiple times in the proof.

Hypothesis

Ref	Expression
sdclem2.1	|- (ph -> A e. B)

Assertion

Ref	Expression
sdclem2	|- ((((ph /\ h:{1}-->A) /\ (j:NN-->S /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w)))) /\ C e. NN) -> (j` C):(1...C)-->A)

Distinct variable groups:   x,q,j,z,y,w,h   x,A,y,z,q,w   x,C   ps,y,w   ph,q   y,S,w,x

Proof of Theorem sdclem2

Step	Hyp	Ref	Expression
1		fveq2 3835	. . . . . 6 |- (b = 1 -> (j` b) = (j` 1))
2	1	feq1d 3731	. . . . 5 |- (b = 1 -> ((j` b):(1...b)-->A <-> (j` 1):(1...b)-->A))
3		opreq2 4027	. . . . . 6 |- (b = 1 -> (1...b) = (1...1))
4		feq2 3728	. . . . . 6 |- ((1...b) = (1...1) -> ((j` 1):(1...b)-->A <-> (j` 1):(1...1)-->A))
5	3, 4	syl 10	. . . . 5 |- (b = 1 -> ((j` 1):(1...b)-->A <-> (j` 1):(1...1)-->A))
6	2, 5	bitrd 531	. . . 4 |- (b = 1 -> ((j` b):(1...b)-->A <-> (j` 1):(1...1)-->A))
7	6	imbi2d 615	. . 3 |- (b = 1 -> ((((ph /\ h:{1}-->A) /\ (j:NN-->S /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w)))) -> (j` b):(1...b)-->A) <-> (((ph /\ h:{1}-->A) /\ (j:NN-->S /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w)))) -> (j` 1):(1...1)-->A)))
8		fveq2 3835	. . . . . 6 |- (b = d -> (j` b) = (j` d))
9	8	feq1d 3731	. . . . 5 |- (b = d -> ((j` b):(1...b)-->A <-> (j` d):(1...b)-->A))
10		opreq2 4027	. . . . . 6 |- (b = d -> (1...b) = (1...d))
11		feq2 3728	. . . . . 6 |- ((1...b) = (1...d) -> ((j` d):(1...b)-->A <-> (j` d):(1...d)-->A))
12	10, 11	syl 10	. . . . 5 |- (b = d -> ((j` d):(1...b)-->A <-> (j` d):(1...d)-->A))
13	9, 12	bitrd 531	. . . 4 |- (b = d -> ((j` b):(1...b)-->A <-> (j` d):(1...d)-->A))
14	13	imbi2d 615	. . 3 |- (b = d -> ((((ph /\ h:{1}-->A) /\ (j:NN-->S /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w)))) -> (j` b):(1...b)-->A) <-> (((ph /\ h:{1}-->A) /\ (j:NN-->S /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w)))) -> (j` d):(1...d)-->A)))
15		fveq2 3835	. . . . . 6 |- (b = (d + 1) -> (j` b) = (j` (d + 1)))
16	15	feq1d 3731	. . . . 5 |- (b = (d + 1) -> ((j` b):(1...b)-->A <-> (j` (d + 1)):(1...b)-->A))
17		opreq2 4027	. . . . . 6 |- (b = (d + 1) -> (1...b) = (1...(d + 1)))
18		feq2 3728	. . . . . 6 |- ((1...b) = (1...(d + 1)) -> ((j` (d + 1)):(1...b)-->A <-> (j` (d + 1)):(1...(d + 1))-->A))
19	17, 18	syl 10	. . . . 5 |- (b = (d + 1) -> ((j` (d + 1)):(1...b)-->A <-> (j` (d + 1)):(1...(d + 1))-->A))
20	16, 19	bitrd 531	. . . 4 |- (b = (d + 1) -> ((j` b):(1...b)-->A <-> (j` (d + 1)):(1...(d + 1))-->A))
21	20	imbi2d 615	. . 3 |- (b = (d + 1) -> ((((ph /\ h:{1}-->A) /\ (j:NN-->S /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w)))) -> (j` b):(1...b)-->A) <-> (((ph /\ h:{1}-->A) /\ (j:NN-->S /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w)))) -> (j` (d + 1)):(1...(d + 1))-->A)))
22		fveq2 3835	. . . . . 6 |- (b = C -> (j` b) = (j` C))
23	22	feq1d 3731	. . . . 5 |- (b = C -> ((j` b):(1...b)-->A <-> (j` C):(1...b)-->A))
24		opreq2 4027	. . . . . 6 |- (b = C -> (1...b) = (1...C))
25		feq2 3728	. . . . . 6 |- ((1...b) = (1...C) -> ((j` C):(1...b)-->A <-> (j` C):(1...C)-->A))
26	24, 25	syl 10	. . . . 5 |- (b = C -> ((j` C):(1...b)-->A <-> (j` C):(1...C)-->A))
27	23, 26	bitrd 531	. . . 4 |- (b = C -> ((j` b):(1...b)-->A <-> (j` C):(1...C)-->A))
28	27	imbi2d 615	. . 3 |- (b = C -> ((((ph /\ h:{1}-->A) /\ (j:NN-->S /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w)))) -> (j` b):(1...b)-->A) <-> (((ph /\ h:{1}-->A) /\ (j:NN-->S /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w)))) -> (j` C):(1...C)-->A)))
29		feq1 3727	. . . . . 6 |- ((j` 1) = h -> ((j` 1):(1...1)-->A <-> h:(1...1)-->A))
30	29	biimparc 419	. . . . 5 |- ((h:(1...1)-->A /\ (j` 1) = h) -> (j` 1):(1...1)-->A)
31		1z 6327	. . . . . . . . 9 |- 1 e. ZZ
32		fzsn 11865	. . . . . . . . 9 |- (1 e. ZZ -> (1...1) = {1})
33	31, 32	ax-mp 7	. . . . . . . 8 |- (1...1) = {1}
34		feq2 3728	. . . . . . . 8 |- ((1...1) = {1} -> (h:(1...1)-->A <-> h:{1}-->A))
35	33, 34	ax-mp 7	. . . . . . 7 |- (h:(1...1)-->A <-> h:{1}-->A)
36	35	biimpri 150	. . . . . 6 |- (h:{1}-->A -> h:(1...1)-->A)
37	36	adantl 388	. . . . 5 |- ((ph /\ h:{1}-->A) -> h:(1...1)-->A)
38	30, 37	sylan 450	. . . 4 |- (((ph /\ h:{1}-->A) /\ (j` 1) = h) -> (j` 1):(1...1)-->A)
39	38	3ad2antr2 819	. . 3 |- (((ph /\ h:{1}-->A) /\ (j:NN-->S /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w)))) -> (j` 1):(1...1)-->A)
40		ax-17 1007	. . . . . . . . . . . . . . . 16 |- (u e. (j` d) -> A.x u e. (j` d))
41		ax-17 1007	. . . . . . . . . . . . . . . . . 18 |- (q e. NN -> A.x q e. NN)
42		ax-17 1007	. . . . . . . . . . . . . . . . . . 19 |- (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) -> A.x((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A))
43		fvex 3843	. . . . . . . . . . . . . . . . . . . 20 |- (j` d) e. V
44	43	hbsbc1v 1995	. . . . . . . . . . . . . . . . . . 19 |- ([(j` d) / x]ps -> A.x[(j` d) / x]ps)
45	42, 44	hban 1045	. . . . . . . . . . . . . . . . . 18 |- ((((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps) -> A.x(((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps))
46	41, 45	hbrex 1734	. . . . . . . . . . . . . . . . 17 |- (E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps) -> A.xE.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps))
47	46	hbab 1509	. . . . . . . . . . . . . . . 16 |- (u e. {z | E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} -> A.x u e. {z | E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)})
48		feq1 3727	. . . . . . . . . . . . . . . . . . . 20 |- (x = (j` d) -> (x:(1...q)-->A <-> (j` d):(1...q)-->A))
49	48	anbi1d 620	. . . . . . . . . . . . . . . . . . 19 |- (x = (j` d) -> ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) <-> ((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A)))
50		sbceq1a 1989	. . . . . . . . . . . . . . . . . . 19 |- (x = (j` d) -> (ps <-> [(j` d) / x]ps))
51	49, 50	anbi12d 631	. . . . . . . . . . . . . . . . . 18 |- (x = (j` d) -> (((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps) <-> (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)))
52	51	rexbidv 1710	. . . . . . . . . . . . . . . . 17 |- (x = (j` d) -> (E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps) <-> E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)))
53	52	abbidv 1620	. . . . . . . . . . . . . . . 16 |- (x = (j` d) -> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)} = {z | E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)})
54		eqid 1518	. . . . . . . . . . . . . . . 16 |- {<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})} = {<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}
55	40, 47, 53, 54	fvopab4gf 3892	. . . . . . . . . . . . . . 15 |- (((j` d) e. S /\ {z | E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} e. V) -> ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` d)) = {z | E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)})
56		abrexex2g 11825	. . . . . . . . . . . . . . . 16 |- ((NN e. V /\ A.q e. NN {z | (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} e. V) -> {z | E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} e. V)
57		nnex 6078	. . . . . . . . . . . . . . . 16 |- NN e. V
58		ssexg 2795	. . . . . . . . . . . . . . . . . . 19 |- (({z | (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} (_ {z | z:(1...(q + 1))-->A} /\ {z | z:(1...(q + 1))-->A} e. V) -> {z | (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} e. V)
59		simplr 413	. . . . . . . . . . . . . . . . . . . 20 |- ((((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps) -> z:(1...(q + 1))-->A)
60	59	ss2abi 2172	. . . . . . . . . . . . . . . . . . 19 |- {z | (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} (_ {z | z:(1...(q + 1))-->A}
61		mapex 4469	. . . . . . . . . . . . . . . . . . . 20 |- (((1...(q + 1)) e. V /\ A e. B) -> {z | z:(1...(q + 1))-->A} e. V)
62		oprex 4041	. . . . . . . . . . . . . . . . . . . 20 |- (1...(q + 1)) e. V
63		sdclem2.1	. . . . . . . . . . . . . . . . . . . 20 |- (ph -> A e. B)
64	61, 62, 63	sylancr 474	. . . . . . . . . . . . . . . . . . 19 |- (ph -> {z | z:(1...(q + 1))-->A} e. V)
65	58, 60, 64	sylancr 474	. . . . . . . . . . . . . . . . . 18 |- (ph -> {z | (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} e. V)
66	65	a1d 12	. . . . . . . . . . . . . . . . 17 |- (ph -> (q e. NN -> {z | (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} e. V))
67	66	r19.21aiv 1759	. . . . . . . . . . . . . . . 16 |- (ph -> A.q e. NN {z | (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} e. V)
68	56, 57, 67	sylancr 474	. . . . . . . . . . . . . . 15 |- (ph -> {z | E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} e. V)
69	55, 68	sylan2 453	. . . . . . . . . . . . . 14 |- (((j` d) e. S /\ ph) -> ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` d)) = {z | E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)})
70	69	ancoms 438	. . . . . . . . . . . . 13 |- ((ph /\ (j` d) e. S) -> ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` d)) = {z | E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)})
71	70	eleq2d 1584	. . . . . . . . . . . 12 |- ((ph /\ (j` d) e. S) -> ((j` (d + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` d)) <-> (j` (d + 1)) e. {z | E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)}))
72	71	biimpd 151	. . . . . . . . . . 11 |- ((ph /\ (j` d) e. S) -> ((j` (d + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` d)) -> (j` (d + 1)) e. {z | E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)}))
73	72	expimpd 373	. . . . . . . . . 10 |- (ph -> (((j` d) e. S /\ (j` (d + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` d))) -> (j` (d + 1)) e. {z | E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)}))
74		ax-17 1007	. . . . . . . . . . . . 13 |- (q e. NN -> A.z q e. NN)
75		ax-17 1007	. . . . . . . . . . . . . 14 |- (((j` d):(1...q)-->A /\ (j` (d + 1)):(1...(q + 1))-->A) -> A.z((j` d):(1...q)-->A /\ (j` (d + 1)):(1...(q + 1))-->A))
76		fvex 3843	. . . . . . . . . . . . . . 15 |- (j` (d + 1)) e. V
77	76	hbsbc1v 1995	. . . . . . . . . . . . . 14 |- ([(j` (d + 1)) / z][(j` d) / x]ps -> A.z[(j` (d + 1)) / z][(j` d) / x]ps)
78	75, 77	hban 1045	. . . . . . . . . . . . 13 |- ((((j` d):(1...q)-->A /\ (j` (d + 1)):(1...(q + 1))-->A) /\ [(j` (d + 1)) / z][(j` d) / x]ps) -> A.z(((j` d):(1...q)-->A /\ (j` (d + 1)):(1...(q + 1))-->A) /\ [(j` (d + 1)) / z][(j` d) / x]ps))
79	74, 78	hbrex 1734	. . . . . . . . . . . 12 |- (E.q e. NN (((j` d):(1...q)-->A /\ (j` (d + 1)):(1...(q + 1))-->A) /\ [(j` (d + 1)) / z][(j` d) / x]ps) -> A.zE.q e. NN (((j` d):(1...q)-->A /\ (j` (d + 1)):(1...(q + 1))-->A) /\ [(j` (d + 1)) / z][(j` d) / x]ps))
80		feq1 3727	. . . . . . . . . . . . . . 15 |- (z = (j` (d + 1)) -> (z:(1...(q + 1))-->A <-> (j` (d + 1)):(1...(q + 1))-->A))
81	80	anbi2d 619	. . . . . . . . . . . . . 14 |- (z = (j` (d + 1)) -> (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) <-> ((j` d):(1...q)-->A /\ (j` (d + 1)):(1...(q + 1))-->A)))
82		sbceq1a 1989	. . . . . . . . . . . . . 14 |- (z = (j` (d + 1)) -> ([(j` d) / x]ps <-> [(j` (d + 1)) / z][(j` d) / x]ps))
83	81, 82	anbi12d 631	. . . . . . . . . . . . 13 |- (z = (j` (d + 1)) -> ((((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps) <-> (((j` d):(1...q)-->A /\ (j` (d + 1)):(1...(q + 1))-->A) /\ [(j` (d + 1)) / z][(j` d) / x]ps)))
84	83	rexbidv 1710	. . . . . . . . . . . 12 |- (z = (j` (d + 1)) -> (E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps) <-> E.q e. NN (((j` d):(1...q)-->A /\ (j` (d + 1)):(1...(q + 1))-->A) /\ [(j` (d + 1)) / z][(j` d) / x]ps)))
85	79, 76, 84	elabf 1942	. . . . . . . . . . 11 |- ((j` (d + 1)) e. {z | E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} <-> E.q e. NN (((j` d):(1...q)-->A /\ (j` (d + 1)):(1...(q + 1))-->A) /\ [(j` (d + 1)) / z][(j` d) / x]ps))
86		visset 1859	. . . . . . . . . . . . . . . . . . . 20 |- d e. V
87		fzopth 6632	. . . . . . . . . . . . . . . . . . . . 21 |- ((q e. (ZZ>=` 1) /\ d e. V) -> ((1...q) = (1...d) <-> (1 = 1 /\ q = d)))
88		elnnuz 6567	. . . . . . . . . . . . . . . . . . . . 21 |- (q e. NN <-> q e. (ZZ>=` 1))
89	87, 88	sylanb 451	. . . . . . . . . . . . . . . . . . . 20 |- ((q e. NN /\ d e. V) -> ((1...q) = (1...d) <-> (1 = 1 /\ q = d)))
90	86, 89	mpan2 700	. . . . . . . . . . . . . . . . . . 19 |- (q e. NN -> ((1...q) = (1...d) <-> (1 = 1 /\ q = d)))
91		opreq1 4026	. . . . . . . . . . . . . . . . . . . . . . 23 |- (q = d -> (q + 1) = (d + 1))
92	91	opreq2d 4034	. . . . . . . . . . . . . . . . . . . . . 22 |- (q = d -> (1...(q + 1)) = (1...(d + 1)))
93		feq2 3728	. . . . . . . . . . . . . . . . . . . . . 22 |- ((1...(q + 1)) = (1...(d + 1)) -> ((j` (d + 1)):(1...(q + 1))-->A <-> (j` (d + 1)):(1...(d + 1))-->A))
94	92, 93	syl 10	. . . . . . . . . . . . . . . . . . . . 21 |- (q = d -> ((j` (d + 1)):(1...(q + 1))-->A <-> (j` (d + 1)):(1...(d + 1))-->A))
95	94	biimpd 151	. . . . . . . . . . . . . . . . . . . 20 |- (q = d -> ((j` (d + 1)):(1...(q + 1))-->A -> (j` (d + 1)):(1...(d + 1))-->A))
96	95	adantl 388	. . . . . . . . . . . . . . . . . . 19 |- ((1 = 1 /\ q = d) -> ((j` (d + 1)):(1...(q + 1))-->A -> (j` (d + 1)):(1...(d + 1))-->A))
97	90, 96	syl6bi 212	. . . . . . . . . . . . . . . . . 18 |- (q e. NN -> ((1...q) = (1...d) -> ((j` (d + 1)):(1...(q + 1))-->A -> (j` (d + 1)):(1...(d + 1))-->A)))
98		fndmu 3695	. . . . . . . . . . . . . . . . . . 19 |- (((j` d) Fn (1...q) /\ (j` d) Fn (1...d)) -> (1...q) = (1...d))
99		ffn 3734	. . . . . . . . . . . . . . . . . . 19 |- ((j` d):(1...q)-->A -> (j` d) Fn (1...q))
100		ffn 3734	. . . . . . . . . . . . . . . . . . 19 |- ((j` d):(1...d)-->A -> (j` d) Fn (1...d))
101	98, 99, 100	syl2an 456	. . . . . . . . . . . . . . . . . 18 |- (((j` d):(1...q)-->A /\ (j` d):(1...d)-->A) -> (1...q) = (1...d))
102	97, 101	syl5com 52	. . . . . . . . . . . . . . . . 17 |- (((j` d):(1...q)-->A /\ (j` d):(1...d)-->A) -> (q e. NN -> ((j` (d + 1)):(1...(q + 1))-->A -> (j` (d + 1)):(1...(d + 1))-->A)))
103	102	ex 371	. . . . . . . . . . . . . . . 16 |- ((j` d):(1...q)-->A -> ((j` d):(1...d)-->A -> (q e. NN -> ((j` (d + 1)):(1...(q + 1))-->A -> (j` (d + 1)):(1...(d + 1))-->A))))
104	103	com24 37	. . . . . . . . . . . . . . 15 |- ((j` d):(1...q)-->A -> ((j` (d + 1)):(1...(q + 1))-->A -> (q e. NN -> ((j` d):(1...d)-->A -> (j` (d + 1)):(1...(d + 1))-->A))))
105	104	imp 348	. . . . . . . . . . . . . 14 |- (((j` d):(1...q)-->A /\ (j` (d + 1)):(1...(q + 1))-->A) -> (q e. NN -> ((j` d):(1...d)-->A -> (j` (d + 1)):(1...(d + 1))-->A)))
106	105	impcom 349	. . . . . . . . . . . . 13 |- ((q e. NN /\ ((j` d):(1...q)-->A /\ (j` (d + 1)):(1...(q + 1))-->A)) -> ((j` d):(1...d)-->A -> (j` (d + 1)):(1...(d + 1))-->A))
107	106	adantrr 395	. . . . . . . . . . . 12 |- ((q e. NN /\ (((j` d):(1...q)-->A /\ (j` (d + 1)):(1...(q + 1))-->A) /\ [(j` (d + 1)) / z][(j` d) / x]ps)) -> ((j` d):(1...d)-->A -> (j` (d + 1)):(1...(d + 1))-->A))
108	107	r19.23aiva 1790	. . . . . . . . . . 11 |- (E.q e. NN (((j` d):(1...q)-->A /\ (j` (d + 1)):(1...(q + 1))-->A) /\ [(j` (d + 1)) / z][(j` d) / x]ps) -> ((j` d):(1...d)-->A -> (j` (d + 1)):(1...(d + 1))-->A))
109	85, 108	sylbi 197	. . . . . . . . . 10 |- ((j` (d + 1)) e. {z | E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} -> ((j` d):(1...d)-->A -> (j` (d + 1)):(1...(d + 1))-->A))
110	73, 109	syl6 22	. . . . . . . . 9 |- (ph -> (((j` d) e. S /\ (j` (d + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` d))) -> ((j` d):(1...d)-->A -> (j` (d + 1)):(1...(d + 1))-->A)))
111		ffvelrn 3928	. . . . . . . . . . . 12 |- ((j:NN-->S /\ d e. NN) -> (j` d) e. S)
112	111	expcom 372	. . . . . . . . . . 11 |- (d e. NN -> (j:NN-->S -> (j` d) e. S))
113		opreq1 4026	. . . . . . . . . . . . . 14 |- (w = d -> (w + 1) = (d + 1))
114	113	fveq2d 3839	. . . . . . . . . . . . 13 |- (w = d -> (j` (w + 1)) = (j` (d + 1)))
115		fveq2 3835	. . . . . . . . . . . . . 14 |- (w = d -> (j` w) = (j` d))
116	115	fveq2d 3839	. . . . . . . . . . . . 13 |- (w = d -> ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w)) = ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` d)))
117	114, 116	eleq12d 1585	. . . . . . . . . . . 12 |- (w = d -> ((j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w)) <-> (j` (d + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` d))))
118	117	rcla4v 1919	. . . . . . . . . . 11 |- (d e. NN -> (A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w)) -> (j` (d + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` d))))
119	112, 118	anim12d 561	. . . . . . . . . 10 |- (d e. NN -> ((j:NN-->S /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w))) -> ((j` d) e. S /\ (j` (d + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` d)))))
120	119	impcom 349	. . . . . . . . 9 |- (((j:NN-->S /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w))) /\ d e. NN) -> ((j` d) e. S /\ (j` (d + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` d))))
121	110, 120	syl5 21	. . . . . . . 8 |- (ph -> (((j:NN-->S /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w))) /\ d e. NN) -> ((j` d):(1...d)-->A -> (j` (d + 1)):(1...(d + 1))-->A)))
122	121	expdimp 375	. . . . . . 7 |- ((ph /\ (j:NN-->S /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w)))) -> (d e. NN -> ((j` d):(1...d)-->A -> (j` (d + 1)):(1...(d + 1))-->A)))
123	122	adantlr 393	. . . . . 6 |- (((ph /\ h:{1}-->A) /\ (j:NN-->S /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. S /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ ps)})}` (j` w)))) -> (d e. NN -> ((j` d):(1...d)-->A -> (j` (d + 1)):(1...(d + 1))-->A)))
124	123	3adantr2 813	. . . . 5 |- ((