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 10228 . . . . . 6
2 iftrue 3737 . . . . . . 7
3 eqid 2435 . . . . . . 7
4 0ex 4331 . . . . . . 7
52, 3, 4fvmpt 5798 . . . . . 6
61, 5ax-mp 8 . . . . 5
74prid1 3904 . . . . . 6
8 df2o3 6729 . . . . . 6
97, 8eleqtrri 2508 . . . . 5
106, 9eqeltri 2505 . . . 4
1110a1i 11 . . 3
13 1on 6723 . . . . . . . . . . . 12
1413elexi 2957 . . . . . . . . . . 11
1514prid2 3905 . . . . . . . . . 10
1615, 8eleqtrri 2508 . . . . . . . . 9
1716, 9keepel 3788 . . . . . . . 8 cadd
1817rgen2w 2766 . . . . . . 7 cadd
19 eqid 2435 . . . . . . . 8 cadd cadd
2118, 20mpbi 200 . . . . . 6 cadd
2221, 9f0cli 5872 . . . . 5 cadd
2312, 22eqeltri 2505 . . . 4 cadd
2423a1i 11 . . 3 cadd
25 nn0uz 10512 . . 3
26 0z 10285 . . . 4
2726a1i 11 . . 3
28 fvex 5734 . . . 4
2928a1i 11 . . 3
3011, 24, 25, 27, 29seqf2 11334 . 2 cadd