Theorem nnnninfeq 7104

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 7099	. . . 4 |- ( P e. ℕ∞ -> P : om --> 2o )
3	1, 2	syl 14	. . 3 |- ( ph -> P : om --> 2o )
4	3	ffnd 5348	. 2 |- ( ph -> P Fn om )
5		1lt2o 6421	. . . . . 6 |- 1o e. 2o
6	5	a1i 9	. . . . 5 |- ( ( ph /\ i e. om ) -> 1o e. 2o )
7		0lt2o 6420	. . . . . 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 6479	. . . . . 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 3561	. . . 4 |- ( ( ph /\ i e. om ) -> if ( i e. N , 1o , (/) ) e. 2o )
15	14	ralrimiva 2543	. . 3 |- ( ph -> A. i e. om if ( i e. N , 1o , (/) ) e. 2o )
16		eqid 2170	. . . 4 |- ( i e. om |-> if ( i e. N , 1o , (/) ) ) = ( i e. om |-> if ( i e. N , 1o , (/) ) )
17	16	fnmpt 5324	. . 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 5496	. . . . . . 7 |- ( w = (/) -> ( P ` w ) = ( P ` (/) ) )
20		eleq1 2233	. . . . . . . 8 |- ( w = (/) -> ( w e. N <-> (/) e. N ) )
21	20	ifbid 3547	. . . . . . 7 |- ( w = (/) -> if ( w e. N , 1o , (/) ) = if ( (/) e. N , 1o , (/) ) )
22	19, 21	eqeq12d 2185	. . . . . 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 5496	. . . . . . 7 |- ( w = k -> ( P ` w ) = ( P ` k ) )
25		eleq1w 2231	. . . . . . . 8 |- ( w = k -> ( w e. N <-> k e. N ) )
26	25	ifbid 3547	. . . . . . 7 |- ( w = k -> if ( w e. N , 1o , (/) ) = if ( k e. N , 1o , (/) ) )
27	24, 26	eqeq12d 2185	. . . . . 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 5496	. . . . . . 7 |- ( w = suc k -> ( P ` w ) = ( P ` suc k ) )
30		eleq1 2233	. . . . . . . 8 |- ( w = suc k -> ( w e. N <-> suc k e. N ) )
31	30	ifbid 3547	. . . . . . 7 |- ( w = suc k -> if ( w e. N , 1o , (/) ) = if ( suc k e. N , 1o , (/) ) )
32	29, 31	eqeq12d 2185	. . . . . 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 5496	. . . . . . 7 |- ( w = j -> ( P ` w ) = ( P ` j ) )
35		eleq1w 2231	. . . . . . . 8 |- ( w = j -> ( w e. N <-> j e. N ) )
36	35	ifbid 3547	. . . . . . 7 |- ( w = j -> if ( w e. N , 1o , (/) ) = if ( j e. N , 1o , (/) ) )
37	34, 36	eqeq12d 2185	. . . . . 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 3418	. . . . . . . . 9 |- -. (/) e. (/)
40		simpr 109	. . . . . . . . . 10 |- ( ( ph /\ N = (/) ) -> N = (/) )
41	40	eleq2d 2240	. . . . . . . . 9 |- ( ( ph /\ N = (/) ) -> ( (/) e. N <-> (/) e. (/) ) )
42	39, 41	mtbiri 670	. . . . . . . 8 |- ( ( ph /\ N = (/) ) -> -. (/) e. N )
43	42	iffalsed 3536	. . . . . . 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 5500	. . . . . . 7 |- ( ( ph /\ N = (/) ) -> ( P ` N ) = ( P ` (/) ) )
47	43, 45, 46	3eqtr2rd 2210	. . . . . 6 |- ( ( ph /\ N = (/) ) -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) )
48		fveq2 5496	. . . . . . . . 9 |- ( x = (/) -> ( P ` x ) = ( P ` (/) ) )
49	48	eqeq1d 2179	. . . . . . . 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 2839	. . . . . . 7 |- ( ( ph /\ (/) e. N ) -> ( P ` (/) ) = 1o )
54	52	iftrued 3533	. . . . . . 7 |- ( ( ph /\ (/) e. N ) -> if ( (/) e. N , 1o , (/) ) = 1o )
55	53, 54	eqtr4d 2206	. . . . . 6 |- ( ( ph /\ (/) e. N ) -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) )
56		0elnn 4603	. . . . . . 7 |- ( N e. om -> ( N = (/) \/ (/) e. N ) )
57	10, 56	syl 14	. . . . . 6 |- ( ph -> ( N = (/) \/ (/) e. N ) )
58	47, 55, 57	mpjaodan 793	. . . . 5 |- ( ph -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) )
59		fveq2 5496	. . . . . . . . . . 11 |- ( x = suc k -> ( P ` x ) = ( P ` suc k ) )
60	59	eqeq1d 2179	. . . . . . . . . 10 |- ( x = suc k -> ( ( P ` x ) = 1o <-> ( P ` suc k ) = 1o ) )
61	50	ad3antlr 490	. . . . . . . . . 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 2839	. . . . . . . . 9 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k e. N ) -> ( P ` suc k ) = 1o )
64	62	iftrued 3533	. . . . . . . . 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 2206	. . . . . . . 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 490	. . . . . . . . 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 5500	. . . . . . . . 9 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> ( P ` suc k ) = ( P ` N ) )
69	10	ad2antlr 486	. . . . . . . . . . . . 13 |- ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) -> N e. om )
70		nnord 4596	. . . . . . . . . . . . 13 |- ( N e. om -> Ord N )
71		ordirr 4526	. . . . . . . . . . . . 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 2266	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> -. suc k e. N )
75	74	iffalsed 3536	. . . . . . . . 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 2213	. . . . . . . 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 4387	. . . . . . . . . . . . . 14 |- ( j = k -> suc j = suc k )
78	77	fveq2d 5500	. . . . . . . . . . . . 13 |- ( j = k -> ( P ` suc j ) = ( P ` suc k ) )
79		fveq2 5496	. . . . . . . . . . . . 13 |- ( j = k -> ( P ` j ) = ( P ` k ) )
80	78, 79	sseq12d 3178	. . . . . . . . . . . 12 |- ( j = k -> ( ( P ` suc j ) C_ ( P ` j ) <-> ( P ` suc k ) C_ ( P ` k ) ) )
81	1	ad3antlr 490	. . . . . . . . . . . . 13 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> P e. ℕ∞ )
82		fveq1 5495	. . . . . . . . . . . . . . . . 17 |- ( f = P -> ( f ` suc j ) = ( P ` suc j ) )
83		fveq1 5495	. . . . . . . . . . . . . . . . 17 |- ( f = P -> ( f ` j ) = ( P ` j ) )
84	82, 83	sseq12d 3178	. . . . . . . . . . . . . . . 16 |- ( f = P -> ( ( f ` suc j ) C_ ( f ` j ) <-> ( P ` suc j ) C_ ( P ` j ) ) )
85	84	ralbidv 2470	. . . . . . . . . . . . . . 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 7097	. . . . . . . . . . . . . . 15 |- ℕ∞ = { f e. ( 2o ^m om ) | A. j e. om ( f ` suc j ) C_ ( f ` j ) }
87	85, 86	elrab2 2889	. . . . . . . . . . . . . 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 528	. . . . . . . . . . . 12 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> k e. om )
91	80, 89, 90	rspcdva 2839	. . . . . . . . . . 11 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` suc k ) C_ ( P ` k ) )
92		simplr 525	. . . . . . . . . . . 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 4596	. . . . . . . . . . . . . . . 16 |- ( k e. om -> Ord k )
95		ordtr 4363	. . . . . . . . . . . . . . . 16 |- ( Ord k -> Tr k )
96		trsucss 4408	. . . . . . . . . . . . . . . 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 6475	. . . . . . . . . . . . . . 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 3536	. . . . . . . . . . . 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 2203	. . . . . . . . . . 11 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` k ) = (/) )
105	91, 104	sseqtrd 3185	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` suc k ) C_ (/) )
106		ss0 3455	. . . . . . . . . 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 4529	. . . . . . . . . . . 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 525	. . . . . . . . . . . 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 660	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> -. suc k e. N )
114	113	iffalsed 3536	. . . . . . . . 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 2206	. . . . . . . 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 4579	. . . . . . . . . 10 |- ( k e. om -> suc k e. om )
117	116	ad2antrr 485	. . . . . . . . 9 |- ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) -> suc k e. om )
118		nntri3or 6472	. . . . . . . . 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 1302	. . . . . . 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 4584	. . . 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 6479	. . . . . 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 3561	. . . 4 |- ( ( ph /\ j e. om ) -> if ( j e. N , 1o , (/) ) e. 2o )
132		eleq1w 2231	. . . . . 6 |- ( i = j -> ( i e. N <-> j e. N ) )
133	132	ifbid 3547	. . . . 5 |- ( i = j -> if ( i e. N , 1o , (/) ) = if ( j e. N , 1o , (/) ) )
134	133, 16	fvmptg 5572	. . . 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 2206	. 2 |- ( ( ph /\ j e. om ) -> ( P ` j ) = ( ( i e. om |-> if ( i e. N , 1o , (/) ) ) ` j ) )
137	4, 18, 136	eqfnfvd 5596	1 |- ( ph -> P = ( i e. om |-> if ( i e. N , 1o , (/) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   \/ wo 703  DECID wdc 829   \/ w3o 972   = wceq 1348   e. wcel 2141   A.wral 2448   C_ wss 3121   (/)c0 3414   ifcif 3526   |-> cmpt 4050   Tr wtr 4087   Ord word 4347   suc csuc 4350   omcom 4574   Fn wfn 5193   -->wf 5194   ` cfv 5198  (class class class)co 5853   1oc1o 6388   2oc2o 6389   ^m cmap 6626  ℕ_∞xnninf 7096

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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572

This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3527  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-id 4278  df-iord 4351  df-on 4353  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-fv 5206  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1o 6395  df-2o 6396  df-map 6628  df-nninf 7097

This theorem is referenced by:  nnnninfeq2  7105  nninfisollem0  7106  nninfalllem1  14041  nninfsellemeq  14047