Theorem pitonn 6744

Description: Mapping from N. to NN. (Contributed by Jim Kingdon, 22-Apr-2020.)

Assertion

Ref	Expression
pitonn	|- ( n e. N. -> <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. |^| {x | ( 1 e. x /\ A.y e. x (y + 1) e. x) })

Distinct variable group:   n, l,u,x,y

Proof of Theorem pitonn

Dummy variables k w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opeq1 3540	. . . . . . . . . . . . . . 15 |- (w = 1o -> <.w , 1o >. = <. 1o , 1o >.)
2	1	eceq1d 6078	. . . . . . . . . . . . . 14 |- (w = 1o -> [ <.w , 1o >.] ~Q = [ <. 1o , 1o >.] ~Q )
3	2	breq2d 3767	. . . . . . . . . . . . 13 |- (w = 1o -> ( l <Q [ <.w , 1o >.] ~Q <-> l <Q [ <. 1o , 1o >.] ~Q ))
4	3	abbidv 2152	. . . . . . . . . . . 12 |- (w = 1o -> { l | l <Q [ <.w , 1o >.] ~Q } = { l | l <Q [ <. 1o , 1o >.] ~Q })
5	2	breq1d 3765	. . . . . . . . . . . . 13 |- (w = 1o -> ([ <.w , 1o >.] ~Q <Q u <-> [ <. 1o , 1o >.] ~Q <Q u))
6	5	abbidv 2152	. . . . . . . . . . . 12 |- (w = 1o -> {u | [ <.w , 1o >.] ~Q <Q u } = {u | [ <. 1o , 1o >.] ~Q <Q u })
7	4, 6	opeq12d 3548	. . . . . . . . . . 11 |- (w = 1o -> <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. = <. { l | l <Q [ <. 1o , 1o >.] ~Q } , {u | [ <. 1o , 1o >.] ~Q <Q u } >.)
8	7	oveq1d 5470	. . . . . . . . . 10 |- (w = 1o -> ( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) = ( <. { l | l <Q [ <. 1o , 1o >.] ~Q } , {u | [ <. 1o , 1o >.] ~Q <Q u } >. +P. 1P))
9	8	opeq1d 3546	. . . . . . . . 9 |- (w = 1o -> <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >. = <.( <. { l | l <Q [ <. 1o , 1o >.] ~Q } , {u | [ <. 1o , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.)
10	9	eceq1d 6078	. . . . . . . 8 |- (w = 1o -> [ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R = [ <.( <. { l | l <Q [ <. 1o , 1o >.] ~Q } , {u | [ <. 1o , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R )
11	10	opeq1d 3546	. . . . . . 7 |- (w = 1o -> <.[ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. = <.[ <.( <. { l | l <Q [ <. 1o , 1o >.] ~Q } , {u | [ <. 1o , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >.)
12	11	eleq1d 2103	. . . . . 6 |- (w = 1o -> ( <.[ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z <-> <.[ <.( <. { l | l <Q [ <. 1o , 1o >.] ~Q } , {u | [ <. 1o , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z))
13	12	imbi2d 219	. . . . 5 |- (w = 1o -> ((( 1 e. z /\ A.y e. z (y + 1) e. z) -> <.[ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z) <-> (( 1 e. z /\ A.y e. z (y + 1) e. z) -> <.[ <.( <. { l | l <Q [ <. 1o , 1o >.] ~Q } , {u | [ <. 1o , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z)))
14		opeq1 3540	. . . . . . . . . . . . . . 15 |- (w = k -> <.w , 1o >. = <. k , 1o >.)
15	14	eceq1d 6078	. . . . . . . . . . . . . 14 |- (w = k -> [ <.w , 1o >.] ~Q = [ <. k , 1o >.] ~Q )
16	15	breq2d 3767	. . . . . . . . . . . . 13 |- (w = k -> ( l <Q [ <.w , 1o >.] ~Q <-> l <Q [ <. k , 1o >.] ~Q ))
17	16	abbidv 2152	. . . . . . . . . . . 12 |- (w = k -> { l | l <Q [ <.w , 1o >.] ~Q } = { l | l <Q [ <. k , 1o >.] ~Q })
18	15	breq1d 3765	. . . . . . . . . . . . 13 |- (w = k -> ([ <.w , 1o >.] ~Q <Q u <-> [ <. k , 1o >.] ~Q <Q u))
19	18	abbidv 2152	. . . . . . . . . . . 12 |- (w = k -> {u | [ <.w , 1o >.] ~Q <Q u } = {u | [ <. k , 1o >.] ~Q <Q u })
20	17, 19	opeq12d 3548	. . . . . . . . . . 11 |- (w = k -> <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. = <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >.)
21	20	oveq1d 5470	. . . . . . . . . 10 |- (w = k -> ( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) = ( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P))
22	21	opeq1d 3546	. . . . . . . . 9 |- (w = k -> <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >. = <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.)
23	22	eceq1d 6078	. . . . . . . 8 |- (w = k -> [ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R = [ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R )
24	23	opeq1d 3546	. . . . . . 7 |- (w = k -> <.[ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. = <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >.)
25	24	eleq1d 2103	. . . . . 6 |- (w = k -> ( <.[ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z <-> <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z))
26	25	imbi2d 219	. . . . 5 |- (w = k -> ((( 1 e. z /\ A.y e. z (y + 1) e. z) -> <.[ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z) <-> (( 1 e. z /\ A.y e. z (y + 1) e. z) -> <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z)))
27		opeq1 3540	. . . . . . . . . . . . . . 15 |- (w = ( k +N 1o) -> <.w , 1o >. = <.( k +N 1o) , 1o >.)
28	27	eceq1d 6078	. . . . . . . . . . . . . 14 |- (w = ( k +N 1o) -> [ <.w , 1o >.] ~Q = [ <.( k +N 1o) , 1o >.] ~Q )
29	28	breq2d 3767	. . . . . . . . . . . . 13 |- (w = ( k +N 1o) -> ( l <Q [ <.w , 1o >.] ~Q <-> l <Q [ <.( k +N 1o) , 1o >.] ~Q ))
30	29	abbidv 2152	. . . . . . . . . . . 12 |- (w = ( k +N 1o) -> { l | l <Q [ <.w , 1o >.] ~Q } = { l | l <Q [ <.( k +N 1o) , 1o >.] ~Q })
31	28	breq1d 3765	. . . . . . . . . . . . 13 |- (w = ( k +N 1o) -> ([ <.w , 1o >.] ~Q <Q u <-> [ <.( k +N 1o) , 1o >.] ~Q <Q u))
32	31	abbidv 2152	. . . . . . . . . . . 12 |- (w = ( k +N 1o) -> {u | [ <.w , 1o >.] ~Q <Q u } = {u | [ <.( k +N 1o) , 1o >.] ~Q <Q u })
33	30, 32	opeq12d 3548	. . . . . . . . . . 11 |- (w = ( k +N 1o) -> <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. = <. { l | l <Q [ <.( k +N 1o) , 1o >.] ~Q } , {u | [ <.( k +N 1o) , 1o >.] ~Q <Q u } >.)
34	33	oveq1d 5470	. . . . . . . . . 10 |- (w = ( k +N 1o) -> ( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) = ( <. { l | l <Q [ <.( k +N 1o) , 1o >.] ~Q } , {u | [ <.( k +N 1o) , 1o >.] ~Q <Q u } >. +P. 1P))
35	34	opeq1d 3546	. . . . . . . . 9 |- (w = ( k +N 1o) -> <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >. = <.( <. { l | l <Q [ <.( k +N 1o) , 1o >.] ~Q } , {u | [ <.( k +N 1o) , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.)
36	35	eceq1d 6078	. . . . . . . 8 |- (w = ( k +N 1o) -> [ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R = [ <.( <. { l | l <Q [ <.( k +N 1o) , 1o >.] ~Q } , {u | [ <.( k +N 1o) , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R )
37	36	opeq1d 3546	. . . . . . 7 |- (w = ( k +N 1o) -> <.[ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. = <.[ <.( <. { l | l <Q [ <.( k +N 1o) , 1o >.] ~Q } , {u | [ <.( k +N 1o) , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >.)
38	37	eleq1d 2103	. . . . . 6 |- (w = ( k +N 1o) -> ( <.[ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z <-> <.[ <.( <. { l | l <Q [ <.( k +N 1o) , 1o >.] ~Q } , {u | [ <.( k +N 1o) , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z))
39	38	imbi2d 219	. . . . 5 |- (w = ( k +N 1o) -> ((( 1 e. z /\ A.y e. z (y + 1) e. z) -> <.[ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z) <-> (( 1 e. z /\ A.y e. z (y + 1) e. z) -> <.[ <.( <. { l | l <Q [ <.( k +N 1o) , 1o >.] ~Q } , {u | [ <.( k +N 1o) , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z)))
40		opeq1 3540	. . . . . . . . . . . . . . 15 |- (w = n -> <.w , 1o >. = <. n , 1o >.)
41	40	eceq1d 6078	. . . . . . . . . . . . . 14 |- (w = n -> [ <.w , 1o >.] ~Q = [ <. n , 1o >.] ~Q )
42	41	breq2d 3767	. . . . . . . . . . . . 13 |- (w = n -> ( l <Q [ <.w , 1o >.] ~Q <-> l <Q [ <. n , 1o >.] ~Q ))
43	42	abbidv 2152	. . . . . . . . . . . 12 |- (w = n -> { l | l <Q [ <.w , 1o >.] ~Q } = { l | l <Q [ <. n , 1o >.] ~Q })
44	41	breq1d 3765	. . . . . . . . . . . . 13 |- (w = n -> ([ <.w , 1o >.] ~Q <Q u <-> [ <. n , 1o >.] ~Q <Q u))
45	44	abbidv 2152	. . . . . . . . . . . 12 |- (w = n -> {u | [ <.w , 1o >.] ~Q <Q u } = {u | [ <. n , 1o >.] ~Q <Q u })
46	43, 45	opeq12d 3548	. . . . . . . . . . 11 |- (w = n -> <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. = <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >.)
47	46	oveq1d 5470	. . . . . . . . . 10 |- (w = n -> ( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) = ( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P))
48	47	opeq1d 3546	. . . . . . . . 9 |- (w = n -> <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >. = <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.)
49	48	eceq1d 6078	. . . . . . . 8 |- (w = n -> [ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R = [ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R )
50	49	opeq1d 3546	. . . . . . 7 |- (w = n -> <.[ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. = <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >.)
51	50	eleq1d 2103	. . . . . 6 |- (w = n -> ( <.[ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z <-> <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z))
52	51	imbi2d 219	. . . . 5 |- (w = n -> ((( 1 e. z /\ A.y e. z (y + 1) e. z) -> <.[ <.( <. { l | l <Q [ <.w , 1o >.] ~Q } , {u | [ <.w , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z) <-> (( 1 e. z /\ A.y e. z (y + 1) e. z) -> <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z)))
53		pitonnlem1 6741	. . . . . . . 8 |- <.[ <.( <. { l | l <Q [ <. 1o , 1o >.] ~Q } , {u | [ <. 1o , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. = 1
54	53	eleq1i 2100	. . . . . . 7 |- ( <.[ <.( <. { l | l <Q [ <. 1o , 1o >.] ~Q } , {u | [ <. 1o , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z <-> 1 e. z)
55	54	biimpri 124	. . . . . 6 |- ( 1 e. z -> <.[ <.( <. { l | l <Q [ <. 1o , 1o >.] ~Q } , {u | [ <. 1o , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z)
56	55	adantr 261	. . . . 5 |- (( 1 e. z /\ A.y e. z (y + 1) e. z) -> <.[ <.( <. { l | l <Q [ <. 1o , 1o >.] ~Q } , {u | [ <. 1o , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z)
57		oveq1 5462	. . . . . . . . . . 11 |- (y = <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. -> (y + 1) = ( <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. + 1))
58	57	eleq1d 2103	. . . . . . . . . 10 |- (y = <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. -> ((y + 1) e. z <-> ( <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. + 1) e. z))
59	58	rspccv 2647	. . . . . . . . 9 |- (A.y e. z (y + 1) e. z -> ( <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z -> ( <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. + 1) e. z))
60	59	ad2antll 460	. . . . . . . 8 |- (( k e. N. /\ ( 1 e. z /\ A.y e. z (y + 1) e. z)) -> ( <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z -> ( <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. + 1) e. z))
61		pitonnlem2 6743	. . . . . . . . . 10 |- ( k e. N. -> ( <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. + 1) = <.[ <.( <. { l | l <Q [ <.( k +N 1o) , 1o >.] ~Q } , {u | [ <.( k +N 1o) , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >.)
62	61	eleq1d 2103	. . . . . . . . 9 |- ( k e. N. -> (( <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. + 1) e. z <-> <.[ <.( <. { l | l <Q [ <.( k +N 1o) , 1o >.] ~Q } , {u | [ <.( k +N 1o) , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z))
63	62	adantr 261	. . . . . . . 8 |- (( k e. N. /\ ( 1 e. z /\ A.y e. z (y + 1) e. z)) -> (( <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. + 1) e. z <-> <.[ <.( <. { l | l <Q [ <.( k +N 1o) , 1o >.] ~Q } , {u | [ <.( k +N 1o) , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z))
64	60, 63	sylibd 138	. . . . . . 7 |- (( k e. N. /\ ( 1 e. z /\ A.y e. z (y + 1) e. z)) -> ( <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z -> <.[ <.( <. { l | l <Q [ <.( k +N 1o) , 1o >.] ~Q } , {u | [ <.( k +N 1o) , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z))
65	64	ex 108	. . . . . 6 |- ( k e. N. -> (( 1 e. z /\ A.y e. z (y + 1) e. z) -> ( <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z -> <.[ <.( <. { l | l <Q [ <.( k +N 1o) , 1o >.] ~Q } , {u | [ <.( k +N 1o) , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z)))
66	65	a2d 23	. . . . 5 |- ( k e. N. -> ((( 1 e. z /\ A.y e. z (y + 1) e. z) -> <.[ <.( <. { l | l <Q [ <. k , 1o >.] ~Q } , {u | [ <. k , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z) -> (( 1 e. z /\ A.y e. z (y + 1) e. z) -> <.[ <.( <. { l | l <Q [ <.( k +N 1o) , 1o >.] ~Q } , {u | [ <.( k +N 1o) , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z)))
67	13, 26, 39, 52, 56, 66	indpi 6326	. . . 4 |- ( n e. N. -> (( 1 e. z /\ A.y e. z (y + 1) e. z) -> <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z))
68	67	alrimiv 1751	. . 3 |- ( n e. N. -> A.z(( 1 e. z /\ A.y e. z (y + 1) e. z) -> <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z))
69		eleq2 2098	. . . . 5 |- (x = z -> ( 1 e. x <-> 1 e. z))
70		eleq2 2098	. . . . . 6 |- (x = z -> ((y + 1) e. x <-> (y + 1) e. z))
71	70	raleqbi1dv 2507	. . . . 5 |- (x = z -> (A.y e. x (y + 1) e. x <-> A.y e. z (y + 1) e. z))
72	69, 71	anbi12d 442	. . . 4 |- (x = z -> (( 1 e. x /\ A.y e. x (y + 1) e. x) <-> ( 1 e. z /\ A.y e. z (y + 1) e. z)))
73	72	ralab 2695	. . 3 |- (A.z e. {x | ( 1 e. x /\ A.y e. x (y + 1) e. x) } <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z <-> A.z(( 1 e. z /\ A.y e. z (y + 1) e. z) -> <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z))
74	68, 73	sylibr 137	. 2 |- ( n e. N. -> A.z e. {x | ( 1 e. x /\ A.y e. x (y + 1) e. x) } <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z)
75		nnprlu 6534	. . . . . . 7 |- ( n e. N. -> <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. e. P.)
76		1pr 6535	. . . . . . 7 |- 1P e. P.
77		addclpr 6520	. . . . . . 7 |- (( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. e. P. /\ 1P e. P.) -> ( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) e. P.)
78	75, 76, 77	sylancl 392	. . . . . 6 |- ( n e. N. -> ( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) e. P.)
79		opelxpi 4319	. . . . . 6 |- ((( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) e. P. /\ 1P e. P.) -> <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >. e. ( P. X. P.))
80	78, 76, 79	sylancl 392	. . . . 5 |- ( n e. N. -> <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >. e. ( P. X. P.))
81		enrex 6665	. . . . . 6 |- ~R e. _V
82	81	ecelqsi 6096	. . . . 5 |- ( <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >. e. ( P. X. P.) -> [ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R e. (( P. X. P.) /. ~R ))
83	80, 82	syl 14	. . . 4 |- ( n e. N. -> [ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R e. (( P. X. P.) /. ~R ))
84		0r 6678	. . . 4 |- 0R e. R.
85		opelxpi 4319	. . . 4 |- (([ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R e. (( P. X. P.) /. ~R ) /\ 0R e. R.) -> <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. ((( P. X. P.) /. ~R ) X. R.))
86	83, 84, 85	sylancl 392	. . 3 |- ( n e. N. -> <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. ((( P. X. P.) /. ~R ) X. R.))
87		elintg 3614	. . 3 |- ( <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. ((( P. X. P.) /. ~R ) X. R.) -> ( <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. |^| {x | ( 1 e. x /\ A.y e. x (y + 1) e. x) } <-> A.z e. {x | ( 1 e. x /\ A.y e. x (y + 1) e. x) } <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z))
88	86, 87	syl 14	. 2 |- ( n e. N. -> ( <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. |^| {x | ( 1 e. x /\ A.y e. x (y + 1) e. x) } <-> A.z e. {x | ( 1 e. x /\ A.y e. x (y + 1) e. x) } <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. z))
89	74, 88	mpbird 156	1 |- ( n e. N. -> <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. |^| {x | ( 1 e. x /\ A.y e. x (y + 1) e. x) })

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98  A.wal 1240   = wceq 1242   e. wcel 1390   {cab 2023  A.wral 2300   <.cop 3370   |^|cint 3606   class class class wbr 3755   X. cxp 4286  (class class class)co 5455   1oc1o 5933  [cec 6040   /.cqs 6041   N.cnpi 6256   +N cpli 6257   ~Q ceq 6263   <Q cltq 6269   P.cnp 6275   1Pc1p 6276   +P. cpp 6277   ~R cer 6280   R.cnr 6281   0Rc0r 6282   1c1 6712   + caddc 6714

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254

This theorem depends on definitions:  df-bi 110  df-dc 742  df-3or 885  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-eprel 4017  df-id 4021  df-po 4024  df-iso 4025  df-iord 4069  df-on 4071  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-recs 5861  df-irdg 5897  df-1o 5940  df-2o 5941  df-oadd 5944  df-omul 5945  df-er 6042  df-ec 6044  df-qs 6048  df-ni 6288  df-pli 6289  df-mi 6290  df-lti 6291  df-plpq 6328  df-mpq 6329  df-enq 6331  df-nqqs 6332  df-plqqs 6333  df-mqqs 6334  df-1nqqs 6335  df-rq 6336  df-ltnqqs 6337  df-enq0 6407  df-nq0 6408  df-0nq0 6409  df-plq0 6410  df-mq0 6411  df-inp 6449  df-i1p 6450  df-iplp 6451  df-enr 6654  df-nr 6655  df-plr 6656  df-0r 6659  df-1r 6660  df-c 6717  df-1 6719  df-add 6722

This theorem is referenced by:  axarch  6773