Theorem fseq1cl 13619

Description: Closure of the partial values of the 1-based recursive sequence builder on a finite sequence. (Contributed by Paul Chapman, 22-Jun-2011.)

Assertion

Ref	Expression
fseq1cl	|- (((A e. B /\ S:(A X. A)-->A) /\ (N e. ZZ /\ F:(1...N)-->A /\ K e. (1...N))) -> ((S seq1 F)` K) e. A)

Proof of Theorem fseq1cl

Step	Hyp	Ref	Expression
1		oprex 4907	. . . . . . . . . . . . . 14 |- (1...N) e. _V
2		fex 4595	. . . . . . . . . . . . . 14 |- ((F:(1...N)-->A /\ (1...N) e. _V) -> F e. _V)
3	1, 2	mpan2 760	. . . . . . . . . . . . 13 |- (F:(1...N)-->A -> F e. _V)
4		fex 4595	. . . . . . . . . . . . . 14 |- ((S:(A X. A)-->A /\ (A X. A) e. _V) -> S e. _V)
5		xpexg 4095	. . . . . . . . . . . . . . 15 |- ((A e. B /\ A e. B) -> (A X. A) e. _V)
6	5	anidms 480	. . . . . . . . . . . . . 14 |- (A e. B -> (A X. A) e. _V)
7	4, 6	sylan2 500	. . . . . . . . . . . . 13 |- ((S:(A X. A)-->A /\ A e. B) -> S e. _V)
8	3, 7	anim12i 360	. . . . . . . . . . . 12 |- ((F:(1...N)-->A /\ (S:(A X. A)-->A /\ A e. B)) -> (F e. _V /\ S e. _V))
9	8	3impb 1063	. . . . . . . . . . 11 |- ((F:(1...N)-->A /\ S:(A X. A)-->A /\ A e. B) -> (F e. _V /\ S e. _V))
10	9	3comr 1076	. . . . . . . . . 10 |- ((A e. B /\ F:(1...N)-->A /\ S:(A X. A)-->A) -> (F e. _V /\ S e. _V))
11		1z 7368	. . . . . . . . . . . . . . . . . 18 |- 1 e. ZZ
12		elfz1 7640	. . . . . . . . . . . . . . . . . . 19 |- ((1 e. ZZ /\ N e. ZZ) -> (K e. (1...N) <-> (K e. ZZ /\ 1 <_ K /\ K <_ N)))
13		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . 23 |- (m = 1 -> ((s seq1 f)` m) = ((s seq1 f)` 1))
14	13	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . 22 |- (m = 1 -> (((s seq1 f)` m) e. A <-> ((s seq1 f)` 1) e. A))
15	14	imbi2d 674	. . . . . . . . . . . . . . . . . . . . 21 |- (m = 1 -> (((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` m) e. A) <-> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` 1) e. A)))
16		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . 23 |- (m = k -> ((s seq1 f)` m) = ((s seq1 f)` k))
17	16	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . 22 |- (m = k -> (((s seq1 f)` m) e. A <-> ((s seq1 f)` k) e. A))
18	17	imbi2d 674	. . . . . . . . . . . . . . . . . . . . 21 |- (m = k -> (((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` m) e. A) <-> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` k) e. A)))
19		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . 23 |- (m = (k + 1) -> ((s seq1 f)` m) = ((s seq1 f)` (k + 1)))
20	19	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . 22 |- (m = (k + 1) -> (((s seq1 f)` m) e. A <-> ((s seq1 f)` (k + 1)) e. A))
21	20	imbi2d 674	. . . . . . . . . . . . . . . . . . . . 21 |- (m = (k + 1) -> (((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` m) e. A) <-> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` (k + 1)) e. A)))
22		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . 23 |- (m = K -> ((s seq1 f)` m) = ((s seq1 f)` K))
23	22	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . 22 |- (m = K -> (((s seq1 f)` m) e. A <-> ((s seq1 f)` K) e. A))
24	23	imbi2d 674	. . . . . . . . . . . . . . . . . . . . 21 |- (m = K -> (((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` m) e. A) <-> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` K) e. A)))
25		elnnz1 7364	. . . . . . . . . . . . . . . . . . . . . . 23 |- (N e. NN <-> (N e. ZZ /\ 1 <_ N))
26		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f:(1...N)-->A /\ 1 e. (1...N)) -> (f` 1) e. A)
27		elnnuz 7609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (N e. NN <-> N e. (ZZ>=` 1))
28		eluzfz1 7657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (N e. (ZZ>=` 1) -> 1 e. (1...N))
29	27, 28	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (N e. NN -> 1 e. (1...N))
30	26, 29	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((f:(1...N)-->A /\ N e. NN) -> (f` 1) e. A)
31	30	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((N e. NN /\ f:(1...N)-->A) -> (f` 1) e. A)
32		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- s e. _V
33		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- f e. _V
34	32, 33	seq11 7730	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((s seq1 f)` 1) = (f` 1)
35	31, 34	syl5eqel 1975	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((N e. NN /\ f:(1...N)-->A) -> ((s seq1 f)` 1) e. A)
36	35	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((N e. NN /\ (f:(1...N)-->A /\ s:(A X. A)-->A)) -> ((s seq1 f)` 1) e. A)
37	36	ex 402	. . . . . . . . . . . . . . . . . . . . . . 23 |- (N e. NN -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` 1) e. A))
38	25, 37	sylbir 218	. . . . . . . . . . . . . . . . . . . . . 22 |- ((N e. ZZ /\ 1 <_ N) -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` 1) e. A))
39	38	3adant1 894	. . . . . . . . . . . . . . . . . . . . 21 |- ((1 e. ZZ /\ N e. ZZ /\ 1 <_ N) -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` 1) e. A))
40	32, 33	seq1p1 7731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (k e. NN -> ((s seq1 f)` (k + 1)) = (((s seq1 f)` k)s(f` (k + 1))))
41	40	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((k e. NN /\ (k < N /\ N e. ZZ)) -> ((s seq1 f)` (k + 1)) = (((s seq1 f)` k)s(f` (k + 1))))
42	41	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((f:(1...N)-->A /\ (k e. NN /\ (k < N /\ N e. ZZ))) -> ((s seq1 f)` (k + 1)) = (((s seq1 f)` k)s(f` (k + 1))))
43	42	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((s:(A X. A)-->A /\ (f:(1...N)-->A /\ (k e. NN /\ (k < N /\ N e. ZZ))) /\ ((s seq1 f)` k) e. A) -> ((s seq1 f)` (k + 1)) = (((s seq1 f)` k)s(f` (k + 1))))
44		foprrn 4965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((s:(A X. A)-->A /\ ((s seq1 f)` k) e. A /\ (f` (k + 1)) e. A) -> (((s seq1 f)` k)s(f` (k + 1))) e. A)
45	44	3com23 1074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((s:(A X. A)-->A /\ (f` (k + 1)) e. A /\ ((s seq1 f)` k) e. A) -> (((s seq1 f)` k)s(f` (k + 1))) e. A)
46		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((f:(1...N)-->A /\ (k + 1) e. (1...N)) -> (f` (k + 1)) e. A)
47		nnnn0 7315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (k e. NN -> k e. NN0)
48		elnn0z 7356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (k e. NN0 <-> (k e. ZZ /\ 0 <_ k))
49		elfz 7641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (((k + 1) e. ZZ /\ 1 e. ZZ /\ N e. ZZ) -> ((k + 1) e. (1...N) <-> (1 <_ (k + 1) /\ (k + 1) <_ N)))
50	11, 49	mp3an2 1179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (((k + 1) e. ZZ /\ N e. ZZ) -> ((k + 1) e. (1...N) <-> (1 <_ (k + 1) /\ (k + 1) <_ N)))
51		peano2z 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (k e. ZZ -> (k + 1) e. ZZ)
52	50, 51	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((k e. ZZ /\ N e. ZZ) -> ((k + 1) e. (1...N) <-> (1 <_ (k + 1) /\ (k + 1) <_ N)))
53		zre 7348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (k e. ZZ -> k e. RR)
54		1re 6598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- 1 e. RR
55		addge02 6862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ((1 e. RR /\ k e. RR) -> (0 <_ k <-> 1 <_ (k + 1)))
56	54, 55	mpan 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (k e. RR -> (0 <_ k <-> 1 <_ (k + 1)))
57	53, 56	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (k e. ZZ -> (0 <_ k <-> 1 <_ (k + 1)))
58	57	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((k e. ZZ /\ N e. ZZ) -> (0 <_ k <-> 1 <_ (k + 1)))
59		zltp1le 7390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((k e. ZZ /\ N e. ZZ) -> (k < N <-> (k + 1) <_ N))
60	58, 59	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((k e. ZZ /\ N e. ZZ) -> ((0 <_ k /\ k < N) <-> (1 <_ (k + 1) /\ (k + 1) <_ N)))
61	52, 60	bitr4d 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((k e. ZZ /\ N e. ZZ) -> ((k + 1) e. (1...N) <-> (0 <_ k /\ k < N)))
62	61	exbiri 421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (k e. ZZ -> (N e. ZZ -> ((0 <_ k /\ k < N) -> (k + 1) e. (1...N))))
63	62	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (k e. ZZ -> ((0 <_ k /\ k < N) -> (N e. ZZ -> (k + 1) e. (1...N))))
64	63	expdimp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((k e. ZZ /\ 0 <_ k) -> (k < N -> (N e. ZZ -> (k + 1) e. (1...N))))
65	48, 64	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (k e. NN0 -> (k < N -> (N e. ZZ -> (k + 1) e. (1...N))))
66	47, 65	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (k e. NN -> (k < N -> (N e. ZZ -> (k + 1) e. (1...N))))
67	66	imp32 390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((k e. NN /\ (k < N /\ N e. ZZ)) -> (k + 1) e. (1...N))
68	46, 67	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((f:(1...N)-->A /\ (k e. NN /\ (k < N /\ N e. ZZ))) -> (f` (k + 1)) e. A)
69	45, 68	syl3an2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((s:(A X. A)-->A /\ (f:(1...N)-->A /\ (k e. NN /\ (k < N /\ N e. ZZ))) /\ ((s seq1 f)` k) e. A) -> (((s seq1 f)` k)s(f` (k + 1))) e. A)
70	43, 69	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((s:(A X. A)-->A /\ (f:(1...N)-->A /\ (k e. NN /\ (k < N /\ N e. ZZ))) /\ ((s seq1 f)` k) e. A) -> ((s seq1 f)` (k + 1)) e. A)
71	70	3expia 1069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((s:(A X. A)-->A /\ (f:(1...N)-->A /\ (k e. NN /\ (k < N /\ N e. ZZ)))) -> (((s seq1 f)` k) e. A -> ((s seq1 f)` (k + 1)) e. A))
72	71	anassrs 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((s:(A X. A)-->A /\ f:(1...N)-->A) /\ (k e. NN /\ (k < N /\ N e. ZZ))) -> (((s seq1 f)` k) e. A -> ((s seq1 f)` (k + 1)) e. A))
73	72	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((k e. NN /\ (k < N /\ N e. ZZ)) -> ((s:(A X. A)-->A /\ f:(1...N)-->A) -> (((s seq1 f)` k) e. A -> ((s seq1 f)` (k + 1)) e. A)))
74	73	ancomsd 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((k e. NN /\ (k < N /\ N e. ZZ)) -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> (((s seq1 f)` k) e. A -> ((s seq1 f)` (k + 1)) e. A)))
75		elnnz1 7364	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (k e. NN <-> (k e. ZZ /\ 1 <_ k))
76	74, 75	sylanbr 499	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((k e. ZZ /\ 1 <_ k) /\ (k < N /\ N e. ZZ)) -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> (((s seq1 f)` k) e. A -> ((s seq1 f)` (k + 1)) e. A)))
77	76	anassrs 489	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((k e. ZZ /\ 1 <_ k) /\ k < N) /\ N e. ZZ) -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> (((s seq1 f)` k) e. A -> ((s seq1 f)` (k + 1)) e. A)))
78	77	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((k e. ZZ /\ 1 <_ k) /\ k < N) -> (N e. ZZ -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> (((s seq1 f)` k) e. A -> ((s seq1 f)` (k + 1)) e. A))))
79	78	3impa 1062	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((k e. ZZ /\ 1 <_ k /\ k < N) -> (N e. ZZ -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> (((s seq1 f)` k) e. A -> ((s seq1 f)` (k + 1)) e. A))))
80	79	impcom 378	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((N e. ZZ /\ (k e. ZZ /\ 1 <_ k /\ k < N)) -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> (((s seq1 f)` k) e. A -> ((s seq1 f)` (k + 1)) e. A)))
81	80	adantll 428	. . . . . . . . . . . . . . . . . . . . . 22 |- (((1 e. ZZ /\ N e. ZZ) /\ (k e. ZZ /\ 1 <_ k /\ k < N)) -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> (((s seq1 f)` k) e. A -> ((s seq1 f)` (k + 1)) e. A)))
82	81	a2d 16	. . . . . . . . . . . . . . . . . . . . 21 |- (((1 e. ZZ /\ N e. ZZ) /\ (k e. ZZ /\ 1 <_ k /\ k < N)) -> (((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` k) e. A) -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` (k + 1)) e. A)))
83	15, 18, 21, 24, 39, 82	fzind 13610	. . . . . . . . . . . . . . . . . . . 20 |- (((1 e. ZZ /\ N e. ZZ) /\ (K e. ZZ /\ 1 <_ K /\ K <_ N)) -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` K) e. A))
84	83	ex 402	. . . . . . . . . . . . . . . . . . 19 |- ((1 e. ZZ /\ N e. ZZ) -> ((K e. ZZ /\ 1 <_ K /\ K <_ N) -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` K) e. A)))
85	12, 84	sylbid 220	. . . . . . . . . . . . . . . . . 18 |- ((1 e. ZZ /\ N e. ZZ) -> (K e. (1...N) -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` K) e. A)))
86	11, 85	mpan 759	. . . . . . . . . . . . . . . . 17 |- (N e. ZZ -> (K e. (1...N) -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` K) e. A)))
87	86	imp 377	. . . . . . . . . . . . . . . 16 |- ((N e. ZZ /\ K e. (1...N)) -> ((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` K) e. A))
88	87	19.21aivv 1665	. . . . . . . . . . . . . . 15 |- ((N e. ZZ /\ K e. (1...N)) -> A.fA.s((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` K) e. A))
89		feq1 4551	. . . . . . . . . . . . . . . . . 18 |- (f = F -> (f:(1...N)-->A <-> F:(1...N)-->A))
90		feq1 4551	. . . . . . . . . . . . . . . . . 18 |- (s = S -> (s:(A X. A)-->A <-> S:(A X. A)-->A))
91	89, 90	bi2anan9 694	. . . . . . . . . . . . . . . . 17 |- ((f = F /\ s = S) -> ((f:(1...N)-->A /\ s:(A X. A)-->A) <-> (F:(1...N)-->A /\ S:(A X. A)-->A)))
92		opreq12 4891	. . . . . . . . . . . . . . . . . . . 20 |- ((s = S /\ f = F) -> (s seq1 f) = (S seq1 F))
93	92	ancoms 484	. . . . . . . . . . . . . . . . . . 19 |- ((f = F /\ s = S) -> (s seq1 f) = (S seq1 F))
94	93	fveq1d 4683	. . . . . . . . . . . . . . . . . 18 |- ((f = F /\ s = S) -> ((s seq1 f)` K) = ((S seq1 F)` K))
95	94	eleq1d 1963	. . . . . . . . . . . . . . . . 17 |- ((f = F /\ s = S) -> (((s seq1 f)` K) e. A <-> ((S seq1 F)` K) e. A))
96	91, 95	imbi12d 688	. . . . . . . . . . . . . . . 16 |- ((f = F /\ s = S) -> (((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` K) e. A) <-> ((F:(1...N)-->A /\ S:(A X. A)-->A) -> ((S seq1 F)` K) e. A)))
97	96	cla42gv 2367	. . . . . . . . . . . . . . 15 |- ((F e. _V /\ S e. _V) -> (A.fA.s((f:(1...N)-->A /\ s:(A X. A)-->A) -> ((s seq1 f)` K) e. A) -> ((F:(1...N)-->A /\ S:(A X. A)-->A) -> ((S seq1 F)` K) e. A)))
98	88, 97	mpan9 521	. . . . . . . . . . . . . 14 |- (((N e. ZZ /\ K e. (1...N)) /\ (F e. _V /\ S e. _V)) -> ((F:(1...N)-->A /\ S:(A X. A)-->A) -> ((S seq1 F)` K) e. A))
99	98	com12 14	. . . . . . . . . . . . 13 |- ((F:(1...N)-->A /\ S:(A X. A)-->A) -> (((N e. ZZ /\ K e. (1...N)) /\ (F e. _V /\ S e. _V)) -> ((S seq1 F)` K) e. A))
100	99	3adant1 894	. . . . . . . . . . . 12 |- ((A e. B /\ F:(1...N)-->A /\ S:(A X. A)-->A) -> (((N e. ZZ /\ K e. (1...N)) /\ (F e. _V /\ S e. _V)) -> ((S seq1 F)` K) e. A))
101	100	exp3a 405	. . . . . . . . . . 11 |- ((A e. B /\ F:(1...N)-->A /\ S:(A X. A)-->A) -> ((N e. ZZ /\ K e. (1...N)) -> ((F e. _V /\ S e. _V) -> ((S seq1 F)` K) e. A)))
102	101	com12 14	. . . . . . . . . 10 |- ((N e. ZZ /\ K e. (1...N)) -> ((A e. B /\ F:(1...N)-->A /\ S:(A X. A)-->A) -> ((F e. _V /\ S e. _V) -> ((S seq1 F)` K) e. A)))
103	10, 102	mpdi 59	. . . . . . . . 9 |- ((N e. ZZ /\ K e. (1...N)) -> ((A e. B /\ F:(1...N)-->A /\ S:(A X. A)-->A) -> ((S seq1 F)` K) e. A))
104	103	com12 14	. . . . . . . 8 |- ((A e. B /\ F:(1...N)-->A /\ S:(A X. A)-->A) -> ((N e. ZZ /\ K e. (1...N)) -> ((S seq1 F)` K) e. A))
105	104	3com23 1074	. . . . . . 7 |- ((A e. B /\ S:(A X. A)-->A /\ F:(1...N)-->A) -> ((N e. ZZ /\ K e. (1...N)) -> ((S seq1 F)` K) e. A))
106	105	3expia 1069	. . . . . 6 |- ((A e. B /\ S:(A X. A)-->A) -> (F:(1...N)-->A -> ((N e. ZZ /\ K e. (1...N)) -> ((S seq1 F)` K) e. A)))
107	106	imp3a 388	. . . . 5 |- ((A e. B /\ S:(A X. A)-->A) -> ((F:(1...N)-->A /\ (N e. ZZ /\ K e. (1...N))) -> ((S seq1 F)` K) e. A))
108	107	com12 14	. . . 4 |- ((F:(1...N)-->A /\ (N e. ZZ /\ K e. (1...N))) -> ((A e. B /\ S:(A X. A)-->A) -> ((S seq1 F)` K) e. A))
109	108	3impb 1063	. . 3 |- ((F:(1...N)-->A /\ N e. ZZ /\ K e. (1...N)) -> ((A e. B /\ S:(A X. A)-->A) -> ((S seq1 F)` K) e. A))
110	109	3com12 1071	. 2 |- ((N e. ZZ /\ F:(1...N)-->A /\ K e. (1...N)) -> ((A e. B /\ S:(A X. A)-->A) -> ((S seq1 F)` K) e. A))
111	110	impcom 378	1 |- (((A e. B /\ S:(A X. A)-->A) /\ (N e. ZZ /\ F:(1...N)-->A /\ K e. (1...N))) -> ((S seq1 F)` K) e. A)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  _Vcvv 2292   class class class wbr 3338   X. cxp 3984  -->wf 3994  ` cfv 3998  (class class class)co 4884  RRcr 6385  0cc0 6386  1c1 6387   + caddc 6389   <_ cle 6448  NNcn 6449  NN0cn0 6450  ZZcz 6451   < clt 6653  ZZ>=cuz 7586  ...cfz 7637   seq1 cseq1 7720

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  df-seq1 7721

Copyright terms: Public domain