Theorem listfnisf | index | src |

theorem listfnisf (l: nat): $ isfun (listfn l) $;
StepHypRefExpression
1 isf0
isfun 0
2 listfn0
listfn 0 = 0
3 listfneq
l = 0 -> listfn l = listfn 0
4 2, 3 syl6eq
l = 0 -> listfn l = 0
5 4 nseqd
l = 0 -> listfn l == 0
6 5 isfeqd
l = 0 -> (isfun (listfn l) <-> isfun 0)
7 1, 6 mpbiri
l = 0 -> isfun (listfn l)
8 rlamisf
isfun (\. i e. upto (suc (size (Dom (listfn (snd (l - 1)))))), if (i = 0) (fst (l - 1)) (listfn (snd (l - 1)) @ (i - 1)))
9 listfnS2
listfn (fst (l - 1) : snd (l - 1)) = \. i e. upto (suc (size (Dom (listfn (snd (l - 1)))))), if (i = 0) (fst (l - 1)) (listfn (snd (l - 1)) @ (i - 1))
10 consfstsnd
l != 0 -> fst (l - 1) : snd (l - 1) = l
11 10 conv ne
~l = 0 -> fst (l - 1) : snd (l - 1) = l
12 11 listfneqd
~l = 0 -> listfn (fst (l - 1) : snd (l - 1)) = listfn l
13 9, 12 syl5eqr
~l = 0 -> \. i e. upto (suc (size (Dom (listfn (snd (l - 1)))))), if (i = 0) (fst (l - 1)) (listfn (snd (l - 1)) @ (i - 1)) = listfn l
14 13 nseqd
~l = 0 -> \. i e. upto (suc (size (Dom (listfn (snd (l - 1)))))), if (i = 0) (fst (l - 1)) (listfn (snd (l - 1)) @ (i - 1)) == listfn l
15 14 isfeqd
~l = 0 -> (isfun (\. i e. upto (suc (size (Dom (listfn (snd (l - 1)))))), if (i = 0) (fst (l - 1)) (listfn (snd (l - 1)) @ (i - 1))) <-> isfun (listfn l))
16 8, 15 mpbii
~l = 0 -> isfun (listfn l)
17 7, 16 cases
isfun (listfn l)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)