Theorem nnnninfeq 7126

Description: Mapping of a natural number to an element of ℕ_∞. (Contributed by Jim Kingdon, 4-Aug-2022.)

Hypotheses

Ref	Expression
nnnninfeq.p	|- ( ph -> P e. ℕ∞ )
nnnninfeq.n	|- ( ph -> N e. om )
nnnninfeq.1	|- ( ph -> A. x e. N ( P ` x ) = 1o )
nnnninfeq.0	|- ( ph -> ( P ` N ) = (/) )

Assertion

Ref	Expression
nnnninfeq	|- ( ph -> P = ( i e. om |-> if ( i e. N , 1o , (/) ) ) )

Distinct variable groups:   i, N   x, N   x, P   ph, i

Allowed substitution hints:   ph( x)   P( i)

Proof of Theorem nnnninfeq

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

Step	Hyp	Ref	Expression
1		nnnninfeq.p	. . . 4 |- ( ph -> P e. ℕ∞ )
2		nninff 7121	. . . 4 |- ( P e. ℕ∞ -> P : om --> 2o )
3	1, 2	syl 14	. . 3 |- ( ph -> P : om --> 2o )
4	3	ffnd 5367	. 2 |- ( ph -> P Fn om )
5		1lt2o 6443	. . . . . 6 |- 1o e. 2o
6	5	a1i 9	. . . . 5 |- ( ( ph /\ i e. om ) -> 1o e. 2o )
7		0lt2o 6442	. . . . . 6 |- (/) e. 2o
8	7	a1i 9	. . . . 5 |- ( ( ph /\ i e. om ) -> (/) e. 2o )
9		simpr 110	. . . . . 6 |- ( ( ph /\ i e. om ) -> i e. om )
10		nnnninfeq.n	. . . . . . 7 |- ( ph -> N e. om )
11	10	adantr 276	. . . . . 6 |- ( ( ph /\ i e. om ) -> N e. om )
12		nndcel 6501	. . . . . 6 |- ( ( i e. om /\ N e. om ) -> DECID i e. N )
13	9, 11, 12	syl2anc 411	. . . . 5 |- ( ( ph /\ i e. om ) -> DECID i e. N )
14	6, 8, 13	ifcldcd 3571	. . . 4 |- ( ( ph /\ i e. om ) -> if ( i e. N , 1o , (/) ) e. 2o )
15	14	ralrimiva 2550	. . 3 |- ( ph -> A. i e. om if ( i e. N , 1o , (/) ) e. 2o )
16		eqid 2177	. . . 4 |- ( i e. om |-> if ( i e. N , 1o , (/) ) ) = ( i e. om |-> if ( i e. N , 1o , (/) ) )
17	16	fnmpt 5343	. . 3 |- ( A. i e. om if ( i e. N , 1o , (/) ) e. 2o -> ( i e. om |-> if ( i e. N , 1o , (/) ) ) Fn om )
18	15, 17	syl 14	. 2 |- ( ph -> ( i e. om |-> if ( i e. N , 1o , (/) ) ) Fn om )
19		fveq2 5516	. . . . . . 7 |- ( w = (/) -> ( P ` w ) = ( P ` (/) ) )
20		eleq1 2240	. . . . . . . 8 |- ( w = (/) -> ( w e. N <-> (/) e. N ) )
21	20	ifbid 3556	. . . . . . 7 |- ( w = (/) -> if ( w e. N , 1o , (/) ) = if ( (/) e. N , 1o , (/) ) )
22	19, 21	eqeq12d 2192	. . . . . 6 |- ( w = (/) -> ( ( P ` w ) = if ( w e. N , 1o , (/) ) <-> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) ) )
23	22	imbi2d 230	. . . . 5 |- ( w = (/) -> ( ( ph -> ( P ` w ) = if ( w e. N , 1o , (/) ) ) <-> ( ph -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) ) ) )
24		fveq2 5516	. . . . . . 7 |- ( w = k -> ( P ` w ) = ( P ` k ) )
25		eleq1w 2238	. . . . . . . 8 |- ( w = k -> ( w e. N <-> k e. N ) )
26	25	ifbid 3556	. . . . . . 7 |- ( w = k -> if ( w e. N , 1o , (/) ) = if ( k e. N , 1o , (/) ) )
27	24, 26	eqeq12d 2192	. . . . . 6 |- ( w = k -> ( ( P ` w ) = if ( w e. N , 1o , (/) ) <-> ( P ` k ) = if ( k e. N , 1o , (/) ) ) )
28	27	imbi2d 230	. . . . 5 |- ( w = k -> ( ( ph -> ( P ` w ) = if ( w e. N , 1o , (/) ) ) <-> ( ph -> ( P ` k ) = if ( k e. N , 1o , (/) ) ) ) )
29		fveq2 5516	. . . . . . 7 |- ( w = suc k -> ( P ` w ) = ( P ` suc k ) )
30		eleq1 2240	. . . . . . . 8 |- ( w = suc k -> ( w e. N <-> suc k e. N ) )
31	30	ifbid 3556	. . . . . . 7 |- ( w = suc k -> if ( w e. N , 1o , (/) ) = if ( suc k e. N , 1o , (/) ) )
32	29, 31	eqeq12d 2192	. . . . . 6 |- ( w = suc k -> ( ( P ` w ) = if ( w e. N , 1o , (/) ) <-> ( P ` suc k ) = if ( suc k e. N , 1o , (/) ) ) )
33	32	imbi2d 230	. . . . 5 |- ( w = suc k -> ( ( ph -> ( P ` w ) = if ( w e. N , 1o , (/) ) ) <-> ( ph -> ( P ` suc k ) = if ( suc k e. N , 1o , (/) ) ) ) )
34		fveq2 5516	. . . . . . 7 |- ( w = j -> ( P ` w ) = ( P ` j ) )
35		eleq1w 2238	. . . . . . . 8 |- ( w = j -> ( w e. N <-> j e. N ) )
36	35	ifbid 3556	. . . . . . 7 |- ( w = j -> if ( w e. N , 1o , (/) ) = if ( j e. N , 1o , (/) ) )
37	34, 36	eqeq12d 2192	. . . . . 6 |- ( w = j -> ( ( P ` w ) = if ( w e. N , 1o , (/) ) <-> ( P ` j ) = if ( j e. N , 1o , (/) ) ) )
38	37	imbi2d 230	. . . . 5 |- ( w = j -> ( ( ph -> ( P ` w ) = if ( w e. N , 1o , (/) ) ) <-> ( ph -> ( P ` j ) = if ( j e. N , 1o , (/) ) ) ) )
39		noel 3427	. . . . . . . . 9 |- -. (/) e. (/)
40		simpr 110	. . . . . . . . . 10 |- ( ( ph /\ N = (/) ) -> N = (/) )
41	40	eleq2d 2247	. . . . . . . . 9 |- ( ( ph /\ N = (/) ) -> ( (/) e. N <-> (/) e. (/) ) )
42	39, 41	mtbiri 675	. . . . . . . 8 |- ( ( ph /\ N = (/) ) -> -. (/) e. N )
43	42	iffalsed 3545	. . . . . . 7 |- ( ( ph /\ N = (/) ) -> if ( (/) e. N , 1o , (/) ) = (/) )
44		nnnninfeq.0	. . . . . . . 8 |- ( ph -> ( P ` N ) = (/) )
45	44	adantr 276	. . . . . . 7 |- ( ( ph /\ N = (/) ) -> ( P ` N ) = (/) )
46	40	fveq2d 5520	. . . . . . 7 |- ( ( ph /\ N = (/) ) -> ( P ` N ) = ( P ` (/) ) )
47	43, 45, 46	3eqtr2rd 2217	. . . . . 6 |- ( ( ph /\ N = (/) ) -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) )
48		fveq2 5516	. . . . . . . . 9 |- ( x = (/) -> ( P ` x ) = ( P ` (/) ) )
49	48	eqeq1d 2186	. . . . . . . 8 |- ( x = (/) -> ( ( P ` x ) = 1o <-> ( P ` (/) ) = 1o ) )
50		nnnninfeq.1	. . . . . . . . 9 |- ( ph -> A. x e. N ( P ` x ) = 1o )
51	50	adantr 276	. . . . . . . 8 |- ( ( ph /\ (/) e. N ) -> A. x e. N ( P ` x ) = 1o )
52		simpr 110	. . . . . . . 8 |- ( ( ph /\ (/) e. N ) -> (/) e. N )
53	49, 51, 52	rspcdva 2847	. . . . . . 7 |- ( ( ph /\ (/) e. N ) -> ( P ` (/) ) = 1o )
54	52	iftrued 3542	. . . . . . 7 |- ( ( ph /\ (/) e. N ) -> if ( (/) e. N , 1o , (/) ) = 1o )
55	53, 54	eqtr4d 2213	. . . . . 6 |- ( ( ph /\ (/) e. N ) -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) )
56		0elnn 4619	. . . . . . 7 |- ( N e. om -> ( N = (/) \/ (/) e. N ) )
57	10, 56	syl 14	. . . . . 6 |- ( ph -> ( N = (/) \/ (/) e. N ) )
58	47, 55, 57	mpjaodan 798	. . . . 5 |- ( ph -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) )
59		fveq2 5516	. . . . . . . . . . 11 |- ( x = suc k -> ( P ` x ) = ( P ` suc k ) )
60	59	eqeq1d 2186	. . . . . . . . . 10 |- ( x = suc k -> ( ( P ` x ) = 1o <-> ( P ` suc k ) = 1o ) )
61	50	ad3antlr 493	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k e. N ) -> A. x e. N ( P ` x ) = 1o )
62		simpr 110	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k e. N ) -> suc k e. N )
63	60, 61, 62	rspcdva 2847	. . . . . . . . 9 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k e. N ) -> ( P ` suc k ) = 1o )
64	62	iftrued 3542	. . . . . . . . 9 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k e. N ) -> if ( suc k e. N , 1o , (/) ) = 1o )
65	63, 64	eqtr4d 2213	. . . . . . . 8 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k e. N ) -> ( P ` suc k ) = if ( suc k e. N , 1o , (/) ) )
66	44	ad3antlr 493	. . . . . . . . 9 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> ( P ` N ) = (/) )
67		simpr 110	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> suc k = N )
68	67	fveq2d 5520	. . . . . . . . 9 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> ( P ` suc k ) = ( P ` N ) )
69	10	ad2antlr 489	. . . . . . . . . . . . 13 |- ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) -> N e. om )
70		nnord 4612	. . . . . . . . . . . . 13 |- ( N e. om -> Ord N )
71		ordirr 4542	. . . . . . . . . . . . 13 |- ( Ord N -> -. N e. N )
72	69, 70, 71	3syl 17	. . . . . . . . . . . 12 |- ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) -> -. N e. N )
73	72	adantr 276	. . . . . . . . . . 11 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> -. N e. N )
74	67, 73	eqneltrd 2273	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> -. suc k e. N )
75	74	iffalsed 3545	. . . . . . . . 9 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> if ( suc k e. N , 1o , (/) ) = (/) )
76	66, 68, 75	3eqtr4d 2220	. . . . . . . 8 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> ( P ` suc k ) = if ( suc k e. N , 1o , (/) ) )
77		suceq 4403	. . . . . . . . . . . . . 14 |- ( j = k -> suc j = suc k )
78	77	fveq2d 5520	. . . . . . . . . . . . 13 |- ( j = k -> ( P ` suc j ) = ( P ` suc k ) )
79		fveq2 5516	. . . . . . . . . . . . 13 |- ( j = k -> ( P ` j ) = ( P ` k ) )
80	78, 79	sseq12d 3187	. . . . . . . . . . . 12 |- ( j = k -> ( ( P ` suc j ) C_ ( P ` j ) <-> ( P ` suc k ) C_ ( P ` k ) ) )
81	1	ad3antlr 493	. . . . . . . . . . . . 13 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> P e. ℕ∞ )
82		fveq1 5515	. . . . . . . . . . . . . . . . 17 |- ( f = P -> ( f ` suc j ) = ( P ` suc j ) )
83		fveq1 5515	. . . . . . . . . . . . . . . . 17 |- ( f = P -> ( f ` j ) = ( P ` j ) )
84	82, 83	sseq12d 3187	. . . . . . . . . . . . . . . 16 |- ( f = P -> ( ( f ` suc j ) C_ ( f ` j ) <-> ( P ` suc j ) C_ ( P ` j ) ) )
85	84	ralbidv 2477	. . . . . . . . . . . . . . 15 |- ( f = P -> ( A. j e. om ( f ` suc j ) C_ ( f ` j ) <-> A. j e. om ( P ` suc j ) C_ ( P ` j ) ) )
86		df-nninf 7119	. . . . . . . . . . . . . . 15 |- ℕ∞ = { f e. ( 2o ^m om ) | A. j e. om ( f ` suc j ) C_ ( f ` j ) }
87	85, 86	elrab2 2897	. . . . . . . . . . . . . 14 |- ( P e. ℕ∞ <-> ( P e. ( 2o ^m om ) /\ A. j e. om ( P ` suc j ) C_ ( P ` j ) ) )
88	87	simprbi 275	. . . . . . . . . . . . 13 |- ( P e. ℕ∞ -> A. j e. om ( P ` suc j ) C_ ( P ` j ) )
89	81, 88	syl 14	. . . . . . . . . . . 12 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> A. j e. om ( P ` suc j ) C_ ( P ` j ) )
90		simplll 533	. . . . . . . . . . . 12 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> k e. om )
91	80, 89, 90	rspcdva 2847	. . . . . . . . . . 11 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` suc k ) C_ ( P ` k ) )
92		simplr 528	. . . . . . . . . . . 12 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` k ) = if ( k e. N , 1o , (/) ) )
93		simpr 110	. . . . . . . . . . . . . . 15 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> N e. suc k )
94		nnord 4612	. . . . . . . . . . . . . . . 16 |- ( k e. om -> Ord k )
95		ordtr 4379	. . . . . . . . . . . . . . . 16 |- ( Ord k -> Tr k )
96		trsucss 4424	. . . . . . . . . . . . . . . 16 |- ( Tr k -> ( N e. suc k -> N C_ k ) )
97	94, 95, 96	3syl 17	. . . . . . . . . . . . . . 15 |- ( k e. om -> ( N e. suc k -> N C_ k ) )
98	90, 93, 97	sylc 62	. . . . . . . . . . . . . 14 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> N C_ k )
99	69	adantr 276	. . . . . . . . . . . . . . 15 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> N e. om )
100		nntri1 6497	. . . . . . . . . . . . . . 15 |- ( ( N e. om /\ k e. om ) -> ( N C_ k <-> -. k e. N ) )
101	99, 90, 100	syl2anc 411	. . . . . . . . . . . . . 14 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( N C_ k <-> -. k e. N ) )
102	98, 101	mpbid 147	. . . . . . . . . . . . 13 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> -. k e. N )
103	102	iffalsed 3545	. . . . . . . . . . . 12 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> if ( k e. N , 1o , (/) ) = (/) )
104	92, 103	eqtrd 2210	. . . . . . . . . . 11 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` k ) = (/) )
105	91, 104	sseqtrd 3194	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` suc k ) C_ (/) )
106		ss0 3464	. . . . . . . . . 10 |- ( ( P ` suc k ) C_ (/) -> ( P ` suc k ) = (/) )
107	105, 106	syl 14	. . . . . . . . 9 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` suc k ) = (/) )
108		ordn2lp 4545	. . . . . . . . . . . 12 |- ( Ord N -> -. ( N e. suc k /\ suc k e. N ) )
109	99, 70, 108	3syl 17	. . . . . . . . . . 11 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> -. ( N e. suc k /\ suc k e. N ) )
110		simplr 528	. . . . . . . . . . . 12 |- ( ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) /\ suc k e. N ) -> N e. suc k )
111		simpr 110	. . . . . . . . . . . 12 |- ( ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) /\ suc k e. N ) -> suc k e. N )
112	110, 111	jca 306	. . . . . . . . . . 11 |- ( ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) /\ suc k e. N ) -> ( N e. suc k /\ suc k e. N ) )
113	109, 112	mtand 665	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> -. suc k e. N )
114	113	iffalsed 3545	. . . . . . . . 9 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> if ( suc k e. N , 1o , (/) ) = (/) )
115	107, 114	eqtr4d 2213	. . . . . . . 8 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` suc k ) = if ( suc k e. N , 1o , (/) ) )
116		peano2 4595	. . . . . . . . . 10 |- ( k e. om -> suc k e. om )
117	116	ad2antrr 488	. . . . . . . . 9 |- ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) -> suc k e. om )
118		nntri3or 6494	. . . . . . . . 9 |- ( ( suc k e. om /\ N e. om ) -> ( suc k e. N \/ suc k = N \/ N e. suc k ) )
119	117, 69, 118	syl2anc 411	. . . . . . . 8 |- ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) -> ( suc k e. N \/ suc k = N \/ N e. suc k ) )
120	65, 76, 115, 119	mpjao3dan 1307	. . . . . . 7 |- ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) -> ( P ` suc k ) = if ( suc k e. N , 1o , (/) ) )
121	120	exp31 364	. . . . . 6 |- ( k e. om -> ( ph -> ( ( P ` k ) = if ( k e. N , 1o , (/) ) -> ( P ` suc k ) = if ( suc k e. N , 1o , (/) ) ) ) )
122	121	a2d 26	. . . . 5 |- ( k e. om -> ( ( ph -> ( P ` k ) = if ( k e. N , 1o , (/) ) ) -> ( ph -> ( P ` suc k ) = if ( suc k e. N , 1o , (/) ) ) ) )
123	23, 28, 33, 38, 58, 122	finds 4600	. . . 4 |- ( j e. om -> ( ph -> ( P ` j ) = if ( j e. N , 1o , (/) ) ) )
124	123	impcom 125	. . 3 |- ( ( ph /\ j e. om ) -> ( P ` j ) = if ( j e. N , 1o , (/) ) )
125		simpr 110	. . . 4 |- ( ( ph /\ j e. om ) -> j e. om )
126	5	a1i 9	. . . . 5 |- ( ( ph /\ j e. om ) -> 1o e. 2o )
127	7	a1i 9	. . . . 5 |- ( ( ph /\ j e. om ) -> (/) e. 2o )
128	10	adantr 276	. . . . . 6 |- ( ( ph /\ j e. om ) -> N e. om )
129		nndcel 6501	. . . . . 6 |- ( ( j e. om /\ N e. om ) -> DECID j e. N )
130	125, 128, 129	syl2anc 411	. . . . 5 |- ( ( ph /\ j e. om ) -> DECID j e. N )
131	126, 127, 130	ifcldcd 3571	. . . 4 |- ( ( ph /\ j e. om ) -> if ( j e. N , 1o , (/) ) e. 2o )
132		eleq1w 2238	. . . . . 6 |- ( i = j -> ( i e. N <-> j e. N ) )
133	132	ifbid 3556	. . . . 5 |- ( i = j -> if ( i e. N , 1o , (/) ) = if ( j e. N , 1o , (/) ) )
134	133, 16	fvmptg 5593	. . . 4 |- ( ( j e. om /\ if ( j e. N , 1o , (/) ) e. 2o ) -> ( ( i e. om |-> if ( i e. N , 1o , (/) ) ) ` j ) = if ( j e. N , 1o , (/) ) )
135	125, 131, 134	syl2anc 411	. . 3 |- ( ( ph /\ j e. om ) -> ( ( i e. om |-> if ( i e. N , 1o , (/) ) ) ` j ) = if ( j e. N , 1o , (/) ) )
136	124, 135	eqtr4d 2213	. 2 |- ( ( ph /\ j e. om ) -> ( P ` j ) = ( ( i e. om |-> if ( i e. N , 1o , (/) ) ) ` j ) )
137	4, 18, 136	eqfnfvd 5617	1 |- ( ph -> P = ( i e. om |-> if ( i e. N , 1o , (/) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 708  DECID wdc 834   \/ w3o 977   = wceq 1353   e. wcel 2148   A.wral 2455   C_ wss 3130   (/)c0 3423   ifcif 3535   |-> cmpt 4065   Tr wtr 4102   Ord word 4363   suc csuc 4366   omcom 4590   Fn wfn 5212   -->wf 5213   ` cfv 5217  (class class class)co 5875   1oc1o 6410   2oc2o 6411   ^m cmap 6648  ℕ_∞xnninf 7118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-iinf 4588

This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-if 3536  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-br 4005  df-opab 4066  df-mpt 4067  df-tr 4103  df-id 4294  df-iord 4367  df-on 4369  df-suc 4372  df-iom 4591  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-fv 5225  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1o 6417  df-2o 6418  df-map 6650  df-nninf 7119

This theorem is referenced by:  nnnninfeq2  7127  nninfisollem0  7128  nninfalllem1  14760  nninfsellemeq  14766