ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nnnninfeq GIF version

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

Proof of Theorem nnnninfeq
Dummy variables 𝑗 𝑘 𝑤 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnnninfeq.p . . . 4 (𝜑𝑃 ∈ ℕ)
2 nninff 7115 . . . 4 (𝑃 ∈ ℕ𝑃:ω⟶2o)
31, 2syl 14 . . 3 (𝜑𝑃:ω⟶2o)
43ffnd 5362 . 2 (𝜑𝑃 Fn ω)
5 1lt2o 6437 . . . . . 6 1o ∈ 2o
65a1i 9 . . . . 5 ((𝜑𝑖 ∈ ω) → 1o ∈ 2o)
7 0lt2o 6436 . . . . . 6 ∅ ∈ 2o
87a1i 9 . . . . 5 ((𝜑𝑖 ∈ ω) → ∅ ∈ 2o)
9 simpr 110 . . . . . 6 ((𝜑𝑖 ∈ ω) → 𝑖 ∈ ω)
10 nnnninfeq.n . . . . . . 7 (𝜑𝑁 ∈ ω)
1110adantr 276 . . . . . 6 ((𝜑𝑖 ∈ ω) → 𝑁 ∈ ω)
12 nndcel 6495 . . . . . 6 ((𝑖 ∈ ω ∧ 𝑁 ∈ ω) → DECID 𝑖𝑁)
139, 11, 12syl2anc 411 . . . . 5 ((𝜑𝑖 ∈ ω) → DECID 𝑖𝑁)
146, 8, 13ifcldcd 3569 . . . 4 ((𝜑𝑖 ∈ ω) → if(𝑖𝑁, 1o, ∅) ∈ 2o)
1514ralrimiva 2550 . . 3 (𝜑 → ∀𝑖 ∈ ω if(𝑖𝑁, 1o, ∅) ∈ 2o)
16 eqid 2177 . . . 4 (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) = (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))
1716fnmpt 5338 . . 3 (∀𝑖 ∈ ω if(𝑖𝑁, 1o, ∅) ∈ 2o → (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) Fn ω)
1815, 17syl 14 . 2 (𝜑 → (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)) Fn ω)
19 fveq2 5511 . . . . . . 7 (𝑤 = ∅ → (𝑃𝑤) = (𝑃‘∅))
20 eleq1 2240 . . . . . . . 8 (𝑤 = ∅ → (𝑤𝑁 ↔ ∅ ∈ 𝑁))
2120ifbid 3555 . . . . . . 7 (𝑤 = ∅ → if(𝑤𝑁, 1o, ∅) = if(∅ ∈ 𝑁, 1o, ∅))
2219, 21eqeq12d 2192 . . . . . 6 (𝑤 = ∅ → ((𝑃𝑤) = if(𝑤𝑁, 1o, ∅) ↔ (𝑃‘∅) = if(∅ ∈ 𝑁, 1o, ∅)))
2322imbi2d 230 . . . . 5 (𝑤 = ∅ → ((𝜑 → (𝑃𝑤) = if(𝑤𝑁, 1o, ∅)) ↔ (𝜑 → (𝑃‘∅) = if(∅ ∈ 𝑁, 1o, ∅))))
24 fveq2 5511 . . . . . . 7 (𝑤 = 𝑘 → (𝑃𝑤) = (𝑃𝑘))
25 eleq1w 2238 . . . . . . . 8 (𝑤 = 𝑘 → (𝑤𝑁𝑘𝑁))
2625ifbid 3555 . . . . . . 7 (𝑤 = 𝑘 → if(𝑤𝑁, 1o, ∅) = if(𝑘𝑁, 1o, ∅))
2724, 26eqeq12d 2192 . . . . . 6 (𝑤 = 𝑘 → ((𝑃𝑤) = if(𝑤𝑁, 1o, ∅) ↔ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)))
2827imbi2d 230 . . . . 5 (𝑤 = 𝑘 → ((𝜑 → (𝑃𝑤) = if(𝑤𝑁, 1o, ∅)) ↔ (𝜑 → (𝑃𝑘) = if(𝑘𝑁, 1o, ∅))))
29 fveq2 5511 . . . . . . 7 (𝑤 = suc 𝑘 → (𝑃𝑤) = (𝑃‘suc 𝑘))
30 eleq1 2240 . . . . . . . 8 (𝑤 = suc 𝑘 → (𝑤𝑁 ↔ suc 𝑘𝑁))
3130ifbid 3555 . . . . . . 7 (𝑤 = suc 𝑘 → if(𝑤𝑁, 1o, ∅) = if(suc 𝑘𝑁, 1o, ∅))
3229, 31eqeq12d 2192 . . . . . 6 (𝑤 = suc 𝑘 → ((𝑃𝑤) = if(𝑤𝑁, 1o, ∅) ↔ (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅)))
3332imbi2d 230 . . . . 5 (𝑤 = suc 𝑘 → ((𝜑 → (𝑃𝑤) = if(𝑤𝑁, 1o, ∅)) ↔ (𝜑 → (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅))))
34 fveq2 5511 . . . . . . 7 (𝑤 = 𝑗 → (𝑃𝑤) = (𝑃𝑗))
35 eleq1w 2238 . . . . . . . 8 (𝑤 = 𝑗 → (𝑤𝑁𝑗𝑁))
3635ifbid 3555 . . . . . . 7 (𝑤 = 𝑗 → if(𝑤𝑁, 1o, ∅) = if(𝑗𝑁, 1o, ∅))
3734, 36eqeq12d 2192 . . . . . 6 (𝑤 = 𝑗 → ((𝑃𝑤) = if(𝑤𝑁, 1o, ∅) ↔ (𝑃𝑗) = if(𝑗𝑁, 1o, ∅)))
3837imbi2d 230 . . . . 5 (𝑤 = 𝑗 → ((𝜑 → (𝑃𝑤) = if(𝑤𝑁, 1o, ∅)) ↔ (𝜑 → (𝑃𝑗) = if(𝑗𝑁, 1o, ∅))))
39 noel 3426 . . . . . . . . 9 ¬ ∅ ∈ ∅
40 simpr 110 . . . . . . . . . 10 ((𝜑𝑁 = ∅) → 𝑁 = ∅)
4140eleq2d 2247 . . . . . . . . 9 ((𝜑𝑁 = ∅) → (∅ ∈ 𝑁 ↔ ∅ ∈ ∅))
4239, 41mtbiri 675 . . . . . . . 8 ((𝜑𝑁 = ∅) → ¬ ∅ ∈ 𝑁)
4342iffalsed 3544 . . . . . . 7 ((𝜑𝑁 = ∅) → if(∅ ∈ 𝑁, 1o, ∅) = ∅)
44 nnnninfeq.0 . . . . . . . 8 (𝜑 → (𝑃𝑁) = ∅)
4544adantr 276 . . . . . . 7 ((𝜑𝑁 = ∅) → (𝑃𝑁) = ∅)
4640fveq2d 5515 . . . . . . 7 ((𝜑𝑁 = ∅) → (𝑃𝑁) = (𝑃‘∅))
4743, 45, 463eqtr2rd 2217 . . . . . 6 ((𝜑𝑁 = ∅) → (𝑃‘∅) = if(∅ ∈ 𝑁, 1o, ∅))
48 fveq2 5511 . . . . . . . . 9 (𝑥 = ∅ → (𝑃𝑥) = (𝑃‘∅))
4948eqeq1d 2186 . . . . . . . 8 (𝑥 = ∅ → ((𝑃𝑥) = 1o ↔ (𝑃‘∅) = 1o))
50 nnnninfeq.1 . . . . . . . . 9 (𝜑 → ∀𝑥𝑁 (𝑃𝑥) = 1o)
5150adantr 276 . . . . . . . 8 ((𝜑 ∧ ∅ ∈ 𝑁) → ∀𝑥𝑁 (𝑃𝑥) = 1o)
52 simpr 110 . . . . . . . 8 ((𝜑 ∧ ∅ ∈ 𝑁) → ∅ ∈ 𝑁)
5349, 51, 52rspcdva 2846 . . . . . . 7 ((𝜑 ∧ ∅ ∈ 𝑁) → (𝑃‘∅) = 1o)
5452iftrued 3541 . . . . . . 7 ((𝜑 ∧ ∅ ∈ 𝑁) → if(∅ ∈ 𝑁, 1o, ∅) = 1o)
5553, 54eqtr4d 2213 . . . . . 6 ((𝜑 ∧ ∅ ∈ 𝑁) → (𝑃‘∅) = if(∅ ∈ 𝑁, 1o, ∅))
56 0elnn 4615 . . . . . . 7 (𝑁 ∈ ω → (𝑁 = ∅ ∨ ∅ ∈ 𝑁))
5710, 56syl 14 . . . . . 6 (𝜑 → (𝑁 = ∅ ∨ ∅ ∈ 𝑁))
5847, 55, 57mpjaodan 798 . . . . 5 (𝜑 → (𝑃‘∅) = if(∅ ∈ 𝑁, 1o, ∅))
59 fveq2 5511 . . . . . . . . . . 11 (𝑥 = suc 𝑘 → (𝑃𝑥) = (𝑃‘suc 𝑘))
6059eqeq1d 2186 . . . . . . . . . 10 (𝑥 = suc 𝑘 → ((𝑃𝑥) = 1o ↔ (𝑃‘suc 𝑘) = 1o))
6150ad3antlr 493 . . . . . . . . . 10 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘𝑁) → ∀𝑥𝑁 (𝑃𝑥) = 1o)
62 simpr 110 . . . . . . . . . 10 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘𝑁) → suc 𝑘𝑁)
6360, 61, 62rspcdva 2846 . . . . . . . . 9 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘𝑁) → (𝑃‘suc 𝑘) = 1o)
6462iftrued 3541 . . . . . . . . 9 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘𝑁) → if(suc 𝑘𝑁, 1o, ∅) = 1o)
6563, 64eqtr4d 2213 . . . . . . . 8 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘𝑁) → (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅))
6644ad3antlr 493 . . . . . . . . 9 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → (𝑃𝑁) = ∅)
67 simpr 110 . . . . . . . . . 10 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → suc 𝑘 = 𝑁)
6867fveq2d 5515 . . . . . . . . 9 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → (𝑃‘suc 𝑘) = (𝑃𝑁))
6910ad2antlr 489 . . . . . . . . . . . . 13 (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) → 𝑁 ∈ ω)
70 nnord 4608 . . . . . . . . . . . . 13 (𝑁 ∈ ω → Ord 𝑁)
71 ordirr 4538 . . . . . . . . . . . . 13 (Ord 𝑁 → ¬ 𝑁𝑁)
7269, 70, 713syl 17 . . . . . . . . . . . 12 (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) → ¬ 𝑁𝑁)
7372adantr 276 . . . . . . . . . . 11 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → ¬ 𝑁𝑁)
7467, 73eqneltrd 2273 . . . . . . . . . 10 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → ¬ suc 𝑘𝑁)
7574iffalsed 3544 . . . . . . . . 9 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → if(suc 𝑘𝑁, 1o, ∅) = ∅)
7666, 68, 753eqtr4d 2220 . . . . . . . 8 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅))
77 suceq 4399 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → suc 𝑗 = suc 𝑘)
7877fveq2d 5515 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → (𝑃‘suc 𝑗) = (𝑃‘suc 𝑘))
79 fveq2 5511 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → (𝑃𝑗) = (𝑃𝑘))
8078, 79sseq12d 3186 . . . . . . . . . . . 12 (𝑗 = 𝑘 → ((𝑃‘suc 𝑗) ⊆ (𝑃𝑗) ↔ (𝑃‘suc 𝑘) ⊆ (𝑃𝑘)))
811ad3antlr 493 . . . . . . . . . . . . 13 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → 𝑃 ∈ ℕ)
82 fveq1 5510 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑃 → (𝑓‘suc 𝑗) = (𝑃‘suc 𝑗))
83 fveq1 5510 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑃 → (𝑓𝑗) = (𝑃𝑗))
8482, 83sseq12d 3186 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑃 → ((𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ (𝑃‘suc 𝑗) ⊆ (𝑃𝑗)))
8584ralbidv 2477 . . . . . . . . . . . . . . 15 (𝑓 = 𝑃 → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃𝑗)))
86 df-nninf 7113 . . . . . . . . . . . . . . 15 = {𝑓 ∈ (2o𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗)}
8785, 86elrab2 2896 . . . . . . . . . . . . . 14 (𝑃 ∈ ℕ ↔ (𝑃 ∈ (2o𝑚 ω) ∧ ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃𝑗)))
8887simprbi 275 . . . . . . . . . . . . 13 (𝑃 ∈ ℕ → ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃𝑗))
8981, 88syl 14 . . . . . . . . . . . 12 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃𝑗))
90 simplll 533 . . . . . . . . . . . 12 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → 𝑘 ∈ ω)
9180, 89, 90rspcdva 2846 . . . . . . . . . . 11 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃‘suc 𝑘) ⊆ (𝑃𝑘))
92 simplr 528 . . . . . . . . . . . 12 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃𝑘) = if(𝑘𝑁, 1o, ∅))
93 simpr 110 . . . . . . . . . . . . . . 15 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → 𝑁 ∈ suc 𝑘)
94 nnord 4608 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ω → Ord 𝑘)
95 ordtr 4375 . . . . . . . . . . . . . . . 16 (Ord 𝑘 → Tr 𝑘)
96 trsucss 4420 . . . . . . . . . . . . . . . 16 (Tr 𝑘 → (𝑁 ∈ suc 𝑘𝑁𝑘))
9794, 95, 963syl 17 . . . . . . . . . . . . . . 15 (𝑘 ∈ ω → (𝑁 ∈ suc 𝑘𝑁𝑘))
9890, 93, 97sylc 62 . . . . . . . . . . . . . 14 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → 𝑁𝑘)
9969adantr 276 . . . . . . . . . . . . . . 15 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → 𝑁 ∈ ω)
100 nntri1 6491 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ω ∧ 𝑘 ∈ ω) → (𝑁𝑘 ↔ ¬ 𝑘𝑁))
10199, 90, 100syl2anc 411 . . . . . . . . . . . . . 14 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑁𝑘 ↔ ¬ 𝑘𝑁))
10298, 101mpbid 147 . . . . . . . . . . . . 13 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → ¬ 𝑘𝑁)
103102iffalsed 3544 . . . . . . . . . . . 12 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → if(𝑘𝑁, 1o, ∅) = ∅)
10492, 103eqtrd 2210 . . . . . . . . . . 11 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃𝑘) = ∅)
10591, 104sseqtrd 3193 . . . . . . . . . 10 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃‘suc 𝑘) ⊆ ∅)
106 ss0 3463 . . . . . . . . . 10 ((𝑃‘suc 𝑘) ⊆ ∅ → (𝑃‘suc 𝑘) = ∅)
107105, 106syl 14 . . . . . . . . 9 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃‘suc 𝑘) = ∅)
108 ordn2lp 4541 . . . . . . . . . . . 12 (Ord 𝑁 → ¬ (𝑁 ∈ suc 𝑘 ∧ suc 𝑘𝑁))
10999, 70, 1083syl 17 . . . . . . . . . . 11 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → ¬ (𝑁 ∈ suc 𝑘 ∧ suc 𝑘𝑁))
110 simplr 528 . . . . . . . . . . . 12 (((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) ∧ suc 𝑘𝑁) → 𝑁 ∈ suc 𝑘)
111 simpr 110 . . . . . . . . . . . 12 (((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) ∧ suc 𝑘𝑁) → suc 𝑘𝑁)
112110, 111jca 306 . . . . . . . . . . 11 (((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) ∧ suc 𝑘𝑁) → (𝑁 ∈ suc 𝑘 ∧ suc 𝑘𝑁))
113109, 112mtand 665 . . . . . . . . . 10 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → ¬ suc 𝑘𝑁)
114113iffalsed 3544 . . . . . . . . 9 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → if(suc 𝑘𝑁, 1o, ∅) = ∅)
115107, 114eqtr4d 2213 . . . . . . . 8 ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅))
116 peano2 4591 . . . . . . . . . 10 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
117116ad2antrr 488 . . . . . . . . 9 (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) → suc 𝑘 ∈ ω)
118 nntri3or 6488 . . . . . . . . 9 ((suc 𝑘 ∈ ω ∧ 𝑁 ∈ ω) → (suc 𝑘𝑁 ∨ suc 𝑘 = 𝑁𝑁 ∈ suc 𝑘))
119117, 69, 118syl2anc 411 . . . . . . . 8 (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) → (suc 𝑘𝑁 ∨ suc 𝑘 = 𝑁𝑁 ∈ suc 𝑘))
12065, 76, 115, 119mpjao3dan 1307 . . . . . . 7 (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) → (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅))
121120exp31 364 . . . . . 6 (𝑘 ∈ ω → (𝜑 → ((𝑃𝑘) = if(𝑘𝑁, 1o, ∅) → (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅))))
122121a2d 26 . . . . 5 (𝑘 ∈ ω → ((𝜑 → (𝑃𝑘) = if(𝑘𝑁, 1o, ∅)) → (𝜑 → (𝑃‘suc 𝑘) = if(suc 𝑘𝑁, 1o, ∅))))
12323, 28, 33, 38, 58, 122finds 4596 . . . 4 (𝑗 ∈ ω → (𝜑 → (𝑃𝑗) = if(𝑗𝑁, 1o, ∅)))
124123impcom 125 . . 3 ((𝜑𝑗 ∈ ω) → (𝑃𝑗) = if(𝑗𝑁, 1o, ∅))
125 simpr 110 . . . 4 ((𝜑𝑗 ∈ ω) → 𝑗 ∈ ω)
1265a1i 9 . . . . 5 ((𝜑𝑗 ∈ ω) → 1o ∈ 2o)
1277a1i 9 . . . . 5 ((𝜑𝑗 ∈ ω) → ∅ ∈ 2o)
12810adantr 276 . . . . . 6 ((𝜑𝑗 ∈ ω) → 𝑁 ∈ ω)
129 nndcel 6495 . . . . . 6 ((𝑗 ∈ ω ∧ 𝑁 ∈ ω) → DECID 𝑗𝑁)
130125, 128, 129syl2anc 411 . . . . 5 ((𝜑𝑗 ∈ ω) → DECID 𝑗𝑁)
131126, 127, 130ifcldcd 3569 . . . 4 ((𝜑𝑗 ∈ ω) → if(𝑗𝑁, 1o, ∅) ∈ 2o)
132 eleq1w 2238 . . . . . 6 (𝑖 = 𝑗 → (𝑖𝑁𝑗𝑁))
133132ifbid 3555 . . . . 5 (𝑖 = 𝑗 → if(𝑖𝑁, 1o, ∅) = if(𝑗𝑁, 1o, ∅))
134133, 16fvmptg 5588 . . . 4 ((𝑗 ∈ ω ∧ if(𝑗𝑁, 1o, ∅) ∈ 2o) → ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑗) = if(𝑗𝑁, 1o, ∅))
135125, 131, 134syl2anc 411 . . 3 ((𝜑𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑗) = if(𝑗𝑁, 1o, ∅))
136124, 135eqtr4d 2213 . 2 ((𝜑𝑗 ∈ ω) → (𝑃𝑗) = ((𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅))‘𝑗))
1374, 18, 136eqfnfvd 5612 1 (𝜑𝑃 = (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  DECID wdc 834  w3o 977   = wceq 1353  wcel 2148  wral 2455  wss 3129  c0 3422  ifcif 3534  cmpt 4061  Tr wtr 4098  Ord word 4359  suc csuc 4362  ωcom 4586   Fn wfn 5207  wf 5208  cfv 5212  (class class class)co 5869  1oc1o 6404  2oc2o 6405  𝑚 cmap 6642  xnninf 7112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-iord 4363  df-on 4365  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-fv 5220  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1o 6411  df-2o 6412  df-map 6644  df-nninf 7113
This theorem is referenced by:  nnnninfeq2  7121  nninfisollem0  7122  nninfalllem1  14413  nninfsellemeq  14419
  Copyright terms: Public domain W3C validator