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=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=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=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1
4 0nn0 ⊢0∈ℕ0
5 iftrue ⊢n=0→ifn=0∅n−1=∅
6 eqid ⊢n∈ℕ0⟼ifn=0∅n−1=n∈ℕ0⟼ifn=0∅n−1
7 0ex ⊢∅∈V
8 5 6 7 fvmpt ⊢0∈ℕ0→n∈ℕ0⟼ifn=0∅n−1⁡0=∅
9 4 8 ax-mp ⊢n∈ℕ0⟼ifn=0∅n−1⁡0=∅
10 7 prid1 ⊢∅∈∅1𝑜
11 df2o3 ⊢2𝑜=∅1𝑜
12 10 11 eleqtrri ⊢∅∈2𝑜
13 9 12 eqeltri ⊢n∈ℕ0⟼ifn=0∅n−1⁡0∈2𝑜
14 13 a1i ⊢φ→n∈ℕ0⟼ifn=0∅n−1⁡0∈2𝑜
15 df-ov ⊢xc∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅y=c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅⁡xy
16 1oex ⊢1𝑜∈V
17 16 prid2 ⊢1𝑜∈∅1𝑜
18 17 11 eleqtrri ⊢1𝑜∈2𝑜
19 18 12 ifcli ⊢ifcaddm∈Am∈B∅∈c1𝑜∅∈2𝑜
20 19 rgen2w ⊢∀c∈2𝑜∀m∈ℕ0ifcaddm∈Am∈B∅∈c1𝑜∅∈2𝑜
21 eqid ⊢c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅=c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅
22 21 fmpo ⊢∀c∈2𝑜∀m∈ℕ0ifcaddm∈Am∈B∅∈c1𝑜∅∈2𝑜↔c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅:2𝑜×ℕ0⟶2𝑜
23 20 22 mpbi ⊢c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅:2𝑜×ℕ0⟶2𝑜
24 23 12 f0cli ⊢c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅⁡xy∈2𝑜
25 15 24 eqeltri ⊢xc∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅y∈2𝑜
26 25 a1i ⊢φ∧x∈2𝑜∧y∈V→xc∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅y∈2𝑜
27 nn0uz ⊢ℕ0=ℤ≥0
28 0zd ⊢φ→0∈ℤ
29 fvexd ⊢φ∧x∈ℤ≥0+1→n∈ℕ0⟼ifn=0∅n−1⁡x∈V
30 14 26 27 28 29 seqf2 ⊢φ→seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1:ℕ0⟶2𝑜
31 3 feq1i ⊢C:ℕ0⟶2𝑜↔seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1:ℕ0⟶2𝑜
32 30 31 sylibr ⊢φ→C:ℕ0⟶2𝑜