| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0nn0 12541 | . . . . 5
⊢ 0 ∈
ℕ0 | 
| 2 |  | iftrue 4531 | . . . . . 6
⊢ (𝑛 = 0 → if(𝑛 = 0, ∅, (𝑛 − 1)) =
∅) | 
| 3 |  | eqid 2737 | . . . . . 6
⊢ (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 − 1))) = (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1))) | 
| 4 |  | 0ex 5307 | . . . . . 6
⊢ ∅
∈ V | 
| 5 | 2, 3, 4 | fvmpt 7016 | . . . . 5
⊢ (0 ∈
ℕ0 → ((𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))‘0) =
∅) | 
| 6 | 1, 5 | mp1i 13 | . . . 4
⊢ (𝜑 → ((𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))‘0) =
∅) | 
| 7 |  | 0elpw 5356 | . . . 4
⊢ ∅
∈ 𝒫 ℕ0 | 
| 8 | 6, 7 | eqeltrdi 2849 | . . 3
⊢ (𝜑 → ((𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))‘0) ∈
𝒫 ℕ0) | 
| 9 |  | df-ov 7434 | . . . . 5
⊢ (𝑥(𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)}))𝑦) = ((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)}))‘〈𝑥, 𝑦〉) | 
| 10 |  | elpwi 4607 | . . . . . . . . . . 11
⊢ (𝑝 ∈ 𝒫
ℕ0 → 𝑝 ⊆
ℕ0) | 
| 11 | 10 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑝 ∈ 𝒫
ℕ0 ∧ 𝑚
∈ ℕ0) → 𝑝 ⊆
ℕ0) | 
| 12 |  | ssrab2 4080 | . . . . . . . . . 10
⊢ {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)} ⊆
ℕ0 | 
| 13 |  | sadcl 16499 | . . . . . . . . . 10
⊢ ((𝑝 ⊆ ℕ0
∧ {𝑛 ∈
ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)} ⊆ ℕ0) →
(𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)}) ⊆
ℕ0) | 
| 14 | 11, 12, 13 | sylancl 586 | . . . . . . . . 9
⊢ ((𝑝 ∈ 𝒫
ℕ0 ∧ 𝑚
∈ ℕ0) → (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)}) ⊆
ℕ0) | 
| 15 |  | nn0ex 12532 | . . . . . . . . . 10
⊢
ℕ0 ∈ V | 
| 16 | 15 | elpw2 5334 | . . . . . . . . 9
⊢ ((𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)}) ∈ 𝒫 ℕ0
↔ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)}) ⊆
ℕ0) | 
| 17 | 14, 16 | sylibr 234 | . . . . . . . 8
⊢ ((𝑝 ∈ 𝒫
ℕ0 ∧ 𝑚
∈ ℕ0) → (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)}) ∈ 𝒫
ℕ0) | 
| 18 | 17 | rgen2 3199 | . . . . . . 7
⊢
∀𝑝 ∈
𝒫 ℕ0∀𝑚 ∈ ℕ0 (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)}) ∈ 𝒫
ℕ0 | 
| 19 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})) = (𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})) | 
| 20 | 19 | fmpo 8093 | . . . . . . 7
⊢
(∀𝑝 ∈
𝒫 ℕ0∀𝑚 ∈ ℕ0 (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)}) ∈ 𝒫 ℕ0
↔ (𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})):(𝒫 ℕ0 ×
ℕ0)⟶𝒫 ℕ0) | 
| 21 | 18, 20 | mpbi 230 | . . . . . 6
⊢ (𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})):(𝒫 ℕ0 ×
ℕ0)⟶𝒫 ℕ0 | 
| 22 | 21, 7 | f0cli 7118 | . . . . 5
⊢ ((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)}))‘〈𝑥, 𝑦〉) ∈ 𝒫
ℕ0 | 
| 23 | 9, 22 | eqeltri 2837 | . . . 4
⊢ (𝑥(𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)}))𝑦) ∈ 𝒫
ℕ0 | 
| 24 | 23 | a1i 11 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 ℕ0 ∧
𝑦 ∈ V)) → (𝑥(𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)}))𝑦) ∈ 𝒫
ℕ0) | 
| 25 |  | nn0uz 12920 | . . 3
⊢
ℕ0 = (ℤ≥‘0) | 
| 26 |  | 0zd 12625 | . . 3
⊢ (𝜑 → 0 ∈
ℤ) | 
| 27 |  | fvexd 6921 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(0 +
1))) → ((𝑛 ∈
ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))‘𝑥) ∈ V) | 
| 28 | 8, 24, 25, 26, 27 | seqf2 14062 | . 2
⊢ (𝜑 → seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 −
1)))):ℕ0⟶𝒫
ℕ0) | 
| 29 |  | smuval.p | . . 3
⊢ 𝑃 = seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) | 
| 30 | 29 | feq1i 6727 | . 2
⊢ (𝑃:ℕ0⟶𝒫
ℕ0 ↔ seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 −
1)))):ℕ0⟶𝒫
ℕ0) | 
| 31 | 28, 30 | sylibr 234 | 1
⊢ (𝜑 → 𝑃:ℕ0⟶𝒫
ℕ0) |