Theorem sdc 15811

Description: Strong dependent choice. Suppose we may choose an element of A such that property ps holds, and suppose that if we have already chosen the first k elements (represented here by a function from 1...k to A), we may choose another element so that all k + 1 elements taken together have property ps. Then there exists an infinite sequence of elements of A such that the first n terms of this sequence satisfy ps for all n. This theorem allows us to construct infinite seqeunces where each term depends on all the previous terms in the sequence.

Hypotheses

Ref	Expression
sdc.1	|- (g = h -> (ps <-> ch))
sdc.2	|- (g = r -> (ps <-> ta))
sdc.3	|- (g = s -> (ps <-> ze))
sdc.4	|- (g = (f |` (1...n)) -> (ps <-> rh))
sdc.5	|- (n = 1 -> (ch <-> th))
sdc.6	|- (n = k -> (ta <-> et))
sdc.7	|- (n = (k + 1) -> (ze <-> si))
sdc.8	|- (ph -> A e. C)
sdc.9	|- (ph -> E.h(h:{1}-->A /\ th))
sdc.10	|- ((ph /\ k e. NN) -> ((r:(1...k)-->A /\ et) -> E.s(s:(1...(k + 1))-->A /\ A.v e. (1...k)(s` v) = (r` v) /\ si)))

Assertion

Ref	Expression
sdc	|- (ph -> E.f(f:NN-->A /\ A.n e. NN rh))

Distinct variable groups:   A,g,h,n,r,s,k,v,f   rh,h,g   th,n   ta,g,k   ph,g,n,h,r,k   si,n   ze,g   ch,g   ps,r,s,k,f

Proof of Theorem sdc

Step	Hyp	Ref	Expression
1		sdc.9	. 2 |- (ph -> E.h(h:{1}-->A /\ th))
2		abrexex2g 15738	. . . . . . . 8 |- ((NN e. _V /\ A.n e. NN {g | (g:(1...n)-->A /\ ps)} e. _V) -> {g | E.n e. NN (g:(1...n)-->A /\ ps)} e. _V)
3		nnex 7116	. . . . . . . 8 |- NN e. _V
4		ssexg 3457	. . . . . . . . . . 11 |- (({g | (g:(1...n)-->A /\ ps)} C_ {g | g:(1...n)-->A} /\ {g | g:(1...n)-->A} e. _V) -> {g | (g:(1...n)-->A /\ ps)} e. _V)
5		simpl 346	. . . . . . . . . . . 12 |- ((g:(1...n)-->A /\ ps) -> g:(1...n)-->A)
6	5	ss2abi 2679	. . . . . . . . . . 11 |- {g | (g:(1...n)-->A /\ ps)} C_ {g | g:(1...n)-->A}
7		mapex 5387	. . . . . . . . . . . 12 |- (((1...n) e. _V /\ A e. C) -> {g | g:(1...n)-->A} e. _V)
8		oprex 4907	. . . . . . . . . . . 12 |- (1...n) e. _V
9		sdc.8	. . . . . . . . . . . 12 |- (ph -> A e. C)
10	7, 8, 9	sylancr 526	. . . . . . . . . . 11 |- (ph -> {g | g:(1...n)-->A} e. _V)
11	4, 6, 10	sylancr 526	. . . . . . . . . 10 |- (ph -> {g | (g:(1...n)-->A /\ ps)} e. _V)
12	11	a1d 15	. . . . . . . . 9 |- (ph -> (n e. NN -> {g | (g:(1...n)-->A /\ ps)} e. _V))
13	12	r19.21aiv 2175	. . . . . . . 8 |- (ph -> A.n e. NN {g | (g:(1...n)-->A /\ ps)} e. _V)
14	2, 3, 13	sylancr 526	. . . . . . 7 |- (ph -> {g | E.n e. NN (g:(1...n)-->A /\ ps)} e. _V)
15	14	adantr 425	. . . . . 6 |- ((ph /\ (h:{1}-->A /\ th)) -> {g | E.n e. NN (g:(1...n)-->A /\ ps)} e. _V)
16		ax-17 1317	. . . . . . . . . 10 |- ((ph /\ (h:{1}-->A /\ th)) -> A.n(ph /\ (h:{1}-->A /\ th)))
17		ax-17 1317	. . . . . . . . . . . . 13 |- (q e. NN -> A.n q e. NN)
18		ax-17 1317	. . . . . . . . . . . . . 14 |- ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) -> A.n(x:(1...q)-->A /\ z:(1...(q + 1))-->A))
19		ax-17 1317	. . . . . . . . . . . . . . 15 |- (A.v e. (1...q)(z` v) = (x` v) -> A.nA.v e. (1...q)(z` v) = (x` v))
20		oprex 4907	. . . . . . . . . . . . . . . 16 |- (q + 1) e. _V
21	20	hbsbc1v 2464	. . . . . . . . . . . . . . 15 |- ([(q + 1) / n][z / g]ps -> A.n[(q + 1) / n][z / g]ps)
22	19, 21	hban 1356	. . . . . . . . . . . . . 14 |- ((A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps) -> A.n(A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))
23	18, 22	hban 1356	. . . . . . . . . . . . 13 |- (((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps)) -> A.n((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps)))
24	17, 23	hbrex 2149	. . . . . . . . . . . 12 |- (E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps)) -> A.nE.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps)))
25	24	hbab 1875	. . . . . . . . . . 11 |- (u e. {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} -> A.n u e. {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})
26		hbre1 2150	. . . . . . . . . . . . . 14 |- (E.n e. NN (g:(1...n)-->A /\ ps) -> A.nE.n e. NN (g:(1...n)-->A /\ ps))
27	26	hbab 1875	. . . . . . . . . . . . 13 |- (u e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} -> A.n u e. {g | E.n e. NN (g:(1...n)-->A /\ ps)})
28	27	hbpw 3041	. . . . . . . . . . . 12 |- (u e. ~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} -> A.n u e. ~P{g | E.n e. NN (g:(1...n)-->A /\ ps)})
29		ax-17 1317	. . . . . . . . . . . 12 |- (u e. {(/)} -> A.n u e. {(/)})
30	28, 29	hbdif 2729	. . . . . . . . . . 11 |- (u e. (~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} \ {(/)}) -> A.n u e. (~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} \ {(/)}))
31	25, 30	hbel 1996	. . . . . . . . . 10 |- ({z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} e. (~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} \ {(/)}) -> A.n{z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} e. (~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} \ {(/)}))
32		eldifsn 3123	. . . . . . . . . . . 12 |- ({z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} e. (~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} \ {(/)}) <-> ({z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} e. ~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} =/= (/)))
33		ax-17 1317	. . . . . . . . . . . . . . . . . . . . 21 |- (z:(1...(q + 1))-->A -> A.n z:(1...(q + 1))-->A)
34	33, 21	hban 1356	. . . . . . . . . . . . . . . . . . . 20 |- ((z:(1...(q + 1))-->A /\ [(q + 1) / n][z / g]ps) -> A.n(z:(1...(q + 1))-->A /\ [(q + 1) / n][z / g]ps))
35		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . 22 |- (n = (q + 1) -> (1...n) = (1...(q + 1)))
36	35	feq2d 4557	. . . . . . . . . . . . . . . . . . . . 21 |- (n = (q + 1) -> (z:(1...n)-->A <-> z:(1...(q + 1))-->A))
37		sbceq1a 2456	. . . . . . . . . . . . . . . . . . . . 21 |- (n = (q + 1) -> ([z / g]ps <-> [(q + 1) / n][z / g]ps))
38	36, 37	anbi12d 690	. . . . . . . . . . . . . . . . . . . 20 |- (n = (q + 1) -> ((z:(1...n)-->A /\ [z / g]ps) <-> (z:(1...(q + 1))-->A /\ [(q + 1) / n][z / g]ps)))
39	34, 38	rcla4e 2375	. . . . . . . . . . . . . . . . . . 19 |- (((q + 1) e. NN /\ (z:(1...(q + 1))-->A /\ [(q + 1) / n][z / g]ps)) -> E.n e. NN (z:(1...n)-->A /\ [z / g]ps))
40		peano2nn 7118	. . . . . . . . . . . . . . . . . . 19 |- (q e. NN -> (q + 1) e. NN)
41	39, 40	sylan 497	. . . . . . . . . . . . . . . . . 18 |- ((q e. NN /\ (z:(1...(q + 1))-->A /\ [(q + 1) / n][z / g]ps)) -> E.n e. NN (z:(1...n)-->A /\ [z / g]ps))
42		ax-17 1317	. . . . . . . . . . . . . . . . . . . 20 |- (n e. NN -> A.g n e. NN)
43		ax-17 1317	. . . . . . . . . . . . . . . . . . . . 21 |- (z:(1...n)-->A -> A.g z:(1...n)-->A)
44		visset 2295	. . . . . . . . . . . . . . . . . . . . . 22 |- z e. _V
45	44	hbsbc1v 2464	. . . . . . . . . . . . . . . . . . . . 21 |- ([z / g]ps -> A.g[z / g]ps)
46	43, 45	hban 1356	. . . . . . . . . . . . . . . . . . . 20 |- ((z:(1...n)-->A /\ [z / g]ps) -> A.g(z:(1...n)-->A /\ [z / g]ps))
47	42, 46	hbrex 2149	. . . . . . . . . . . . . . . . . . 19 |- (E.n e. NN (z:(1...n)-->A /\ [z / g]ps) -> A.gE.n e. NN (z:(1...n)-->A /\ [z / g]ps))
48		feq1 4551	. . . . . . . . . . . . . . . . . . . . 21 |- (g = z -> (g:(1...n)-->A <-> z:(1...n)-->A))
49		sbceq1a 2456	. . . . . . . . . . . . . . . . . . . . 21 |- (g = z -> (ps <-> [z / g]ps))
50	48, 49	anbi12d 690	. . . . . . . . . . . . . . . . . . . 20 |- (g = z -> ((g:(1...n)-->A /\ ps) <-> (z:(1...n)-->A /\ [z / g]ps)))
51	50	rexbidv 2124	. . . . . . . . . . . . . . . . . . 19 |- (g = z -> (E.n e. NN (g:(1...n)-->A /\ ps) <-> E.n e. NN (z:(1...n)-->A /\ [z / g]ps)))
52	47, 44, 51	elabf 2402	. . . . . . . . . . . . . . . . . 18 |- (z e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} <-> E.n e. NN (z:(1...n)-->A /\ [z / g]ps))
53	41, 52	sylibr 217	. . . . . . . . . . . . . . . . 17 |- ((q e. NN /\ (z:(1...(q + 1))-->A /\ [(q + 1) / n][z / g]ps)) -> z e. {g | E.n e. NN (g:(1...n)-->A /\ ps)})
54	53	adantrrl 438	. . . . . . . . . . . . . . . 16 |- ((q e. NN /\ (z:(1...(q + 1))-->A /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))) -> z e. {g | E.n e. NN (g:(1...n)-->A /\ ps)})
55	54	adantrll 436	. . . . . . . . . . . . . . 15 |- ((q e. NN /\ ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))) -> z e. {g | E.n e. NN (g:(1...n)-->A /\ ps)})
56	55	r19.23aiva 2212	. . . . . . . . . . . . . 14 |- (E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps)) -> z e. {g | E.n e. NN (g:(1...n)-->A /\ ps)})
57	56	abssi 2682	. . . . . . . . . . . . 13 |- {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} C_ {g | E.n e. NN (g:(1...n)-->A /\ ps)}
58		elpw2g 3463	. . . . . . . . . . . . . . . 16 |- ({g | E.n e. NN (g:(1...n)-->A /\ ps)} e. _V -> ({z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} e. ~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} <-> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} C_ {g | E.n e. NN (g:(1...n)-->A /\ ps)}))
59	14, 58	syl 12	. . . . . . . . . . . . . . 15 |- (ph -> ({z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} e. ~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} <-> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} C_ {g | E.n e. NN (g:(1...n)-->A /\ ps)}))
60	59	adantr 425	. . . . . . . . . . . . . 14 |- ((ph /\ (h:{1}-->A /\ th)) -> ({z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} e. ~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} <-> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} C_ {g | E.n e. NN (g:(1...n)-->A /\ ps)}))
61	60	ad2antrr 440	. . . . . . . . . . . . 13 |- ((((ph /\ (h:{1}-->A /\ th)) /\ n e. NN) /\ (x:(1...n)-->A /\ [x / g]ps)) -> ({z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} e. ~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} <-> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} C_ {g | E.n e. NN (g:(1...n)-->A /\ ps)}))
62	57, 61	mpbiri 211	. . . . . . . . . . . 12 |- ((((ph /\ (h:{1}-->A /\ th)) /\ n e. NN) /\ (x:(1...n)-->A /\ [x / g]ps)) -> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} e. ~P{g | E.n e. NN (g:(1...n)-->A /\ ps)})
63		feq1 4551	. . . . . . . . . . . . . . . . 17 |- (r = x -> (r:(1...n)-->A <-> x:(1...n)-->A))
64		dfsbcq 2455	. . . . . . . . . . . . . . . . . 18 |- (r = x -> ([r / g]ps <-> [x / g]ps))
65		visset 2295	. . . . . . . . . . . . . . . . . . 19 |- r e. _V
66		sdc.2	. . . . . . . . . . . . . . . . . . 19 |- (g = r -> (ps <-> ta))
67	65, 66	sbcie 2485	. . . . . . . . . . . . . . . . . 18 |- ([r / g]ps <-> ta)
68	64, 67	syl5bbr 593	. . . . . . . . . . . . . . . . 17 |- (r = x -> (ta <-> [x / g]ps))
69	63, 68	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (r = x -> ((r:(1...n)-->A /\ ta) <-> (x:(1...n)-->A /\ [x / g]ps)))
70	69	anbi2d 678	. . . . . . . . . . . . . . 15 |- (r = x -> (((ph /\ n e. NN) /\ (r:(1...n)-->A /\ ta)) <-> ((ph /\ n e. NN) /\ (x:(1...n)-->A /\ [x / g]ps))))
71		feq1 4551	. . . . . . . . . . . . . . . . . . . 20 |- (r = x -> (r:(1...q)-->A <-> x:(1...q)-->A))
72	71	anbi1d 679	. . . . . . . . . . . . . . . . . . 19 |- (r = x -> ((r:(1...q)-->A /\ z:(1...(q + 1))-->A) <-> (x:(1...q)-->A /\ z:(1...(q + 1))-->A)))
73		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . 22 |- (r = x -> (r` v) = (x` v))
74	73	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . 21 |- (r = x -> ((z` v) = (r` v) <-> (z` v) = (x` v)))
75	74	ralbidv 2123	. . . . . . . . . . . . . . . . . . . 20 |- (r = x -> (A.v e. (1...q)(z` v) = (r` v) <-> A.v e. (1...q)(z` v) = (x` v)))
76	75	anbi1d 679	. . . . . . . . . . . . . . . . . . 19 |- (r = x -> ((A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps) <-> (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps)))
77	72, 76	anbi12d 690	. . . . . . . . . . . . . . . . . 18 |- (r = x -> (((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps)) <-> ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))))
78	77	rexbidv 2124	. . . . . . . . . . . . . . . . 17 |- (r = x -> (E.q e. NN ((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps)) <-> E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))))
79	78	abbidv 2008	. . . . . . . . . . . . . . . 16 |- (r = x -> {z | E.q e. NN ((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps))} = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})
80	79	neeq1d 2028	. . . . . . . . . . . . . . 15 |- (r = x -> ({z | E.q e. NN ((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps))} =/= (/) <-> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} =/= (/)))
81	70, 80	imbi12d 688	. . . . . . . . . . . . . 14 |- (r = x -> ((((ph /\ n e. NN) /\ (r:(1...n)-->A /\ ta)) -> {z | E.q e. NN ((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps))} =/= (/)) <-> (((ph /\ n e. NN) /\ (x:(1...n)-->A /\ [x / g]ps)) -> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} =/= (/))))
82		eleq1 1957	. . . . . . . . . . . . . . . . . 18 |- (k = n -> (k e. NN <-> n e. NN))
83	82	anbi2d 678	. . . . . . . . . . . . . . . . 17 |- (k = n -> ((ph /\ k e. NN) <-> (ph /\ n e. NN)))
84		opreq2 4890	. . . . . . . . . . . . . . . . . . 19 |- (k = n -> (1...k) = (1...n))
85	84	feq2d 4557	. . . . . . . . . . . . . . . . . 18 |- (k = n -> (r:(1...k)-->A <-> r:(1...n)-->A))
86		sdc.6	. . . . . . . . . . . . . . . . . . . 20 |- (n = k -> (ta <-> et))
87	86	bicomd 580	. . . . . . . . . . . . . . . . . . 19 |- (n = k -> (et <-> ta))
88	87	eqcoms 1887	. . . . . . . . . . . . . . . . . 18 |- (k = n -> (et <-> ta))
89	85, 88	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (k = n -> ((r:(1...k)-->A /\ et) <-> (r:(1...n)-->A /\ ta)))
90	83, 89	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (k = n -> (((ph /\ k e. NN) /\ (r:(1...k)-->A /\ et)) <-> ((ph /\ n e. NN) /\ (r:(1...n)-->A /\ ta))))
91	90	imbi1d 675	. . . . . . . . . . . . . . 15 |- (k = n -> ((((ph /\ k e. NN) /\ (r:(1...k)-->A /\ et)) -> {z | E.q e. NN ((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps))} =/= (/)) <-> (((ph /\ n e. NN) /\ (r:(1...n)-->A /\ ta)) -> {z | E.q e. NN ((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps))} =/= (/))))
92		simplr 449	. . . . . . . . . . . . . . . . . 18 |- (((ph /\ k e. NN) /\ (r:(1...k)-->A /\ et)) -> k e. NN)
93		simprl 450	. . . . . . . . . . . . . . . . . . . 20 |- (((ph /\ k e. NN) /\ (r:(1...k)-->A /\ et)) -> r:(1...k)-->A)
94		sdc.10	. . . . . . . . . . . . . . . . . . . . 21 |- ((ph /\ k e. NN) -> ((r:(1...k)-->A /\ et) -> E.s(s:(1...(k + 1))-->A /\ A.v e. (1...k)(s` v) = (r` v) /\ si)))
95	94	imp 377	. . . . . . . . . . . . . . . . . . . 20 |- (((ph /\ k e. NN) /\ (r:(1...k)-->A /\ et)) -> E.s(s:(1...(k + 1))-->A /\ A.v e. (1...k)(s` v) = (r` v) /\ si))
96	93, 95	jca 310	. . . . . . . . . . . . . . . . . . 19 |- (((ph /\ k e. NN) /\ (r:(1...k)-->A /\ et)) -> (r:(1...k)-->A /\ E.s(s:(1...(k + 1))-->A /\ A.v e. (1...k)(s` v) = (r` v) /\ si)))
97		19.42v 1688	. . . . . . . . . . . . . . . . . . . 20 |- (E.s(r:(1...k)-->A /\ (s:(1...(k + 1))-->A /\ A.v e. (1...k)(s` v) = (r` v) /\ si)) <-> (r:(1...k)-->A /\ E.s(s:(1...(k + 1))-->A /\ A.v e. (1...k)(s` v) = (r` v) /\ si)))
98		3anass 862	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((s:(1...(k + 1))-->A /\ A.v e. (1...k)(s` v) = (r` v) /\ si) <-> (s:(1...(k + 1))-->A /\ (A.v e. (1...k)(s` v) = (r` v) /\ si)))
99	98	anbi2i 538	. . . . . . . . . . . . . . . . . . . . . 22 |- ((r:(1...k)-->A /\ (s:(1...(k + 1))-->A /\ A.v e. (1...k)(s` v) = (r` v) /\ si)) <-> (r:(1...k)-->A /\ (s:(1...(k + 1))-->A /\ (A.v e. (1...k)(s` v) = (r` v) /\ si))))
100		anass 487	. . . . . . . . . . . . . . . . . . . . . 22 |- (((r:(1...k)-->A /\ s:(1...(k + 1))-->A) /\ (A.v e. (1...k)(s` v) = (r` v) /\ si)) <-> (r:(1...k)-->A /\ (s:(1...(k + 1))-->A /\ (A.v e. (1...k)(s` v) = (r` v) /\ si))))
101	99, 100	bitr4i 193	. . . . . . . . . . . . . . . . . . . . 21 |- ((r:(1...k)-->A /\ (s:(1...(k + 1))-->A /\ A.v e. (1...k)(s` v) = (r` v) /\ si)) <-> ((r:(1...k)-->A /\ s:(1...(k + 1))-->A) /\ (A.v e. (1...k)(s` v) = (r` v) /\ si)))
102	101	exbii 1398	. . . . . . . . . . . . . . . . . . . 20 |- (E.s(r:(1...k)-->A /\ (s:(1...(k + 1))-->A /\ A.v e. (1...k)(s` v) = (r` v) /\ si)) <-> E.s((r:(1...k)-->A /\ s:(1...(k + 1))-->A) /\ (A.v e. (1...k)(s` v) = (r` v) /\ si)))
103	97, 102	bitr3i 192	. . . . . . . . . . . . . . . . . . 19 |- ((r:(1...k)-->A /\ E.s(s:(1...(k + 1))-->A /\ A.v e. (1...k)(s` v) = (r` v) /\ si)) <-> E.s((r:(1...k)-->A /\ s:(1...(k + 1))-->A) /\ (A.v e. (1...k)(s` v) = (r` v) /\ si)))
104	96, 103	sylib 215	. . . . . . . . . . . . . . . . . 18 |- (((ph /\ k e. NN) /\ (r:(1...k)-->A /\ et)) -> E.s((r:(1...k)-->A /\ s:(1...(k + 1))-->A) /\ (A.v e. (1...k)(s` v) = (r` v) /\ si)))
105		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . 23 |- (q = k -> (1...q) = (1...k))
106	105	feq2d 4557	. . . . . . . . . . . . . . . . . . . . . 22 |- (q = k -> (r:(1...q)-->A <-> r:(1...k)-->A))
107		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (q = k -> (q + 1) = (k + 1))
108	107	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . 23 |- (q = k -> (1...(q + 1)) = (1...(k + 1)))
109	108	feq2d 4557	. . . . . . . . . . . . . . . . . . . . . 22 |- (q = k -> (s:(1...(q + 1))-->A <-> s:(1...(k + 1))-->A))
110	106, 109	anbi12d 690	. . . . . . . . . . . . . . . . . . . . 21 |- (q = k -> ((r:(1...q)-->A /\ s:(1...(q + 1))-->A) <-> (r:(1...k)-->A /\ s:(1...(k + 1))-->A)))
111	105	raleqdv 2269	. . . . . . . . . . . . . . . . . . . . . 22 |- (q = k -> (A.v e. (1...q)(s` v) = (r` v) <-> A.v e. (1...k)(s` v) = (r` v)))
112		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((q + 1) = (k + 1) -> ([(q + 1) / n]ze <-> [(k + 1) / n]ze))
113		oprex 4907	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (k + 1) e. _V
114		sdc.7	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (n = (k + 1) -> (ze <-> si))
115	113, 114	sbcie 2485	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ([(k + 1) / n]ze <-> si)
116	112, 115	syl6bb 595	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((q + 1) = (k + 1) -> ([(q + 1) / n]ze <-> si))
117	107, 116	syl 12	. . . . . . . . . . . . . . . . . . . . . 22 |- (q = k -> ([(q + 1) / n]ze <-> si))
118	111, 117	anbi12d 690	. . . . . . . . . . . . . . . . . . . . 21 |- (q = k -> ((A.v e. (1...q)(s` v) = (r` v) /\ [(q + 1) / n]ze) <-> (A.v e. (1...k)(s` v) = (r` v) /\ si)))
119	110, 118	anbi12d 690	. . . . . . . . . . . . . . . . . . . 20 |- (q = k -> (((r:(1...q)-->A /\ s:(1...(q + 1))-->A) /\ (A.v e. (1...q)(s` v) = (r` v) /\ [(q + 1) / n]ze)) <-> ((r:(1...k)-->A /\ s:(1...(k + 1))-->A) /\ (A.v e. (1...k)(s` v) = (r` v) /\ si))))
120	119	exbidv 1657	. . . . . . . . . . . . . . . . . . 19 |- (q = k -> (E.s((r:(1...q)-->A /\ s:(1...(q + 1))-->A) /\ (A.v e. (1...q)(s` v) = (r` v) /\ [(q + 1) / n]ze)) <-> E.s((r:(1...k)-->A /\ s:(1...(k + 1))-->A) /\ (A.v e. (1...k)(s` v) = (r` v) /\ si))))
121	120	rcla4ev 2381	. . . . . . . . . . . . . . . . . 18 |- ((k e. NN /\ E.s((r:(1...k)-->A /\ s:(1...(k + 1))-->A) /\ (A.v e. (1...k)(s` v) = (r` v) /\ si))) -> E.q e. NN E.s((r:(1...q)-->A /\ s:(1...(q + 1))-->A) /\ (A.v e. (1...q)(s` v) = (r` v) /\ [(q + 1) / n]ze)))
122	92, 104, 121	syl11anc 524	. . . . . . . . . . . . . . . . 17 |- (((ph /\ k e. NN) /\ (r:(1...k)-->A /\ et)) -> E.q e. NN E.s((r:(1...q)-->A /\ s:(1...(q + 1))-->A) /\ (A.v e. (1...q)(s` v) = (r` v) /\ [(q + 1) / n]ze)))
123		feq1 4551	. . . . . . . . . . . . . . . . . . . . . 22 |- (s = z -> (s:(1...(q + 1))-->A <-> z:(1...(q + 1))-->A))
124	123	anbi2d 678	. . . . . . . . . . . . . . . . . . . . 21 |- (s = z -> ((r:(1...q)-->A /\ s:(1...(q + 1))-->A) <-> (r:(1...q)-->A /\ z:(1...(q + 1))-->A)))
125		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (s = z -> (s` v) = (z` v))
126	125	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . . . . 23 |- (s = z -> ((s` v) = (r` v) <-> (z` v) = (r` v)))
127	126	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . 22 |- (s = z -> (A.v e. (1...q)(s` v) = (r` v) <-> A.v e. (1...q)(z` v) = (r` v)))
128		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (s = z -> ([s / g]ps <-> [z / g]ps))
129		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- s e. _V
130		sdc.3	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (g = s -> (ps <-> ze))
131	129, 130	sbcie 2485	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ([s / g]ps <-> ze)
132	128, 131	syl5bbr 593	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (s = z -> (ze <-> [z / g]ps))
133	132	sbcbidv 2505	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((s = z /\ (q + 1) e. _V) -> ([(q + 1) / n]ze <-> [(q + 1) / n][z / g]ps))
134	20, 133	mpan2 760	. . . . . . . . . . . . . . . . . . . . . 22 |- (s = z -> ([(q + 1) / n]ze <-> [(q + 1) / n][z / g]ps))
135	127, 134	anbi12d 690	. . . . . . . . . . . . . . . . . . . . 21 |- (s = z -> ((A.v e. (1...q)(s` v) = (r` v) /\ [(q + 1) / n]ze) <-> (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps)))
136	124, 135	anbi12d 690	. . . . . . . . . . . . . . . . . . . 20 |- (s = z -> (((r:(1...q)-->A /\ s:(1...(q + 1))-->A) /\ (A.v e. (1...q)(s` v) = (r` v) /\ [(q + 1) / n]ze)) <-> ((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps))))
137	136	cbvexv 1697	. . . . . . . . . . . . . . . . . . 19 |- (E.s((r:(1...q)-->A /\ s:(1...(q + 1))-->A) /\ (A.v e. (1...q)(s` v) = (r` v) /\ [(q + 1) / n]ze)) <-> E.z((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps)))
138	137	rexbii 2128	. . . . . . . . . . . . . . . . . 18 |- (E.q e. NN E.s((r:(1...q)-->A /\ s:(1...(q + 1))-->A) /\ (A.v e. (1...q)(s` v) = (r` v) /\ [(q + 1) / n]ze)) <-> E.q e. NN E.z((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps)))
139		rexcom4 2312	. . . . . . . . . . . . . . . . . 18 |- (E.q e. NN E.z((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps)) <-> E.zE.q e. NN ((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps)))
140	138, 139	bitri 190	. . . . . . . . . . . . . . . . 17 |- (E.q e. NN E.s((r:(1...q)-->A /\ s:(1...(q + 1))-->A) /\ (A.v e. (1...q)(s` v) = (r` v) /\ [(q + 1) / n]ze)) <-> E.zE.q e. NN ((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps)))
141	122, 140	sylib 215	. . . . . . . . . . . . . . . 16 |- (((ph /\ k e. NN) /\ (r:(1...k)-->A /\ et)) -> E.zE.q e. NN ((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps)))
142		abn0 2892	. . . . . . . . . . . . . . . 16 |- ({z | E.q e. NN ((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps))} =/= (/) <-> E.zE.q e. NN ((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps)))
143	141, 142	sylibr 217	. . . . . . . . . . . . . . 15 |- (((ph /\ k e. NN) /\ (r:(1...k)-->A /\ et)) -> {z | E.q e. NN ((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps))} =/= (/))
144	91, 143	chvarv 1712	. . . . . . . . . . . . . 14 |- (((ph /\ n e. NN) /\ (r:(1...n)-->A /\ ta)) -> {z | E.q e. NN ((r:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (r` v) /\ [(q + 1) / n][z / g]ps))} =/= (/))
145	81, 144	chvarv 1712	. . . . . . . . . . . . 13 |- (((ph /\ n e. NN) /\ (x:(1...n)-->A /\ [x / g]ps)) -> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} =/= (/))
146	145	adantllr 433	. . . . . . . . . . . 12 |- ((((ph /\ (h:{1}-->A /\ th)) /\ n e. NN) /\ (x:(1...n)-->A /\ [x / g]ps)) -> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} =/= (/))
147	32, 62, 146	sylanbrc 527	. . . . . . . . . . 11 |- ((((ph /\ (h:{1}-->A /\ th)) /\ n e. NN) /\ (x:(1...n)-->A /\ [x / g]ps)) -> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} e. (~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} \ {(/)}))
148	147	exp31 407	. . . . . . . . . 10 |- ((ph /\ (h:{1}-->A /\ th)) -> (n e. NN -> ((x:(1...n)-->A /\ [x / g]ps) -> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} e. (~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} \ {(/)}))))
149	16, 31, 148	r19.23ad 2213	. . . . . . . . 9 |- ((ph /\ (h:{1}-->A /\ th)) -> (E.n e. NN (x:(1...n)-->A /\ [x / g]ps) -> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} e. (~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} \ {(/)})))
150		ax-17 1317	. . . . . . . . . . . 12 |- (x:(1...n)-->A -> A.g x:(1...n)-->A)
151		visset 2295	. . . . . . . . . . . . 13 |- x e. _V
152	151	hbsbc1v 2464	. . . . . . . . . . . 12 |- ([x / g]ps -> A.g[x / g]ps)
153	150, 152	hban 1356	. . . . . . . . . . 11 |- ((x:(1...n)-->A /\ [x / g]ps) -> A.g(x:(1...n)-->A /\ [x / g]ps))
154	42, 153	hbrex 2149	. . . . . . . . . 10 |- (E.n e. NN (x:(1...n)-->A /\ [x / g]ps) -> A.gE.n e. NN (x:(1...n)-->A /\ [x / g]ps))
155		feq1 4551	. . . . . . . . . . . 12 |- (g = x -> (g:(1...n)-->A <-> x:(1...n)-->A))
156		sbceq1a 2456	. . . . . . . . . . . 12 |- (g = x -> (ps <-> [x / g]ps))
157	155, 156	anbi12d 690	. . . . . . . . . . 11 |- (g = x -> ((g:(1...n)-->A /\ ps) <-> (x:(1...n)-->A /\ [x / g]ps)))
158	157	rexbidv 2124	. . . . . . . . . 10 |- (g = x -> (E.n e. NN (g:(1...n)-->A /\ ps) <-> E.n e. NN (x:(1...n)-->A /\ [x / g]ps)))
159	154, 151, 158	elabf 2402	. . . . . . . . 9 |- (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} <-> E.n e. NN (x:(1...n)-->A /\ [x / g]ps))
160	149, 159	syl5ib 223	. . . . . . . 8 |- ((ph /\ (h:{1}-->A /\ th)) -> (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} -> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} e. (~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} \ {(/)})))
161	160	r19.21aiv 2175	. . . . . . 7 |- ((ph /\ (h:{1}-->A /\ th)) -> A.x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)}{z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} e. (~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} \ {(/)}))
162		eqid 1884	. . . . . . . 8 |- {<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})} = {<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}
163	162	fopab2 4796	. . . . . . 7 |- (A.x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)}{z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} e. (~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} \ {(/)}) <-> {<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}:{g | E.n e. NN (g:(1...n)-->A /\ ps)}-->(~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} \ {(/)}))
164	161, 163	sylib 215	. . . . . 6 |- ((ph /\ (h:{1}-->A /\ th)) -> {<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}:{g | E.n e. NN (g:(1...n)-->A /\ ps)}-->(~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} \ {(/)}))
165		1nn 7117	. . . . . . . . 9 |- 1 e. NN
166		opreq2 4890	. . . . . . . . . . . . 13 |- (n = 1 -> (1...n) = (1...1))
167		1z 7368	. . . . . . . . . . . . . 14 |- 1 e. ZZ
168		fzsn 7684	. . . . . . . . . . . . . 14 |- (1 e. ZZ -> (1...1) = {1})
169	167, 168	ax-mp 7	. . . . . . . . . . . . 13 |- (1...1) = {1}
170	166, 169	syl6eq 1944	. . . . . . . . . . . 12 |- (n = 1 -> (1...n) = {1})
171	170	feq2d 4557	. . . . . . . . . . 11 |- (n = 1 -> (h:(1...n)-->A <-> h:{1}-->A))
172		sdc.5	. . . . . . . . . . 11 |- (n = 1 -> (ch <-> th))
173	171, 172	anbi12d 690	. . . . . . . . . 10 |- (n = 1 -> ((h:(1...n)-->A /\ ch) <-> (h:{1}-->A /\ th)))
174	173	rcla4ev 2381	. . . . . . . . 9 |- ((1 e. NN /\ (h:{1}-->A /\ th)) -> E.n e. NN (h:(1...n)-->A /\ ch))
175	165, 174	mpan 759	. . . . . . . 8 |- ((h:{1}-->A /\ th) -> E.n e. NN (h:(1...n)-->A /\ ch))
176		visset 2295	. . . . . . . . 9 |- h e. _V
177		feq1 4551	. . . . . . . . . . 11 |- (g = h -> (g:(1...n)-->A <-> h:(1...n)-->A))
178		sdc.1	. . . . . . . . . . 11 |- (g = h -> (ps <-> ch))
179	177, 178	anbi12d 690	. . . . . . . . . 10 |- (g = h -> ((g:(1...n)-->A /\ ps) <-> (h:(1...n)-->A /\ ch)))
180	179	rexbidv 2124	. . . . . . . . 9 |- (g = h -> (E.n e. NN (g:(1...n)-->A /\ ps) <-> E.n e. NN (h:(1...n)-->A /\ ch)))
181	176, 180	elab 2403	. . . . . . . 8 |- (h e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} <-> E.n e. NN (h:(1...n)-->A /\ ch))
182	175, 181	sylibr 217	. . . . . . 7 |- ((h:{1}-->A /\ th) -> h e. {g | E.n e. NN (g:(1...n)-->A /\ ps)})
183	182	adantl 424	. . . . . 6 |- ((ph /\ (h:{1}-->A /\ th)) -> h e. {g | E.n e. NN (g:(1...n)-->A /\ ps)})
184		acdc3g 15751	. . . . . 6 |- (({g | E.n e. NN (g:(1...n)-->A /\ ps)} e. _V /\ {<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}:{g | E.n e. NN (g:(1...n)-->A /\ ps)}-->(~P{g | E.n e. NN (g:(1...n)-->A /\ ps)} \ {(/)}) /\ h e. {g | E.n e. NN (g:(1...n)-->A /\ ps)}) -> E.j(j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w))))
185	15, 164, 183, 184	syl111anc 1100	. . . . 5 |- ((ph /\ (h:{1}-->A /\ th)) -> E.j(j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w))))
186	167	a1i 8	. . . . . . . . . 10 |- (((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> 1 e. ZZ)
187		ffn 4562	. . . . . . . . . . . 12 |- (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} -> j Fn NN)
188	187	3ad2ant1 897	. . . . . . . . . . 11 |- ((j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w))) -> j Fn NN)
189	188	adantl 424	. . . . . . . . . 10 |- (((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> j Fn NN)
190	9	sdclem2 15810	. . . . . . . . . . . . 13 |- ((((ph /\ h:{1}-->A) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ c e. NN) -> (j` c):(1...c)-->A)
191		id 73	. . . . . . . . . . . . . 14 |- ((ph /\ h:{1}-->A) -> (ph /\ h:{1}-->A))
192	191	adantrr 431	. . . . . . . . . . . . 13 |- ((ph /\ (h:{1}-->A /\ th)) -> (ph /\ h:{1}-->A))
193	190, 192	sylanl1 509	. . . . . . . . . . . 12 |- ((((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ c e. NN) -> (j` c):(1...c)-->A)
194		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w = c -> (w + 1) = (c + 1))
195	194	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . 22 |- (w = c -> (j` (w + 1)) = (j` (c + 1)))
196		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w = c -> (j` w) = (j` c))
197	196	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . 22 |- (w = c -> ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)) = ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` c)))
198	195, 197	eleq12d 1965	. . . . . . . . . . . . . . . . . . . . 21 |- (w = c -> ((j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)) <-> (j` (c + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` c))))
199	198	rcla4va 2378	. . . . . . . . . . . . . . . . . . . 20 |- ((c e. NN /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w))) -> (j` (c + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` c)))
200	199	adantll 428	. . . . . . . . . . . . . . . . . . 19 |- (((ph /\ c e. NN) /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w))) -> (j` (c + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` c)))
201	200	adantlr 429	. . . . . . . . . . . . . . . . . 18 |- ((((ph /\ c e. NN) /\ j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)}) /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w))) -> (j` (c + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` c)))
202		feq1 4551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x = (j` c) -> (x:(1...q)-->A <-> (j` c):(1...q)-->A))
203	202	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = (j` c) -> ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) <-> ((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A)))
204		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (x = (j` c) -> (x` v) = ((j` c)` v))
205	204	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (x = (j` c) -> ((z` v) = (x` v) <-> (z` v) = ((j` c)` v)))
206	205	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x = (j` c) -> (A.v e. (1...q)(z` v) = (x` v) <-> A.v e. (1...q)(z` v) = ((j` c)` v)))
207	206	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = (j` c) -> ((A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps) <-> (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps)))
208	203, 207	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x = (j` c) -> (((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps)) <-> (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))))
209	208	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x = (j` c) -> (E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps)) <-> E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))))
210	209	abbidv 2008	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x = (j` c) -> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} = {z | E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))})
211	210, 162	fvopab4g 4742	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((j` c) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ {z | E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))} e. _V) -> ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` c)) = {z | E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))})
212		abrexex2g 15738	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((NN e. _V /\ A.q e. NN {z | (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))} e. _V) -> {z | E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))} e. _V)
213		ssexg 3457	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (({z | (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))} C_ {z | z:(1...(q + 1))-->A} /\ {z | z:(1...(q + 1))-->A} e. _V) -> {z | (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))} e. _V)
214		simplr 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps)) -> z:(1...(q + 1))-->A)
215	214	ss2abi 2679	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- {z | (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))} C_ {z | z:(1...(q + 1))-->A}
216		mapex 5387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((1...(q + 1)) e. _V /\ A e. C) -> {z | z:(1...(q + 1))-->A} e. _V)
217		oprex 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (1...(q + 1)) e. _V
218	216, 217, 9	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (ph -> {z | z:(1...(q + 1))-->A} e. _V)
219	213, 215, 218	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (ph -> {z | (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))} e. _V)
220	219	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((ph /\ q e. NN) -> {z | (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))} e. _V)
221	220	r19.21aiva 2176	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (ph -> A.q e. NN {z | (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))} e. _V)
222	212, 3, 221	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (ph -> {z | E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))} e. _V)
223	211, 222	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((j` c) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ ph) -> ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` c)) = {z | E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))})
224	223	ancoms 484	. . . . . . . . . . . . . . . . . . . . . 22 |- ((ph /\ (j` c) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)}) -> ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` c)) = {z | E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))})
225		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ c e. NN) -> (j` c) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)})
226	225	ancoms 484	. . . . . . . . . . . . . . . . . . . . . 22 |- ((c e. NN /\ j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)}) -> (j` c) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)})
227	224, 226	sylan2 500	. . . . . . . . . . . . . . . . . . . . 21 |- ((ph /\ (c e. NN /\ j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)})) -> ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` c)) = {z | E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))})
228	227	anassrs 489	. . . . . . . . . . . . . . . . . . . 20 |- (((ph /\ c e. NN) /\ j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)}) -> ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` c)) = {z | E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))})
229	228	eleq2d 1964	. . . . . . . . . . . . . . . . . . 19 |- (((ph /\ c e. NN) /\ j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)}) -> ((j` (c + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` c)) <-> (j` (c + 1)) e. {z | E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))}))
230	229	biimpa 460	. . . . . . . . . . . . . . . . . 18 |- ((((ph /\ c e. NN) /\ j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)}) /\ (j` (c + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` c))) -> (j` (c + 1)) e. {z | E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))})
231	201, 230	syldan 516	. . . . . . . . . . . . . . . . 17 |- ((((ph /\ c e. NN) /\ j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)}) /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w))) -> (j` (c + 1)) e. {z | E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))})
232	231	anasss 488	. . . . . . . . . . . . . . . 16 |- (((ph /\ c e. NN) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> (j` (c + 1)) e. {z | E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))})
233		fndmu 4514	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((j` c) Fn (1...q) /\ (j` c) Fn (1...c)) -> (1...q) = (1...c))
234		ffn 4562	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((j` c):(1...q)-->A -> (j` c) Fn (1...q))
235		ffn 4562	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((j` c):(1...c)-->A -> (j` c) Fn (1...c))
236	233, 234, 235	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((j` c):(1...q)-->A /\ (j` c):(1...c)-->A) -> (1...q) = (1...c))
237		raleq 2266	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((1...q) = (1...c) -> (A.t e. (1...q)((j` c)` t) = ((j` (c + 1))` t) <-> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t)))
238		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (v = t -> ((j` c)` v) = ((j` c)` t))
239		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (v = t -> ((j` (c + 1))` v) = ((j` (c + 1))` t))
240	238, 239	eqeq12d 1899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (v = t -> (((j` c)` v) = ((j` (c + 1))` v) <-> ((j` c)` t) = ((j` (c + 1))` t)))
241		eqcom 1886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((j` (c + 1))` v) = ((j` c)` v) <-> ((j` c)` v) = ((j` (c + 1))` v))
242	240, 241	syl5bb 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (v = t -> (((j` (c + 1))` v) = ((j` c)` v) <-> ((j` c)` t) = ((j` (c + 1))` t)))
243	242	cbvralv 2280	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v) <-> A.t e. (1...q)((j` c)` t) = ((j` (c + 1))` t))
244	237, 243	syl5bb 591	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((1...q) = (1...c) -> (A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v) <-> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t)))
245	244	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((1...q) = (1...c) -> (A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v) -> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t)))
246	245	a1d 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((1...q) = (1...c) -> (q e. NN -> (A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v) -> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t))))
247	236, 246	syl 12	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((j` c):(1...q)-->A /\ (j` c):(1...c)-->A) -> (q e. NN -> (A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v) -> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t))))
248	247	ex 402	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((j` c):(1...q)-->A -> ((j` c):(1...c)-->A -> (q e. NN -> (A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v) -> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t)))))
249	248	com24 41	. . . . . . . . . . . . . . . . . . . . . 22 |- ((j` c):(1...q)-->A -> (A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v) -> (q e. NN -> ((j` c):(1...c)-->A -> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t)))))
250	249	imp 377	. . . . . . . . . . . . . . . . . . . . 21 |- (((j` c):(1...q)-->A /\ A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v)) -> (q e. NN -> ((j` c):(1...c)-->A -> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t))))
251	250	ad2ant2r 445	. . . . . . . . . . . . . . . . . . . 20 |- ((((j` c):(1...q)-->A /\ (j` (c + 1)):(1...(q + 1))-->A) /\ (A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v) /\ [(q + 1) / n][(j` (c + 1)) / g]ps)) -> (q e. NN -> ((j` c):(1...c)-->A -> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t))))
252	251	com12 14	. . . . . . . . . . . . . . . . . . 19 |- (q e. NN -> ((((j` c):(1...q)-->A /\ (j` (c + 1)):(1...(q + 1))-->A) /\ (A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v) /\ [(q + 1) / n][(j` (c + 1)) / g]ps)) -> ((j` c):(1...c)-->A -> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t))))
253	252	r19.23aiv 2211	. . . . . . . . . . . . . . . . . 18 |- (E.q e. NN (((j` c):(1...q)-->A /\ (j` (c + 1)):(1...(q + 1))-->A) /\ (A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v) /\ [(q + 1) / n][(j` (c + 1)) / g]ps)) -> ((j` c):(1...c)-->A -> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t)))
254	253	adantl 424	. . . . . . . . . . . . . . . . 17 |- (((ph /\ c e. NN) /\ E.q e. NN (((j` c):(1...q)-->A /\ (j` (c + 1)):(1...(q + 1))-->A) /\ (A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v) /\ [(q + 1) / n][(j` (c + 1)) / g]ps))) -> ((j` c):(1...c)-->A -> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t)))
255		fvex 4689	. . . . . . . . . . . . . . . . . 18 |- (j` (c + 1)) e. _V
256		feq1 4551	. . . . . . . . . . . . . . . . . . . . 21 |- (z = (j` (c + 1)) -> (z:(1...(q + 1))-->A <-> (j` (c + 1)):(1...(q + 1))-->A))
257	256	anbi2d 678	. . . . . . . . . . . . . . . . . . . 20 |- (z = (j` (c + 1)) -> (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) <-> ((j` c):(1...q)-->A /\ (j` (c + 1)):(1...(q + 1))-->A)))
258		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z = (j` (c + 1)) -> (z` v) = ((j` (c + 1))` v))
259	258	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = (j` (c + 1)) -> ((z` v) = ((j` c)` v) <-> ((j` (c + 1))` v) = ((j` c)` v)))
260	259	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . 21 |- (z = (j` (c + 1)) -> (A.v e. (1...q)(z` v) = ((j` c)` v) <-> A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v)))
261		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z = (j` (c + 1)) -> ([z / g]ps <-> [(j` (c + 1)) / g]ps))
262	261	sbcbidv 2505	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z = (j` (c + 1)) /\ (q + 1) e. _V) -> ([(q + 1) / n][z / g]ps <-> [(q + 1) / n][(j` (c + 1)) / g]ps))
263	20, 262	mpan2 760	. . . . . . . . . . . . . . . . . . . . 21 |- (z = (j` (c + 1)) -> ([(q + 1) / n][z / g]ps <-> [(q + 1) / n][(j` (c + 1)) / g]ps))
264	260, 263	anbi12d 690	. . . . . . . . . . . . . . . . . . . 20 |- (z = (j` (c + 1)) -> ((A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps) <-> (A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v) /\ [(q + 1) / n][(j` (c + 1)) / g]ps)))
265	257, 264	anbi12d 690	. . . . . . . . . . . . . . . . . . 19 |- (z = (j` (c + 1)) -> ((((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps)) <-> (((j` c):(1...q)-->A /\ (j` (c + 1)):(1...(q + 1))-->A) /\ (A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v) /\ [(q + 1) / n][(j` (c + 1)) / g]ps))))
266	265	rexbidv 2124	. . . . . . . . . . . . . . . . . 18 |- (z = (j` (c + 1)) -> (E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps)) <-> E.q e. NN (((j` c):(1...q)-->A /\ (j` (c + 1)):(1...(q + 1))-->A) /\ (A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v) /\ [(q + 1) / n][(j` (c + 1)) / g]ps))))
267	255, 266	elab 2403	. . . . . . . . . . . . . . . . 17 |- ((j` (c + 1)) e. {z | E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))} <-> E.q e. NN (((j` c):(1...q)-->A /\ (j` (c + 1)):(1...(q + 1))-->A) /\ (A.v e. (1...q)((j` (c + 1))` v) = ((j` c)` v) /\ [(q + 1) / n][(j` (c + 1)) / g]ps)))
268	254, 267	sylan2b 501	. . . . . . . . . . . . . . . 16 |- (((ph /\ c e. NN) /\ (j` (c + 1)) e. {z | E.q e. NN (((j` c):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` c)` v) /\ [(q + 1) / n][z / g]ps))}) -> ((j` c):(1...c)-->A -> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t)))
269	232, 268	syldan 516	. . . . . . . . . . . . . . 15 |- (((ph /\ c e. NN) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> ((j` c):(1...c)-->A -> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t)))
270	269	3adantr2 1036	. . . . . . . . . . . . . 14 |- (((ph /\ c e. NN) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> ((j` c):(1...c)-->A -> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t)))
271	270	an1rs 547	. . . . . . . . . . . . 13 |- (((ph /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ c e. NN) -> ((j` c):(1...c)-->A -> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t)))
272	271	adantllr 433	. . . . . . . . . . . 12 |- ((((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ c e. NN) -> ((j` c):(1...c)-->A -> A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t)))
273	193, 272	jcai 313	. . . . . . . . . . 11 |- ((((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ c e. NN) -> ((j` c):(1...c)-->A /\ A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t)))
274	273	r19.21aiva 2176	. . . . . . . . . 10 |- (((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> A.c e. NN ((j` c):(1...c)-->A /\ A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t)))
275		nnuz 7608	. . . . . . . . . . 11 |- NN = (ZZ>=` 1)
276		eqid 1884	. . . . . . . . . . 11 |- {<.a, b>. | (a e. NN /\ b = ((j` a)` a))} = {<.a, b>. | (a e. NN /\ b = ((j` a)` a))}
277	275, 276	sdclem1 15809	. . . . . . . . . 10 |- ((1 e. ZZ /\ j Fn NN /\ A.c e. NN ((j` c):(1...c)-->A /\ A.t e. (1...c)((j` c)` t) = ((j` (c + 1))` t))) -> ({<.a, b>. | (a e. NN /\ b = ((j` a)` a))}:NN-->A /\ A.c e. NN ({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) = (j` c)))
278	186, 189, 274, 277	syl111anc 1100	. . . . . . . . 9 |- (((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> ({<.a, b>. | (a e. NN /\ b = ((j` a)` a))}:NN-->A /\ A.c e. NN ({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) = (j` c)))
279		visset 2295	. . . . . . . . . . . . . 14 |- c e. _V
280		dfsbcq 2455	. . . . . . . . . . . . . . 15 |- (({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) = (j` c) -> ([({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) / g]ps <-> [(j` c) / g]ps))
281	280	sbcbidv 2505	. . . . . . . . . . . . . 14 |- ((({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) = (j` c) /\ c e. _V) -> ([c / n][({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) / g]ps <-> [c / n][(j` c) / g]ps))
282	279, 281	mpan2 760	. . . . . . . . . . . . 13 |- (({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) = (j` c) -> ([c / n][({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) / g]ps <-> [c / n][(j` c) / g]ps))
283		uzm1 15784	. . . . . . . . . . . . . . . 16 |- (c e. (ZZ>=` 1) -> (c = 1 \/ (c - 1) e. (ZZ>=` 1)))
284		elnnuz 7609	. . . . . . . . . . . . . . . 16 |- (c e. NN <-> c e. (ZZ>=` 1))
285		elnnuz 7609	. . . . . . . . . . . . . . . . 17 |- ((c - 1) e. NN <-> (c - 1) e. (ZZ>=` 1))
286	285	orbi2i 275	. . . . . . . . . . . . . . . 16 |- ((c = 1 \/ (c - 1) e. NN) <-> (c = 1 \/ (c - 1) e. (ZZ>=` 1)))
287	283, 284, 286	3imtr4i 236	. . . . . . . . . . . . . . 15 |- (c e. NN -> (c = 1 \/ (c - 1) e. NN))
288	287	adantl 424	. . . . . . . . . . . . . 14 |- ((((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ c e. NN) -> (c = 1 \/ (c - 1) e. NN))
289		dfsbcq 2455	. . . . . . . . . . . . . . . . . . 19 |- (c = 1 -> ([c / n][(j` c) / g]ps <-> [1 / n][(j` c) / g]ps))
290		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . 22 |- (c = 1 -> (j` c) = (j` 1))
291		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . 22 |- ((j` c) = (j` 1) -> ([(j` c) / g]ps <-> [(j` 1) / g]ps))
292	290, 291	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (c = 1 -> ([(j` c) / g]ps <-> [(j` 1) / g]ps))
293	292	sbcbidv 2505	. . . . . . . . . . . . . . . . . . . 20 |- ((c = 1 /\ 1 e. NN) -> ([1 / n][(j` c) / g]ps <-> [1 / n][(j` 1) / g]ps))
294	165, 293	mpan2 760	. . . . . . . . . . . . . . . . . . 19 |- (c = 1 -> ([1 / n][(j` c) / g]ps <-> [1 / n][(j` 1) / g]ps))
295	289, 294	bitrd 587	. . . . . . . . . . . . . . . . . 18 |- (c = 1 -> ([c / n][(j` c) / g]ps <-> [1 / n][(j` 1) / g]ps))
296		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((j` 1) = h -> ([(j` 1) / g]ps <-> [h / g]ps))
297	176, 178	sbcie 2485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ([h / g]ps <-> ch)
298	296, 297	syl6bb 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((j` 1) = h -> ([(j` 1) / g]ps <-> ch))
299	298	sbcbidv 2505	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((j` 1) = h /\ 1 e. NN) -> ([1 / n][(j` 1) / g]ps <-> [1 / n]ch))
300	165, 299	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((j` 1) = h -> ([1 / n][(j` 1) / g]ps <-> [1 / n]ch))
301	165	elisseti 2301	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 1 e. _V
302	301, 172	sbcie 2485	. . . . . . . . . . . . . . . . . . . . . . 23 |- ([1 / n]ch <-> th)
303	300, 302	syl6bb 595	. . . . . . . . . . . . . . . . . . . . . 22 |- ((j` 1) = h -> ([1 / n][(j` 1) / g]ps <-> th))
304	303	biimprcd 173	. . . . . . . . . . . . . . . . . . . . 21 |- (th -> ((j` 1) = h -> [1 / n][(j` 1) / g]ps))
305	304	ad2antll 443	. . . . . . . . . . . . . . . . . . . 20 |- ((ph /\ (h:{1}-->A /\ th)) -> ((j` 1) = h -> [1 / n][(j` 1) / g]ps))
306	305	imp 377	. . . . . . . . . . . . . . . . . . 19 |- (((ph /\ (h:{1}-->A /\ th)) /\ (j` 1) = h) -> [1 / n][(j` 1) / g]ps)
307	306	3ad2antr2 1042	. . . . . . . . . . . . . . . . . 18 |- (((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> [1 / n][(j` 1) / g]ps)
308	295, 307	syl5cbir 228	. . . . . . . . . . . . . . . . 17 |- (((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> (c = 1 -> [c / n][(j` c) / g]ps))
309	308	imp 377	. . . . . . . . . . . . . . . 16 |- ((((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ c = 1) -> [c / n][(j` c) / g]ps)
310	309	adantlr 429	. . . . . . . . . . . . . . 15 |- (((((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ c e. NN) /\ c = 1) -> [c / n][(j` c) / g]ps)
311		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . 20 |- (c = ((c - 1) + 1) -> ([c / n][(j` c) / g]ps <-> [((c - 1) + 1) / n][(j` c) / g]ps))
312		oprex 4907	. . . . . . . . . . . . . . . . . . . . 21 |- ((c - 1) + 1) e. _V
313		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . 23 |- (c = ((c - 1) + 1) -> (j` c) = (j` ((c - 1) + 1)))
314		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((j` c) = (j` ((c - 1) + 1)) -> ([(j` c) / g]ps <-> [(j` ((c - 1) + 1)) / g]ps))
315	313, 314	syl 12	. . . . . . . . . . . . . . . . . . . . . 22 |- (c = ((c - 1) + 1) -> ([(j` c) / g]ps <-> [(j` ((c - 1) + 1)) / g]ps))
316	315	sbcbidv 2505	. . . . . . . . . . . . . . . . . . . . 21 |- ((c = ((c - 1) + 1) /\ ((c - 1) + 1) e. _V) -> ([((c - 1) + 1) / n][(j` c) / g]ps <-> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
317	312, 316	mpan2 760	. . . . . . . . . . . . . . . . . . . 20 |- (c = ((c - 1) + 1) -> ([((c - 1) + 1) / n][(j` c) / g]ps <-> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
318	311, 317	bitrd 587	. . . . . . . . . . . . . . . . . . 19 |- (c = ((c - 1) + 1) -> ([c / n][(j` c) / g]ps <-> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
319	9	sdclem2 15810	. . . . . . . . . . . . . . . . . . . . 21 |- ((((ph /\ h:{1}-->A) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ (c - 1) e. NN) -> (j` (c - 1)):(1...(c - 1))-->A)
320		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (c - 1) e. NN) -> (j` (c - 1)) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)})
321	320	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((c - 1) e. NN -> (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} -> (j` (c - 1)) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)}))
322		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w = (c - 1) -> (w + 1) = ((c - 1) + 1))
323	322	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = (c - 1) -> (j` (w + 1)) = (j` ((c - 1) + 1)))
324		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w = (c - 1) -> (j` w) = (j` (c - 1)))
325	324	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = (c - 1) -> ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)) = ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` (c - 1))))
326	323, 325	eleq12d 1965	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = (c - 1) -> ((j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)) <-> (j` ((c - 1) + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` (c - 1)))))
327	326	rcla4v 2376	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((c - 1) e. NN -> (A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)) -> (j` ((c - 1) + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` (c - 1)))))
328	321, 327	anim12d 617	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((c - 1) e. NN -> ((j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w))) -> ((j` (c - 1)) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` ((c - 1) + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` (c - 1))))))
329	328	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((c - 1) e. NN /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> ((j` (c - 1)) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` ((c - 1) + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` (c - 1)))))
330	329	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((ph /\ h:{1}-->A) /\ (c - 1) e. NN) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> ((j` (c - 1)) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` ((c - 1) + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` (c - 1)))))
331		feq1 4551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x = (j` (c - 1)) -> (x:(1...q)-->A <-> (j` (c - 1)):(1...q)-->A))
332	331	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x = (j` (c - 1)) -> ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) <-> ((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A)))
333		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (x = (j` (c - 1)) -> (x` v) = ((j` (c - 1))` v))
334	333	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (x = (j` (c - 1)) -> ((z` v) = (x` v) <-> (z` v) = ((j` (c - 1))` v)))
335	334	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x = (j` (c - 1)) -> (A.v e. (1...q)(z` v) = (x` v) <-> A.v e. (1...q)(z` v) = ((j` (c - 1))` v)))
336	335	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x = (j` (c - 1)) -> ((A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps) <-> (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps)))
337	332, 336	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x = (j` (c - 1)) -> (((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps)) <-> (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))))
338	337	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (x = (j` (c - 1)) -> (E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps)) <-> E.q e. NN (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))))
339	338	abbidv 2008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (x = (j` (c - 1)) -> {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))} = {z | E.q e. NN (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))})
340	339, 162	fvopab4g 4742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((j` (c - 1)) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ {z | E.q e. NN (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))} e. _V) -> ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` (c - 1))) = {z | E.q e. NN (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))})
341		abrexex2g 15738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((NN e. _V /\ A.q e. NN {z | (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))} e. _V) -> {z | E.q e. NN (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))} e. _V)
342		ssexg 3457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (({z | (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))} C_ {z | z:(1...(q + 1))-->A} /\ {z | z:(1...(q + 1))-->A} e. _V) -> {z | (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))} e. _V)
343		simplr 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps)) -> z:(1...(q + 1))-->A)
344	343	ss2abi 2679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- {z | (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))} C_ {z | z:(1...(q + 1))-->A}
345	342, 344, 218	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (ph -> {z | (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))} e. _V)
346	345	a1d 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (ph -> (q e. NN -> {z | (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))} e. _V))
347	346	r19.21aiv 2175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (ph -> A.q e. NN {z | (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))} e. _V)
348	341, 3, 347	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (ph -> {z | E.q e. NN (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))} e. _V)
349	340, 348	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((j` (c - 1)) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ ph) -> ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` (c - 1))) = {z | E.q e. NN (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))})
350	349	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((ph /\ (j` (c - 1)) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)}) -> ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` (c - 1))) = {z | E.q e. NN (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))})
351	350	eleq2d 1964	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((ph /\ (j` (c - 1)) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)}) -> ((j` ((c - 1) + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` (c - 1))) <-> (j` ((c - 1) + 1)) e. {z | E.q e. NN (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))}))
352		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (j` ((c - 1) + 1)) e. _V
353		feq1 4551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (z = (j` ((c - 1) + 1)) -> (z:(1...(q + 1))-->A <-> (j` ((c - 1) + 1)):(1...(q + 1))-->A))
354	353	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (z = (j` ((c - 1) + 1)) -> (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) <-> ((j` (c - 1)):(1...q)-->A /\ (j` ((c - 1) + 1)):(1...(q + 1))-->A)))
355		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (z = (j` ((c - 1) + 1)) -> (z` v) = ((j` ((c - 1) + 1))` v))
356	355	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (z = (j` ((c - 1) + 1)) -> ((z` v) = ((j` (c - 1))` v) <-> ((j` ((c - 1) + 1))` v) = ((j` (c - 1))` v)))
357	356	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (z = (j` ((c - 1) + 1)) -> (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) <-> A.v e. (1...q)((j` ((c - 1) + 1))` v) = ((j` (c - 1))` v)))
358		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (z = (j` ((c - 1) + 1)) -> ([z / g]ps <-> [(j` ((c - 1) + 1)) / g]ps))
359	358	sbcbidv 2505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((z = (j` ((c - 1) + 1)) /\ (q + 1) e. _V) -> ([(q + 1) / n][z / g]ps <-> [(q + 1) / n][(j` ((c - 1) + 1)) / g]ps))
360	20, 359	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (z = (j` ((c - 1) + 1)) -> ([(q + 1) / n][z / g]ps <-> [(q + 1) / n][(j` ((c - 1) + 1)) / g]ps))
361	357, 360	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (z = (j` ((c - 1) + 1)) -> ((A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps) <-> (A.v e. (1...q)((j` ((c - 1) + 1))` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][(j` ((c - 1) + 1)) / g]ps)))
362	354, 361	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (z = (j` ((c - 1) + 1)) -> ((((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps)) <-> (((j` (c - 1)):(1...q)-->A /\ (j` ((c - 1) + 1)):(1...(q + 1))-->A) /\ (A.v e. (1...q)((j` ((c - 1) + 1))` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][(j` ((c - 1) + 1)) / g]ps))))
363	362	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (z = (j` ((c - 1) + 1)) -> (E.q e. NN (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps)) <-> E.q e. NN (((j` (c - 1)):(1...q)-->A /\ (j` ((c - 1) + 1)):(1...(q + 1))-->A) /\ (A.v e. (1...q)((j` ((c - 1) + 1))` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][(j` ((c - 1) + 1)) / g]ps))))
364	352, 363	elab 2403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((j` ((c - 1) + 1)) e. {z | E.q e. NN (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))} <-> E.q e. NN (((j` (c - 1)):(1...q)-->A /\ (j` ((c - 1) + 1)):(1...(q + 1))-->A) /\ (A.v e. (1...q)((j` ((c - 1) + 1))` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][(j` ((c - 1) + 1)) / g]ps)))
365		fndmu 4514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((j` (c - 1)) Fn (1...q) /\ (j` (c - 1)) Fn (1...(c - 1))) -> (1...q) = (1...(c - 1)))
366		ffn 4562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((j` (c - 1)):(1...q)-->A -> (j` (c - 1)) Fn (1...q))
367		ffn 4562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((j` (c - 1)):(1...(c - 1))-->A -> (j` (c - 1)) Fn (1...(c - 1)))
368	365, 366, 367	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((j` (c - 1)):(1...q)-->A /\ (j` (c - 1)):(1...(c - 1))-->A) -> (1...q) = (1...(c - 1)))
369		elnnuz 7609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (q e. NN <-> q e. (ZZ>=` 1))
370		oprex 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (c - 1) e. _V
371		fzopth 7674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((q e. (ZZ>=` 1) /\ (c - 1) e. _V) -> ((1...q) = (1...(c - 1)) <-> (1 = 1 /\ q = (c - 1))))
372	370, 371	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (q e. (ZZ>=` 1) -> ((1...q) = (1...(c - 1)) <-> (1 = 1 /\ q = (c - 1))))
373	369, 372	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (q e. NN -> ((1...q) = (1...(c - 1)) <-> (1 = 1 /\ q = (c - 1))))
374		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (q = (c - 1) -> (q + 1) = ((c - 1) + 1))
375		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((q + 1) = ((c - 1) + 1) -> ([(q + 1) / n][(j` ((c - 1) + 1)) / g]ps <-> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
376	374, 375	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (q = (c - 1) -> ([(q + 1) / n][(j` ((c - 1) + 1)) / g]ps <-> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
377	376	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (q = (c - 1) -> ([(q + 1) / n][(j` ((c - 1) + 1)) / g]ps -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
378	377	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((1 = 1 /\ q = (c - 1)) -> ([(q + 1) / n][(j` ((c - 1) + 1)) / g]ps -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
379	373, 378	syl6bi 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (q e. NN -> ((1...q) = (1...(c - 1)) -> ([(q + 1) / n][(j` ((c - 1) + 1)) / g]ps -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps)))
380	379	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((1...q) = (1...(c - 1)) -> (q e. NN -> ([(q + 1) / n][(j` ((c - 1) + 1)) / g]ps -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps)))
381	380	imp3a 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((1...q) = (1...(c - 1)) -> ((q e. NN /\ [(q + 1) / n][(j` ((c - 1) + 1)) / g]ps) -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
382	368, 381	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((j` (c - 1)):(1...q)-->A /\ (j` (c - 1)):(1...(c - 1))-->A) -> ((q e. NN /\ [(q + 1) / n][(j` ((c - 1) + 1)) / g]ps) -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
383	382	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((j` (c - 1)):(1...q)-->A -> ((j` (c - 1)):(1...(c - 1))-->A -> ((q e. NN /\ [(q + 1) / n][(j` ((c - 1) + 1)) / g]ps) -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps)))
384	383	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((j` (c - 1)):(1...q)-->A -> ((q e. NN /\ [(q + 1) / n][(j` ((c - 1) + 1)) / g]ps) -> ((j` (c - 1)):(1...(c - 1))-->A -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps)))
385	384	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((j` (c - 1)):(1...q)-->A /\ (q e. NN /\ [(q + 1) / n][(j` ((c - 1) + 1)) / g]ps)) -> ((j` (c - 1)):(1...(c - 1))-->A -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
386	385	an1s 544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((q e. NN /\ ((j` (c - 1)):(1...q)-->A /\ [(q + 1) / n][(j` ((c - 1) + 1)) / g]ps)) -> ((j` (c - 1)):(1...(c - 1))-->A -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
387	386	adantrrl 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((q e. NN /\ ((j` (c - 1)):(1...q)-->A /\ (A.v e. (1...q)((j` ((c - 1) + 1))` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][(j` ((c - 1) + 1)) / g]ps))) -> ((j` (c - 1)):(1...(c - 1))-->A -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
388	387	adantrlr 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((q e. NN /\ (((j` (c - 1)):(1...q)-->A /\ (j` ((c - 1) + 1)):(1...(q + 1))-->A) /\ (A.v e. (1...q)((j` ((c - 1) + 1))` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][(j` ((c - 1) + 1)) / g]ps))) -> ((j` (c - 1)):(1...(c - 1))-->A -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
389	388	r19.23aiva 2212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (E.q e. NN (((j` (c - 1)):(1...q)-->A /\ (j` ((c - 1) + 1)):(1...(q + 1))-->A) /\ (A.v e. (1...q)((j` ((c - 1) + 1))` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][(j` ((c - 1) + 1)) / g]ps)) -> ((j` (c - 1)):(1...(c - 1))-->A -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
390	364, 389	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((j` ((c - 1) + 1)) e. {z | E.q e. NN (((j` (c - 1)):(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = ((j` (c - 1))` v) /\ [(q + 1) / n][z / g]ps))} -> ((j` (c - 1)):(1...(c - 1))-->A -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
391	351, 390	syl6bi 231	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((ph /\ (j` (c - 1)) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)}) -> ((j` ((c - 1) + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` (c - 1))) -> ((j` (c - 1)):(1...(c - 1))-->A -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps)))
392	391	impr 422	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((ph /\ ((j` (c - 1)) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` ((c - 1) + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` (c - 1))))) -> ((j` (c - 1)):(1...(c - 1))-->A -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
393	392	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((ph /\ h:{1}-->A) /\ ((j` (c - 1)) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` ((c - 1) + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` (c - 1))))) -> ((j` (c - 1)):(1...(c - 1))-->A -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
394	393	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((ph /\ h:{1}-->A) /\ (c - 1) e. NN) /\ ((j` (c - 1)) e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` ((c - 1) + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` (c - 1))))) -> ((j` (c - 1)):(1...(c - 1))-->A -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
395	330, 394	syldan 516	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((ph /\ h:{1}-->A) /\ (c - 1) e. NN) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> ((j` (c - 1)):(1...(c - 1))-->A -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
396	395	3adantr2 1036	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((ph /\ h:{1}-->A) /\ (c - 1) e. NN) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> ((j` (c - 1)):(1...(c - 1))-->A -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
397	396	an1rs 547	. . . . . . . . . . . . . . . . . . . . 21 |- ((((ph /\ h:{1}-->A) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ (c - 1) e. NN) -> ((j` (c - 1)):(1...(c - 1))-->A -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps))
398	319, 397	mpd 29	. . . . . . . . . . . . . . . . . . . 20 |- ((((ph /\ h:{1}-->A) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ (c - 1) e. NN) -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps)
399	398, 192	sylanl1 509	. . . . . . . . . . . . . . . . . . 19 |- ((((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ (c - 1) e. NN) -> [((c - 1) + 1) / n][(j` ((c - 1) + 1)) / g]ps)
400	318, 399	syl5cbir 228	. . . . . . . . . . . . . . . . . 18 |- ((((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ (c - 1) e. NN) -> (c = ((c - 1) + 1) -> [c / n][(j` c) / g]ps))
401	400	imp 377	. . . . . . . . . . . . . . . . 17 |- (((((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ (c - 1) e. NN) /\ c = ((c - 1) + 1)) -> [c / n][(j` c) / g]ps)
402		npcan 6559	. . . . . . . . . . . . . . . . . . 19 |- ((c e. CC /\ 1 e. CC) -> ((c - 1) + 1) = c)
403	402	eqcomd 1889	. . . . . . . . . . . . . . . . . 18 |- ((c e. CC /\ 1 e. CC) -> c = ((c - 1) + 1))
404		nncn 7113	. . . . . . . . . . . . . . . . . 18 |- (c e. NN -> c e. CC)
405		ax1cn 6422	. . . . . . . . . . . . . . . . . 18 |- 1 e. CC
406	403, 404, 405	sylancl 525	. . . . . . . . . . . . . . . . 17 |- (c e. NN -> c = ((c - 1) + 1))
407	401, 406	sylan2 500	. . . . . . . . . . . . . . . 16 |- (((((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ (c - 1) e. NN) /\ c e. NN) -> [c / n][(j` c) / g]ps)
408	407	an1rs 547	. . . . . . . . . . . . . . 15 |- (((((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ c e. NN) /\ (c - 1) e. NN) -> [c / n][(j` c) / g]ps)
409	310, 408	jaodan 471	. . . . . . . . . . . . . 14 |- (((((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ c e. NN) /\ (c = 1 \/ (c - 1) e. NN)) -> [c / n][(j` c) / g]ps)
410	288, 409	mpdan 768	. . . . . . . . . . . . 13 |- ((((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ c e. NN) -> [c / n][(j` c) / g]ps)
411	282, 410	syl5cbir 228	. . . . . . . . . . . 12 |- ((((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) /\ c e. NN) -> (({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) = (j` c) -> [c / n][({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) / g]ps))
412	411	ralimdvaa 2171	. . . . . . . . . . 11 |- (((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> (A.c e. NN ({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) = (j` c) -> A.c e. NN [c / n][({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) / g]ps))
413		ax-17 1317	. . . . . . . . . . . 12 |- ([({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) / g]ps -> A.c[({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) / g]ps)
414	279	hbsbc1v 2464	. . . . . . . . . . . 12 |- ([c / n][({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) / g]ps -> A.n[c / n][({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) / g]ps)
415		opreq2 4890	. . . . . . . . . . . . . 14 |- (n = c -> (1...n) = (1...c))
416		reseq2 4219	. . . . . . . . . . . . . 14 |- ((1...n) = (1...c) -> ({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) = ({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)))
417		dfsbcq 2455	. . . . . . . . . . . . . 14 |- (({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) = ({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) -> ([({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) / g]ps <-> [({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) / g]ps))
418	415, 416, 417	3syl 24	. . . . . . . . . . . . 13 |- (n = c -> ([({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) / g]ps <-> [({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) / g]ps))
419		sbceq1a 2456	. . . . . . . . . . . . 13 |- (n = c -> ([({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) / g]ps <-> [c / n][({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) / g]ps))
420	418, 419	bitrd 587	. . . . . . . . . . . 12 |- (n = c -> ([({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) / g]ps <-> [c / n][({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) / g]ps))
421	413, 414, 420	cbvral 2278	. . . . . . . . . . 11 |- (A.n e. NN [({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) / g]ps <-> A.c e. NN [c / n][({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) / g]ps)
422	412, 421	syl6ibr 230	. . . . . . . . . 10 |- (((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> (A.c e. NN ({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) = (j` c) -> A.n e. NN [({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) / g]ps))
423	422	anim2d 620	. . . . . . . . 9 |- (((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> (({<.a, b>. | (a e. NN /\ b = ((j` a)` a))}:NN-->A /\ A.c e. NN ({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...c)) = (j` c)) -> ({<.a, b>. | (a e. NN /\ b = ((j` a)` a))}:NN-->A /\ A.n e. NN [({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) / g]ps)))
424	278, 423	mpd 29	. . . . . . . 8 |- (((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> ({<.a, b>. | (a e. NN /\ b = ((j` a)` a))}:NN-->A /\ A.n e. NN [({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) / g]ps))
425	3	opabex2 4539	. . . . . . . . 9 |- {<.a, b>. | (a e. NN /\ b = ((j` a)` a))} e. _V
426		feq1 4551	. . . . . . . . . 10 |- (f = {<.a, b>. | (a e. NN /\ b = ((j` a)` a))} -> (f:NN-->A <-> {<.a, b>. | (a e. NN /\ b = ((j` a)` a))}:NN-->A))
427		reseq1 4218	. . . . . . . . . . . . 13 |- (f = {<.a, b>. | (a e. NN /\ b = ((j` a)` a))} -> (f |` (1...n)) = ({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)))
428		dfsbcq 2455	. . . . . . . . . . . . 13 |- ((f |` (1...n)) = ({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) -> ([(f |` (1...n)) / g]ps <-> [({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) / g]ps))
429	427, 428	syl 12	. . . . . . . . . . . 12 |- (f = {<.a, b>. | (a e. NN /\ b = ((j` a)` a))} -> ([(f |` (1...n)) / g]ps <-> [({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) / g]ps))
430		visset 2295	. . . . . . . . . . . . . 14 |- f e. _V
431		resexg 4250	. . . . . . . . . . . . . 14 |- (f e. _V -> (f |` (1...n)) e. _V)
432	430, 431	ax-mp 7	. . . . . . . . . . . . 13 |- (f |` (1...n)) e. _V
433		sdc.4	. . . . . . . . . . . . 13 |- (g = (f |` (1...n)) -> (ps <-> rh))
434	432, 433	sbcie 2485	. . . . . . . . . . . 12 |- ([(f |` (1...n)) / g]ps <-> rh)
435	429, 434	syl5bbr 593	. . . . . . . . . . 11 |- (f = {<.a, b>. | (a e. NN /\ b = ((j` a)` a))} -> (rh <-> [({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) / g]ps))
436	435	ralbidv 2123	. . . . . . . . . 10 |- (f = {<.a, b>. | (a e. NN /\ b = ((j` a)` a))} -> (A.n e. NN rh <-> A.n e. NN [({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) / g]ps))
437	426, 436	anbi12d 690	. . . . . . . . 9 |- (f = {<.a, b>. | (a e. NN /\ b = ((j` a)` a))} -> ((f:NN-->A /\ A.n e. NN rh) <-> ({<.a, b>. | (a e. NN /\ b = ((j` a)` a))}:NN-->A /\ A.n e. NN [({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) / g]ps)))
438	425, 437	cla4ev 2371	. . . . . . . 8 |- (({<.a, b>. | (a e. NN /\ b = ((j` a)` a))}:NN-->A /\ A.n e. NN [({<.a, b>. | (a e. NN /\ b = ((j` a)` a))} |` (1...n)) / g]ps) -> E.f(f:NN-->A /\ A.n e. NN rh))
439	424, 438	syl 12	. . . . . . 7 |- (((ph /\ (h:{1}-->A /\ th)) /\ (j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w)))) -> E.f(f:NN-->A /\ A.n e. NN rh))
440	439	ex 402	. . . . . 6 |- ((ph /\ (h:{1}-->A /\ th)) -> ((j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w))) -> E.f(f:NN-->A /\ A.n e. NN rh)))
441	440	19.23adv 1584	. . . . 5 |- ((ph /\ (h:{1}-->A /\ th)) -> (E.j(j:NN-->{g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ (j` 1) = h /\ A.w e. NN (j` (w + 1)) e. ({<.x, y>. | (x e. {g | E.n e. NN (g:(1...n)-->A /\ ps)} /\ y = {z | E.q e. NN ((x:(1...q)-->A /\ z:(1...(q + 1))-->A) /\ (A.v e. (1...q)(z` v) = (x` v) /\ [(q + 1) / n][z / g]ps))})}` (j` w))) -> E.f(f:NN-->A /\ A.n e. NN rh)))
442	185, 441	mpd 29	. . . 4 |- ((ph /\ (h:{1}-->A /\ th)) -> E.f(f:NN-->A /\ A.n e. NN rh))
443	442	ex 402	. . 3 |- (ph -> ((h:{1}-->A /\ th) -> E.f(f:NN-->A /\ A.n e. NN rh)))
444	443	19.23adv 1584	. 2 |- (ph -> (E.h(h:{1}-->A /\ th) -> E.f(f:NN-->A /\ A.n e. NN rh)))
445	1, 444	mpd 29	1 |- (ph -> E.f(f:NN-->A /\ A.n e. NN rh))

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  [wsbc 1534  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   \ cdif 2590   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  {csn 3044  {copab 3395   |` cres 3988   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884  CCcc 6384  1c1 6387   + caddc 6389   - cmin 6445  NNcn 6449  ZZcz 6451  ZZ>=cuz 7586  ...cfz 7637

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  ax-ac 5906

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-iso 4015  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-n0 7309  df-z 7345  df-uz 7587  df-fz 7638  df-seq1 7721

Copyright terms: Public domain