Theorem elArrayS ≪ | index | src | ≫ 

theorem elArrayS (A: set) (a b n: nat):
  $ a : b e. Array A (suc n) <-> a e. A /\ b e. Array A n $;
StepHypRefExpression
1 bitr 
(a : b e. Array A (suc n) <-> a : b e. List A /\ len (a : b) = suc n) ->
  (a : b e. List A /\ len (a : b) = suc n <-> a e. A /\ b e. Array A n) ->
  (a : b e. Array A (suc n) <-> a e. A /\ b e. Array A n)
2 elArray 
a : b e. Array A (suc n) <-> a : b e. List A /\ len (a : b) = suc n
3 1, 2 ax_mp 
(a : b e. List A /\ len (a : b) = suc n <-> a e. A /\ b e. Array A n) -> (a : b e. Array A (suc n) <-> a e. A /\ b e. Array A n)
4 bitr 
(a : b e. List A /\ len (a : b) = suc n <-> a e. A /\ b e. List A /\ len b = n) ->
  (a e. A /\ b e. List A /\ len b = n <-> a e. A /\ b e. Array A n) ->
  (a : b e. List A /\ len (a : b) = suc n <-> a e. A /\ b e. Array A n)
5 aneq 
(a : b e. List A <-> a e. A /\ b e. List A) ->
  (len (a : b) = suc n <-> len b = n) ->
  (a : b e. List A /\ len (a : b) = suc n <-> a e. A /\ b e. List A /\ len b = n)
6 elListS 
a : b e. List A <-> a e. A /\ b e. List A
7 5, 6 ax_mp 
(len (a : b) = suc n <-> len b = n) -> (a : b e. List A /\ len (a : b) = suc n <-> a e. A /\ b e. List A /\ len b = n)
8 bitr 
(len (a : b) = suc n <-> suc (len b) = suc n) -> (suc (len b) = suc n <-> len b = n) -> (len (a : b) = suc n <-> len b = n)
9 eqeq1 
len (a : b) = suc (len b) -> (len (a : b) = suc n <-> suc (len b) = suc n)
10 lenS 
len (a : b) = suc (len b)
11 9, 10 ax_mp 
len (a : b) = suc n <-> suc (len b) = suc n
12 8, 11 ax_mp 
(suc (len b) = suc n <-> len b = n) -> (len (a : b) = suc n <-> len b = n)
13 peano2 
suc (len b) = suc n <-> len b = n
14 12, 13 ax_mp 
len (a : b) = suc n <-> len b = n
15 7, 14 ax_mp 
a : b e. List A /\ len (a : b) = suc n <-> a e. A /\ b e. List A /\ len b = n
16 4, 15 ax_mp 
(a e. A /\ b e. List A /\ len b = n <-> a e. A /\ b e. Array A n) -> (a : b e. List A /\ len (a : b) = suc n <-> a e. A /\ b e. Array A n)
17 bitr4 
(a e. A /\ b e. List A /\ len b = n <-> a e. A /\ (b e. List A /\ len b = n)) ->
  (a e. A /\ b e. Array A n <-> a e. A /\ (b e. List A /\ len b = n)) ->
  (a e. A /\ b e. List A /\ len b = n <-> a e. A /\ b e. Array A n)
18 anass 
a e. A /\ b e. List A /\ len b = n <-> a e. A /\ (b e. List A /\ len b = n)
19 17, 18 ax_mp 
(a e. A /\ b e. Array A n <-> a e. A /\ (b e. List A /\ len b = n)) -> (a e. A /\ b e. List A /\ len b = n <-> a e. A /\ b e. Array A n)
20 elArray 
b e. Array A n <-> b e. List A /\ len b = n
21 20 aneq2i 
a e. A /\ b e. Array A n <-> a e. A /\ (b e. List A /\ len b = n)
22 19, 21 ax_mp 
a e. A /\ b e. List A /\ len b = n <-> a e. A /\ b e. Array A n
23 16, 22 ax_mp 
a : b e. List A /\ len (a : b) = suc n <-> a e. A /\ b e. Array A n
24 3, 23 ax_mp 
a : b e. Array A (suc n) <-> a e. A /\ b e. Array A n

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)