Theorem sdclem2 15810

Description: Lemma for sdc 15811. A consequence of acdc5g 15752 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 4681	. . . . . 6 |- (b = 1 -> (j` b) = (j` 1))
2	1	feq1d 4556	. . . . 5 |- (b = 1 -> ((j` b):(1...b)-->A <-> (j` 1):(1...b)-->A))
3		opreq2 4890	. . . . . 6 |- (b = 1 -> (1...b) = (1...1))
4	3	feq2d 4557	. . . . 5 |- (b = 1 -> ((j` 1):(1...b)-->A <-> (j` 1):(1...1)-->A))
5	2, 4	bitrd 587	. . . 4 |- (b = 1 -> ((j` b):(1...b)-->A <-> (j` 1):(1...1)-->A))
6	5	imbi2d 674	. . 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)))
7		fveq2 4681	. . . . . 6 |- (b = d -> (j` b) = (j` d))
8	7	feq1d 4556	. . . . 5 |- (b = d -> ((j` b):(1...b)-->A <-> (j` d):(1...b)-->A))
9		opreq2 4890	. . . . . 6 |- (b = d -> (1...b) = (1...d))
10	9	feq2d 4557	. . . . 5 |- (b = d -> ((j` d):(1...b)-->A <-> (j` d):(1...d)-->A))
11	8, 10	bitrd 587	. . . 4 |- (b = d -> ((j` b):(1...b)-->A <-> (j` d):(1...d)-->A))
12	11	imbi2d 674	. . 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)))
13		fveq2 4681	. . . . . 6 |- (b = (d + 1) -> (j` b) = (j` (d + 1)))
14	13	feq1d 4556	. . . . 5 |- (b = (d + 1) -> ((j` b):(1...b)-->A <-> (j` (d + 1)):(1...b)-->A))
15		opreq2 4890	. . . . . 6 |- (b = (d + 1) -> (1...b) = (1...(d + 1)))
16	15	feq2d 4557	. . . . 5 |- (b = (d + 1) -> ((j` (d + 1)):(1...b)-->A <-> (j` (d + 1)):(1...(d + 1))-->A))
17	14, 16	bitrd 587	. . . 4 |- (b = (d + 1) -> ((j` b):(1...b)-->A <-> (j` (d + 1)):(1...(d + 1))-->A))
18	17	imbi2d 674	. . 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)))
19		fveq2 4681	. . . . . 6 |- (b = C -> (j` b) = (j` C))
20	19	feq1d 4556	. . . . 5 |- (b = C -> ((j` b):(1...b)-->A <-> (j` C):(1...b)-->A))
21		opreq2 4890	. . . . . 6 |- (b = C -> (1...b) = (1...C))
22	21	feq2d 4557	. . . . 5 |- (b = C -> ((j` C):(1...b)-->A <-> (j` C):(1...C)-->A))
23	20, 22	bitrd 587	. . . 4 |- (b = C -> ((j` b):(1...b)-->A <-> (j` C):(1...C)-->A))
24	23	imbi2d 674	. . 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)))
25		feq1 4551	. . . . . 6 |- ((j` 1) = h -> ((j` 1):(1...1)-->A <-> h:(1...1)-->A))
26	25	biimparc 463	. . . . 5 |- ((h:(1...1)-->A /\ (j` 1) = h) -> (j` 1):(1...1)-->A)
27		1z 7368	. . . . . . . . 9 |- 1 e. ZZ
28		fzsn 7684	. . . . . . . . 9 |- (1 e. ZZ -> (1...1) = {1})
29	27, 28	ax-mp 7	. . . . . . . 8 |- (1...1) = {1}
30	29	feq2i 4559	. . . . . . 7 |- (h:(1...1)-->A <-> h:{1}-->A)
31	30	biimpri 169	. . . . . 6 |- (h:{1}-->A -> h:(1...1)-->A)
32	31	adantl 424	. . . . 5 |- ((ph /\ h:{1}-->A) -> h:(1...1)-->A)
33	26, 32	sylan 497	. . . 4 |- (((ph /\ h:{1}-->A) /\ (j` 1) = h) -> (j` 1):(1...1)-->A)
34	33	3ad2antr2 1042	. . 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)
35		ax-17 1317	. . . . . . . . . . . . . . . 16 |- (u e. (j` d) -> A.x u e. (j` d))
36		ax-17 1317	. . . . . . . . . . . . . . . . . 18 |- (q e. NN -> A.x q e. NN)
37		ax-17 1317	. . . . . . . . . . . . . . . . . . 19 |- (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) -> A.x((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A))
38		fvex 4689	. . . . . . . . . . . . . . . . . . . 20 |- (j` d) e. _V
39	38	hbsbc1v 2464	. . . . . . . . . . . . . . . . . . 19 |- ([(j` d) / x]ps -> A.x[(j` d) / x]ps)
40	37, 39	hban 1356	. . . . . . . . . . . . . . . . . 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))
41	36, 40	hbrex 2149	. . . . . . . . . . . . . . . . 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))
42	41	hbab 1875	. . . . . . . . . . . . . . . 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)})
43		feq1 4551	. . . . . . . . . . . . . . . . . . . 20 |- (x = (j` d) -> (x:(1...q)-->A <-> (j` d):(1...q)-->A))
44	43	anbi1d 679	. . . . . . . . . . . . . . . . . . 19 |- (x = (j` d) -> ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) <-> ((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A)))
45		sbceq1a 2456	. . . . . . . . . . . . . . . . . . 19 |- (x = (j` d) -> (ps <-> [(j` d) / x]ps))
46	44, 45	anbi12d 690	. . . . . . . . . . . . . . . . . 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)))
47	46	rexbidv 2124	. . . . . . . . . . . . . . . . 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)))
48	47	abbidv 2008	. . . . . . . . . . . . . . . 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)})
49		eqid 1884	. . . . . . . . . . . . . . . 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)})}
50	35, 42, 48, 49	fvopab4gf 4744	. . . . . . . . . . . . . . 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)})
51		abrexex2g 15738	. . . . . . . . . . . . . . . 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)
52		nnex 7116	. . . . . . . . . . . . . . . 16 |- NN e. _V
53		ssexg 3457	. . . . . . . . . . . . . . . . . . 19 |- (({z | (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} C_ {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)
54		simplr 449	. . . . . . . . . . . . . . . . . . . 20 |- ((((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps) -> z:(1...(q + 1))-->A)
55	54	ss2abi 2679	. . . . . . . . . . . . . . . . . . 19 |- {z | (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} C_ {z | z:(1...(q + 1))-->A}
56		mapex 5387	. . . . . . . . . . . . . . . . . . . 20 |- (((1...(q + 1)) e. _V /\ A e. B) -> {z | z:(1...(q + 1))-->A} e. _V)
57		oprex 4907	. . . . . . . . . . . . . . . . . . . 20 |- (1...(q + 1)) e. _V
58		sdclem2.1	. . . . . . . . . . . . . . . . . . . 20 |- (ph -> A e. B)
59	56, 57, 58	sylancr 526	. . . . . . . . . . . . . . . . . . 19 |- (ph -> {z | z:(1...(q + 1))-->A} e. _V)
60	53, 55, 59	sylancr 526	. . . . . . . . . . . . . . . . . 18 |- (ph -> {z | (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} e. _V)
61	60	a1d 15	. . . . . . . . . . . . . . . . 17 |- (ph -> (q e. NN -> {z | (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} e. _V))
62	61	r19.21aiv 2175	. . . . . . . . . . . . . . . 16 |- (ph -> A.q e. NN {z | (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} e. _V)
63	51, 52, 62	sylancr 526	. . . . . . . . . . . . . . 15 |- (ph -> {z | E.q e. NN (((j` d):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ [(j` d) / x]ps)} e. _V)
64	50, 63	sylan2 500	. . . . . . . . . . . . . 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)})
65	64	ancoms 484	. . . . . . . . . . . . 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)})
66	65	eleq2d 1964	. . . . . . . . . . . 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)}))
67	66	biimpd 170	. . . . . . . . . . 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)}))
68	67	expimpd 404	. . . . . . . . . 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)}))
69		ax-17 1317	. . . . . . . . . . . . 13 |- (q e. NN -> A.z q e. NN)
70		ax-17 1317	. . . . . . . . . . . . . 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))
71		fvex 4689	. . . . . . . . . . . . . . 15 |- (j` (d + 1)) e. _V
72	71	hbsbc1v 2464	. . . . . . . . . . . . . 14 |- ([(j` (d + 1)) / z][(j` d) / x]ps -> A.z[(j` (d + 1)) / z][(j` d) / x]ps)
73	70, 72	hban 1356	. . . . . . . . . . . . 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))
74	69, 73	hbrex 2149	. . . . . . . . . . . 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))
75		feq1 4551	. . . . . . . . . . . . . . 15 |- (z = (j` (d + 1)) -> (z:(1...(q + 1))-->A <-> (j` (d + 1)):(1...(q + 1))-->A))
76	75	anbi2d 678	. . . . . . . . . . . . . 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)))
77		sbceq1a 2456	. . . . . . . . . . . . . 14 |- (z = (j` (d + 1)) -> ([(j` d) / x]ps <-> [(j` (d + 1)) / z][(j` d) / x]ps))
78	76, 77	anbi12d 690	. . . . . . . . . . . . 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)))
79	78	rexbidv 2124	. . . . . . . . . . . 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)))
80	74, 71, 79	elabf 2402	. . . . . . . . . . 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))
81		visset 2295	. . . . . . . . . . . . . . . . . . . 20 |- d e. _V
82		fzopth 7674	. . . . . . . . . . . . . . . . . . . . 21 |- ((q e. (ZZ>=` 1) /\ d e. _V) -> ((1...q) = (1...d) <-> (1 = 1 /\ q = d)))
83		elnnuz 7609	. . . . . . . . . . . . . . . . . . . . 21 |- (q e. NN <-> q e. (ZZ>=` 1))
84	82, 83	sylanb 498	. . . . . . . . . . . . . . . . . . . 20 |- ((q e. NN /\ d e. _V) -> ((1...q) = (1...d) <-> (1 = 1 /\ q = d)))
85	81, 84	mpan2 760	. . . . . . . . . . . . . . . . . . 19 |- (q e. NN -> ((1...q) = (1...d) <-> (1 = 1 /\ q = d)))
86		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . 23 |- (q = d -> (q + 1) = (d + 1))
87	86	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . 22 |- (q = d -> (1...(q + 1)) = (1...(d + 1)))
88	87	feq2d 4557	. . . . . . . . . . . . . . . . . . . . 21 |- (q = d -> ((j` (d + 1)):(1...(q + 1))-->A <-> (j` (d + 1)):(1...(d + 1))-->A))
89	88	biimpd 170	. . . . . . . . . . . . . . . . . . . 20 |- (q = d -> ((j` (d + 1)):(1...(q + 1))-->A -> (j` (d + 1)):(1...(d + 1))-->A))
90	89	adantl 424	. . . . . . . . . . . . . . . . . . 19 |- ((1 = 1 /\ q = d) -> ((j` (d + 1)):(1...(q + 1))-->A -> (j` (d + 1)):(1...(d + 1))-->A))
91	85, 90	syl6bi 231	. . . . . . . . . . . . . . . . . 18 |- (q e. NN -> ((1...q) = (1...d) -> ((j` (d + 1)):(1...(q + 1))-->A -> (j` (d + 1)):(1...(d + 1))-->A)))
92		fndmu 4514	. . . . . . . . . . . . . . . . . . 19 |- (((j` d) Fn (1...q) /\ (j` d) Fn (1...d)) -> (1...q) = (1...d))
93		ffn 4562	. . . . . . . . . . . . . . . . . . 19 |- ((j` d):(1...q)-->A -> (j` d) Fn (1...q))
94		ffn 4562	. . . . . . . . . . . . . . . . . . 19 |- ((j` d):(1...d)-->A -> (j` d) Fn (1...d))
95	92, 93, 94	syl2an 503	. . . . . . . . . . . . . . . . . 18 |- (((j` d):(1...q)-->A /\ (j` d):(1...d)-->A) -> (1...q) = (1...d))
96	91, 95	syl5com 63	. . . . . . . . . . . . . . . . 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)))
97	96	ex 402	. . . . . . . . . . . . . . . 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))))
98	97	com24 41	. . . . . . . . . . . . . . 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))))
99	98	imp 377	. . . . . . . . . . . . . 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)))
100	99	impcom 378	. . . . . . . . . . . . 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))
101	100	adantrr 431	. . . . . . . . . . . 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))
102	101	r19.23aiva 2212	. . . . . . . . . . 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))
103	80, 102	sylbi 216	. . . . . . . . . 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))
104	68, 103	syl6 25	. . . . . . . . 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)))
105		ffvelrn 4787	. . . . . . . . . . . 12 |- ((j:NN-->S /\ d e. NN) -> (j` d) e. S)
106	105	expcom 403	. . . . . . . . . . 11 |- (d e. NN -> (j:NN-->S -> (j` d) e. S))
107		opreq1 4889	. . . . . . . . . . . . . 14 |- (w = d -> (w + 1) = (d + 1))
108	107	fveq2d 4685	. . . . . . . . . . . . 13 |- (w = d -> (j` (w + 1)) = (j` (d + 1)))
109		fveq2 4681	. . . . . . . . . . . . . 14 |- (w = d -> (j` w) = (j` d))
110	109	fveq2d 4685	. . . . . . . . . . . . 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)))
111	108, 110	eleq12d 1965	. . . . . . . . . . . 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))))
112	111	rcla4v 2376	. . . . . . . . . . 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))))
113	106, 112	anim12d 617	. . . . . . . . . 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)))))
114	113	impcom 378	. . . . . . . . 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))))
115	104, 114	syl5 20	. . . . . . . 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)))
116	115	expdimp 406	. . . . . . 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)))
117	116	adantlr 429	. . . . . 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)))
118	117	3adantr2 1036	. . . . 5 |- (((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)))) -> (d e. NN -> ((j` d):(1...d)-->A -> (j` (d + 1)):(1...(d + 1))-->A)))
119	118	com12 14	. . . 4 |- (d e. NN -> (((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 -> (j` (d + 1)):(1...(d + 1))-->A)))
120	119	a2d 16	. . 3 |- (d e. NN -> ((((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) -> (((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)))
121	6, 12, 18, 24, 34, 120	nnind 7120	. 2 |- (C e. NN -> (((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))
122	121	impcom 378	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)))) /\ C e. NN) -> (j` C):(1...C)-->A)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  [wsbc 1534  {cab 1871  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593  {csn 3044  {copab 3395   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884  1c1 6387   + caddc 6389  NNcn 6449  ZZcz 6451  ZZ>=cuz 7586  ...cfz 7637

This theorem is referenced by:  sdc 15811

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-n 7108  df-z 7345  df-uz 7587  df-fz 7638

Copyright terms: Public domain