Theorem fdc 15812

Description: Finite version of dependent choice. Construct a function whose value depends on the previous function value, except at a final point at which no new value can be chosen. The final hypothesis ensures that the process will terminate. The proof does not use the Axiom of Choice.

Hypotheses

Ref	Expression
fdc.1	|- A e. _V
fdc.2	|- M e. ZZ
fdc.3	|- Z = (ZZ>=` M)
fdc.4	|- N = (M + 1)
fdc.5	|- (a = (f` (k - 1)) -> (ph <-> ps))
fdc.6	|- (b = (f` k) -> (ps <-> ch))
fdc.7	|- (a = (f` n) -> (th <-> ta))
fdc.8	|- (et -> C e. A)
fdc.9	|- (et -> R Fr A)
fdc.10	|- ((et /\ a e. A) -> (th \/ E.b e. A ph))
fdc.11	|- (((et /\ ph) /\ (a e. A /\ b e. A)) -> bRa)

Assertion

Ref	Expression
fdc	|- (et -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = C /\ ta) /\ A.k e. (N...n)ch))

Distinct variable groups:   C,f,n   A,a,b,f,n   M,a,b,f,k,n   Z,a,b,n   N,a,b,f,k,n   R,a,b   ph,f,k   ps,a   ch,a,b,n   th,f,n   ta,a,b   et,a,b

Proof of Theorem fdc

Step	Hyp	Ref	Expression
1		fdc.8	. 2 |- (et -> C e. A)
2		fdc.10	. . . . . . . . . . . . . 14 |- ((et /\ a e. A) -> (th \/ E.b e. A ph))
3		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . 23 |- (n = M -> (M...n) = (M...M))
4	3	feq2d 4557	. . . . . . . . . . . . . . . . . . . . . 22 |- (n = M -> (f:(M...n)-->A <-> f:(M...M)-->A))
5		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (n = M -> (f` n) = (f` M))
6		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f` n) = (f` M) -> ([(f` n) / a]th <-> [(f` M) / a]th))
7	5, 6	syl 12	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (n = M -> ([(f` n) / a]th <-> [(f` M) / a]th))
8		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f` n) e. _V
9		fdc.7	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (a = (f` n) -> (th <-> ta))
10	8, 9	sbcie 2485	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ([(f` n) / a]th <-> ta)
11	7, 10	syl5bbr 593	. . . . . . . . . . . . . . . . . . . . . . 23 |- (n = M -> (ta <-> [(f` M) / a]th))
12	11	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . 22 |- (n = M -> (((f` M) = a /\ ta) <-> ((f` M) = a /\ [(f` M) / a]th)))
13		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (n = M -> (N...n) = (N...M))
14		fdc.4	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- N = (M + 1)
15	14	opreq1i 4892	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (N...M) = ((M + 1)...M)
16		fdc.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- M e. ZZ
17	16	zrei 7350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- M e. RR
18	17	ltp1i 6991	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- M < (M + 1)
19		peano2z 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (M e. ZZ -> (M + 1) e. ZZ)
20	16, 19	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (M + 1) e. ZZ
21		fzn 7663	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((M + 1) e. ZZ /\ M e. ZZ) -> (M < (M + 1) <-> ((M + 1)...M) = (/)))
22	20, 16, 21	mp2an 761	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (M < (M + 1) <-> ((M + 1)...M) = (/))
23	18, 22	mpbi 206	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((M + 1)...M) = (/)
24	15, 23	eqtri 1908	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (N...M) = (/)
25	13, 24	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . 23 |- (n = M -> (N...n) = (/))
26	25	raleqdv 2269	. . . . . . . . . . . . . . . . . . . . . 22 |- (n = M -> (A.k e. (N...n)ch <-> A.k e. (/) ch))
27	4, 12, 26	3anbi123d 1168	. . . . . . . . . . . . . . . . . . . . 21 |- (n = M -> ((f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch) <-> (f:(M...M)-->A /\ ((f` M) = a /\ [(f` M) / a]th) /\ A.k e. (/) ch)))
28		df-3an 860	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f:(M...M)-->A /\ ((f` M) = a /\ [(f` M) / a]th) /\ A.k e. (/) ch) <-> ((f:(M...M)-->A /\ ((f` M) = a /\ [(f` M) / a]th)) /\ A.k e. (/) ch))
29		ral0 2974	. . . . . . . . . . . . . . . . . . . . . 22 |- A.k e. (/) ch
30	28, 29	mpbiran2 799	. . . . . . . . . . . . . . . . . . . . 21 |- ((f:(M...M)-->A /\ ((f` M) = a /\ [(f` M) / a]th) /\ A.k e. (/) ch) <-> (f:(M...M)-->A /\ ((f` M) = a /\ [(f` M) / a]th)))
31	27, 30	syl6bb 595	. . . . . . . . . . . . . . . . . . . 20 |- (n = M -> ((f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch) <-> (f:(M...M)-->A /\ ((f` M) = a /\ [(f` M) / a]th))))
32	31	exbidv 1657	. . . . . . . . . . . . . . . . . . 19 |- (n = M -> (E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch) <-> E.f(f:(M...M)-->A /\ ((f` M) = a /\ [(f` M) / a]th))))
33	32	rcla4ev 2381	. . . . . . . . . . . . . . . . . 18 |- ((M e. Z /\ E.f(f:(M...M)-->A /\ ((f` M) = a /\ [(f` M) / a]th))) -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch))
34		uzid 7596	. . . . . . . . . . . . . . . . . . . 20 |- (M e. ZZ -> M e. (ZZ>=` M))
35	16, 34	ax-mp 7	. . . . . . . . . . . . . . . . . . 19 |- M e. (ZZ>=` M)
36		fdc.3	. . . . . . . . . . . . . . . . . . 19 |- Z = (ZZ>=` M)
37	35, 36	eleqtrri 1970	. . . . . . . . . . . . . . . . . 18 |- M e. Z
38		fss 4571	. . . . . . . . . . . . . . . . . . . . . 22 |- (({<.M, a>.}:{M}-->{a} /\ {a} C_ A) -> {<.M, a>.}:{M}-->A)
39		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . 23 |- {<.M, a>.} = {<.M, a>.}
40	16	elisseti 2301	. . . . . . . . . . . . . . . . . . . . . . . 24 |- M e. _V
41		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . 24 |- a e. _V
42	40, 41	fsn 4807	. . . . . . . . . . . . . . . . . . . . . . 23 |- ({<.M, a>.}:{M}-->{a} <-> {<.M, a>.} = {<.M, a>.})
43	39, 42	mpbir 207	. . . . . . . . . . . . . . . . . . . . . 22 |- {<.M, a>.}:{M}-->{a}
44		snssi 3129	. . . . . . . . . . . . . . . . . . . . . 22 |- (a e. A -> {a} C_ A)
45	38, 43, 44	sylancr 526	. . . . . . . . . . . . . . . . . . . . 21 |- (a e. A -> {<.M, a>.}:{M}-->A)
46		fzsn 7684	. . . . . . . . . . . . . . . . . . . . . . 23 |- (M e. ZZ -> (M...M) = {M})
47	16, 46	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . 22 |- (M...M) = {M}
48	47	feq2i 4559	. . . . . . . . . . . . . . . . . . . . 21 |- ({<.M, a>.}:(M...M)-->A <-> {<.M, a>.}:{M}-->A)
49	45, 48	sylibr 217	. . . . . . . . . . . . . . . . . . . 20 |- (a e. A -> {<.M, a>.}:(M...M)-->A)
50	49	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- ((a e. A /\ th) -> {<.M, a>.}:(M...M)-->A)
51	40, 41	fvsn 4758	. . . . . . . . . . . . . . . . . . . 20 |- ({<.M, a>.}` M) = a
52	51	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- ((a e. A /\ th) -> ({<.M, a>.}` M) = a)
53		simpr 350	. . . . . . . . . . . . . . . . . . 19 |- ((a e. A /\ th) -> th)
54		snex 3492	. . . . . . . . . . . . . . . . . . . 20 |- {<.M, a>.} e. _V
55		feq1 4551	. . . . . . . . . . . . . . . . . . . . 21 |- (f = {<.M, a>.} -> (f:(M...M)-->A <-> {<.M, a>.}:(M...M)-->A))
56		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f = {<.M, a>.} -> (f` M) = ({<.M, a>.}` M))
57	56	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . . . 22 |- (f = {<.M, a>.} -> ((f` M) = a <-> ({<.M, a>.}` M) = a))
58	56, 51	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f = {<.M, a>.} -> (f` M) = a)
59		sbceq1a 2456	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (a = (f` M) -> (th <-> [(f` M) / a]th))
60	59	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((f` M) = a -> (th <-> [(f` M) / a]th))
61	60	bicomd 580	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f` M) = a -> ([(f` M) / a]th <-> th))
62	58, 61	syl 12	. . . . . . . . . . . . . . . . . . . . . 22 |- (f = {<.M, a>.} -> ([(f` M) / a]th <-> th))
63	57, 62	anbi12d 690	. . . . . . . . . . . . . . . . . . . . 21 |- (f = {<.M, a>.} -> (((f` M) = a /\ [(f` M) / a]th) <-> (({<.M, a>.}` M) = a /\ th)))
64	55, 63	anbi12d 690	. . . . . . . . . . . . . . . . . . . 20 |- (f = {<.M, a>.} -> ((f:(M...M)-->A /\ ((f` M) = a /\ [(f` M) / a]th)) <-> ({<.M, a>.}:(M...M)-->A /\ (({<.M, a>.}` M) = a /\ th))))
65	54, 64	cla4ev 2371	. . . . . . . . . . . . . . . . . . 19 |- (({<.M, a>.}:(M...M)-->A /\ (({<.M, a>.}` M) = a /\ th)) -> E.f(f:(M...M)-->A /\ ((f` M) = a /\ [(f` M) / a]th)))
66	50, 52, 53, 65	syl12anc 1098	. . . . . . . . . . . . . . . . . 18 |- ((a e. A /\ th) -> E.f(f:(M...M)-->A /\ ((f` M) = a /\ [(f` M) / a]th)))
67	33, 37, 66	sylancr 526	. . . . . . . . . . . . . . . . 17 |- ((a e. A /\ th) -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch))
68	67	adantll 428	. . . . . . . . . . . . . . . 16 |- (((et /\ a e. A) /\ th) -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch))
69	68	a1d 15	. . . . . . . . . . . . . . 15 |- (((et /\ a e. A) /\ th) -> (A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch)))
70		fdc.11	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((et /\ ph) /\ (a e. A /\ b e. A)) -> bRa)
71		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (d = b -> (dRa <-> bRa))
72	71	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((b e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) /\ bRa) -> E.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})dRa)
73	72	expcom 403	. . . . . . . . . . . . . . . . . . . . . . 23 |- (bRa -> (b e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -> E.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})dRa))
74	70, 73	syl 12	. . . . . . . . . . . . . . . . . . . . . 22 |- (((et /\ ph) /\ (a e. A /\ b e. A)) -> (b e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -> E.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})dRa))
75		dfrex2 2116	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})dRa <-> -. A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa)
76	74, 75	syl6ib 229	. . . . . . . . . . . . . . . . . . . . 21 |- (((et /\ ph) /\ (a e. A /\ b e. A)) -> (b e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -> -. A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa))
77	76	con2d 107	. . . . . . . . . . . . . . . . . . . 20 |- (((et /\ ph) /\ (a e. A /\ b e. A)) -> (A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa -> -. b e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})))
78		eldif 2609	. . . . . . . . . . . . . . . . . . . . . . 23 |- (b e. (A \ (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})) <-> (b e. A /\ -. b e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})))
79	78	simplbi2 466	. . . . . . . . . . . . . . . . . . . . . 22 |- (b e. A -> (-. b e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -> b e. (A \ (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}))))
80		eqeq2 1893	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (c = b -> ((f` M) = c <-> (f` M) = b))
81	80	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (c = b -> (((f` M) = c /\ ta) <-> ((f` M) = b /\ ta)))
82	81	3anbi2d 1173	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (c = b -> ((f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch) <-> (f:(M...n)-->A /\ ((f` M) = b /\ ta) /\ A.k e. (N...n)ch)))
83	82	exbidv 1657	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (c = b -> (E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch) <-> E.f(f:(M...n)-->A /\ ((f` M) = b /\ ta) /\ A.k e. (N...n)ch)))
84	83	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (c = b -> (E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch) <-> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = b /\ ta) /\ A.k e. (N...n)ch)))
85	84	elrab3 2415	. . . . . . . . . . . . . . . . . . . . . . 23 |- (b e. A -> (b e. {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)} <-> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = b /\ ta) /\ A.k e. (N...n)ch)))
86		ssrab2 2692	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)} C_ A
87		dfss4 2827	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ({c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)} C_ A <-> (A \ (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})) = {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})
88	86, 87	mpbi 206	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A \ (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})) = {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}
89	88	eleq2i 1961	. . . . . . . . . . . . . . . . . . . . . . 23 |- (b e. (A \ (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})) <-> b e. {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})
90	85, 89	syl5bb 591	. . . . . . . . . . . . . . . . . . . . . 22 |- (b e. A -> (b e. (A \ (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})) <-> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = b /\ ta) /\ A.k e. (N...n)ch)))
91	79, 90	sylibd 219	. . . . . . . . . . . . . . . . . . . . 21 |- (b e. A -> (-. b e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = b /\ ta) /\ A.k e. (N...n)ch)))
92	91	ad2antll 443	. . . . . . . . . . . . . . . . . . . 20 |- (((et /\ ph) /\ (a e. A /\ b e. A)) -> (-. b e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = b /\ ta) /\ A.k e. (N...n)ch)))
93		peano2uz 7616	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (m e. (ZZ>=` M) -> (m + 1) e. (ZZ>=` M))
94	36	eleq2i 1961	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (m e. Z <-> m e. (ZZ>=` M))
95	36	eleq2i 1961	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((m + 1) e. Z <-> (m + 1) e. (ZZ>=` M))
96	93, 94, 95	3imtr4i 236	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (m e. Z -> (m + 1) e. Z)
97	96	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((et /\ ph) /\ (a e. A /\ b e. A)) /\ m e. Z) /\ (g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) -> (m + 1) e. Z)
98		sbequ12r 1546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (d = b -> ([d / b]ph <-> ph))
99	98	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (d = b -> (([d / b]ph /\ a e. A) <-> (ph /\ a e. A)))
100	99	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (d = b -> ((([d / b]ph /\ a e. A) /\ m e. Z) <-> ((ph /\ a e. A) /\ m e. Z)))
101		eqeq2 1893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (d = b -> ((g` M) = d <-> (g` M) = b))
102	101	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (d = b -> (((g` M) = d /\ [(g` m) / a]th) <-> ((g` M) = b /\ [(g` m) / a]th)))
103	102	3anbi2d 1173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (d = b -> ((g:(M...m)-->A /\ ((g` M) = d /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) <-> (g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)))
104	103	imbi1d 675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (d = b -> (((g:(M...m)-->A /\ ((g` M) = d /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch)) <-> ((g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch))))
105	100, 104	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (d = b -> (((([d / b]ph /\ a e. A) /\ m e. Z) -> ((g:(M...m)-->A /\ ((g` M) = d /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch))) <-> (((ph /\ a e. A) /\ m e. Z) -> ((g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch)))))
106		sbequ12r 1546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (c = a -> ([c / a][d / b]ph <-> [d / b]ph))
107		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (c = a -> (c e. A <-> a e. A))
108	106, 107	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (c = a -> (([c / a][d / b]ph /\ c e. A) <-> ([d / b]ph /\ a e. A)))
109	108	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (c = a -> ((([c / a][d / b]ph /\ c e. A) /\ m e. Z) <-> (([d / b]ph /\ a e. A) /\ m e. Z)))
110		eqeq2 1893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (c = a -> ((f` M) = c <-> (f` M) = a))
111	110	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (c = a -> (((f` M) = c /\ [(f` (m + 1)) / a]th) <-> ((f` M) = a /\ [(f` (m + 1)) / a]th)))
112	111	3anbi2d 1173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (c = a -> ((f:(M...(m + 1))-->A /\ ((f` M) = c /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch) <-> (f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch)))
113	112	exbidv 1657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (c = a -> (E.f(f:(M...(m + 1))-->A /\ ((f` M) = c /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch) <-> E.f(f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch)))
114	113	imbi2d 674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (c = a -> (((g:(M...m)-->A /\ ((g` M) = d /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = c /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch)) <-> ((g:(M...m)-->A /\ ((g` M) = d /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch))))
115	109, 114	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (c = a -> (((([c / a][d / b]ph /\ c e. A) /\ m e. Z) -> ((g:(M...m)-->A /\ ((g` M) = d /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = c /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch))) <-> ((([d / b]ph /\ a e. A) /\ m e. Z) -> ((g:(M...m)-->A /\ ((g` M) = d /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch)))))
116	94, 93	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (m e. Z -> (m + 1) e. (ZZ>=` M))
117		elfzp12 15795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((m + 1) e. (ZZ>=` M) -> (x e. (M...(m + 1)) <-> (x = M \/ x e. ((M + 1)...(m + 1)))))
118	116, 117	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (m e. Z -> (x e. (M...(m + 1)) <-> (x = M \/ x e. ((M + 1)...(m + 1)))))
119	118	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((c e. A /\ m e. Z) /\ g:(M...m)-->A) -> (x e. (M...(m + 1)) <-> (x = M \/ x e. ((M + 1)...(m + 1)))))
120		iftrue 2989	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (x = M -> if(x = M, c, (g` (x - 1))) = c)
121	120	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (x = M -> (if(x = M, c, (g` (x - 1))) e. A <-> c e. A))
122	121	biimprcd 173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (c e. A -> (x = M -> if(x = M, c, (g` (x - 1))) e. A))
123	122	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((c e. A /\ m e. Z) /\ g:(M...m)-->A) -> (x = M -> if(x = M, c, (g` (x - 1))) e. A))
124		1re 6598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- 1 e. RR
125	17, 124	readdcli 6487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (M + 1) e. RR
126	17, 125	ltnlei 6754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (M < (M + 1) <-> -. (M + 1) <_ M)
127	18, 126	mpbi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- -. (M + 1) <_ M
128		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (x = M -> (x e. ((M + 1)...(m + 1)) <-> M e. ((M + 1)...(m + 1))))
129		elfzle1 7653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (M e. ((M + 1)...(m + 1)) -> (M + 1) <_ M)
130	128, 129	syl6bi 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (x = M -> (x e. ((M + 1)...(m + 1)) -> (M + 1) <_ M))
131	130	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (x e. ((M + 1)...(m + 1)) -> (x = M -> (M + 1) <_ M))
132	127, 131	mtoi 122	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (x e. ((M + 1)...(m + 1)) -> -. x = M)
133	132	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (((m e. Z /\ g:(M...m)-->A) /\ x e. ((M + 1)...(m + 1))) -> -. x = M)
134		iffalse 2991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (-. x = M -> if(x = M, c, (g` (x - 1))) = (g` (x - 1)))
135	133, 134	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((m e. Z /\ g:(M...m)-->A) /\ x e. ((M + 1)...(m + 1))) -> if(x = M, c, (g` (x - 1))) = (g` (x - 1)))
136		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((g:(M...m)-->A /\ (x - 1) e. (M...m)) -> (g` (x - 1)) e. A)
137		elfzelz 7652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (x e. ((M + 1)...(m + 1)) -> x e. ZZ)
138	137	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((m e. Z /\ x e. ((M + 1)...(m + 1))) -> x e. ZZ)
139		eluzelz 7592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (m e. (ZZ>=` M) -> m e. ZZ)
140	94, 139	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (m e. Z -> m e. ZZ)
141		peano2z 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (m e. ZZ -> (m + 1) e. ZZ)
142		1z 7368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- 1 e. ZZ
143		fzsubel 7673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- ((((M + 1) e. ZZ /\ (m + 1) e. ZZ) /\ (x e. ZZ /\ 1 e. ZZ)) -> (x e. ((M + 1)...(m + 1)) <-> (x - 1) e. (((M + 1) - 1)...((m + 1) - 1))))
144	143	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ((((M + 1) e. ZZ /\ (m + 1) e. ZZ) /\ (x e. ZZ /\ 1 e. ZZ)) -> (x e. ((M + 1)...(m + 1)) -> (x - 1) e. (((M + 1) - 1)...((m + 1) - 1))))
145	142, 144	mpanr2 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ((((M + 1) e. ZZ /\ (m + 1) e. ZZ) /\ x e. ZZ) -> (x e. ((M + 1)...(m + 1)) -> (x - 1) e. (((M + 1) - 1)...((m + 1) - 1))))
146	20, 145	mpanl1 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (((m + 1) e. ZZ /\ x e. ZZ) -> (x e. ((M + 1)...(m + 1)) -> (x - 1) e. (((M + 1) - 1)...((m + 1) - 1))))
147	146	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((m + 1) e. ZZ -> (x e. ZZ -> (x e. ((M + 1)...(m + 1)) -> (x - 1) e. (((M + 1) - 1)...((m + 1) - 1)))))
148	140, 141, 147	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (m e. Z -> (x e. ZZ -> (x e. ((M + 1)...(m + 1)) -> (x - 1) e. (((M + 1) - 1)...((m + 1) - 1)))))
149	148	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (m e. Z -> (x e. ((M + 1)...(m + 1)) -> (x e. ZZ -> (x - 1) e. (((M + 1) - 1)...((m + 1) - 1)))))
150	149	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((m e. Z /\ x e. ((M + 1)...(m + 1))) -> (x e. ZZ -> (x - 1) e. (((M + 1) - 1)...((m + 1) - 1))))
151	138, 150	mpd 29	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((m e. Z /\ x e. ((M + 1)...(m + 1))) -> (x - 1) e. (((M + 1) - 1)...((m + 1) - 1)))
152	17	recni 6467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- M e. CC
153		ax1cn 6422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- 1 e. CC
154		pncan 6557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((M e. CC /\ 1 e. CC) -> ((M + 1) - 1) = M)
155	152, 153, 154	mp2an 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((M + 1) - 1) = M
156	155	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (m e. Z -> ((M + 1) - 1) = M)
157		pncan 6557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((m e. CC /\ 1 e. CC) -> ((m + 1) - 1) = m)
158		zcn 7349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (m e. ZZ -> m e. CC)
159	140, 158	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (m e. Z -> m e. CC)
160	157, 159, 153	sylancl 525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (m e. Z -> ((m + 1) - 1) = m)
161	156, 160	opreq12d 4900	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (m e. Z -> (((M + 1) - 1)...((m + 1) - 1)) = (M...m))
162	161	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((m e. Z /\ x e. ((M + 1)...(m + 1))) -> (((M + 1) - 1)...((m + 1) - 1)) = (M...m))
163	151, 162	eleqtrd 1973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((m e. Z /\ x e. ((M + 1)...(m + 1))) -> (x - 1) e. (M...m))
164	136, 163	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((g:(M...m)-->A /\ (m e. Z /\ x e. ((M + 1)...(m + 1)))) -> (g` (x - 1)) e. A)
165	164	anassrs 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (((g:(M...m)-->A /\ m e. Z) /\ x e. ((M + 1)...(m + 1))) -> (g` (x - 1)) e. A)
166	165	ancom1s 548	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((m e. Z /\ g:(M...m)-->A) /\ x e. ((M + 1)...(m + 1))) -> (g` (x - 1)) e. A)
167	135, 166	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((m e. Z /\ g:(M...m)-->A) /\ x e. ((M + 1)...(m + 1))) -> if(x = M, c, (g` (x - 1))) e. A)
168	167	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((m e. Z /\ g:(M...m)-->A) -> (x e. ((M + 1)...(m + 1)) -> if(x = M, c, (g` (x - 1))) e. A))
169	168	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((c e. A /\ m e. Z) /\ g:(M...m)-->A) -> (x e. ((M + 1)...(m + 1)) -> if(x = M, c, (g` (x - 1))) e. A))
170	123, 169	jaod 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((c e. A /\ m e. Z) /\ g:(M...m)-->A) -> ((x = M \/ x e. ((M + 1)...(m + 1))) -> if(x = M, c, (g` (x - 1))) e. A))
171	119, 170	sylbid 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((c e. A /\ m e. Z) /\ g:(M...m)-->A) -> (x e. (M...(m + 1)) -> if(x = M, c, (g` (x - 1))) e. A))
172	171	r19.21aiv 2175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((c e. A /\ m e. Z) /\ g:(M...m)-->A) -> A.x e. (M...(m + 1))if(x = M, c, (g` (x - 1))) e. A)
173		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}
174	173	fopab2 4796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (A.x e. (M...(m + 1))if(x = M, c, (g` (x - 1))) e. A <-> {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}:(M...(m + 1))-->A)
175	172, 174	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((c e. A /\ m e. Z) /\ g:(M...m)-->A) -> {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}:(M...(m + 1))-->A)
176	175	adantlll 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((([c / a][d / b]ph /\ c e. A) /\ m e. Z) /\ g:(M...m)-->A) -> {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}:(M...(m + 1))-->A)
177	176	3ad2antr1 1041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((([c / a][d / b]ph /\ c e. A) /\ m e. Z) /\ (g:(M...m)-->A /\ ((g` M) = d /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) -> {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}:(M...(m + 1))-->A)
178		eluzfz1 7657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((m + 1) e. (ZZ>=` M) -> M e. (M...(m + 1)))
179	93, 178	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (m e. (ZZ>=` M) -> M e. (M...(m + 1)))
180	94, 179	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (m e. Z -> M e. (M...(m + 1)))
181		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- c e. _V
182	120, 173, 181	fvopab4 4743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (M e. (M...(m + 1)) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` M) = c)
183	180, 182	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (m e. Z -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` M) = c)
184	183	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((([c / a][d / b]ph /\ c e. A) /\ m e. Z) /\ (g:(M...m)-->A /\ ((g` M) = d /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` M) = c)
185		eluzfz2 7659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((m + 1) e. (ZZ>=` M) -> (m + 1) e. (M...(m + 1)))
186	93, 185	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (m e. (ZZ>=` M) -> (m + 1) e. (M...(m + 1)))
187	94, 186	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (m e. Z -> (m + 1) e. (M...(m + 1)))
188		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (x = (m + 1) -> (x = M <-> (m + 1) = M))
189		eqidd 1885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (x = (m + 1) -> c = c)
190		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (x = (m + 1) -> (x - 1) = ((m + 1) - 1))
191	190	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (x = (m + 1) -> (g` (x - 1)) = (g` ((m + 1) - 1)))
192	188, 189, 191	ifbieq12d 2998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (x = (m + 1) -> if(x = M, c, (g` (x - 1))) = if((m + 1) = M, c, (g` ((m + 1) - 1))))
193		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (g` ((m + 1) - 1)) e. _V
194	181, 193	ifex 3031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- if((m + 1) = M, c, (g` ((m + 1) - 1))) e. _V
195	192, 173, 194	fvopab4 4743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((m + 1) e. (M...(m + 1)) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)) = if((m + 1) = M, c, (g` ((m + 1) - 1))))
196	187, 195	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (m e. Z -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)) = if((m + 1) = M, c, (g` ((m + 1) - 1))))
197	17	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (m e. Z -> M e. RR)
198		zre 7348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((m + 1) e. ZZ -> (m + 1) e. RR)
199	140, 141, 198	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (m e. Z -> (m + 1) e. RR)
200		eluzle 7594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (m e. (ZZ>=` M) -> M <_ m)
201	94, 200	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (m e. Z -> M <_ m)
202		zleltp1 7391	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((M e. ZZ /\ m e. ZZ) -> (M <_ m <-> M < (m + 1)))
203	202, 16, 140	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (m e. Z -> (M <_ m <-> M < (m + 1)))
204	201, 203	mpbid 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (m e. Z -> M < (m + 1))
205		ltne 6686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((M e. RR /\ (m + 1) e. RR /\ M < (m + 1)) -> (m + 1) =/= M)
206	197, 199, 204, 205	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (m e. Z -> (m + 1) =/= M)
207		df-ne 2019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((m + 1) =/= M <-> -. (m + 1) = M)
208	206, 207	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (m e. Z -> -. (m + 1) = M)
209		iffalse 2991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (-. (m + 1) = M -> if((m + 1) = M, c, (g` ((m + 1) - 1))) = (g` ((m + 1) - 1)))
210	208, 209	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (m e. Z -> if((m + 1) = M, c, (g` ((m + 1) - 1))) = (g` ((m + 1) - 1)))
211	160	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (m e. Z -> (g` ((m + 1) - 1)) = (g` m))
212	196, 210, 211	3eqtrd 1929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (m e. Z -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)) = (g` m))
213		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)) = (g` m) -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)) / a]th <-> [(g` m) / a]th))
214	212, 213	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (m e. Z -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)) / a]th <-> [(g` m) / a]th))
215	214	biimpar 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((m e. Z /\ [(g` m) / a]th) -> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)) / a]th)
216	215	ad2ant2l 444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((([c / a][d / b]ph /\ c e. A) /\ m e. Z) /\ ((g` M) = d /\ [(g` m) / a]th)) -> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)) / a]th)
217	216	3ad2antr2 1042	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((([c / a][d / b]ph /\ c e. A) /\ m e. Z) /\ (g:(M...m)-->A /\ ((g` M) = d /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) -> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)) / a]th)
218		eluzp1p1 7604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (m e. (ZZ>=` M) -> (m + 1) e. (ZZ>=` (M + 1)))
219	94, 218	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (m e. Z -> (m + 1) e. (ZZ>=` (M + 1)))
220	14	fveq2i 4684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (ZZ>=` N) = (ZZ>=` (M + 1))
221	219, 220	syl6eleqr 1982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (m e. Z -> (m + 1) e. (ZZ>=` N))
222		elfzp12 15795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((m + 1) e. (ZZ>=` N) -> (j e. (N...(m + 1)) <-> (j = N \/ j e. ((N + 1)...(m + 1)))))
223	221, 222	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (m e. Z -> (j e. (N...(m + 1)) <-> (j = N \/ j e. ((N + 1)...(m + 1)))))
224	223	biimpa 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((m e. Z /\ j e. (N...(m + 1))) -> (j = N \/ j e. ((N + 1)...(m + 1))))
225	224	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((([c / a][d / b]ph /\ m e. Z) /\ j e. (N...(m + 1))) -> (j = N \/ j e. ((N + 1)...(m + 1))))
226	225	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((([c / a][d / b]ph /\ m e. Z) /\ ((g` M) = d /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) /\ j e. (N...(m + 1))) -> (j = N \/ j e. ((N + 1)...(m + 1))))
227		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (j = N -> (j - 1) = (N - 1))
228	14	opreq1i 4892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (N - 1) = ((M + 1) - 1)
229	228, 155	eqtri 1908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (N - 1) = M
230	227, 229	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (j = N -> (j - 1) = M)
231	230	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (j = N -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` M))
232	231	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((m e. Z /\ ((g` M) = d /\ j = N)) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` M))
233	183	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((m e. Z /\ ((g` M) = d /\ j = N)) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` M) = c)
234	232, 233	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((m e. Z /\ ((g` M) = d /\ j = N)) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) = c)
235		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) = c -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [c / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph))
236	234, 235	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((m e. Z /\ ((g` M) = d /\ j = N)) -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [c / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph))
237	14	eqeq2i 1894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (j = N <-> j = (M + 1))
238		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (j = (M + 1) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (M + 1)))
239	237, 238	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (j = N -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (M + 1)))
240	239	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((m e. Z /\ ((g` M) = d /\ j = N)) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (M + 1)))
241		fzss1 7675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (((M + 1) e. (ZZ>=` M) /\ (m + 1) e. ZZ) -> ((M + 1)...(m + 1)) C_ (M...(m + 1)))
242		eluz2 7590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- ((M + 1) e. (ZZ>=` M) <-> (M e. ZZ /\ (M + 1) e. ZZ /\ M <_ (M + 1)))
243	17, 125, 18	ltleii 6756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- M <_ (M + 1)
244	242, 16, 20, 243	mpbir3an 1052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (M + 1) e. (ZZ>=` M)
245	140	peano2zdi 7376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (m e. Z -> (m + 1) e. ZZ)
246	241, 244, 245	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (m e. Z -> ((M + 1)...(m + 1)) C_ (M...(m + 1)))
247		eluzfz1 7657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- (m e. (ZZ>=` M) -> M e. (M...m))
248	94, 247	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (m e. Z -> M e. (M...m))
249		fzaddel 7672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 |- (((M e. ZZ /\ m e. ZZ) /\ (M e. ZZ /\ 1 e. ZZ)) -> (M e. (M...m) <-> (M + 1) e. ((M + 1)...(m + 1))))
250	16, 142, 249	mpanr12 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- ((M e. ZZ /\ m e. ZZ) -> (M e. (M...m) <-> (M + 1) e. ((M + 1)...(m + 1))))
251	250, 16, 140	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (m e. Z -> (M e. (M...m) <-> (M + 1) e. ((M + 1)...(m + 1))))
252	248, 251	mpbid 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (m e. Z -> (M + 1) e. ((M + 1)...(m + 1)))
253	246, 252	sseldd 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (m e. Z -> (M + 1) e. (M...(m + 1)))
254		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (x = (M + 1) -> (x = M <-> (M + 1) = M))
255		eqidd 1885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (x = (M + 1) -> c = c)
256		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 |- (x = (M + 1) -> (x - 1) = ((M + 1) - 1))
257	256, 155	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- (x = (M + 1) -> (x - 1) = M)
258	257	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (x = (M + 1) -> (g` (x - 1)) = (g` M))
259	254, 255, 258	ifbieq12d 2998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (x = (M + 1) -> if(x = M, c, (g` (x - 1))) = if((M + 1) = M, c, (g` M)))
260		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (g` M) e. _V
261	181, 260	ifex 3031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- if((M + 1) = M, c, (g` M)) e. _V
262	259, 173, 261	fvopab4 4743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ((M + 1) e. (M...(m + 1)) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (M + 1)) = if((M + 1) = M, c, (g` M)))
263	253, 262	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (m e. Z -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (M + 1)) = if((M + 1) = M, c, (g` M)))
264	17, 125	ltnei 6758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (M < (M + 1) -> (M + 1) =/= M)
265	18, 264	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (M + 1) =/= M
266		df-ne 2019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ((M + 1) =/= M <-> -. (M + 1) = M)
267	265, 266	mpbi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- -. (M + 1) = M
268		iffalse 2991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (-. (M + 1) = M -> if((M + 1) = M, c, (g` M)) = (g` M))
269	267, 268	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- if((M + 1) = M, c, (g` M)) = (g` M)
270	263, 269	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (m e. Z -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (M + 1)) = (g` M))
271	270	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((m e. Z /\ ((g` M) = d /\ j = N)) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (M + 1)) = (g` M))
272		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((m e. Z /\ ((g` M) = d /\ j = N)) -> (g` M) = d)
273	240, 271, 272	3eqtrd 1929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((m e. Z /\ ((g` M) = d /\ j = N)) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) = d)
274		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) = d -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [d / b]ph))
275	273, 274	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((m e. Z /\ ((g` M) = d /\ j = N)) -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [d / b]ph))
276	275	sbcbidv 2505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (((m e. Z /\ ((g` M) = d /\ j = N)) /\ c e. _V) -> ([c / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [c / a][d / b]ph))
277	181, 276	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((m e. Z /\ ((g` M) = d /\ j = N)) -> ([c / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [c / a][d / b]ph))
278	236, 277	bitrd 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((m e. Z /\ ((g` M) = d /\ j = N)) -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [c / a][d / b]ph))
279	278	biimparc 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (([c / a][d / b]ph /\ (m e. Z /\ ((g` M) = d /\ j = N))) -> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph)
280	279	anassrs 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((([c / a][d / b]ph /\ m e. Z) /\ ((g` M) = d /\ j = N)) -> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph)
281	280	anassrs 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((([c / a][d / b]ph /\ m e. Z) /\ (g` M) = d) /\ j = N) -> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph)
282	281	adantlrr 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((([c / a][d / b]ph /\ m e. Z) /\ ((g` M) = d /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) /\ j = N) -> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph)
283		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (k = (j - 1) -> (k - 1) = ((j - 1) - 1))
284	283	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (k = (j - 1) -> (g` (k - 1)) = (g` ((j - 1) - 1)))
285		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((g` (k - 1)) = (g` ((j - 1) - 1)) -> ([(g` (k - 1)) / a][(g` k) / b]ph <-> [(g` ((j - 1) - 1)) / a][(g` k) / b]ph))
286	284, 285	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (k = (j - 1) -> ([(g` (k - 1)) / a][(g` k) / b]ph <-> [(g` ((j - 1) - 1)) / a][(g` k) / b]ph))
287		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (g` ((j - 1) - 1)) e. _V
288		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (k = (j - 1) -> (g` k) = (g` (j - 1)))
289		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((g` k) = (g` (j - 1)) -> ([(g` k) / b]ph <-> [(g` (j - 1)) / b]ph))
290	288, 289	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (k = (j - 1) -> ([(g` k) / b]ph <-> [(g` (j - 1)) / b]ph))
291	290	sbcbidv 2505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((k = (j - 1) /\ (g` ((j - 1) - 1)) e. _V) -> ([(g` ((j - 1) - 1)) / a][(g` k) / b]ph <-> [(g` ((j - 1) - 1)) / a][(g` (j - 1)) / b]ph))
292	287, 291	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (k = (j - 1) -> ([(g` ((j - 1) - 1)) / a][(g` k) / b]ph <-> [(g` ((j - 1) - 1)) / a][(g` (j - 1)) / b]ph))
293	286, 292	bitrd 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (k = (j - 1) -> ([(g` (k - 1)) / a][(g` k) / b]ph <-> [(g` ((j - 1) - 1)) / a][(g` (j - 1)) / b]ph))
294	293	rcla4va 2378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (((j - 1) e. (N...m) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> [(g` ((j - 1) - 1)) / a][(g` (j - 1)) / b]ph)
295		elfzelz 7652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (j e. ((N + 1)...(m + 1)) -> j e. ZZ)
296	295	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> j e. ZZ)
297		fzsubel 7673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ((((N + 1) e. ZZ /\ (m + 1) e. ZZ) /\ (j e. ZZ /\ 1 e. ZZ)) -> (j e. ((N + 1)...(m + 1)) <-> (j - 1) e. (((N + 1) - 1)...((m + 1) - 1))))
298	297	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ((((N + 1) e. ZZ /\ (m + 1) e. ZZ) /\ (j e. ZZ /\ 1 e. ZZ)) -> (j e. ((N + 1)...(m + 1)) -> (j - 1) e. (((N + 1) - 1)...((m + 1) - 1))))
299	142, 298	mpanr2 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((((N + 1) e. ZZ /\ (m + 1) e. ZZ) /\ j e. ZZ) -> (j e. ((N + 1)...(m + 1)) -> (j - 1) e. (((N + 1) - 1)...((m + 1) - 1))))
300	299	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (((N + 1) e. ZZ /\ (m + 1) e. ZZ) -> (j e. ZZ -> (j e. ((N + 1)...(m + 1)) -> (j - 1) e. (((N + 1) - 1)...((m + 1) - 1)))))
301	14, 20	eqeltri 1967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- N e. ZZ
302		peano2z 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (N e. ZZ -> (N + 1) e. ZZ)
303	301, 302	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (N + 1) e. ZZ
304	300, 303, 245	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (m e. Z -> (j e. ZZ -> (j e. ((N + 1)...(m + 1)) -> (j - 1) e. (((N + 1) - 1)...((m + 1) - 1)))))
305	304	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (m e. Z -> (j e. ((N + 1)...(m + 1)) -> (j e. ZZ -> (j - 1) e. (((N + 1) - 1)...((m + 1) - 1)))))
306	305	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> (j e. ZZ -> (j - 1) e. (((N + 1) - 1)...((m + 1) - 1))))
307	296, 306	mpd 29	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> (j - 1) e. (((N + 1) - 1)...((m + 1) - 1)))
308	301	zrei 7350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- N e. RR
309	308	recni 6467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- N e. CC
310		pncan 6557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((N e. CC /\ 1 e. CC) -> ((N + 1) - 1) = N)
311	309, 153, 310	mp2an 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((N + 1) - 1) = N
312	311	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (m e. Z -> ((N + 1) - 1) = N)
313	312, 160	opreq12d 4900	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (m e. Z -> (((N + 1) - 1)...((m + 1) - 1)) = (N...m))
314	313	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> (((N + 1) - 1)...((m + 1) - 1)) = (N...m))
315	307, 314	eleqtrd 1973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> (j - 1) e. (N...m))
316	294, 315	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (((m e. Z /\ j e. ((N + 1)...(m + 1))) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> [(g` ((j - 1) - 1)) / a][(g` (j - 1)) / b]ph)
317		fzss1 7675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ((N e. (ZZ>=` M) /\ (m + 1) e. ZZ) -> (N...(m + 1)) C_ (M...(m + 1)))
318	14, 244	eqeltri 1967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- N e. (ZZ>=` M)
319	317, 318, 245	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (m e. Z -> (N...(m + 1)) C_ (M...(m + 1)))
320	319	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> (N...(m + 1)) C_ (M...(m + 1)))
321		fzss2 7676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (((m + 1) e. (ZZ>=` m) /\ N e. ZZ) -> (N...m) C_ (N...(m + 1)))
322		zre 7348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 |- (m e. ZZ -> m e. RR)
323		ltp1 6989	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 |- (m e. RR -> m < (m + 1))
324	140, 322, 323	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 |- (m e. Z -> m < (m + 1))
325	140, 322	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 |- (m e. Z -> m e. RR)
326		ltle 6690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 |- ((m e. RR /\ (m + 1) e. RR) -> (m < (m + 1) -> m <_ (m + 1)))
327	325, 199, 326	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 |- (m e. Z -> (m < (m + 1) -> m <_ (m + 1)))
328	324, 327	mpd 29	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- (m e. Z -> m <_ (m + 1))
329	140, 245, 328	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (m e. Z -> (m e. ZZ /\ (m + 1) e. ZZ /\ m <_ (m + 1)))
330		eluz2 7590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- ((m + 1) e. (ZZ>=` m) <-> (m e. ZZ /\ (m + 1) e. ZZ /\ m <_ (m + 1)))
331	329, 330	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (m e. Z -> (m + 1) e. (ZZ>=` m))
332	321, 331, 301	sylancl 525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (m e. Z -> (N...m) C_ (N...(m + 1)))
333	332	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> (N...m) C_ (N...(m + 1)))
334	333, 315	sseldd 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> (j - 1) e. (N...(m + 1)))
335	320, 334	sseldd 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> (j - 1) e. (M...(m + 1)))
336		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (x = (j - 1) -> (x = M <-> (j - 1) = M))
337		eqidd 1885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (x = (j - 1) -> c = c)
338		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (x = (j - 1) -> (x - 1) = ((j - 1) - 1))
339	338	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (x = (j - 1) -> (g` (x - 1)) = (g` ((j - 1) - 1)))
340	336, 337, 339	ifbieq12d 2998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (x = (j - 1) -> if(x = M, c, (g` (x - 1))) = if((j - 1) = M, c, (g` ((j - 1) - 1))))
341	181, 287	ifex 3031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- if((j - 1) = M, c, (g` ((j - 1) - 1))) e. _V
342	340, 173, 341	fvopab4 4743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((j - 1) e. (M...(m + 1)) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) = if((j - 1) = M, c, (g` ((j - 1) - 1))))
343	335, 342	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) = if((j - 1) = M, c, (g` ((j - 1) - 1))))
344	125	ltp1i 6991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (M + 1) < ((M + 1) + 1)
345	14	opreq1i 4892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (N + 1) = ((M + 1) + 1)
346	344, 345	breqtrri 3362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (M + 1) < (N + 1)
347	308, 124	readdcli 6487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (N + 1) e. RR
348	125, 347	ltnlei 6754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ((M + 1) < (N + 1) <-> -. (N + 1) <_ (M + 1))
349	346, 348	mpbi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- -. (N + 1) <_ (M + 1)
350		zcn 7349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (j e. ZZ -> j e. CC)
351		subadd 6532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- ((j e. CC /\ 1 e. CC /\ M e. CC) -> ((j - 1) = M <-> (1 + M) = j))
352	153, 152, 351	mp3an23 1183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (j e. CC -> ((j - 1) = M <-> (1 + M) = j))
353	295, 350, 352	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (j e. ((N + 1)...(m + 1)) -> ((j - 1) = M <-> (1 + M) = j))
354		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- (j = (M + 1) -> (j e. ((N + 1)...(m + 1)) <-> (M + 1) e. ((N + 1)...(m + 1))))
355		elfzle1 7653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- ((M + 1) e. ((N + 1)...(m + 1)) -> (N + 1) <_ (M + 1))
356	354, 355	syl6bi 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (j = (M + 1) -> (j e. ((N + 1)...(m + 1)) -> (N + 1) <_ (M + 1)))
357	356	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (j e. ((N + 1)...(m + 1)) -> (j = (M + 1) -> (N + 1) <_ (M + 1)))
358		eqcom 1886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- ((1 + M) = j <-> j = (1 + M))
359	153, 152	addcomi 6475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- (1 + M) = (M + 1)
360	359	eqeq2i 1894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (j = (1 + M) <-> j = (M + 1))
361	358, 360	bitri 190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ((1 + M) = j <-> j = (M + 1))
362	357, 361	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (j e. ((N + 1)...(m + 1)) -> ((1 + M) = j -> (N + 1) <_ (M + 1)))
363	353, 362	sylbid 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (j e. ((N + 1)...(m + 1)) -> ((j - 1) = M -> (N + 1) <_ (M + 1)))
364	349, 363	mtoi 122	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (j e. ((N + 1)...(m + 1)) -> -. (j - 1) = M)
365	364	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> -. (j - 1) = M)
366		iffalse 2991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (-. (j - 1) = M -> if((j - 1) = M, c, (g` ((j - 1) - 1))) = (g` ((j - 1) - 1)))
367	365, 366	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> if((j - 1) = M, c, (g` ((j - 1) - 1))) = (g` ((j - 1) - 1)))
368	343, 367	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) = (g` ((j - 1) - 1)))
369		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) = (g` ((j - 1) - 1)) -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [(g` ((j - 1) - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph))
370	368, 369	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [(g` ((j - 1) - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph))
371		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ((((N + 1)...(m + 1)) C_ (M...(m + 1)) /\ j e. ((N + 1)...(m + 1))) -> j e. (M...(m + 1)))
372		fzss1 7675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (((N + 1) e. (ZZ>=` M) /\ (m + 1) e. ZZ) -> ((N + 1)...(m + 1)) C_ (M...(m + 1)))
373		peano2uz 7616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (N e. (ZZ>=` M) -> (N + 1) e. (ZZ>=` M))
374	318, 373	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (N + 1) e. (ZZ>=` M)
375	372, 374, 245	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (m e. Z -> ((N + 1)...(m + 1)) C_ (M...(m + 1)))
376	371, 375	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> j e. (M...(m + 1)))
377		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (x = j -> (x = M <-> j = M))
378		eqidd 1885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (x = j -> c = c)
379		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (x = j -> (x - 1) = (j - 1))
380	379	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (x = j -> (g` (x - 1)) = (g` (j - 1)))
381	377, 378, 380	ifbieq12d 2998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (x = j -> if(x = M, c, (g` (x - 1))) = if(j = M, c, (g` (j - 1))))
382		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (g` (j - 1)) e. _V
383	181, 382	ifex 3031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- if(j = M, c, (g` (j - 1))) e. _V
384	381, 173, 383	fvopab4 4743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (j e. (M...(m + 1)) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) = if(j = M, c, (g` (j - 1))))
385	376, 384	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) = if(j = M, c, (g` (j - 1))))
386	18, 14	breqtrri 3362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- M < N
387	308	ltp1i 6991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- N < (N + 1)
388	17, 308, 347	lttri 6760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- ((M < N /\ N < (N + 1)) -> M < (N + 1))
389	386, 387, 388	mp2an 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- M < (N + 1)
390	17, 347	ltnlei 6754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (M < (N + 1) <-> -. (N + 1) <_ M)
391	389, 390	mpbi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- -. (N + 1) <_ M
392		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- (j = M -> (j e. ((N + 1)...(m + 1)) <-> M e. ((N + 1)...(m + 1))))
393		elfzle1 7653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- (M e. ((N + 1)...(m + 1)) -> (N + 1) <_ M)
394	392, 393	syl6bi 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- (j = M -> (j e. ((N + 1)...(m + 1)) -> (N + 1) <_ M))
395	394	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (j e. ((N + 1)...(m + 1)) -> (j = M -> (N + 1) <_ M))
396	391, 395	mtoi 122	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (j e. ((N + 1)...(m + 1)) -> -. j = M)
397	396	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> -. j = M)
398		iffalse 2991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (-. j = M -> if(j = M, c, (g` (j - 1))) = (g` (j - 1)))
399	397, 398	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> if(j = M, c, (g` (j - 1))) = (g` (j - 1)))
400	385, 399	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) = (g` (j - 1)))
401		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) = (g` (j - 1)) -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [(g` (j - 1)) / b]ph))
402	400, 401	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [(g` (j - 1)) / b]ph))
403	402	sbcbidv 2505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (((m e. Z /\ j e. ((N + 1)...(m + 1))) /\ (g` ((j - 1) - 1)) e. _V) -> ([(g` ((j - 1) - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [(g` ((j - 1) - 1)) / a][(g` (j - 1)) / b]ph))
404	287, 403	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> ([(g` ((j - 1) - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [(g` ((j - 1) - 1)) / a][(g` (j - 1)) / b]ph))
405	370, 404	bitrd 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((m e. Z /\ j e. ((N + 1)...(m + 1))) -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [(g` ((j - 1) - 1)) / a][(g` (j - 1)) / b]ph))
406	405	biimpar 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (((m e. Z /\ j e. ((N + 1)...(m + 1))) /\ [(g` ((j - 1) - 1)) / a][(g` (j - 1)) / b]ph) -> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph)
407	316, 406	syldan 516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (((m e. Z /\ j e. ((N + 1)...(m + 1))) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph)
408	407	an1rs 547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((m e. Z /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) /\ j e. ((N + 1)...(m + 1))) -> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph)
409	408	adantlrl 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((m e. Z /\ ((g` M) = d /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) /\ j e. ((N + 1)...(m + 1))) -> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph)
410	409	adantlll 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((([c / a][d / b]ph /\ m e. Z) /\ ((g` M) = d /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) /\ j e. ((N + 1)...(m + 1))) -> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph)
411	282, 410	jaodan 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((([c / a][d / b]ph /\ m e. Z) /\ ((g` M) = d /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) /\ (j = N \/ j e. ((N + 1)...(m + 1)))) -> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph)
412	226, 411	syldan 516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((([c / a][d / b]ph /\ m e. Z) /\ ((g` M) = d /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) /\ j e. (N...(m + 1))) -> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph)
413	412	r19.21aiva 2176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((([c / a][d / b]ph /\ m e. Z) /\ ((g` M) = d /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) -> A.j e. (N...(m + 1))[({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph)
414		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (j = k -> (j - 1) = (k - 1))
415	414	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (j = k -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)))
416		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph))
417	415, 416	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (j = k -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph))
418		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) e. _V
419		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (j = k -> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k))
420		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph))
421	419, 420	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (j = k -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph))
422	421	sbcbidv 2505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((j = k /\ ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) e. _V) -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph))
423	418, 422	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (j = k -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph))
424	417, 423	bitrd 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (j = k -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph))
425	424	cbvralv 2280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (A.j e. (N...(m + 1))[({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (j - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` j) / b]ph <-> A.k e. (N...(m + 1))[({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph)
426	413, 425	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((([c / a][d / b]ph /\ m e. Z) /\ ((g` M) = d /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) -> A.k e. (N...(m + 1))[({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph)
427	426	adantllr 433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((([c / a][d / b]ph /\ c e. A) /\ m e. Z) /\ ((g` M) = d /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) -> A.k e. (N...(m + 1))[({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph)
428	427	adantrlr 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((([c / a][d / b]ph /\ c e. A) /\ m e. Z) /\ (((g` M) = d /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) -> A.k e. (N...(m + 1))[({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph)
429	428	3adantr1 1035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((([c / a][d / b]ph /\ c e. A) /\ m e. Z) /\ (g:(M...m)-->A /\ ((g` M) = d /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) -> A.k e. (N...(m + 1))[({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph)
430		oprex 4907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (M...(m + 1)) e. _V
431	430	opabex2 4539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} e. _V
432		feq1 4551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} -> (f:(M...(m + 1))-->A <-> {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}:(M...(m + 1))-->A))
433		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} -> (f` M) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` M))
434	433	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} -> ((f` M) = c <-> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` M) = c))
435		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} -> (f` (m + 1)) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)))
436		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((f` (m + 1)) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)) -> ([(f` (m + 1)) / a]th <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)) / a]th))
437	435, 436	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} -> ([(f` (m + 1)) / a]th <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)) / a]th))
438	434, 437	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} -> (((f` M) = c /\ [(f` (m + 1)) / a]th) <-> (({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` M) = c /\ [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)) / a]th)))
439		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} -> (f` (k - 1)) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)))
440		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((f` (k - 1)) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) -> ([(f` (k - 1)) / a][(f` k) / b]ph <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][(f` k) / b]ph))
441	439, 440	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} -> ([(f` (k - 1)) / a][(f` k) / b]ph <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][(f` k) / b]ph))
442		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} -> (f` k) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k))
443		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((f` k) = ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) -> ([(f` k) / b]ph <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph))
444	442, 443	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} -> ([(f` k) / b]ph <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph))
445	444	sbcbidv 2505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} /\ ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) e. _V) -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][(f` k) / b]ph <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph))
446	418, 445	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} -> ([({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][(f` k) / b]ph <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph))
447	441, 446	bitrd 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} -> ([(f` (k - 1)) / a][(f` k) / b]ph <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph))
448		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (f` (k - 1)) e. _V
449		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (f` k) e. _V
450		fdc.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (a = (f` (k - 1)) -> (ph <-> ps))
451	450	sbcbidv 2505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((a = (f` (k - 1)) /\ (f` k) e. _V) -> ([(f` k) / b]ph <-> [(f` k) / b]ps))
452	449, 451	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (a = (f` (k - 1)) -> ([(f` k) / b]ph <-> [(f` k) / b]ps))
453	448, 452	sbcie 2485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ([(f` (k - 1)) / a][(f` k) / b]ph <-> [(f` k) / b]ps)
454		fdc.6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (b = (f` k) -> (ps <-> ch))
455	449, 454	sbcie 2485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ([(f` k) / b]ps <-> ch)
456	453, 455	bitri 190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ([(f` (k - 1)) / a][(f` k) / b]ph <-> ch)
457	447, 456	syl5bbr 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} -> (ch <-> [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph))
458	457	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} -> (A.k e. (N...(m + 1))ch <-> A.k e. (N...(m + 1))[({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph))
459	432, 438, 458	3anbi123d 1168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f = {<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))} -> ((f:(M...(m + 1))-->A /\ ((f` M) = c /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch) <-> ({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}:(M...(m + 1))-->A /\ (({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` M) = c /\ [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))[({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph)))
460	431, 459	cla4ev 2371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}:(M...(m + 1))-->A /\ (({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` M) = c /\ [({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))[({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` (k - 1)) / a][({<.x, y>. | (x e. (M...(m + 1)) /\ y = if(x = M, c, (g` (x - 1))))}` k) / b]ph) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = c /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch))
461	177, 184, 217, 429, 460	syl121anc 1105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((([c / a][d / b]ph /\ c e. A) /\ m e. Z) /\ (g:(M...m)-->A /\ ((g` M) = d /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = c /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch))
462	461	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((([c / a][d / b]ph /\ c e. A) /\ m e. Z) -> ((g:(M...m)-->A /\ ((g` M) = d /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = c /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch)))
463	115, 462	chvarv 1712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((([d / b]ph /\ a e. A) /\ m e. Z) -> ((g:(M...m)-->A /\ ((g` M) = d /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch)))
464	105, 463	chvarv 1712	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((ph /\ a e. A) /\ m e. Z) -> ((g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch)))
465	464	adantlrr 435	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((ph /\ (a e. A /\ b e. A)) /\ m e. Z) -> ((g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch)))
466	465	adantlll 432	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((et /\ ph) /\ (a e. A /\ b e. A)) /\ m e. Z) -> ((g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch)))
467	466	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((et /\ ph) /\ (a e. A /\ b e. A)) /\ m e. Z) /\ (g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) -> E.f(f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch))
468		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (n = (m + 1) -> (M...n) = (M...(m + 1)))
469	468	feq2d 4557	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (n = (m + 1) -> (f:(M...n)-->A <-> f:(M...(m + 1))-->A))
470		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (n = (m + 1) -> (f` n) = (f` (m + 1)))
471		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((f` n) = (f` (m + 1)) -> ([(f` n) / a]th <-> [(f` (m + 1)) / a]th))
472	470, 471	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (n = (m + 1) -> ([(f` n) / a]th <-> [(f` (m + 1)) / a]th))
473	472, 10	syl5bbr 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (n = (m + 1) -> (ta <-> [(f` (m + 1)) / a]th))
474	473	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (n = (m + 1) -> (((f` M) = a /\ ta) <-> ((f` M) = a /\ [(f` (m + 1)) / a]th)))
475		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (n = (m + 1) -> (N...n) = (N...(m + 1)))
476	475	raleqdv 2269	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (n = (m + 1) -> (A.k e. (N...n)ch <-> A.k e. (N...(m + 1))ch))
477	469, 474, 476	3anbi123d 1168	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (n = (m + 1) -> ((f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch) <-> (f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch)))
478	477	exbidv 1657	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (n = (m + 1) -> (E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch) <-> E.f(f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch)))
479	478	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((m + 1) e. Z /\ E.f(f:(M...(m + 1))-->A /\ ((f` M) = a /\ [(f` (m + 1)) / a]th) /\ A.k e. (N...(m + 1))ch)) -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch))
480	97, 467, 479	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((et /\ ph) /\ (a e. A /\ b e. A)) /\ m e. Z) /\ (g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)) -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch))
481	480	ex 402	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((et /\ ph) /\ (a e. A /\ b e. A)) /\ m e. Z) -> ((g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch)))
482	481	19.23adv 1584	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((et /\ ph) /\ (a e. A /\ b e. A)) /\ m e. Z) -> (E.g(g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch)))
483	482	r19.23adva 2216	. . . . . . . . . . . . . . . . . . . . 21 |- (((et /\ ph) /\ (a e. A /\ b e. A)) -> (E.m e. Z E.g(g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph) -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch)))
484		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (n = m -> (M...n) = (M...m))
485	484	feq2d 4557	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (n = m -> (f:(M...n)-->A <-> f:(M...m)-->A))
486		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (n = m -> (f` n) = (f` m))
487		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f` n) = (f` m) -> ([(f` n) / a]th <-> [(f` m) / a]th))
488	486, 487	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (n = m -> ([(f` n) / a]th <-> [(f` m) / a]th))
489	488, 10	syl5bbr 593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (n = m -> (ta <-> [(f` m) / a]th))
490	489	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (n = m -> (((f` M) = b /\ ta) <-> ((f` M) = b /\ [(f` m) / a]th)))
491		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (n = m -> (N...n) = (N...m))
492	491	raleqdv 2269	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (n = m -> (A.k e. (N...n)ch <-> A.k e. (N...m)ch))
493	485, 490, 492	3anbi123d 1168	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (n = m -> ((f:(M...n)-->A /\ ((f` M) = b /\ ta) /\ A.k e. (N...n)ch) <-> (f:(M...m)-->A /\ ((f` M) = b /\ [(f` m) / a]th) /\ A.k e. (N...m)ch)))
494	493	exbidv 1657	. . . . . . . . . . . . . . . . . . . . . . 23 |- (n = m -> (E.f(f:(M...n)-->A /\ ((f` M) = b /\ ta) /\ A.k e. (N...n)ch) <-> E.f(f:(M...m)-->A /\ ((f` M) = b /\ [(f` m) / a]th) /\ A.k e. (N...m)ch)))
495	494	cbvrexv 2281	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = b /\ ta) /\ A.k e. (N...n)ch) <-> E.m e. Z E.f(f:(M...m)-->A /\ ((f` M) = b /\ [(f` m) / a]th) /\ A.k e. (N...m)ch))
496		feq1 4551	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f = g -> (f:(M...m)-->A <-> g:(M...m)-->A))
497		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f = g -> (f` M) = (g` M))
498	497	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f = g -> ((f` M) = b <-> (g` M) = b))
499		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f = g -> (f` m) = (g` m))
500		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((f` m) = (g` m) -> ([(f` m) / a]th <-> [(g` m) / a]th))
501	499, 500	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f = g -> ([(f` m) / a]th <-> [(g` m) / a]th))
502	498, 501	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f = g -> (((f` M) = b /\ [(f` m) / a]th) <-> ((g` M) = b /\ [(g` m) / a]th)))
503		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f = g -> (f` (k - 1)) = (g` (k - 1)))
504		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f` (k - 1)) = (g` (k - 1)) -> ([(f` (k - 1)) / a][(f` k) / b]ph <-> [(g` (k - 1)) / a][(f` k) / b]ph))
505	503, 504	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f = g -> ([(f` (k - 1)) / a][(f` k) / b]ph <-> [(g` (k - 1)) / a][(f` k) / b]ph))
506		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (g` (k - 1)) e. _V
507		fveq1 4680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f = g -> (f` k) = (g` k))
508		dfsbcq 2455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((f` k) = (g` k) -> ([(f` k) / b]ph <-> [(g` k) / b]ph))
509	507, 508	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f = g -> ([(f` k) / b]ph <-> [(g` k) / b]ph))
510	509	sbcbidv 2505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f = g /\ (g` (k - 1)) e. _V) -> ([(g` (k - 1)) / a][(f` k) / b]ph <-> [(g` (k - 1)) / a][(g` k) / b]ph))
511	506, 510	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f = g -> ([(g` (k - 1)) / a][(f` k) / b]ph <-> [(g` (k - 1)) / a][(g` k) / b]ph))
512	505, 511	bitrd 587	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f = g -> ([(f` (k - 1)) / a][(f` k) / b]ph <-> [(g` (k - 1)) / a][(g` k) / b]ph))
513	512, 456	syl5bbr 593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f = g -> (ch <-> [(g` (k - 1)) / a][(g` k) / b]ph))
514	513	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f = g -> (A.k e. (N...m)ch <-> A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph))
515	496, 502, 514	3anbi123d 1168	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f = g -> ((f:(M...m)-->A /\ ((f` M) = b /\ [(f` m) / a]th) /\ A.k e. (N...m)ch) <-> (g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph)))
516	515	cbvexv 1697	. . . . . . . . . . . . . . . . . . . . . . 23 |- (E.f(f:(M...m)-->A /\ ((f` M) = b /\ [(f` m) / a]th) /\ A.k e. (N...m)ch) <-> E.g(g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph))
517	516	rexbii 2128	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.m e. Z E.f(f:(M...m)-->A /\ ((f` M) = b /\ [(f` m) / a]th) /\ A.k e. (N...m)ch) <-> E.m e. Z E.g(g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph))
518	495, 517	bitri 190	. . . . . . . . . . . . . . . . . . . . 21 |- (E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = b /\ ta) /\ A.k e. (N...n)ch) <-> E.m e. Z E.g(g:(M...m)-->A /\ ((g` M) = b /\ [(g` m) / a]th) /\ A.k e. (N...m)[(g` (k - 1)) / a][(g` k) / b]ph))
519	483, 518	syl5ib 223	. . . . . . . . . . . . . . . . . . . 20 |- (((et /\ ph) /\ (a e. A /\ b e. A)) -> (E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = b /\ ta) /\ A.k e. (N...n)ch) -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch)))
520	77, 92, 519	3syld 31	. . . . . . . . . . . . . . . . . . 19 |- (((et /\ ph) /\ (a e. A /\ b e. A)) -> (A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch)))
521	520	an42s 567	. . . . . . . . . . . . . . . . . 18 |- (((et /\ a e. A) /\ (b e. A /\ ph)) -> (A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch)))
522	521	expr 418	. . . . . . . . . . . . . . . . 17 |- (((et /\ a e. A) /\ b e. A) -> (ph -> (A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch))))
523	522	r19.23adva 2216	. . . . . . . . . . . . . . . 16 |- ((et /\ a e. A) -> (E.b e. A ph -> (A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch))))
524	523	imp 377	. . . . . . . . . . . . . . 15 |- (((et /\ a e. A) /\ E.b e. A ph) -> (A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch)))
525	69, 524	jaodan 471	. . . . . . . . . . . . . 14 |- (((et /\ a e. A) /\ (th \/ E.b e. A ph)) -> (A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch)))
526	2, 525	mpdan 768	. . . . . . . . . . . . 13 |- ((et /\ a e. A) -> (A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch)))
527	110	anbi1d 679	. . . . . . . . . . . . . . . . . 18 |- (c = a -> (((f` M) = c /\ ta) <-> ((f` M) = a /\ ta)))
528	527	3anbi2d 1173	. . . . . . . . . . . . . . . . 17 |- (c = a -> ((f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch) <-> (f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch)))
529	528	exbidv 1657	. . . . . . . . . . . . . . . 16 |- (c = a -> (E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch) <-> E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch)))
530	529	rexbidv 2124	. . . . . . . . . . . . . . 15 |- (c = a -> (E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch) <-> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch)))
531	530	elrab3 2415	. . . . . . . . . . . . . 14 |- (a e. A -> (a e. {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)} <-> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch)))
532	531	adantl 424	. . . . . . . . . . . . 13 |- ((et /\ a e. A) -> (a e. {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)} <-> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = a /\ ta) /\ A.k e. (N...n)ch)))
533	526, 532	sylibrd 221	. . . . . . . . . . . 12 |- ((et /\ a e. A) -> (A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa -> a e. {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}))
534	533	ex 402	. . . . . . . . . . 11 |- (et -> (a e. A -> (A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa -> a e. {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})))
535	534	com23 36	. . . . . . . . . 10 |- (et -> (A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa -> (a e. A -> a e. {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})))
536		eldif 2609	. . . . . . . . . . . 12 |- (a e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) <-> (a e. A /\ -. a e. {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}))
537	536	notbii 204	. . . . . . . . . . 11 |- (-. a e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) <-> -. (a e. A /\ -. a e. {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}))
538		iman 256	. . . . . . . . . . 11 |- ((a e. A -> a e. {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) <-> -. (a e. A /\ -. a e. {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}))
539	537, 538	bitr4i 193	. . . . . . . . . 10 |- (-. a e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) <-> (a e. A -> a e. {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}))
540	535, 539	syl6ibr 230	. . . . . . . . 9 |- (et -> (A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa -> -. a e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})))
541	540	con2d 107	. . . . . . . 8 |- (et -> (a e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -> -. A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa))
542	541	imp 377	. . . . . . 7 |- ((et /\ a e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})) -> -. A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa)
543	542	nrexdv 2193	. . . . . 6 |- (et -> -. E.a e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa)
544		fdc.1	. . . . . . . . . . 11 |- A e. _V
545		difexg 3458	. . . . . . . . . . 11 |- (A e. _V -> (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) e. _V)
546	544, 545	ax-mp 7	. . . . . . . . . 10 |- (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) e. _V
547		fri 3626	. . . . . . . . . 10 |- ((((A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) e. _V /\ R Fr A) /\ ((A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) C_ A /\ (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) =/= (/))) -> E.a e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa)
548	546, 547	mpanl1 770	. . . . . . . . 9 |- ((R Fr A /\ ((A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) C_ A /\ (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) =/= (/))) -> E.a e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa)
549	548	expr 418	. . . . . . . 8 |- ((R Fr A /\ (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) C_ A) -> ((A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) =/= (/) -> E.a e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa))
550		fdc.9	. . . . . . . 8 |- (et -> R Fr A)
551		difss 2735	. . . . . . . 8 |- (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) C_ A
552	549, 550, 551	sylancl 525	. . . . . . 7 |- (et -> ((A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) =/= (/) -> E.a e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa))
553		df-ne 2019	. . . . . . 7 |- ((A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) =/= (/) <-> -. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) = (/))
554	552, 553	syl5ibr 224	. . . . . 6 |- (et -> (-. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) = (/) -> E.a e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})A.d e. (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) -. dRa))
555	543, 554	mt3d 129	. . . . 5 |- (et -> (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) = (/))
556		ssdif0 2934	. . . . 5 |- (A C_ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)} <-> (A \ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)}) = (/))
557	555, 556	sylibr 217	. . . 4 |- (et -> A C_ {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})
558	86	a1i 8	. . . 4 |- (et -> {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)} C_ A)
559	557, 558	eqssd 2633	. . 3 |- (et -> A = {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)})
560		rabid2 2254	. . 3 |- (A = {c e. A | E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)} <-> A.c e. A E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch))
561	559, 560	sylib 215	. 2 |- (et -> A.c e. A E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch))
562		eqeq2 1893	. . . . . . 7 |- (c = C -> ((f` M) = c <-> (f` M) = C))
563	562	anbi1d 679	. . . . . 6 |- (c = C -> (((f` M) = c /\ ta) <-> ((f` M) = C /\ ta)))
564	563	3anbi2d 1173	. . . . 5 |- (c = C -> ((f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch) <-> (f:(M...n)-->A /\ ((f` M) = C /\ ta) /\ A.k e. (N...n)ch)))
565	564	exbidv 1657	. . . 4 |- (c = C -> (E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch) <-> E.f(f:(M...n)-->A /\ ((f` M) = C /\ ta) /\ A.k e. (N...n)ch)))
566	565	rexbidv 2124	. . 3 |- (c = C -> (E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch) <-> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = C /\ ta) /\ A.k e. (N...n)ch)))
567	566	rcla4va 2378	. 2 |- ((C e. A /\ A.c e. A E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = c /\ ta) /\ A.k e. (N...n)ch)) -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = C /\ ta) /\ A.k e. (N...n)ch))
568	1, 561, 567	syl11anc 524	1 |- (et -> E.n e. Z E.f(f:(M...n)-->A /\ ((f` M) = C /\ ta) /\ A.k e. (N...n)ch))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  [wsbc 1534   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   \ cdif 2590   C_ wss 2593  (/)c0 2875  ifcif 2982  {csn 3044  <.cop 3046   class class class wbr 3338  {copab 3395   Fr wfr 3623  -->wf 3994  ` cfv 3998  (class class class)co 4884  CCcc 6384  RRcr 6385  1c1 6387   + caddc 6389   - cmin 6445   <_ cle 6448  ZZcz 6451   < clt 6653  ZZ>=cuz 7586  ...cfz 7637

This theorem is referenced by:  fdc1 15813

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

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

Copyright terms: Public domain