Metamath Proof Explorer

Theorem sadcf

Description: The carry sequence is a sequence of elements of 2o encoding a "sequence of wffs". (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Hypotheses sadval.a ⊢ φ → A ⊆ ℕ 0
sadval.b ⊢ φ → B ⊆ ℕ 0
sadval.c ⊢ C = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
Assertion sadcf ⊢ φ → C : ℕ 0 ⟶ 2 𝑜

Proof

Step Hyp Ref Expression
1 sadval.a ⊢ φ → A ⊆ ℕ 0
2 sadval.b ⊢ φ → B ⊆ ℕ 0
3 sadval.c ⊢ C = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
4 0nn0 ⊢ 0 ∈ ℕ 0
5 iftrue ⊢ n = 0 → if n = 0 ∅ n − 1 = ∅
6 eqid ⊢ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 = n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
7 0ex ⊢ ∅ ∈ V
8 5 6 7 fvmpt ⊢ 0 ∈ ℕ 0 → n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0 = ∅
9 4 8 ax-mp ⊢ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0 = ∅
10 7 prid1 ⊢ ∅ ∈ ∅ 1 𝑜
11 df2o3 ⊢ 2 𝑜 = ∅ 1 𝑜
12 10 11 eleqtrri ⊢ ∅ ∈ 2 𝑜
13 9 12 eqeltri ⊢ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0 ∈ 2 𝑜
14 13 a1i ⊢ φ → n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ 0 ∈ 2 𝑜
15 df-ov ⊢ x c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ y = c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ ⁡ x y
16 1oelpr ⊢ 1 𝑜 ∈ ∅ 1 𝑜
17 16 11 eleqtrri ⊢ 1 𝑜 ∈ 2 𝑜
18 17 12 ifcli ⊢ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ ∈ 2 𝑜
19 18 rgen2w ⊢ ∀ c ∈ 2 𝑜 ∀ m ∈ ℕ 0 if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ ∈ 2 𝑜
20 eqid ⊢ c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ = c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅
21 20 fmpo ⊢ ∀ c ∈ 2 𝑜 ∀ m ∈ ℕ 0 if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ ∈ 2 𝑜 ↔ c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ : 2 𝑜 × ℕ 0 ⟶ 2 𝑜
22 19 21 mpbi ⊢ c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ : 2 𝑜 × ℕ 0 ⟶ 2 𝑜
23 22 12 f0cli ⊢ c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ ⁡ x y ∈ 2 𝑜
24 15 23 eqeltri ⊢ x c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ y ∈ 2 𝑜
25 24 a1i ⊢ φ ∧ x ∈ 2 𝑜 ∧ y ∈ V → x c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ y ∈ 2 𝑜
26 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
27 0zd ⊢ φ → 0 ∈ ℤ
28 fvexd ⊢ φ ∧ x ∈ ℤ ≥ 0 + 1 → n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ x ∈ V
29 14 25 26 27 28 seqf2 ⊢ φ → seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 : ℕ 0 ⟶ 2 𝑜
30 3 feq1i ⊢ C : ℕ 0 ⟶ 2 𝑜 ↔ seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 : ℕ 0 ⟶ 2 𝑜
31 29 30 sylibr ⊢ φ → C : ℕ 0 ⟶ 2 𝑜