Theorem nnnninfeq 7072

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 7067	. . . 4 |- ( P e. ℕ∞ -> P : om --> 2o )
3	1, 2	syl 14	. . 3 |- ( ph -> P : om --> 2o )
4	3	ffnd 5321	. 2 |- ( ph -> P Fn om )
5		1lt2o 6390	. . . . . 6 |- 1o e. 2o
6	5	a1i 9	. . . . 5 |- ( ( ph /\ i e. om ) -> 1o e. 2o )
7		0lt2o 6389	. . . . . 6 |- (/) e. 2o
8	7	a1i 9	. . . . 5 |- ( ( ph /\ i e. om ) -> (/) e. 2o )
9		simpr 109	. . . . . 6 |- ( ( ph /\ i e. om ) -> i e. om )
10		nnnninfeq.n	. . . . . . 7 |- ( ph -> N e. om )
11	10	adantr 274	. . . . . 6 |- ( ( ph /\ i e. om ) -> N e. om )
12		nndcel 6448	. . . . . 6 |- ( ( i e. om /\ N e. om ) -> DECID i e. N )
13	9, 11, 12	syl2anc 409	. . . . 5 |- ( ( ph /\ i e. om ) -> DECID i e. N )
14	6, 8, 13	ifcldcd 3540	. . . 4 |- ( ( ph /\ i e. om ) -> if ( i e. N , 1o , (/) ) e. 2o )
15	14	ralrimiva 2530	. . 3 |- ( ph -> A. i e. om if ( i e. N , 1o , (/) ) e. 2o )
16		eqid 2157	. . . 4 |- ( i e. om |-> if ( i e. N , 1o , (/) ) ) = ( i e. om |-> if ( i e. N , 1o , (/) ) )
17	16	fnmpt 5297	. . 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 5469	. . . . . . 7 |- ( w = (/) -> ( P ` w ) = ( P ` (/) ) )
20		eleq1 2220	. . . . . . . 8 |- ( w = (/) -> ( w e. N <-> (/) e. N ) )
21	20	ifbid 3526	. . . . . . 7 |- ( w = (/) -> if ( w e. N , 1o , (/) ) = if ( (/) e. N , 1o , (/) ) )
22	19, 21	eqeq12d 2172	. . . . . 6 |- ( w = (/) -> ( ( P ` w ) = if ( w e. N , 1o , (/) ) <-> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) ) )
23	22	imbi2d 229	. . . . 5 |- ( w = (/) -> ( ( ph -> ( P ` w ) = if ( w e. N , 1o , (/) ) ) <-> ( ph -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) ) ) )
24		fveq2 5469	. . . . . . 7 |- ( w = k -> ( P ` w ) = ( P ` k ) )
25		eleq1w 2218	. . . . . . . 8 |- ( w = k -> ( w e. N <-> k e. N ) )
26	25	ifbid 3526	. . . . . . 7 |- ( w = k -> if ( w e. N , 1o , (/) ) = if ( k e. N , 1o , (/) ) )
27	24, 26	eqeq12d 2172	. . . . . 6 |- ( w = k -> ( ( P ` w ) = if ( w e. N , 1o , (/) ) <-> ( P ` k ) = if ( k e. N , 1o , (/) ) ) )
28	27	imbi2d 229	. . . . 5 |- ( w = k -> ( ( ph -> ( P ` w ) = if ( w e. N , 1o , (/) ) ) <-> ( ph -> ( P ` k ) = if ( k e. N , 1o , (/) ) ) ) )
29		fveq2 5469	. . . . . . 7 |- ( w = suc k -> ( P ` w ) = ( P ` suc k ) )
30		eleq1 2220	. . . . . . . 8 |- ( w = suc k -> ( w e. N <-> suc k e. N ) )
31	30	ifbid 3526	. . . . . . 7 |- ( w = suc k -> if ( w e. N , 1o , (/) ) = if ( suc k e. N , 1o , (/) ) )
32	29, 31	eqeq12d 2172	. . . . . 6 |- ( w = suc k -> ( ( P ` w ) = if ( w e. N , 1o , (/) ) <-> ( P ` suc k ) = if ( suc k e. N , 1o , (/) ) ) )
33	32	imbi2d 229	. . . . 5 |- ( w = suc k -> ( ( ph -> ( P ` w ) = if ( w e. N , 1o , (/) ) ) <-> ( ph -> ( P ` suc k ) = if ( suc k e. N , 1o , (/) ) ) ) )
34		fveq2 5469	. . . . . . 7 |- ( w = j -> ( P ` w ) = ( P ` j ) )
35		eleq1w 2218	. . . . . . . 8 |- ( w = j -> ( w e. N <-> j e. N ) )
36	35	ifbid 3526	. . . . . . 7 |- ( w = j -> if ( w e. N , 1o , (/) ) = if ( j e. N , 1o , (/) ) )
37	34, 36	eqeq12d 2172	. . . . . 6 |- ( w = j -> ( ( P ` w ) = if ( w e. N , 1o , (/) ) <-> ( P ` j ) = if ( j e. N , 1o , (/) ) ) )
38	37	imbi2d 229	. . . . 5 |- ( w = j -> ( ( ph -> ( P ` w ) = if ( w e. N , 1o , (/) ) ) <-> ( ph -> ( P ` j ) = if ( j e. N , 1o , (/) ) ) ) )
39		noel 3398	. . . . . . . . 9 |- -. (/) e. (/)
40		simpr 109	. . . . . . . . . 10 |- ( ( ph /\ N = (/) ) -> N = (/) )
41	40	eleq2d 2227	. . . . . . . . 9 |- ( ( ph /\ N = (/) ) -> ( (/) e. N <-> (/) e. (/) ) )
42	39, 41	mtbiri 665	. . . . . . . 8 |- ( ( ph /\ N = (/) ) -> -. (/) e. N )
43	42	iffalsed 3515	. . . . . . 7 |- ( ( ph /\ N = (/) ) -> if ( (/) e. N , 1o , (/) ) = (/) )
44		nnnninfeq.0	. . . . . . . 8 |- ( ph -> ( P ` N ) = (/) )
45	44	adantr 274	. . . . . . 7 |- ( ( ph /\ N = (/) ) -> ( P ` N ) = (/) )
46	40	fveq2d 5473	. . . . . . 7 |- ( ( ph /\ N = (/) ) -> ( P ` N ) = ( P ` (/) ) )
47	43, 45, 46	3eqtr2rd 2197	. . . . . 6 |- ( ( ph /\ N = (/) ) -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) )
48		fveq2 5469	. . . . . . . . 9 |- ( x = (/) -> ( P ` x ) = ( P ` (/) ) )
49	48	eqeq1d 2166	. . . . . . . 8 |- ( x = (/) -> ( ( P ` x ) = 1o <-> ( P ` (/) ) = 1o ) )
50		nnnninfeq.1	. . . . . . . . 9 |- ( ph -> A. x e. N ( P ` x ) = 1o )
51	50	adantr 274	. . . . . . . 8 |- ( ( ph /\ (/) e. N ) -> A. x e. N ( P ` x ) = 1o )
52		simpr 109	. . . . . . . 8 |- ( ( ph /\ (/) e. N ) -> (/) e. N )
53	49, 51, 52	rspcdva 2821	. . . . . . 7 |- ( ( ph /\ (/) e. N ) -> ( P ` (/) ) = 1o )
54	52	iftrued 3512	. . . . . . 7 |- ( ( ph /\ (/) e. N ) -> if ( (/) e. N , 1o , (/) ) = 1o )
55	53, 54	eqtr4d 2193	. . . . . 6 |- ( ( ph /\ (/) e. N ) -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) )
56		0elnn 4579	. . . . . . 7 |- ( N e. om -> ( N = (/) \/ (/) e. N ) )
57	10, 56	syl 14	. . . . . 6 |- ( ph -> ( N = (/) \/ (/) e. N ) )
58	47, 55, 57	mpjaodan 788	. . . . 5 |- ( ph -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) )
59		fveq2 5469	. . . . . . . . . . 11 |- ( x = suc k -> ( P ` x ) = ( P ` suc k ) )
60	59	eqeq1d 2166	. . . . . . . . . 10 |- ( x = suc k -> ( ( P ` x ) = 1o <-> ( P ` suc k ) = 1o ) )
61	50	ad3antlr 485	. . . . . . . . . 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 109	. . . . . . . . . 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 2821	. . . . . . . . 9 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k e. N ) -> ( P ` suc k ) = 1o )
64	62	iftrued 3512	. . . . . . . . 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 2193	. . . . . . . 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 485	. . . . . . . . 9 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> ( P ` N ) = (/) )
67		simpr 109	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> suc k = N )
68	67	fveq2d 5473	. . . . . . . . 9 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> ( P ` suc k ) = ( P ` N ) )
69	10	ad2antlr 481	. . . . . . . . . . . . 13 |- ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) -> N e. om )
70		nnord 4572	. . . . . . . . . . . . 13 |- ( N e. om -> Ord N )
71		ordirr 4502	. . . . . . . . . . . . 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 274	. . . . . . . . . . 11 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> -. N e. N )
74	67, 73	eqneltrd 2253	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> -. suc k e. N )
75	74	iffalsed 3515	. . . . . . . . 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 2200	. . . . . . . 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 4363	. . . . . . . . . . . . . 14 |- ( j = k -> suc j = suc k )
78	77	fveq2d 5473	. . . . . . . . . . . . 13 |- ( j = k -> ( P ` suc j ) = ( P ` suc k ) )
79		fveq2 5469	. . . . . . . . . . . . 13 |- ( j = k -> ( P ` j ) = ( P ` k ) )
80	78, 79	sseq12d 3159	. . . . . . . . . . . 12 |- ( j = k -> ( ( P ` suc j ) C_ ( P ` j ) <-> ( P ` suc k ) C_ ( P ` k ) ) )
81	1	ad3antlr 485	. . . . . . . . . . . . 13 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> P e. ℕ∞ )
82		fveq1 5468	. . . . . . . . . . . . . . . . 17 |- ( f = P -> ( f ` suc j ) = ( P ` suc j ) )
83		fveq1 5468	. . . . . . . . . . . . . . . . 17 |- ( f = P -> ( f ` j ) = ( P ` j ) )
84	82, 83	sseq12d 3159	. . . . . . . . . . . . . . . 16 |- ( f = P -> ( ( f ` suc j ) C_ ( f ` j ) <-> ( P ` suc j ) C_ ( P ` j ) ) )
85	84	ralbidv 2457	. . . . . . . . . . . . . . 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 7065	. . . . . . . . . . . . . . 15 |- ℕ∞ = { f e. ( 2o ^m om ) | A. j e. om ( f ` suc j ) C_ ( f ` j ) }
87	85, 86	elrab2 2871	. . . . . . . . . . . . . 14 |- ( P e. ℕ∞ <-> ( P e. ( 2o ^m om ) /\ A. j e. om ( P ` suc j ) C_ ( P ` j ) ) )
88	87	simprbi 273	. . . . . . . . . . . . 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 523	. . . . . . . . . . . 12 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> k e. om )
91	80, 89, 90	rspcdva 2821	. . . . . . . . . . 11 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` suc k ) C_ ( P ` k ) )
92		simplr 520	. . . . . . . . . . . 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 109	. . . . . . . . . . . . . . 15 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> N e. suc k )
94		nnord 4572	. . . . . . . . . . . . . . . 16 |- ( k e. om -> Ord k )
95		ordtr 4339	. . . . . . . . . . . . . . . 16 |- ( Ord k -> Tr k )
96		trsucss 4384	. . . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . . 15 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> N e. om )
100		nntri1 6444	. . . . . . . . . . . . . . 15 |- ( ( N e. om /\ k e. om ) -> ( N C_ k <-> -. k e. N ) )
101	99, 90, 100	syl2anc 409	. . . . . . . . . . . . . 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 146	. . . . . . . . . . . . 13 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> -. k e. N )
103	102	iffalsed 3515	. . . . . . . . . . . 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 2190	. . . . . . . . . . 11 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` k ) = (/) )
105	91, 104	sseqtrd 3166	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` suc k ) C_ (/) )
106		ss0 3434	. . . . . . . . . 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 4505	. . . . . . . . . . . 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 520	. . . . . . . . . . . 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 109	. . . . . . . . . . . 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 304	. . . . . . . . . . 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 655	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> -. suc k e. N )
114	113	iffalsed 3515	. . . . . . . . 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 2193	. . . . . . . 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 4555	. . . . . . . . . 10 |- ( k e. om -> suc k e. om )
117	116	ad2antrr 480	. . . . . . . . 9 |- ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) -> suc k e. om )
118		nntri3or 6441	. . . . . . . . 9 |- ( ( suc k e. om /\ N e. om ) -> ( suc k e. N \/ suc k = N \/ N e. suc k ) )
119	117, 69, 118	syl2anc 409	. . . . . . . 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 1289	. . . . . . 7 |- ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) -> ( P ` suc k ) = if ( suc k e. N , 1o , (/) ) )
121	120	exp31 362	. . . . . 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 4560	. . . 4 |- ( j e. om -> ( ph -> ( P ` j ) = if ( j e. N , 1o , (/) ) ) )
124	123	impcom 124	. . 3 |- ( ( ph /\ j e. om ) -> ( P ` j ) = if ( j e. N , 1o , (/) ) )
125		simpr 109	. . . 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 274	. . . . . 6 |- ( ( ph /\ j e. om ) -> N e. om )
129		nndcel 6448	. . . . . 6 |- ( ( j e. om /\ N e. om ) -> DECID j e. N )
130	125, 128, 129	syl2anc 409	. . . . 5 |- ( ( ph /\ j e. om ) -> DECID j e. N )
131	126, 127, 130	ifcldcd 3540	. . . 4 |- ( ( ph /\ j e. om ) -> if ( j e. N , 1o , (/) ) e. 2o )
132		eleq1w 2218	. . . . . 6 |- ( i = j -> ( i e. N <-> j e. N ) )
133	132	ifbid 3526	. . . . 5 |- ( i = j -> if ( i e. N , 1o , (/) ) = if ( j e. N , 1o , (/) ) )
134	133, 16	fvmptg 5545	. . . 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 409	. . 3 |- ( ( ph /\ j e. om ) -> ( ( i e. om |-> if ( i e. N , 1o , (/) ) ) ` j ) = if ( j e. N , 1o , (/) ) )
136	124, 135	eqtr4d 2193	. 2 |- ( ( ph /\ j e. om ) -> ( P ` j ) = ( ( i e. om |-> if ( i e. N , 1o , (/) ) ) ` j ) )
137	4, 18, 136	eqfnfvd 5569	1 |- ( ph -> P = ( i e. om |-> if ( i e. N , 1o , (/) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   \/ wo 698  DECID wdc 820   \/ w3o 962   = wceq 1335   e. wcel 2128   A.wral 2435   C_ wss 3102   (/)c0 3394   ifcif 3505   |-> cmpt 4026   Tr wtr 4063   Ord word 4323   suc csuc 4326   omcom 4550   Fn wfn 5166   -->wf 5167   ` cfv 5171  (class class class)co 5825   1oc1o 6357   2oc2o 6358   ^m cmap 6594  ℕ_∞xnninf 7064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4083  ax-nul 4091  ax-pow 4136  ax-pr 4170  ax-un 4394  ax-setind 4497  ax-iinf 4548

This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3774  df-int 3809  df-br 3967  df-opab 4027  df-mpt 4028  df-tr 4064  df-id 4254  df-iord 4327  df-on 4329  df-suc 4332  df-iom 4551  df-xp 4593  df-rel 4594  df-cnv 4595  df-co 4596  df-dm 4597  df-rn 4598  df-iota 5136  df-fun 5173  df-fn 5174  df-f 5175  df-fv 5179  df-ov 5828  df-oprab 5829  df-mpo 5830  df-1o 6364  df-2o 6365  df-map 6596  df-nninf 7065

This theorem is referenced by:  nnnninfeq2  7073  nninfisollem0  7074  nninfalllem1  13622  nninfsellemeq  13628