| Step | Hyp | Ref
 | Expression | 
| 1 |   | nnnninfeq.p | 
. . . 4
⊢ (𝜑 → 𝑃 ∈
ℕ∞) | 
| 2 |   | nninff 7188 | 
. . . 4
⊢ (𝑃 ∈
ℕ∞ → 𝑃:ω⟶2o) | 
| 3 | 1, 2 | syl 14 | 
. . 3
⊢ (𝜑 → 𝑃:ω⟶2o) | 
| 4 | 3 | ffnd 5408 | 
. 2
⊢ (𝜑 → 𝑃 Fn ω) | 
| 5 |   | 1lt2o 6500 | 
. . . . . 6
⊢
1o ∈ 2o | 
| 6 | 5 | a1i 9 | 
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ω) → 1o ∈
2o) | 
| 7 |   | 0lt2o 6499 | 
. . . . . 6
⊢ ∅
∈ 2o | 
| 8 | 7 | a1i 9 | 
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ω) → ∅ ∈
2o) | 
| 9 |   | simpr 110 | 
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ω) → 𝑖 ∈ ω) | 
| 10 |   | nnnninfeq.n | 
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ω) | 
| 11 | 10 | adantr 276 | 
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ω) → 𝑁 ∈ ω) | 
| 12 |   | nndcel 6558 | 
. . . . . 6
⊢ ((𝑖 ∈ ω ∧ 𝑁 ∈ ω) →
DECID 𝑖
∈ 𝑁) | 
| 13 | 9, 11, 12 | syl2anc 411 | 
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ω) → DECID
𝑖 ∈ 𝑁) | 
| 14 | 6, 8, 13 | ifcldcd 3597 | 
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ ω) → if(𝑖 ∈ 𝑁, 1o, ∅) ∈
2o) | 
| 15 | 14 | ralrimiva 2570 | 
. . 3
⊢ (𝜑 → ∀𝑖 ∈ ω if(𝑖 ∈ 𝑁, 1o, ∅) ∈
2o) | 
| 16 |   | eqid 2196 | 
. . . 4
⊢ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) | 
| 17 | 16 | fnmpt 5384 | 
. . 3
⊢
(∀𝑖 ∈
ω if(𝑖 ∈ 𝑁, 1o, ∅) ∈
2o → (𝑖
∈ ω ↦ if(𝑖
∈ 𝑁, 1o,
∅)) Fn ω) | 
| 18 | 15, 17 | syl 14 | 
. 2
⊢ (𝜑 → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) Fn
ω) | 
| 19 |   | fveq2 5558 | 
. . . . . . 7
⊢ (𝑤 = ∅ → (𝑃‘𝑤) = (𝑃‘∅)) | 
| 20 |   | eleq1 2259 | 
. . . . . . . 8
⊢ (𝑤 = ∅ → (𝑤 ∈ 𝑁 ↔ ∅ ∈ 𝑁)) | 
| 21 | 20 | ifbid 3582 | 
. . . . . . 7
⊢ (𝑤 = ∅ → if(𝑤 ∈ 𝑁, 1o, ∅) = if(∅
∈ 𝑁, 1o,
∅)) | 
| 22 | 19, 21 | eqeq12d 2211 | 
. . . . . 6
⊢ (𝑤 = ∅ → ((𝑃‘𝑤) = if(𝑤 ∈ 𝑁, 1o, ∅) ↔ (𝑃‘∅) = if(∅
∈ 𝑁, 1o,
∅))) | 
| 23 | 22 | imbi2d 230 | 
. . . . 5
⊢ (𝑤 = ∅ → ((𝜑 → (𝑃‘𝑤) = if(𝑤 ∈ 𝑁, 1o, ∅)) ↔ (𝜑 → (𝑃‘∅) = if(∅ ∈ 𝑁, 1o,
∅)))) | 
| 24 |   | fveq2 5558 | 
. . . . . . 7
⊢ (𝑤 = 𝑘 → (𝑃‘𝑤) = (𝑃‘𝑘)) | 
| 25 |   | eleq1w 2257 | 
. . . . . . . 8
⊢ (𝑤 = 𝑘 → (𝑤 ∈ 𝑁 ↔ 𝑘 ∈ 𝑁)) | 
| 26 | 25 | ifbid 3582 | 
. . . . . . 7
⊢ (𝑤 = 𝑘 → if(𝑤 ∈ 𝑁, 1o, ∅) = if(𝑘 ∈ 𝑁, 1o, ∅)) | 
| 27 | 24, 26 | eqeq12d 2211 | 
. . . . . 6
⊢ (𝑤 = 𝑘 → ((𝑃‘𝑤) = if(𝑤 ∈ 𝑁, 1o, ∅) ↔ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅))) | 
| 28 | 27 | imbi2d 230 | 
. . . . 5
⊢ (𝑤 = 𝑘 → ((𝜑 → (𝑃‘𝑤) = if(𝑤 ∈ 𝑁, 1o, ∅)) ↔ (𝜑 → (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o,
∅)))) | 
| 29 |   | fveq2 5558 | 
. . . . . . 7
⊢ (𝑤 = suc 𝑘 → (𝑃‘𝑤) = (𝑃‘suc 𝑘)) | 
| 30 |   | eleq1 2259 | 
. . . . . . . 8
⊢ (𝑤 = suc 𝑘 → (𝑤 ∈ 𝑁 ↔ suc 𝑘 ∈ 𝑁)) | 
| 31 | 30 | ifbid 3582 | 
. . . . . . 7
⊢ (𝑤 = suc 𝑘 → if(𝑤 ∈ 𝑁, 1o, ∅) = if(suc 𝑘 ∈ 𝑁, 1o, ∅)) | 
| 32 | 29, 31 | eqeq12d 2211 | 
. . . . . 6
⊢ (𝑤 = suc 𝑘 → ((𝑃‘𝑤) = if(𝑤 ∈ 𝑁, 1o, ∅) ↔ (𝑃‘suc 𝑘) = if(suc 𝑘 ∈ 𝑁, 1o, ∅))) | 
| 33 | 32 | imbi2d 230 | 
. . . . 5
⊢ (𝑤 = suc 𝑘 → ((𝜑 → (𝑃‘𝑤) = if(𝑤 ∈ 𝑁, 1o, ∅)) ↔ (𝜑 → (𝑃‘suc 𝑘) = if(suc 𝑘 ∈ 𝑁, 1o,
∅)))) | 
| 34 |   | fveq2 5558 | 
. . . . . . 7
⊢ (𝑤 = 𝑗 → (𝑃‘𝑤) = (𝑃‘𝑗)) | 
| 35 |   | eleq1w 2257 | 
. . . . . . . 8
⊢ (𝑤 = 𝑗 → (𝑤 ∈ 𝑁 ↔ 𝑗 ∈ 𝑁)) | 
| 36 | 35 | ifbid 3582 | 
. . . . . . 7
⊢ (𝑤 = 𝑗 → if(𝑤 ∈ 𝑁, 1o, ∅) = if(𝑗 ∈ 𝑁, 1o, ∅)) | 
| 37 | 34, 36 | eqeq12d 2211 | 
. . . . . 6
⊢ (𝑤 = 𝑗 → ((𝑃‘𝑤) = if(𝑤 ∈ 𝑁, 1o, ∅) ↔ (𝑃‘𝑗) = if(𝑗 ∈ 𝑁, 1o, ∅))) | 
| 38 | 37 | imbi2d 230 | 
. . . . 5
⊢ (𝑤 = 𝑗 → ((𝜑 → (𝑃‘𝑤) = if(𝑤 ∈ 𝑁, 1o, ∅)) ↔ (𝜑 → (𝑃‘𝑗) = if(𝑗 ∈ 𝑁, 1o,
∅)))) | 
| 39 |   | noel 3454 | 
. . . . . . . . 9
⊢  ¬
∅ ∈ ∅ | 
| 40 |   | simpr 110 | 
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 = ∅) → 𝑁 = ∅) | 
| 41 | 40 | eleq2d 2266 | 
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 = ∅) → (∅ ∈ 𝑁 ↔ ∅ ∈
∅)) | 
| 42 | 39, 41 | mtbiri 676 | 
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 = ∅) → ¬ ∅ ∈
𝑁) | 
| 43 | 42 | iffalsed 3571 | 
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 = ∅) → if(∅ ∈ 𝑁, 1o, ∅) =
∅) | 
| 44 |   | nnnninfeq.0 | 
. . . . . . . 8
⊢ (𝜑 → (𝑃‘𝑁) = ∅) | 
| 45 | 44 | adantr 276 | 
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝑃‘𝑁) = ∅) | 
| 46 | 40 | fveq2d 5562 | 
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝑃‘𝑁) = (𝑃‘∅)) | 
| 47 | 43, 45, 46 | 3eqtr2rd 2236 | 
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝑃‘∅) = if(∅ ∈ 𝑁, 1o,
∅)) | 
| 48 |   | fveq2 5558 | 
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝑃‘𝑥) = (𝑃‘∅)) | 
| 49 | 48 | eqeq1d 2205 | 
. . . . . . . 8
⊢ (𝑥 = ∅ → ((𝑃‘𝑥) = 1o ↔ (𝑃‘∅) =
1o)) | 
| 50 |   | nnnninfeq.1 | 
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝑁 (𝑃‘𝑥) = 1o) | 
| 51 | 50 | adantr 276 | 
. . . . . . . 8
⊢ ((𝜑 ∧ ∅ ∈ 𝑁) → ∀𝑥 ∈ 𝑁 (𝑃‘𝑥) = 1o) | 
| 52 |   | simpr 110 | 
. . . . . . . 8
⊢ ((𝜑 ∧ ∅ ∈ 𝑁) → ∅ ∈ 𝑁) | 
| 53 | 49, 51, 52 | rspcdva 2873 | 
. . . . . . 7
⊢ ((𝜑 ∧ ∅ ∈ 𝑁) → (𝑃‘∅) =
1o) | 
| 54 | 52 | iftrued 3568 | 
. . . . . . 7
⊢ ((𝜑 ∧ ∅ ∈ 𝑁) → if(∅ ∈ 𝑁, 1o, ∅) =
1o) | 
| 55 | 53, 54 | eqtr4d 2232 | 
. . . . . 6
⊢ ((𝜑 ∧ ∅ ∈ 𝑁) → (𝑃‘∅) = if(∅ ∈ 𝑁, 1o,
∅)) | 
| 56 |   | 0elnn 4655 | 
. . . . . . 7
⊢ (𝑁 ∈ ω → (𝑁 = ∅ ∨ ∅ ∈
𝑁)) | 
| 57 | 10, 56 | syl 14 | 
. . . . . 6
⊢ (𝜑 → (𝑁 = ∅ ∨ ∅ ∈ 𝑁)) | 
| 58 | 47, 55, 57 | mpjaodan 799 | 
. . . . 5
⊢ (𝜑 → (𝑃‘∅) = if(∅ ∈ 𝑁, 1o,
∅)) | 
| 59 |   | fveq2 5558 | 
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑘 → (𝑃‘𝑥) = (𝑃‘suc 𝑘)) | 
| 60 | 59 | eqeq1d 2205 | 
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑘 → ((𝑃‘𝑥) = 1o ↔ (𝑃‘suc 𝑘) = 1o)) | 
| 61 | 50 | ad3antlr 493 | 
. . . . . . . . . 10
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ suc 𝑘 ∈ 𝑁) → ∀𝑥 ∈ 𝑁 (𝑃‘𝑥) = 1o) | 
| 62 |   | simpr 110 | 
. . . . . . . . . 10
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ suc 𝑘 ∈ 𝑁) → suc 𝑘 ∈ 𝑁) | 
| 63 | 60, 61, 62 | rspcdva 2873 | 
. . . . . . . . 9
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ suc 𝑘 ∈ 𝑁) → (𝑃‘suc 𝑘) = 1o) | 
| 64 | 62 | iftrued 3568 | 
. . . . . . . . 9
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ suc 𝑘 ∈ 𝑁) → if(suc 𝑘 ∈ 𝑁, 1o, ∅) =
1o) | 
| 65 | 63, 64 | eqtr4d 2232 | 
. . . . . . . 8
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ suc 𝑘 ∈ 𝑁) → (𝑃‘suc 𝑘) = if(suc 𝑘 ∈ 𝑁, 1o, ∅)) | 
| 66 | 44 | ad3antlr 493 | 
. . . . . . . . 9
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → (𝑃‘𝑁) = ∅) | 
| 67 |   | simpr 110 | 
. . . . . . . . . 10
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → suc 𝑘 = 𝑁) | 
| 68 | 67 | fveq2d 5562 | 
. . . . . . . . 9
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → (𝑃‘suc 𝑘) = (𝑃‘𝑁)) | 
| 69 | 10 | ad2antlr 489 | 
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) → 𝑁 ∈
ω) | 
| 70 |   | nnord 4648 | 
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ω → Ord 𝑁) | 
| 71 |   | ordirr 4578 | 
. . . . . . . . . . . . 13
⊢ (Ord
𝑁 → ¬ 𝑁 ∈ 𝑁) | 
| 72 | 69, 70, 71 | 3syl 17 | 
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) → ¬
𝑁 ∈ 𝑁) | 
| 73 | 72 | adantr 276 | 
. . . . . . . . . . 11
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → ¬ 𝑁 ∈ 𝑁) | 
| 74 | 67, 73 | eqneltrd 2292 | 
. . . . . . . . . 10
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → ¬ suc 𝑘 ∈ 𝑁) | 
| 75 | 74 | iffalsed 3571 | 
. . . . . . . . 9
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → if(suc 𝑘 ∈ 𝑁, 1o, ∅) =
∅) | 
| 76 | 66, 68, 75 | 3eqtr4d 2239 | 
. . . . . . . 8
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ suc 𝑘 = 𝑁) → (𝑃‘suc 𝑘) = if(suc 𝑘 ∈ 𝑁, 1o, ∅)) | 
| 77 |   | suceq 4437 | 
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑘 → suc 𝑗 = suc 𝑘) | 
| 78 | 77 | fveq2d 5562 | 
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑘 → (𝑃‘suc 𝑗) = (𝑃‘suc 𝑘)) | 
| 79 |   | fveq2 5558 | 
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑘 → (𝑃‘𝑗) = (𝑃‘𝑘)) | 
| 80 | 78, 79 | sseq12d 3214 | 
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → ((𝑃‘suc 𝑗) ⊆ (𝑃‘𝑗) ↔ (𝑃‘suc 𝑘) ⊆ (𝑃‘𝑘))) | 
| 81 | 1 | ad3antlr 493 | 
. . . . . . . . . . . . 13
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → 𝑃 ∈
ℕ∞) | 
| 82 |   | fveq1 5557 | 
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = 𝑃 → (𝑓‘suc 𝑗) = (𝑃‘suc 𝑗)) | 
| 83 |   | fveq1 5557 | 
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = 𝑃 → (𝑓‘𝑗) = (𝑃‘𝑗)) | 
| 84 | 82, 83 | sseq12d 3214 | 
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑃 → ((𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ (𝑃‘suc 𝑗) ⊆ (𝑃‘𝑗))) | 
| 85 | 84 | ralbidv 2497 | 
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑃 → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃‘𝑗))) | 
| 86 |   | df-nninf 7186 | 
. . . . . . . . . . . . . . 15
⊢
ℕ∞ = {𝑓 ∈ (2o
↑𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗)} | 
| 87 | 85, 86 | elrab2 2923 | 
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈
ℕ∞ ↔ (𝑃 ∈ (2o
↑𝑚 ω) ∧ ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃‘𝑗))) | 
| 88 | 87 | simprbi 275 | 
. . . . . . . . . . . . 13
⊢ (𝑃 ∈
ℕ∞ → ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃‘𝑗)) | 
| 89 | 81, 88 | syl 14 | 
. . . . . . . . . . . 12
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃‘𝑗)) | 
| 90 |   | simplll 533 | 
. . . . . . . . . . . 12
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → 𝑘 ∈ ω) | 
| 91 | 80, 89, 90 | rspcdva 2873 | 
. . . . . . . . . . 11
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃‘suc 𝑘) ⊆ (𝑃‘𝑘)) | 
| 92 |   | simplr 528 | 
. . . . . . . . . . . 12
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) | 
| 93 |   | simpr 110 | 
. . . . . . . . . . . . . . 15
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → 𝑁 ∈ suc 𝑘) | 
| 94 |   | nnord 4648 | 
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ω → Ord 𝑘) | 
| 95 |   | ordtr 4413 | 
. . . . . . . . . . . . . . . 16
⊢ (Ord
𝑘 → Tr 𝑘) | 
| 96 |   | trsucss 4458 | 
. . . . . . . . . . . . . . . 16
⊢ (Tr 𝑘 → (𝑁 ∈ suc 𝑘 → 𝑁 ⊆ 𝑘)) | 
| 97 | 94, 95, 96 | 3syl 17 | 
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ω → (𝑁 ∈ suc 𝑘 → 𝑁 ⊆ 𝑘)) | 
| 98 | 90, 93, 97 | sylc 62 | 
. . . . . . . . . . . . . 14
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → 𝑁 ⊆ 𝑘) | 
| 99 | 69 | adantr 276 | 
. . . . . . . . . . . . . . 15
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → 𝑁 ∈ ω) | 
| 100 |   | nntri1 6554 | 
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ω ∧ 𝑘 ∈ ω) → (𝑁 ⊆ 𝑘 ↔ ¬ 𝑘 ∈ 𝑁)) | 
| 101 | 99, 90, 100 | syl2anc 411 | 
. . . . . . . . . . . . . 14
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑁 ⊆ 𝑘 ↔ ¬ 𝑘 ∈ 𝑁)) | 
| 102 | 98, 101 | mpbid 147 | 
. . . . . . . . . . . . 13
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → ¬ 𝑘 ∈ 𝑁) | 
| 103 | 102 | iffalsed 3571 | 
. . . . . . . . . . . 12
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → if(𝑘 ∈ 𝑁, 1o, ∅) =
∅) | 
| 104 | 92, 103 | eqtrd 2229 | 
. . . . . . . . . . 11
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃‘𝑘) = ∅) | 
| 105 | 91, 104 | sseqtrd 3221 | 
. . . . . . . . . 10
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃‘suc 𝑘) ⊆ ∅) | 
| 106 |   | ss0 3491 | 
. . . . . . . . . 10
⊢ ((𝑃‘suc 𝑘) ⊆ ∅ → (𝑃‘suc 𝑘) = ∅) | 
| 107 | 105, 106 | syl 14 | 
. . . . . . . . 9
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃‘suc 𝑘) = ∅) | 
| 108 |   | ordn2lp 4581 | 
. . . . . . . . . . . 12
⊢ (Ord
𝑁 → ¬ (𝑁 ∈ suc 𝑘 ∧ suc 𝑘 ∈ 𝑁)) | 
| 109 | 99, 70, 108 | 3syl 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 𝑘 ∈ 𝑁) | 
| 112 | 110, 111 | jca 306 | 
. . . . . . . . . . 11
⊢
(((((𝑘 ∈
ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) ∧ suc 𝑘 ∈ 𝑁) → (𝑁 ∈ suc 𝑘 ∧ suc 𝑘 ∈ 𝑁)) | 
| 113 | 109, 112 | mtand 666 | 
. . . . . . . . . 10
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → ¬ suc 𝑘 ∈ 𝑁) | 
| 114 | 113 | iffalsed 3571 | 
. . . . . . . . 9
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → if(suc 𝑘 ∈ 𝑁, 1o, ∅) =
∅) | 
| 115 | 107, 114 | eqtr4d 2232 | 
. . . . . . . 8
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) ∧ 𝑁 ∈ suc 𝑘) → (𝑃‘suc 𝑘) = if(suc 𝑘 ∈ 𝑁, 1o, ∅)) | 
| 116 |   | peano2 4631 | 
. . . . . . . . . 10
⊢ (𝑘 ∈ ω → suc 𝑘 ∈
ω) | 
| 117 | 116 | ad2antrr 488 | 
. . . . . . . . 9
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) → suc 𝑘 ∈
ω) | 
| 118 |   | nntri3or 6551 | 
. . . . . . . . 9
⊢ ((suc
𝑘 ∈ ω ∧
𝑁 ∈ ω) →
(suc 𝑘 ∈ 𝑁 ∨ suc 𝑘 = 𝑁 ∨ 𝑁 ∈ suc 𝑘)) | 
| 119 | 117, 69, 118 | syl2anc 411 | 
. . . . . . . 8
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) → (suc 𝑘 ∈ 𝑁 ∨ suc 𝑘 = 𝑁 ∨ 𝑁 ∈ suc 𝑘)) | 
| 120 | 65, 76, 115, 119 | mpjao3dan 1318 | 
. . . . . . 7
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) → (𝑃‘suc 𝑘) = if(suc 𝑘 ∈ 𝑁, 1o, ∅)) | 
| 121 | 120 | exp31 364 | 
. . . . . 6
⊢ (𝑘 ∈ ω → (𝜑 → ((𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅) → (𝑃‘suc 𝑘) = if(suc 𝑘 ∈ 𝑁, 1o,
∅)))) | 
| 122 | 121 | a2d 26 | 
. . . . 5
⊢ (𝑘 ∈ ω → ((𝜑 → (𝑃‘𝑘) = if(𝑘 ∈ 𝑁, 1o, ∅)) → (𝜑 → (𝑃‘suc 𝑘) = if(suc 𝑘 ∈ 𝑁, 1o,
∅)))) | 
| 123 | 23, 28, 33, 38, 58, 122 | finds 4636 | 
. . . 4
⊢ (𝑗 ∈ ω → (𝜑 → (𝑃‘𝑗) = if(𝑗 ∈ 𝑁, 1o, ∅))) | 
| 124 | 123 | impcom 125 | 
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (𝑃‘𝑗) = if(𝑗 ∈ 𝑁, 1o, ∅)) | 
| 125 |   | simpr 110 | 
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ω) → 𝑗 ∈ ω) | 
| 126 | 5 | a1i 9 | 
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ω) → 1o ∈
2o) | 
| 127 | 7 | a1i 9 | 
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ω) → ∅ ∈
2o) | 
| 128 | 10 | adantr 276 | 
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ω) → 𝑁 ∈ ω) | 
| 129 |   | nndcel 6558 | 
. . . . . 6
⊢ ((𝑗 ∈ ω ∧ 𝑁 ∈ ω) →
DECID 𝑗
∈ 𝑁) | 
| 130 | 125, 128,
129 | syl2anc 411 | 
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ω) → DECID
𝑗 ∈ 𝑁) | 
| 131 | 126, 127,
130 | ifcldcd 3597 | 
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ω) → if(𝑗 ∈ 𝑁, 1o, ∅) ∈
2o) | 
| 132 |   | eleq1w 2257 | 
. . . . . 6
⊢ (𝑖 = 𝑗 → (𝑖 ∈ 𝑁 ↔ 𝑗 ∈ 𝑁)) | 
| 133 | 132 | ifbid 3582 | 
. . . . 5
⊢ (𝑖 = 𝑗 → if(𝑖 ∈ 𝑁, 1o, ∅) = if(𝑗 ∈ 𝑁, 1o, ∅)) | 
| 134 | 133, 16 | fvmptg 5637 | 
. . . 4
⊢ ((𝑗 ∈ ω ∧ if(𝑗 ∈ 𝑁, 1o, ∅) ∈
2o) → ((𝑖
∈ ω ↦ if(𝑖
∈ 𝑁, 1o,
∅))‘𝑗) =
if(𝑗 ∈ 𝑁, 1o,
∅)) | 
| 135 | 125, 131,
134 | syl2anc 411 | 
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘𝑗) = if(𝑗 ∈ 𝑁, 1o, ∅)) | 
| 136 | 124, 135 | eqtr4d 2232 | 
. 2
⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (𝑃‘𝑗) = ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘𝑗)) | 
| 137 | 4, 18, 136 | eqfnfvd 5662 | 
1
⊢ (𝜑 → 𝑃 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))) |