Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sadcf Structured version   Unicode version

 Description: The carry sequence is a sequence of elements of encoding a "sequence of wffs". (Contributed by Mario Carneiro, 5-Sep-2016.)
Hypotheses
Ref Expression
Assertion
Ref Expression
Distinct variable groups:   ,,   ,,   ,,
Allowed substitution hints:   (,,)   ()   ()   (,,)

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0nn0 10590 . . . . . 6
2 iftrue 3794 . . . . . . 7
3 eqid 2441 . . . . . . 7
4 0ex 4419 . . . . . . 7
52, 3, 4fvmpt 5771 . . . . . 6
61, 5ax-mp 5 . . . . 5
74prid1 3980 . . . . . 6
8 df2o3 6929 . . . . . 6
97, 8eleqtrri 2514 . . . . 5
106, 9eqeltri 2511 . . . 4
1110a1i 11 . . 3
13 1on 6923 . . . . . . . . . . . 12
1413elexi 2980 . . . . . . . . . . 11
1514prid2 3981 . . . . . . . . . 10
1615, 8eleqtrri 2514 . . . . . . . . 9
1716, 9keepel 3854 . . . . . . . 8 cadd
1817rgen2w 2782 . . . . . . 7 cadd
19 eqid 2441 . . . . . . . 8 cadd cadd
2118, 20mpbi 208 . . . . . 6 cadd
2221, 9f0cli 5851 . . . . 5 cadd
2312, 22eqeltri 2511 . . . 4 cadd
2423a1i 11 . . 3 cadd
25 nn0uz 10891 . . 3
26 0zd 10654 . . 3
27 fvex 5698 . . . 4
2827a1i 11 . . 3
2911, 24, 25, 26, 28seqf2 11821 . 2 cadd