Theorem fvmptnn04if 19110

Description: The function values of a mapping from the nonnegative integers with four distinct cases. (Contributed by AV, 10-Nov-2019.)

Hypotheses

Ref	Expression
fvmptnn04if.g	|- G = ( n e. NN0 |-> if ( n = 0 , A , if ( n = S , C , if ( S < n , D , B ) ) ) )
fvmptnn04if.s	|- ( ph -> S e. NN )
fvmptnn04if.n	|- ( ph -> N e. NN0 )
fvmptnn04if.y	|- ( ph -> Y e. V )
fvmptnn04if.a	|- ( ( ph /\ N = 0 ) -> Y = [_ N / n ]_ A )
fvmptnn04if.b	|- ( ( ph /\ 0 < N /\ N < S ) -> Y = [_ N / n ]_ B )
fvmptnn04if.c	|- ( ( ph /\ N = S ) -> Y = [_ N / n ]_ C )
fvmptnn04if.d	|- ( ( ph /\ S < N ) -> Y = [_ N / n ]_ D )

Assertion

Ref	Expression
fvmptnn04if	|- ( ph -> ( G ` N ) = Y )

Distinct variable groups:   n, N   S, n

Allowed substitution hints:   ph( n)   A( n)   B( n)   C( n)   D( n)   G( n)   V( n)   Y( n)

Proof of Theorem fvmptnn04if

Step	Hyp	Ref	Expression
1		fvmptnn04if.n	. . . 4 |- ( ph -> N e. NN0 )
2		fvmptnn04if.a	. . . . . . 7 |- ( ( ph /\ N = 0 ) -> Y = [_ N / n ]_ A )
3		fvmptnn04if.y	. . . . . . . . . . 11 |- ( ph -> Y e. V )
4	3	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ N = 0 ) -> Y e. V )
5	4	adantl 466	. . . . . . . . 9 |- ( ( Y = [_ N / n ]_ A /\ ( ph /\ N = 0 ) ) -> Y e. V )
6		simpl 457	. . . . . . . . . . 11 |- ( ( Y = [_ N / n ]_ A /\ ( ph /\ N = 0 ) ) -> Y = [_ N / n ]_ A )
7	6	eqcomd 2468	. . . . . . . . . 10 |- ( ( Y = [_ N / n ]_ A /\ ( ph /\ N = 0 ) ) -> [_ N / n ]_ A = Y )
8	7	eleq1d 2529	. . . . . . . . 9 |- ( ( Y = [_ N / n ]_ A /\ ( ph /\ N = 0 ) ) -> ( [_ N / n ]_ A e. V <-> Y e. V ) )
9	5, 8	mpbird 232	. . . . . . . 8 |- ( ( Y = [_ N / n ]_ A /\ ( ph /\ N = 0 ) ) -> [_ N / n ]_ A e. V )
10	9	ex 434	. . . . . . 7 |- ( Y = [_ N / n ]_ A -> ( ( ph /\ N = 0 ) -> [_ N / n ]_ A e. V ) )
11	2, 10	mpcom 36	. . . . . 6 |- ( ( ph /\ N = 0 ) -> [_ N / n ]_ A e. V )
12	3	ad2antrr 725	. . . . . . . 8 |- ( ( ( ph /\ -. N = 0 ) /\ N = S ) -> Y e. V )
13		fvmptnn04if.c	. . . . . . . . . . . . 13 |- ( ( ph /\ N = S ) -> Y = [_ N / n ]_ C )
14	13	eqcomd 2468	. . . . . . . . . . . 12 |- ( ( ph /\ N = S ) -> [_ N / n ]_ C = Y )
15	14	ex 434	. . . . . . . . . . 11 |- ( ph -> ( N = S -> [_ N / n ]_ C = Y ) )
16	15	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ -. N = 0 ) -> ( N = S -> [_ N / n ]_ C = Y ) )
17	16	imp 429	. . . . . . . . 9 |- ( ( ( ph /\ -. N = 0 ) /\ N = S ) -> [_ N / n ]_ C = Y )
18	17	eleq1d 2529	. . . . . . . 8 |- ( ( ( ph /\ -. N = 0 ) /\ N = S ) -> ( [_ N / n ]_ C e. V <-> Y e. V ) )
19	12, 18	mpbird 232	. . . . . . 7 |- ( ( ( ph /\ -. N = 0 ) /\ N = S ) -> [_ N / n ]_ C e. V )
20	3	ad3antrrr 729	. . . . . . . . 9 |- ( ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ S < N ) -> Y e. V )
21		fvmptnn04if.d	. . . . . . . . . . . . . . 15 |- ( ( ph /\ S < N ) -> Y = [_ N / n ]_ D )
22	21	eqcomd 2468	. . . . . . . . . . . . . 14 |- ( ( ph /\ S < N ) -> [_ N / n ]_ D = Y )
23	22	ex 434	. . . . . . . . . . . . 13 |- ( ph -> ( S < N -> [_ N / n ]_ D = Y ) )
24	23	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ -. N = 0 ) -> ( S < N -> [_ N / n ]_ D = Y ) )
25	24	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) -> ( S < N -> [_ N / n ]_ D = Y ) )
26	25	imp 429	. . . . . . . . . 10 |- ( ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ S < N ) -> [_ N / n ]_ D = Y )
27	26	eleq1d 2529	. . . . . . . . 9 |- ( ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ S < N ) -> ( [_ N / n ]_ D e. V <-> Y e. V ) )
28	20, 27	mpbird 232	. . . . . . . 8 |- ( ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ S < N ) -> [_ N / n ]_ D e. V )
29	3	ad3antrrr 729	. . . . . . . . 9 |- ( ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ -. S < N ) -> Y e. V )
30		simplll 757	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ -. S < N ) -> ph )
31		df-ne 2657	. . . . . . . . . . . . . . . 16 |- ( N =/= 0 <-> -. N = 0 )
32		elnnne0 10798	. . . . . . . . . . . . . . . . . 18 |- ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )
33		nngt0 10554	. . . . . . . . . . . . . . . . . 18 |- ( N e. NN -> 0 < N )
34	32, 33	sylbir 213	. . . . . . . . . . . . . . . . 17 |- ( ( N e. NN0 /\ N =/= 0 ) -> 0 < N )
35	34	expcom 435	. . . . . . . . . . . . . . . 16 |- ( N =/= 0 -> ( N e. NN0 -> 0 < N ) )
36	31, 35	sylbir 213	. . . . . . . . . . . . . . 15 |- ( -. N = 0 -> ( N e. NN0 -> 0 < N ) )
37	36	adantr 465	. . . . . . . . . . . . . 14 |- ( ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) -> ( N e. NN0 -> 0 < N ) )
38	1, 37	mpan9 469	. . . . . . . . . . . . 13 |- ( ( ph /\ ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) ) -> 0 < N )
39		ancom 450	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) ) <-> ( ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) /\ ph ) )
40		anass 649	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( -. N = 0 /\ -. N = S ) /\ -. S < N ) <-> ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) )
41	40	bicomi 202	. . . . . . . . . . . . . . . . . . 19 |- ( ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) <-> ( ( -. N = 0 /\ -. N = S ) /\ -. S < N ) )
42	41	anbi1i 695	. . . . . . . . . . . . . . . . . 18 |- ( ( ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) /\ ph ) <-> ( ( ( -. N = 0 /\ -. N = S ) /\ -. S < N ) /\ ph ) )
43		anass 649	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( -. N = 0 /\ -. N = S ) /\ -. S < N ) /\ ph ) <-> ( ( -. N = 0 /\ -. N = S ) /\ ( -. S < N /\ ph ) ) )
44	42, 43	bitri 249	. . . . . . . . . . . . . . . . 17 |- ( ( ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) /\ ph ) <-> ( ( -. N = 0 /\ -. N = S ) /\ ( -. S < N /\ ph ) ) )
45	39, 44	bitri 249	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) ) <-> ( ( -. N = 0 /\ -. N = S ) /\ ( -. S < N /\ ph ) ) )
46		ancom 450	. . . . . . . . . . . . . . . . . 18 |- ( ( -. S < N /\ ph ) <-> ( ph /\ -. S < N ) )
47	46	anbi2i 694	. . . . . . . . . . . . . . . . 17 |- ( ( ( -. N = 0 /\ -. N = S ) /\ ( -. S < N /\ ph ) ) <-> ( ( -. N = 0 /\ -. N = S ) /\ ( ph /\ -. S < N ) ) )
48		anass 649	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( -. N = 0 /\ -. N = S ) /\ ph ) /\ -. S < N ) <-> ( ( -. N = 0 /\ -. N = S ) /\ ( ph /\ -. S < N ) ) )
49	48	bicomi 202	. . . . . . . . . . . . . . . . 17 |- ( ( ( -. N = 0 /\ -. N = S ) /\ ( ph /\ -. S < N ) ) <-> ( ( ( -. N = 0 /\ -. N = S ) /\ ph ) /\ -. S < N ) )
50	47, 49	bitri 249	. . . . . . . . . . . . . . . 16 |- ( ( ( -. N = 0 /\ -. N = S ) /\ ( -. S < N /\ ph ) ) <-> ( ( ( -. N = 0 /\ -. N = S ) /\ ph ) /\ -. S < N ) )
51	45, 50	bitri 249	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) ) <-> ( ( ( -. N = 0 /\ -. N = S ) /\ ph ) /\ -. S < N ) )
52		anass 649	. . . . . . . . . . . . . . . . . 18 |- ( ( ( -. N = 0 /\ -. N = S ) /\ ph ) <-> ( -. N = 0 /\ ( -. N = S /\ ph ) ) )
53		ancom 450	. . . . . . . . . . . . . . . . . . . 20 |- ( ( -. N = S /\ ph ) <-> ( ph /\ -. N = S ) )
54	53	anbi2i 694	. . . . . . . . . . . . . . . . . . 19 |- ( ( -. N = 0 /\ ( -. N = S /\ ph ) ) <-> ( -. N = 0 /\ ( ph /\ -. N = S ) ) )
55		anass 649	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( -. N = 0 /\ ph ) /\ -. N = S ) <-> ( -. N = 0 /\ ( ph /\ -. N = S ) ) )
56	55	bicomi 202	. . . . . . . . . . . . . . . . . . 19 |- ( ( -. N = 0 /\ ( ph /\ -. N = S ) ) <-> ( ( -. N = 0 /\ ph ) /\ -. N = S ) )
57	54, 56	bitri 249	. . . . . . . . . . . . . . . . . 18 |- ( ( -. N = 0 /\ ( -. N = S /\ ph ) ) <-> ( ( -. N = 0 /\ ph ) /\ -. N = S ) )
58	52, 57	bitri 249	. . . . . . . . . . . . . . . . 17 |- ( ( ( -. N = 0 /\ -. N = S ) /\ ph ) <-> ( ( -. N = 0 /\ ph ) /\ -. N = S ) )
59		ancom 450	. . . . . . . . . . . . . . . . . 18 |- ( ( -. N = 0 /\ ph ) <-> ( ph /\ -. N = 0 ) )
60	59	anbi1i 695	. . . . . . . . . . . . . . . . 17 |- ( ( ( -. N = 0 /\ ph ) /\ -. N = S ) <-> ( ( ph /\ -. N = 0 ) /\ -. N = S ) )
61	58, 60	bitri 249	. . . . . . . . . . . . . . . 16 |- ( ( ( -. N = 0 /\ -. N = S ) /\ ph ) <-> ( ( ph /\ -. N = 0 ) /\ -. N = S ) )
62	61	anbi1i 695	. . . . . . . . . . . . . . 15 |- ( ( ( ( -. N = 0 /\ -. N = S ) /\ ph ) /\ -. S < N ) <-> ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ -. S < N ) )
63	51, 62	bitri 249	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) ) <-> ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ -. S < N ) )
64	63	imbi1i 325	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) ) -> 0 < N ) <-> ( ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ -. S < N ) -> 0 < N ) )
65	38, 64	mpbi 208	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ -. S < N ) -> 0 < N )
66	1	nn0red 10842	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. RR )
67		fvmptnn04if.s	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> S e. NN )
68	67	nnred 10540	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> S e. RR )
69	66, 68	lenltd 9719	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( N <_ S <-> -. S < N ) )
70	69	biimprd 223	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( -. S < N -> N <_ S ) )
71	70	adantld 467	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( -. N = S /\ -. S < N ) -> N <_ S ) )
72	71	adantld 467	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) -> N <_ S ) )
73	72	imp 429	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) ) -> N <_ S )
74		nesym 2732	. . . . . . . . . . . . . . . . . 18 |- ( S =/= N <-> -. N = S )
75	74	biimpri 206	. . . . . . . . . . . . . . . . 17 |- ( -. N = S -> S =/= N )
76	75	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( -. N = S /\ -. S < N ) -> S =/= N )
77	76	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) -> S =/= N )
78	77	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) ) -> S =/= N )
79	66	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) ) -> N e. RR )
80	68	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) ) -> S e. RR )
81	79, 80	ltlend 9718	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) ) -> ( N < S <-> ( N <_ S /\ S =/= N ) ) )
82	73, 78, 81	mpbir2and 915	. . . . . . . . . . . . 13 |- ( ( ph /\ ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) ) -> N < S )
83	63	imbi1i 325	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( -. N = 0 /\ ( -. N = S /\ -. S < N ) ) ) -> N < S ) <-> ( ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ -. S < N ) -> N < S ) )
84	82, 83	mpbi 208	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ -. S < N ) -> N < S )
85	30, 65, 84	3jca 1171	. . . . . . . . . . 11 |- ( ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ -. S < N ) -> ( ph /\ 0 < N /\ N < S ) )
86		fvmptnn04if.b	. . . . . . . . . . . 12 |- ( ( ph /\ 0 < N /\ N < S ) -> Y = [_ N / n ]_ B )
87	86	eqcomd 2468	. . . . . . . . . . 11 |- ( ( ph /\ 0 < N /\ N < S ) -> [_ N / n ]_ B = Y )
88	85, 87	syl 16	. . . . . . . . . 10 |- ( ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ -. S < N ) -> [_ N / n ]_ B = Y )
89	88	eleq1d 2529	. . . . . . . . 9 |- ( ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ -. S < N ) -> ( [_ N / n ]_ B e. V <-> Y e. V ) )
90	29, 89	mpbird 232	. . . . . . . 8 |- ( ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) /\ -. S < N ) -> [_ N / n ]_ B e. V )
91	28, 90	ifclda 3964	. . . . . . 7 |- ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) -> if ( S < N , [_ N / n ]_ D , [_ N / n ]_ B ) e. V )
92	19, 91	ifclda 3964	. . . . . 6 |- ( ( ph /\ -. N = 0 ) -> if ( N = S , [_ N / n ]_ C , if ( S < N , [_ N / n ]_ D , [_ N / n ]_ B ) ) e. V )
93	11, 92	ifclda 3964	. . . . 5 |- ( ph -> if ( N = 0 , [_ N / n ]_ A , if ( N = S , [_ N / n ]_ C , if ( S < N , [_ N / n ]_ D , [_ N / n ]_ B ) ) ) e. V )
94		csbif 3982	. . . . . . . 8 |- [_ N / n ]_ if ( n = 0 , A , if ( n = S , C , if ( S < n , D , B ) ) ) = if ( [. N / n ]. n = 0 , [_ N / n ]_ A , [_ N / n ]_ if ( n = S , C , if ( S < n , D , B ) ) )
95	94	a1i 11	. . . . . . 7 |- ( ph -> [_ N / n ]_ if ( n = 0 , A , if ( n = S , C , if ( S < n , D , B ) ) ) = if ( [. N / n ]. n = 0 , [_ N / n ]_ A , [_ N / n ]_ if ( n = S , C , if ( S < n , D , B ) ) ) )
96		eqsbc3 3364	. . . . . . . . 9 |- ( N e. NN0 -> ( [. N / n ]. n = 0 <-> N = 0 ) )
97	1, 96	syl 16	. . . . . . . 8 |- ( ph -> ( [. N / n ]. n = 0 <-> N = 0 ) )
98		eqidd 2461	. . . . . . . 8 |- ( ph -> [_ N / n ]_ A = [_ N / n ]_ A )
99		csbif 3982	. . . . . . . . . 10 |- [_ N / n ]_ if ( n = S , C , if ( S < n , D , B ) ) = if ( [. N / n ]. n = S , [_ N / n ]_ C , [_ N / n ]_ if ( S < n , D , B ) )
100	99	a1i 11	. . . . . . . . 9 |- ( ph -> [_ N / n ]_ if ( n = S , C , if ( S < n , D , B ) ) = if ( [. N / n ]. n = S , [_ N / n ]_ C , [_ N / n ]_ if ( S < n , D , B ) ) )
101		eqsbc3 3364	. . . . . . . . . . 11 |- ( N e. NN0 -> ( [. N / n ]. n = S <-> N = S ) )
102	1, 101	syl 16	. . . . . . . . . 10 |- ( ph -> ( [. N / n ]. n = S <-> N = S ) )
103		eqidd 2461	. . . . . . . . . 10 |- ( ph -> [_ N / n ]_ C = [_ N / n ]_ C )
104		csbif 3982	. . . . . . . . . . . 12 |- [_ N / n ]_ if ( S < n , D , B ) = if ( [. N / n ]. S < n , [_ N / n ]_ D , [_ N / n ]_ B )
105	104	a1i 11	. . . . . . . . . . 11 |- ( ph -> [_ N / n ]_ if ( S < n , D , B ) = if ( [. N / n ]. S < n , [_ N / n ]_ D , [_ N / n ]_ B ) )
106		sbcbr2g 4496	. . . . . . . . . . . . . 14 |- ( N e. NN0 -> ( [. N / n ]. S < n <-> S < [_ N / n ]_ n ) )
107	1, 106	syl 16	. . . . . . . . . . . . 13 |- ( ph -> ( [. N / n ]. S < n <-> S < [_ N / n ]_ n ) )
108		csbvarg 3841	. . . . . . . . . . . . . . 15 |- ( N e. NN0 -> [_ N / n ]_ n = N )
109	1, 108	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> [_ N / n ]_ n = N )
110	109	breq2d 4452	. . . . . . . . . . . . 13 |- ( ph -> ( S < [_ N / n ]_ n <-> S < N ) )
111	107, 110	bitrd 253	. . . . . . . . . . . 12 |- ( ph -> ( [. N / n ]. S < n <-> S < N ) )
112	111	ifbid 3954	. . . . . . . . . . 11 |- ( ph -> if ( [. N / n ]. S < n , [_ N / n ]_ D , [_ N / n ]_ B ) = if ( S < N , [_ N / n ]_ D , [_ N / n ]_ B ) )
113	105, 112	eqtrd 2501	. . . . . . . . . 10 |- ( ph -> [_ N / n ]_ if ( S < n , D , B ) = if ( S < N , [_ N / n ]_ D , [_ N / n ]_ B ) )
114	102, 103, 113	ifbieq12d 3959	. . . . . . . . 9 |- ( ph -> if ( [. N / n ]. n = S , [_ N / n ]_ C , [_ N / n ]_ if ( S < n , D , B ) ) = if ( N = S , [_ N / n ]_ C , if ( S < N , [_ N / n ]_ D , [_ N / n ]_ B ) ) )
115	100, 114	eqtrd 2501	. . . . . . . 8 |- ( ph -> [_ N / n ]_ if ( n = S , C , if ( S < n , D , B ) ) = if ( N = S , [_ N / n ]_ C , if ( S < N , [_ N / n ]_ D , [_ N / n ]_ B ) ) )
116	97, 98, 115	ifbieq12d 3959	. . . . . . 7 |- ( ph -> if ( [. N / n ]. n = 0 , [_ N / n ]_ A , [_ N / n ]_ if ( n = S , C , if ( S < n , D , B ) ) ) = if ( N = 0 , [_ N / n ]_ A , if ( N = S , [_ N / n ]_ C , if ( S < N , [_ N / n ]_ D , [_ N / n ]_ B ) ) ) )
117	95, 116	eqtrd 2501	. . . . . 6 |- ( ph -> [_ N / n ]_ if ( n = 0 , A , if ( n = S , C , if ( S < n , D , B ) ) ) = if ( N = 0 , [_ N / n ]_ A , if ( N = S , [_ N / n ]_ C , if ( S < N , [_ N / n ]_ D , [_ N / n ]_ B ) ) ) )
118	117	eleq1d 2529	. . . . 5 |- ( ph -> ( [_ N / n ]_ if ( n = 0 , A , if ( n = S , C , if ( S < n , D , B ) ) ) e. V <-> if ( N = 0 , [_ N / n ]_ A , if ( N = S , [_ N / n ]_ C , if ( S < N , [_ N / n ]_ D , [_ N / n ]_ B ) ) ) e. V ) )
119	93, 118	mpbird 232	. . . 4 |- ( ph -> [_ N / n ]_ if ( n = 0 , A , if ( n = S , C , if ( S < n , D , B ) ) ) e. V )
120	1, 119	jca 532	. . 3 |- ( ph -> ( N e. NN0 /\ [_ N / n ]_ if ( n = 0 , A , if ( n = S , C , if ( S < n , D , B ) ) ) e. V ) )
121		fvmptnn04if.g	. . . 4 |- G = ( n e. NN0 |-> if ( n = 0 , A , if ( n = S , C , if ( S < n , D , B ) ) ) )
122	121	fvmpts 5943	. . 3 |- ( ( N e. NN0 /\ [_ N / n ]_ if ( n = 0 , A , if ( n = S , C , if ( S < n , D , B ) ) ) e. V ) -> ( G ` N ) = [_ N / n ]_ if ( n = 0 , A , if ( n = S , C , if ( S < n , D , B ) ) ) )
123	120, 122	syl 16	. 2 |- ( ph -> ( G ` N ) = [_ N / n ]_ if ( n = 0 , A , if ( n = S , C , if ( S < n , D , B ) ) ) )
124		eqcom 2469	. . . . . 6 |- ( Y = [_ N / n ]_ A <-> [_ N / n ]_ A = Y )
125	124	imbi2i 312	. . . . 5 |- ( ( ( ph /\ N = 0 ) -> Y = [_ N / n ]_ A ) <-> ( ( ph /\ N = 0 ) -> [_ N / n ]_ A = Y ) )
126	2, 125	mpbi 208	. . . 4 |- ( ( ph /\ N = 0 ) -> [_ N / n ]_ A = Y )
127	26, 88	ifeqda 3965	. . . . 5 |- ( ( ( ph /\ -. N = 0 ) /\ -. N = S ) -> if ( S < N , [_ N / n ]_ D , [_ N / n ]_ B ) = Y )
128	17, 127	ifeqda 3965	. . . 4 |- ( ( ph /\ -. N = 0 ) -> if ( N = S , [_ N / n ]_ C , if ( S < N , [_ N / n ]_ D , [_ N / n ]_ B ) ) = Y )
129	126, 128	ifeqda 3965	. . 3 |- ( ph -> if ( N = 0 , [_ N / n ]_ A , if ( N = S , [_ N / n ]_ C , if ( S < N , [_ N / n ]_ D , [_ N / n ]_ B ) ) ) = Y )
130	117, 129	eqtrd 2501	. 2 |- ( ph -> [_ N / n ]_ if ( n = 0 , A , if ( n = S , C , if ( S < n , D , B ) ) ) = Y )
131	123, 130	eqtrd 2501	1 |- ( ph -> ( G ` N ) = Y )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 968   = wceq 1374   e. wcel 1762   =/= wne 2655   [.wsbc 3324   [_csb 3428   ifcif 3932   class class class wbr 4440   |-> cmpt 4498   ` cfv 5579   RRcr 9480   0cc0 9481   < clt 9617   <_ cle 9618   NNcn 10525   NN0cn0 10784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-fal 1380  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-nel 2658  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-pss 3485  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-tp 4025  df-op 4027  df-uni 4239  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-tr 4534  df-eprel 4784  df-id 4788  df-po 4793  df-so 4794  df-fr 4831  df-we 4833  df-ord 4874  df-on 4875  df-lim 4876  df-suc 4877  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-riota 6236  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-om 6672  df-recs 7032  df-rdg 7066  df-er 7301  df-en 7507  df-dom 7508  df-sdom 7509  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9796  df-neg 9797  df-nn 10526  df-n0 10785

This theorem is referenced by:  fvmptnn04ifa  19111  fvmptnn04ifb  19112  fvmptnn04ifc  19113  fvmptnn04ifd  19114