Theorem nninfalllemn 13377

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

Hypotheses

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

Assertion

Ref	Expression
nninfalllemn	|- ( 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 nninfalllemn

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

Step	Hyp	Ref	Expression
1		nninfalllemn.p	. . . 4 |- ( ph -> P e. ℕ∞ )
2		nninff 13373	. . . 4 |- ( P e. ℕ∞ -> P : om --> 2o )
3	1, 2	syl 14	. . 3 |- ( ph -> P : om --> 2o )
4	3	ffnd 5281	. 2 |- ( ph -> P Fn om )
5		1lt2o 6347	. . . . . 6 |- 1o e. 2o
6	5	a1i 9	. . . . 5 |- ( ( ph /\ i e. om ) -> 1o e. 2o )
7		0lt2o 6346	. . . . . 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		nninfalllemn.n	. . . . . . 7 |- ( ph -> N e. om )
11	10	adantr 274	. . . . . 6 |- ( ( ph /\ i e. om ) -> N e. om )
12		nndcel 6404	. . . . . 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 3512	. . . 4 |- ( ( ph /\ i e. om ) -> if ( i e. N , 1o , (/) ) e. 2o )
15	14	ralrimiva 2508	. . 3 |- ( ph -> A. i e. om if ( i e. N , 1o , (/) ) e. 2o )
16		eqid 2140	. . . 4 |- ( i e. om |-> if ( i e. N , 1o , (/) ) ) = ( i e. om |-> if ( i e. N , 1o , (/) ) )
17	16	fnmpt 5257	. . 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 5429	. . . . . . 7 |- ( w = (/) -> ( P ` w ) = ( P ` (/) ) )
20		eleq1 2203	. . . . . . . 8 |- ( w = (/) -> ( w e. N <-> (/) e. N ) )
21	20	ifbid 3498	. . . . . . 7 |- ( w = (/) -> if ( w e. N , 1o , (/) ) = if ( (/) e. N , 1o , (/) ) )
22	19, 21	eqeq12d 2155	. . . . . 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 5429	. . . . . . 7 |- ( w = k -> ( P ` w ) = ( P ` k ) )
25		eleq1w 2201	. . . . . . . 8 |- ( w = k -> ( w e. N <-> k e. N ) )
26	25	ifbid 3498	. . . . . . 7 |- ( w = k -> if ( w e. N , 1o , (/) ) = if ( k e. N , 1o , (/) ) )
27	24, 26	eqeq12d 2155	. . . . . 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 5429	. . . . . . 7 |- ( w = suc k -> ( P ` w ) = ( P ` suc k ) )
30		eleq1 2203	. . . . . . . 8 |- ( w = suc k -> ( w e. N <-> suc k e. N ) )
31	30	ifbid 3498	. . . . . . 7 |- ( w = suc k -> if ( w e. N , 1o , (/) ) = if ( suc k e. N , 1o , (/) ) )
32	29, 31	eqeq12d 2155	. . . . . 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 5429	. . . . . . 7 |- ( w = j -> ( P ` w ) = ( P ` j ) )
35		eleq1w 2201	. . . . . . . 8 |- ( w = j -> ( w e. N <-> j e. N ) )
36	35	ifbid 3498	. . . . . . 7 |- ( w = j -> if ( w e. N , 1o , (/) ) = if ( j e. N , 1o , (/) ) )
37	34, 36	eqeq12d 2155	. . . . . 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 3372	. . . . . . . . 9 |- -. (/) e. (/)
40		simpr 109	. . . . . . . . . 10 |- ( ( ph /\ N = (/) ) -> N = (/) )
41	40	eleq2d 2210	. . . . . . . . 9 |- ( ( ph /\ N = (/) ) -> ( (/) e. N <-> (/) e. (/) ) )
42	39, 41	mtbiri 665	. . . . . . . 8 |- ( ( ph /\ N = (/) ) -> -. (/) e. N )
43	42	iffalsed 3489	. . . . . . 7 |- ( ( ph /\ N = (/) ) -> if ( (/) e. N , 1o , (/) ) = (/) )
44		nninfalllemn.0	. . . . . . . 8 |- ( ph -> ( P ` N ) = (/) )
45	44	adantr 274	. . . . . . 7 |- ( ( ph /\ N = (/) ) -> ( P ` N ) = (/) )
46	40	fveq2d 5433	. . . . . . 7 |- ( ( ph /\ N = (/) ) -> ( P ` N ) = ( P ` (/) ) )
47	43, 45, 46	3eqtr2rd 2180	. . . . . 6 |- ( ( ph /\ N = (/) ) -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) )
48		fveq2 5429	. . . . . . . . 9 |- ( x = (/) -> ( P ` x ) = ( P ` (/) ) )
49	48	eqeq1d 2149	. . . . . . . 8 |- ( x = (/) -> ( ( P ` x ) = 1o <-> ( P ` (/) ) = 1o ) )
50		nninfalllemn.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 2798	. . . . . . 7 |- ( ( ph /\ (/) e. N ) -> ( P ` (/) ) = 1o )
54	52	iftrued 3486	. . . . . . 7 |- ( ( ph /\ (/) e. N ) -> if ( (/) e. N , 1o , (/) ) = 1o )
55	53, 54	eqtr4d 2176	. . . . . 6 |- ( ( ph /\ (/) e. N ) -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) )
56		0elnn 4540	. . . . . . 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 5429	. . . . . . . . . . 11 |- ( x = suc k -> ( P ` x ) = ( P ` suc k ) )
60	59	eqeq1d 2149	. . . . . . . . . 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 2798	. . . . . . . . 9 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k e. N ) -> ( P ` suc k ) = 1o )
64	62	iftrued 3486	. . . . . . . . 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 2176	. . . . . . . 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 5433	. . . . . . . . 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 4533	. . . . . . . . . . . . 13 |- ( N e. om -> Ord N )
71		ordirr 4465	. . . . . . . . . . . . 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 2236	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> -. suc k e. N )
75	74	iffalsed 3489	. . . . . . . . 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 2183	. . . . . . . 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 4332	. . . . . . . . . . . . . 14 |- ( j = k -> suc j = suc k )
78	77	fveq2d 5433	. . . . . . . . . . . . 13 |- ( j = k -> ( P ` suc j ) = ( P ` suc k ) )
79		fveq2 5429	. . . . . . . . . . . . 13 |- ( j = k -> ( P ` j ) = ( P ` k ) )
80	78, 79	sseq12d 3133	. . . . . . . . . . . 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 5428	. . . . . . . . . . . . . . . . 17 |- ( f = P -> ( f ` suc j ) = ( P ` suc j ) )
83		fveq1 5428	. . . . . . . . . . . . . . . . 17 |- ( f = P -> ( f ` j ) = ( P ` j ) )
84	82, 83	sseq12d 3133	. . . . . . . . . . . . . . . 16 |- ( f = P -> ( ( f ` suc j ) C_ ( f ` j ) <-> ( P ` suc j ) C_ ( P ` j ) ) )
85	84	ralbidv 2438	. . . . . . . . . . . . . . 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 7015	. . . . . . . . . . . . . . 15 |- ℕ∞ = { f e. ( 2o ^m om ) | A. j e. om ( f ` suc j ) C_ ( f ` j ) }
87	85, 86	elrab2 2847	. . . . . . . . . . . . . 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 2798	. . . . . . . . . . 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 4533	. . . . . . . . . . . . . . . 16 |- ( k e. om -> Ord k )
95		ordtr 4308	. . . . . . . . . . . . . . . 16 |- ( Ord k -> Tr k )
96		trsucss 4353	. . . . . . . . . . . . . . . 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 6400	. . . . . . . . . . . . . . 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 3489	. . . . . . . . . . . 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 2173	. . . . . . . . . . 11 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` k ) = (/) )
105	91, 104	sseqtrd 3140	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` suc k ) C_ (/) )
106		ss0 3408	. . . . . . . . . 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 4468	. . . . . . . . . . . 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 3489	. . . . . . . . 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 2176	. . . . . . . 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 4517	. . . . . . . . . 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 6397	. . . . . . . . 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 1286	. . . . . . 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 4522	. . . 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 6404	. . . . . 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 3512	. . . 4 |- ( ( ph /\ j e. om ) -> if ( j e. N , 1o , (/) ) e. 2o )
132		eleq1w 2201	. . . . . 6 |- ( i = j -> ( i e. N <-> j e. N ) )
133	132	ifbid 3498	. . . . 5 |- ( i = j -> if ( i e. N , 1o , (/) ) = if ( j e. N , 1o , (/) ) )
134	133, 16	fvmptg 5505	. . . 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 2176	. 2 |- ( ( ph /\ j e. om ) -> ( P ` j ) = ( ( i e. om |-> if ( i e. N , 1o , (/) ) ) ` j ) )
137	4, 18, 136	eqfnfvd 5529	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 1332   e. wcel 1481   A.wral 2417   C_ wss 3076   (/)c0 3368   ifcif 3479   |-> cmpt 3997   Tr wtr 4034   Ord word 4292   suc csuc 4295   omcom 4512   Fn wfn 5126   -->wf 5127   ` cfv 5131  (class class class)co 5782   1oc1o 6314   2oc2o 6315   ^m cmap 6550  ℕ_∞xnninf 7013

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-nul 4062  ax-pow 4106  ax-pr 4139  ax-un 4363  ax-setind 4460  ax-iinf 4510

This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2691  df-sbc 2914  df-csb 3008  df-dif 3078  df-un 3080  df-in 3082  df-ss 3089  df-nul 3369  df-if 3480  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-int 3780  df-br 3938  df-opab 3998  df-mpt 3999  df-tr 4035  df-id 4223  df-iord 4296  df-on 4298  df-suc 4301  df-iom 4513  df-xp 4553  df-rel 4554  df-cnv 4555  df-co 4556  df-dm 4557  df-rn 4558  df-iota 5096  df-fun 5133  df-fn 5134  df-f 5135  df-fv 5139  df-ov 5785  df-oprab 5786  df-mpo 5787  df-1o 6321  df-2o 6322  df-map 6552  df-nninf 7015

This theorem is referenced by:  nninfalllem1  13378  nninfsellemeq  13385