Theorem nninfalllemn 13202

Description: Lemma for nninfall 13204. 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 13198	. . . 4 |- ( P e. ℕ∞ -> P : om --> 2o )
3	1, 2	syl 14	. . 3 |- ( ph -> P : om --> 2o )
4	3	ffnd 5273	. 2 |- ( ph -> P Fn om )
5		1lt2o 6339	. . . . . 6 |- 1o e. 2o
6	5	a1i 9	. . . . 5 |- ( ( ph /\ i e. om ) -> 1o e. 2o )
7		0lt2o 6338	. . . . . 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 6396	. . . . . 6 |- ( ( i e. om /\ N e. om ) -> DECID i e. N )
13	9, 11, 12	syl2anc 408	. . . . 5 |- ( ( ph /\ i e. om ) -> DECID i e. N )
14	6, 8, 13	ifcldcd 3507	. . . 4 |- ( ( ph /\ i e. om ) -> if ( i e. N , 1o , (/) ) e. 2o )
15	14	ralrimiva 2505	. . 3 |- ( ph -> A. i e. om if ( i e. N , 1o , (/) ) e. 2o )
16		eqid 2139	. . . 4 |- ( i e. om |-> if ( i e. N , 1o , (/) ) ) = ( i e. om |-> if ( i e. N , 1o , (/) ) )
17	16	fnmpt 5249	. . 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 5421	. . . . . . 7 |- ( w = (/) -> ( P ` w ) = ( P ` (/) ) )
20		eleq1 2202	. . . . . . . 8 |- ( w = (/) -> ( w e. N <-> (/) e. N ) )
21	20	ifbid 3493	. . . . . . 7 |- ( w = (/) -> if ( w e. N , 1o , (/) ) = if ( (/) e. N , 1o , (/) ) )
22	19, 21	eqeq12d 2154	. . . . . 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 5421	. . . . . . 7 |- ( w = k -> ( P ` w ) = ( P ` k ) )
25		eleq1w 2200	. . . . . . . 8 |- ( w = k -> ( w e. N <-> k e. N ) )
26	25	ifbid 3493	. . . . . . 7 |- ( w = k -> if ( w e. N , 1o , (/) ) = if ( k e. N , 1o , (/) ) )
27	24, 26	eqeq12d 2154	. . . . . 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 5421	. . . . . . 7 |- ( w = suc k -> ( P ` w ) = ( P ` suc k ) )
30		eleq1 2202	. . . . . . . 8 |- ( w = suc k -> ( w e. N <-> suc k e. N ) )
31	30	ifbid 3493	. . . . . . 7 |- ( w = suc k -> if ( w e. N , 1o , (/) ) = if ( suc k e. N , 1o , (/) ) )
32	29, 31	eqeq12d 2154	. . . . . 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 5421	. . . . . . 7 |- ( w = j -> ( P ` w ) = ( P ` j ) )
35		eleq1w 2200	. . . . . . . 8 |- ( w = j -> ( w e. N <-> j e. N ) )
36	35	ifbid 3493	. . . . . . 7 |- ( w = j -> if ( w e. N , 1o , (/) ) = if ( j e. N , 1o , (/) ) )
37	34, 36	eqeq12d 2154	. . . . . 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 3367	. . . . . . . . 9 |- -. (/) e. (/)
40		simpr 109	. . . . . . . . . 10 |- ( ( ph /\ N = (/) ) -> N = (/) )
41	40	eleq2d 2209	. . . . . . . . 9 |- ( ( ph /\ N = (/) ) -> ( (/) e. N <-> (/) e. (/) ) )
42	39, 41	mtbiri 664	. . . . . . . 8 |- ( ( ph /\ N = (/) ) -> -. (/) e. N )
43	42	iffalsed 3484	. . . . . . 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 5425	. . . . . . 7 |- ( ( ph /\ N = (/) ) -> ( P ` N ) = ( P ` (/) ) )
47	43, 45, 46	3eqtr2rd 2179	. . . . . 6 |- ( ( ph /\ N = (/) ) -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) )
48		fveq2 5421	. . . . . . . . 9 |- ( x = (/) -> ( P ` x ) = ( P ` (/) ) )
49	48	eqeq1d 2148	. . . . . . . 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 2794	. . . . . . 7 |- ( ( ph /\ (/) e. N ) -> ( P ` (/) ) = 1o )
54	52	iftrued 3481	. . . . . . 7 |- ( ( ph /\ (/) e. N ) -> if ( (/) e. N , 1o , (/) ) = 1o )
55	53, 54	eqtr4d 2175	. . . . . 6 |- ( ( ph /\ (/) e. N ) -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) )
56		0elnn 4532	. . . . . . 7 |- ( N e. om -> ( N = (/) \/ (/) e. N ) )
57	10, 56	syl 14	. . . . . 6 |- ( ph -> ( N = (/) \/ (/) e. N ) )
58	47, 55, 57	mpjaodan 787	. . . . 5 |- ( ph -> ( P ` (/) ) = if ( (/) e. N , 1o , (/) ) )
59		fveq2 5421	. . . . . . . . . . 11 |- ( x = suc k -> ( P ` x ) = ( P ` suc k ) )
60	59	eqeq1d 2148	. . . . . . . . . 10 |- ( x = suc k -> ( ( P ` x ) = 1o <-> ( P ` suc k ) = 1o ) )
61	50	ad3antlr 484	. . . . . . . . . 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 2794	. . . . . . . . 9 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k e. N ) -> ( P ` suc k ) = 1o )
64	62	iftrued 3481	. . . . . . . . 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 2175	. . . . . . . 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 484	. . . . . . . . 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 5425	. . . . . . . . 9 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> ( P ` suc k ) = ( P ` N ) )
69	10	ad2antlr 480	. . . . . . . . . . . . 13 |- ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) -> N e. om )
70		nnord 4525	. . . . . . . . . . . . 13 |- ( N e. om -> Ord N )
71		ordirr 4457	. . . . . . . . . . . . 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 2235	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ suc k = N ) -> -. suc k e. N )
75	74	iffalsed 3484	. . . . . . . . 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 2182	. . . . . . . 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 4324	. . . . . . . . . . . . . 14 |- ( j = k -> suc j = suc k )
78	77	fveq2d 5425	. . . . . . . . . . . . 13 |- ( j = k -> ( P ` suc j ) = ( P ` suc k ) )
79		fveq2 5421	. . . . . . . . . . . . 13 |- ( j = k -> ( P ` j ) = ( P ` k ) )
80	78, 79	sseq12d 3128	. . . . . . . . . . . 12 |- ( j = k -> ( ( P ` suc j ) C_ ( P ` j ) <-> ( P ` suc k ) C_ ( P ` k ) ) )
81	1	ad3antlr 484	. . . . . . . . . . . . 13 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> P e. ℕ∞ )
82		fveq1 5420	. . . . . . . . . . . . . . . . 17 |- ( f = P -> ( f ` suc j ) = ( P ` suc j ) )
83		fveq1 5420	. . . . . . . . . . . . . . . . 17 |- ( f = P -> ( f ` j ) = ( P ` j ) )
84	82, 83	sseq12d 3128	. . . . . . . . . . . . . . . 16 |- ( f = P -> ( ( f ` suc j ) C_ ( f ` j ) <-> ( P ` suc j ) C_ ( P ` j ) ) )
85	84	ralbidv 2437	. . . . . . . . . . . . . . 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 7007	. . . . . . . . . . . . . . 15 |- ℕ∞ = { f e. ( 2o ^m om ) | A. j e. om ( f ` suc j ) C_ ( f ` j ) }
87	85, 86	elrab2 2843	. . . . . . . . . . . . . 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 522	. . . . . . . . . . . 12 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> k e. om )
91	80, 89, 90	rspcdva 2794	. . . . . . . . . . 11 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` suc k ) C_ ( P ` k ) )
92		simplr 519	. . . . . . . . . . . 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 4525	. . . . . . . . . . . . . . . 16 |- ( k e. om -> Ord k )
95		ordtr 4300	. . . . . . . . . . . . . . . 16 |- ( Ord k -> Tr k )
96		trsucss 4345	. . . . . . . . . . . . . . . 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 6392	. . . . . . . . . . . . . . 15 |- ( ( N e. om /\ k e. om ) -> ( N C_ k <-> -. k e. N ) )
101	99, 90, 100	syl2anc 408	. . . . . . . . . . . . . 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 3484	. . . . . . . . . . . 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 2172	. . . . . . . . . . 11 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` k ) = (/) )
105	91, 104	sseqtrd 3135	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> ( P ` suc k ) C_ (/) )
106		ss0 3403	. . . . . . . . . 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 4460	. . . . . . . . . . . 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 519	. . . . . . . . . . . 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 654	. . . . . . . . . 10 |- ( ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) /\ N e. suc k ) -> -. suc k e. N )
114	113	iffalsed 3484	. . . . . . . . 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 2175	. . . . . . . 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 4509	. . . . . . . . . 10 |- ( k e. om -> suc k e. om )
117	116	ad2antrr 479	. . . . . . . . 9 |- ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) -> suc k e. om )
118		nntri3or 6389	. . . . . . . . 9 |- ( ( suc k e. om /\ N e. om ) -> ( suc k e. N \/ suc k = N \/ N e. suc k ) )
119	117, 69, 118	syl2anc 408	. . . . . . . 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 1285	. . . . . . 7 |- ( ( ( k e. om /\ ph ) /\ ( P ` k ) = if ( k e. N , 1o , (/) ) ) -> ( P ` suc k ) = if ( suc k e. N , 1o , (/) ) )
121	120	exp31 361	. . . . . 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 4514	. . . 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 6396	. . . . . 6 |- ( ( j e. om /\ N e. om ) -> DECID j e. N )
130	125, 128, 129	syl2anc 408	. . . . 5 |- ( ( ph /\ j e. om ) -> DECID j e. N )
131	126, 127, 130	ifcldcd 3507	. . . 4 |- ( ( ph /\ j e. om ) -> if ( j e. N , 1o , (/) ) e. 2o )
132		eleq1w 2200	. . . . . 6 |- ( i = j -> ( i e. N <-> j e. N ) )
133	132	ifbid 3493	. . . . 5 |- ( i = j -> if ( i e. N , 1o , (/) ) = if ( j e. N , 1o , (/) ) )
134	133, 16	fvmptg 5497	. . . 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 408	. . 3 |- ( ( ph /\ j e. om ) -> ( ( i e. om |-> if ( i e. N , 1o , (/) ) ) ` j ) = if ( j e. N , 1o , (/) ) )
136	124, 135	eqtr4d 2175	. 2 |- ( ( ph /\ j e. om ) -> ( P ` j ) = ( ( i e. om |-> if ( i e. N , 1o , (/) ) ) ` j ) )
137	4, 18, 136	eqfnfvd 5521	1 |- ( ph -> P = ( i e. om |-> if ( i e. N , 1o , (/) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   \/ wo 697  DECID wdc 819   \/ w3o 961   = wceq 1331   e. wcel 1480   A.wral 2416   C_ wss 3071   (/)c0 3363   ifcif 3474   |-> cmpt 3989   Tr wtr 4026   Ord word 4284   suc csuc 4287   omcom 4504   Fn wfn 5118   -->wf 5119   ` cfv 5123  (class class class)co 5774   1oc1o 6306   2oc2o 6307   ^m cmap 6542  ℕ_∞xnninf 7005

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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502

This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-iord 4288  df-on 4290  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-fv 5131  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1o 6313  df-2o 6314  df-map 6544  df-nninf 7007

This theorem is referenced by:  nninfalllem1  13203  nninfsellemeq  13210