Mathbox for Jim Kingdon < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  nninfalllemn GIF version

Theorem nninfalllemn 13375
 Description: Lemma for nninfall 13377. Mapping of a natural number to an element of ℕ∞. (Contributed by Jim Kingdon, 4-Aug-2022.)
Hypotheses
Ref Expression
nninfalllemn.p (𝜑𝑃 ∈ ℕ)
nninfalllemn.n (𝜑𝑁 ∈ ω)
nninfalllemn.1 (𝜑 → ∀𝑥𝑁 (𝑃𝑥) = 1o)
nninfalllemn.0 (𝜑 → (𝑃𝑁) = ∅)
Assertion
Ref Expression
nninfalllemn (𝜑𝑃 = (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)))
Distinct variable groups:   𝑖,𝑁   𝑥,𝑁   𝑥,𝑃   𝜑,𝑖
Allowed substitution hints:   𝜑(𝑥)   𝑃(𝑖)

Proof of Theorem nninfalllemn
Dummy variables 𝑗 𝑘 𝑤 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nninfalllemn.p . . . 4 (𝜑𝑃 ∈ ℕ)
2 nninff 13371 . . . 4 (𝑃 ∈ ℕ𝑃:ω⟶2o)
31, 2syl 14 . . 3 (𝜑𝑃:ω⟶2o)
43ffnd 5280 . 2 (𝜑𝑃 Fn ω)
5 1lt2o 6346 . . . . . 6 1o ∈ 2o
65a1i 9 . . . . 5 ((𝜑𝑖 ∈ ω) → 1o ∈ 2o)
7 0lt2o 6345 . . . . . 6 ∅ ∈ 2o
87a1i 9 . . . . 5 ((𝜑𝑖 ∈ ω) → ∅ ∈ 2o)
9 simpr 109 . . . . . 6 ((𝜑𝑖 ∈ ω) → 𝑖 ∈ ω)
10 nninfalllemn.n . . . . . . 7 (𝜑𝑁 ∈ ω)
1110adantr 274 . . . . . 6 ((𝜑𝑖 ∈ ω) → 𝑁 ∈ ω)
12 nndcel 6403 . . . . . 6 ((𝑖 ∈ ω ∧ 𝑁 ∈ ω) → DECID 𝑖𝑁)
139, 11, 12syl2anc 409 . . . . 5 ((𝜑𝑖 ∈ ω) → DECID 𝑖𝑁)
146, 8, 13ifcldcd 3511 . . . 4 ((𝜑𝑖 ∈ ω) → if(𝑖𝑁, 1o, ∅) ∈ 2o)
1514ralrimiva 2508 . . 3 (𝜑 → ∀𝑖 ∈ ω if(𝑖𝑁, 1o, ∅) ∈ 2o)
16 eqid 2140 . . . 4 (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))
1716fnmpt 5256 . . 3 (∀𝑖 ∈ ω if(𝑖𝑁, 1o, ∅) ∈ 2o → (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) Fn ω)
1815, 17syl 14 . 2 (𝜑 → (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) Fn ω)
19 fveq2 5428 . . . . . . 7 (𝑤 = ∅ → (𝑃𝑤) = (𝑃‘∅))
20 eleq1 2203 . . . . . . . 8 (𝑤 = ∅ → (𝑤𝑁 ↔ ∅ ∈ 𝑁))
2120ifbid 3497 . . . . . . 7 (𝑤 = ∅ → if(𝑤𝑁, 1o, ∅) = if(∅ ∈ 𝑁, 1o, ∅))
2219, 21eqeq12d 2155 . . . . . 6 (𝑤 = ∅ → ((𝑃𝑤) = if(𝑤𝑁, 1o, ∅) ↔ (𝑃‘∅) = if(∅ ∈ 𝑁, 1o, ∅)))
2322imbi2d 229 . . . . 5 (𝑤 = ∅ → ((𝜑 → (𝑃𝑤) = if(𝑤𝑁, 1o, ∅)) ↔ (𝜑 → (𝑃‘∅) = if(∅ ∈ 𝑁, 1o, ∅))))
24 fveq2 5428 . . . . . . 7 (𝑤 = 𝑘 → (𝑃𝑤) = (𝑃𝑘))
25 eleq1w 2201 . . . . . . . 8 (𝑤 = 𝑘 → (𝑤𝑁𝑘𝑁))
2625ifbid 3497 . . . . . . 7 (𝑤 = 𝑘 → if(𝑤𝑁, 1o, ∅) = if(𝑘𝑁, 1o, ∅))
2724, 26eqeq12d 2155 . . . . . 6 (𝑤 = 𝑘 → ((𝑃𝑤) = if(𝑤𝑁, 1o, ∅) ↔ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)))
2827imbi2d 229 . . . . 5 (𝑤 = 𝑘 → ((𝜑 → (𝑃𝑤) = if(𝑤𝑁, 1o, ∅)) ↔ (𝜑 → (𝑃𝑘) = if(𝑘𝑁, 1o, ∅))))
29 fveq2 5428 . . . . . . 7 (𝑤 = suc 𝑘 → (𝑃𝑤) = (𝑃‘suc 𝑘))
30 eleq1 2203 . . . . . . . 8 (𝑤 = suc 𝑘 → (𝑤𝑁 ↔ suc 𝑘𝑁))
3130ifbid 3497 . . . . . . 7 (𝑤 = suc 𝑘 → if(𝑤𝑁, 1o, ∅) = if(suc 𝑘𝑁, 1o, ∅))
3229, 31eqeq12d 2155 . . . . . 6 (𝑤 = suc 𝑘 → ((𝑃𝑤) = if(𝑤𝑁, 1o, ∅) ↔ (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅)))
3332imbi2d 229 . . . . 5 (𝑤 = suc 𝑘 → ((𝜑 → (𝑃𝑤) = if(𝑤𝑁, 1o, ∅)) ↔ (𝜑 → (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅))))
34 fveq2 5428 . . . . . . 7 (𝑤 = 𝑗 → (𝑃𝑤) = (𝑃𝑗))
35 eleq1w 2201 . . . . . . . 8 (𝑤 = 𝑗 → (𝑤𝑁𝑗𝑁))
3635ifbid 3497 . . . . . . 7 (𝑤 = 𝑗 → if(𝑤𝑁, 1o, ∅) = if(𝑗𝑁, 1o, ∅))
3734, 36eqeq12d 2155 . . . . . 6 (𝑤 = 𝑗 → ((𝑃𝑤) = if(𝑤𝑁, 1o, ∅) ↔ (𝑃𝑗) = if(𝑗𝑁, 1o, ∅)))
3837imbi2d 229 . . . . 5 (𝑤 = 𝑗 → ((𝜑 → (𝑃𝑤) = if(𝑤𝑁, 1o, ∅)) ↔ (𝜑 → (𝑃𝑗) = if(𝑗𝑁, 1o, ∅))))
39 noel 3371 . . . . . . . . 9 ¬ ∅ ∈ ∅
40 simpr 109 . . . . . . . . . 10 ((𝜑𝑁 = ∅) → 𝑁 = ∅)
4140eleq2d 2210 . . . . . . . . 9 ((𝜑𝑁 = ∅) → (∅ ∈ 𝑁 ↔ ∅ ∈ ∅))
4239, 41mtbiri 665 . . . . . . . 8 ((𝜑𝑁 = ∅) → ¬ ∅ ∈ 𝑁)
4342iffalsed 3488 . . . . . . 7 ((𝜑𝑁 = ∅) → if(∅ ∈ 𝑁, 1o, ∅) = ∅)
44 nninfalllemn.0 . . . . . . . 8 (𝜑 → (𝑃𝑁) = ∅)
4544adantr 274 . . . . . . 7 ((𝜑𝑁 = ∅) → (𝑃𝑁) = ∅)
4640fveq2d 5432 . . . . . . 7 ((𝜑𝑁 = ∅) → (𝑃𝑁) = (𝑃‘∅))
4743, 45, 463eqtr2rd 2180 . . . . . 6 ((𝜑𝑁 = ∅) → (𝑃‘∅) = if(∅ ∈ 𝑁, 1o, ∅))
48 fveq2 5428 . . . . . . . . 9 (𝑥 = ∅ → (𝑃𝑥) = (𝑃‘∅))
4948eqeq1d 2149 . . . . . . . 8 (𝑥 = ∅ → ((𝑃𝑥) = 1o ↔ (𝑃‘∅) = 1o))
50 nninfalllemn.1 . . . . . . . . 9 (𝜑 → ∀𝑥𝑁 (𝑃𝑥) = 1o)
5150adantr 274 . . . . . . . 8 ((𝜑 ∧ ∅ ∈ 𝑁) → ∀𝑥𝑁 (𝑃𝑥) = 1o)
52 simpr 109 . . . . . . . 8 ((𝜑 ∧ ∅ ∈ 𝑁) → ∅ ∈ 𝑁)
5349, 51, 52rspcdva 2797 . . . . . . 7 ((𝜑 ∧ ∅ ∈ 𝑁) → (𝑃‘∅) = 1o)
5452iftrued 3485 . . . . . . 7 ((𝜑 ∧ ∅ ∈ 𝑁) → if(∅ ∈ 𝑁, 1o, ∅) = 1o)
5553, 54eqtr4d 2176 . . . . . 6 ((𝜑 ∧ ∅ ∈ 𝑁) → (𝑃‘∅) = if(∅ ∈ 𝑁, 1o, ∅))
56 0elnn 4539 . . . . . . 7 (𝑁 ∈ ω → (𝑁 = ∅ ∨ ∅ ∈ 𝑁))
5710, 56syl 14 . . . . . 6 (𝜑 → (𝑁 = ∅ ∨ ∅ ∈ 𝑁))
5847, 55, 57mpjaodan 788 . . . . 5 (𝜑 → (𝑃‘∅) = if(∅ ∈ 𝑁, 1o, ∅))
59 fveq2 5428 . . . . . . . . . . 11 (𝑥 = suc 𝑘 → (𝑃𝑥) = (𝑃‘suc 𝑘))
6059eqeq1d 2149 . . . . . . . . . 10 (𝑥 = suc 𝑘 → ((𝑃𝑥) = 1o ↔ (𝑃‘suc 𝑘) = 1o))
6150ad3antlr 485 . . . . . . . . . 10 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘𝑁) → ∀𝑥𝑁 (𝑃𝑥) = 1o)
62 simpr 109 . . . . . . . . . 10 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘𝑁) → suc 𝑘𝑁)
6360, 61, 62rspcdva 2797 . . . . . . . . 9 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘𝑁) → (𝑃‘suc 𝑘) = 1o)
6462iftrued 3485 . . . . . . . . 9 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘𝑁) → if(suc 𝑘𝑁, 1o, ∅) = 1o)
6563, 64eqtr4d 2176 . . . . . . . 8 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘𝑁) → (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅))
6644ad3antlr 485 . . . . . . . . 9 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → (𝑃𝑁) = ∅)
67 simpr 109 . . . . . . . . . 10 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → suc 𝑘 = 𝑁)
6867fveq2d 5432 . . . . . . . . 9 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → (𝑃‘suc 𝑘) = (𝑃𝑁))
6910ad2antlr 481 . . . . . . . . . . . . 13 (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) → 𝑁 ∈ ω)
70 nnord 4532 . . . . . . . . . . . . 13 (𝑁 ∈ ω → Ord 𝑁)
71 ordirr 4464 . . . . . . . . . . . . 13 (Ord 𝑁 → ¬ 𝑁𝑁)
7269, 70, 713syl 17 . . . . . . . . . . . 12 (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) → ¬ 𝑁𝑁)
7372adantr 274 . . . . . . . . . . 11 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → ¬ 𝑁𝑁)
7467, 73eqneltrd 2236 . . . . . . . . . 10 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → ¬ suc 𝑘𝑁)
7574iffalsed 3488 . . . . . . . . 9 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → if(suc 𝑘𝑁, 1o, ∅) = ∅)
7666, 68, 753eqtr4d 2183 . . . . . . . 8 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅))
77 suceq 4331 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → suc 𝑗 = suc 𝑘)
7877fveq2d 5432 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → (𝑃‘suc 𝑗) = (𝑃‘suc 𝑘))
79 fveq2 5428 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → (𝑃𝑗) = (𝑃𝑘))
8078, 79sseq12d 3132 . . . . . . . . . . . 12 (𝑗 = 𝑘 → ((𝑃‘suc 𝑗) ⊆ (𝑃𝑗) ↔ (𝑃‘suc 𝑘) ⊆ (𝑃𝑘)))
811ad3antlr 485 . . . . . . . . . . . . 13 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → 𝑃 ∈ ℕ)
82 fveq1 5427 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑃 → (𝑓‘suc 𝑗) = (𝑃‘suc 𝑗))
83 fveq1 5427 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑃 → (𝑓𝑗) = (𝑃𝑗))
8482, 83sseq12d 3132 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑃 → ((𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ (𝑃‘suc 𝑗) ⊆ (𝑃𝑗)))
8584ralbidv 2438 . . . . . . . . . . . . . . 15 (𝑓 = 𝑃 → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃𝑗)))
86 df-nninf 7014 . . . . . . . . . . . . . . 15 = {𝑓 ∈ (2o𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗)}
8785, 86elrab2 2846 . . . . . . . . . . . . . 14 (𝑃 ∈ ℕ ↔ (𝑃 ∈ (2o𝑚 ω) ∧ ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃𝑗)))
8887simprbi 273 . . . . . . . . . . . . 13 (𝑃 ∈ ℕ → ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃𝑗))
8981, 88syl 14 . . . . . . . . . . . 12 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃𝑗))
90 simplll 523 . . . . . . . . . . . 12 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → 𝑘 ∈ ω)
9180, 89, 90rspcdva 2797 . . . . . . . . . . 11 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃‘suc 𝑘) ⊆ (𝑃𝑘))
92 simplr 520 . . . . . . . . . . . 12 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃𝑘) = if(𝑘𝑁, 1o, ∅))
93 simpr 109 . . . . . . . . . . . . . . 15 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → 𝑁 ∈ suc 𝑘)
94 nnord 4532 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ω → Ord 𝑘)
95 ordtr 4307 . . . . . . . . . . . . . . . 16 (Ord 𝑘 → Tr 𝑘)
96 trsucss 4352 . . . . . . . . . . . . . . . 16 (Tr 𝑘 → (𝑁 ∈ suc 𝑘𝑁𝑘))
9794, 95, 963syl 17 . . . . . . . . . . . . . . 15 (𝑘 ∈ ω → (𝑁 ∈ suc 𝑘𝑁𝑘))
9890, 93, 97sylc 62 . . . . . . . . . . . . . 14 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → 𝑁𝑘)
9969adantr 274 . . . . . . . . . . . . . . 15 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → 𝑁 ∈ ω)
100 nntri1 6399 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ω ∧ 𝑘 ∈ ω) → (𝑁𝑘 ↔ ¬ 𝑘𝑁))
10199, 90, 100syl2anc 409 . . . . . . . . . . . . . 14 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑁𝑘 ↔ ¬ 𝑘𝑁))
10298, 101mpbid 146 . . . . . . . . . . . . 13 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → ¬ 𝑘𝑁)
103102iffalsed 3488 . . . . . . . . . . . 12 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → if(𝑘𝑁, 1o, ∅) = ∅)
10492, 103eqtrd 2173 . . . . . . . . . . 11 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃𝑘) = ∅)
10591, 104sseqtrd 3139 . . . . . . . . . 10 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃‘suc 𝑘) ⊆ ∅)
106 ss0 3407 . . . . . . . . . 10 ((𝑃‘suc 𝑘) ⊆ ∅ → (𝑃‘suc 𝑘) = ∅)
107105, 106syl 14 . . . . . . . . 9 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃‘suc 𝑘) = ∅)
108 ordn2lp 4467 . . . . . . . . . . . 12 (Ord 𝑁 → ¬ (𝑁 ∈ suc 𝑘 ∧ suc 𝑘𝑁))
10999, 70, 1083syl 17 . . . . . . . . . . 11 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → ¬ (𝑁 ∈ suc 𝑘 ∧ suc 𝑘𝑁))
110 simplr 520 . . . . . . . . . . . 12 (((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) ∧ suc 𝑘𝑁) → 𝑁 ∈ suc 𝑘)
111 simpr 109 . . . . . . . . . . . 12 (((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) ∧ suc 𝑘𝑁) → suc 𝑘𝑁)
112110, 111jca 304 . . . . . . . . . . 11 (((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) ∧ suc 𝑘𝑁) → (𝑁 ∈ suc 𝑘 ∧ suc 𝑘𝑁))
113109, 112mtand 655 . . . . . . . . . 10 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → ¬ suc 𝑘𝑁)
114113iffalsed 3488 . . . . . . . . 9 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → if(suc 𝑘𝑁, 1o, ∅) = ∅)
115107, 114eqtr4d 2176 . . . . . . . 8 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅))
116 peano2 4516 . . . . . . . . . 10 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
117116ad2antrr 480 . . . . . . . . 9 (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) → suc 𝑘 ∈ ω)
118 nntri3or 6396 . . . . . . . . 9 ((suc 𝑘 ∈ ω ∧ 𝑁 ∈ ω) → (suc 𝑘𝑁 ∨ suc 𝑘 = 𝑁𝑁 ∈ suc 𝑘))
119117, 69, 118syl2anc 409 . . . . . . . 8 (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) → (suc 𝑘𝑁 ∨ suc 𝑘 = 𝑁𝑁 ∈ suc 𝑘))
12065, 76, 115, 119mpjao3dan 1286 . . . . . . 7 (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) → (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅))
121120exp31 362 . . . . . 6 (𝑘 ∈ ω → (𝜑 → ((𝑃𝑘) = if(𝑘𝑁, 1o, ∅) → (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅))))
122121a2d 26 . . . . 5 (𝑘 ∈ ω → ((𝜑 → (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) → (𝜑 → (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅))))
12323, 28, 33, 38, 58, 122finds 4521 . . . 4 (𝑗 ∈ ω → (𝜑 → (𝑃𝑗) = if(𝑗𝑁, 1o, ∅)))
124123impcom 124 . . 3 ((𝜑𝑗 ∈ ω) → (𝑃𝑗) = if(𝑗𝑁, 1o, ∅))
125 simpr 109 . . . 4 ((𝜑𝑗 ∈ ω) → 𝑗 ∈ ω)
1265a1i 9 . . . . 5 ((𝜑𝑗 ∈ ω) → 1o ∈ 2o)
1277a1i 9 . . . . 5 ((𝜑𝑗 ∈ ω) → ∅ ∈ 2o)
12810adantr 274 . . . . . 6 ((𝜑𝑗 ∈ ω) → 𝑁 ∈ ω)
129 nndcel 6403 . . . . . 6 ((𝑗 ∈ ω ∧ 𝑁 ∈ ω) → DECID 𝑗𝑁)
130125, 128, 129syl2anc 409 . . . . 5 ((𝜑𝑗 ∈ ω) → DECID 𝑗𝑁)
131126, 127, 130ifcldcd 3511 . . . 4 ((𝜑𝑗 ∈ ω) → if(𝑗𝑁, 1o, ∅) ∈ 2o)
132 eleq1w 2201 . . . . . 6 (𝑖 = 𝑗 → (𝑖𝑁𝑗𝑁))
133132ifbid 3497 . . . . 5 (𝑖 = 𝑗 → if(𝑖𝑁, 1o, ∅) = if(𝑗𝑁, 1o, ∅))
134133, 16fvmptg 5504 . . . 4 ((𝑗 ∈ ω ∧ if(𝑗𝑁, 1o, ∅) ∈ 2o) → ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑗) = if(𝑗𝑁, 1o, ∅))
135125, 131, 134syl2anc 409 . . 3 ((𝜑𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑗) = if(𝑗𝑁, 1o, ∅))
136124, 135eqtr4d 2176 . 2 ((𝜑𝑗 ∈ ω) → (𝑃𝑗) = ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑗))
1374, 18, 136eqfnfvd 5528 1 (𝜑𝑃 = (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 820   ∨ w3o 962   = wceq 1332   ∈ wcel 1481  ∀wral 2417   ⊆ wss 3075  ∅c0 3367  ifcif 3478   ↦ cmpt 3996  Tr wtr 4033  Ord word 4291  suc csuc 4294  ωcom 4511   Fn wfn 5125  ⟶wf 5126  ‘cfv 5130  (class class class)co 5781  1oc1o 6313  2oc2o 6314   ↑𝑚 cmap 6549  ℕ∞xnninf 7012 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 4053  ax-nul 4061  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-setind 4459  ax-iinf 4509 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 2913  df-csb 3007  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-nul 3368  df-if 3479  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-int 3779  df-br 3937  df-opab 3997  df-mpt 3998  df-tr 4034  df-id 4222  df-iord 4295  df-on 4297  df-suc 4300  df-iom 4512  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-iota 5095  df-fun 5132  df-fn 5133  df-f 5134  df-fv 5138  df-ov 5784  df-oprab 5785  df-mpo 5786  df-1o 6320  df-2o 6321  df-map 6551  df-nninf 7014 This theorem is referenced by:  nninfalllem1  13376  nninfsellemeq  13383
 Copyright terms: Public domain W3C validator