Theorem elArrayS2 | index | src |

theorem elArrayS2 (A: set) {a b: nat} (l n: nat):
  $ l e. Array A (suc n) <->
    E. a E. b (a e. A /\ b e. Array A n /\ l = a : b) $;
StepHypRefExpression
1 bitr2
(E. a E. b (a e. A /\ b e. Array A n /\ l = a : b) <-> l e. Array A (suc n) /\ E. a E. b l = a : b) ->
  (l e. Array A (suc n) /\ E. a E. b l = a : b <-> l e. Array A (suc n)) ->
  (l e. Array A (suc n) <-> E. a E. b (a e. A /\ b e. Array A n /\ l = a : b))
2 aneq1a
(l = a : b -> (a e. A /\ b e. Array A n <-> l e. Array A (suc n))) -> (a e. A /\ b e. Array A n /\ l = a : b <-> l e. Array A (suc n) /\ l = a : b)
3 elArrayS
a : b e. Array A (suc n) <-> a e. A /\ b e. Array A n
4 eleq1
l = a : b -> (l e. Array A (suc n) <-> a : b e. Array A (suc n))
5 3, 4 syl6bb
l = a : b -> (l e. Array A (suc n) <-> a e. A /\ b e. Array A n)
6 5 bicomd
l = a : b -> (a e. A /\ b e. Array A n <-> l e. Array A (suc n))
7 2, 6 ax_mp
a e. A /\ b e. Array A n /\ l = a : b <-> l e. Array A (suc n) /\ l = a : b
8 7 bian1exi
E. b (a e. A /\ b e. Array A n /\ l = a : b) <-> l e. Array A (suc n) /\ E. b l = a : b
9 8 bian1exi
E. a E. b (a e. A /\ b e. Array A n /\ l = a : b) <-> l e. Array A (suc n) /\ E. a E. b l = a : b
10 1, 9 ax_mp
(l e. Array A (suc n) /\ E. a E. b l = a : b <-> l e. Array A (suc n)) -> (l e. Array A (suc n) <-> E. a E. b (a e. A /\ b e. Array A n /\ l = a : b))
11 bian2a
(l e. Array A (suc n) -> E. a E. b l = a : b) -> (l e. Array A (suc n) /\ E. a E. b l = a : b <-> l e. Array A (suc n))
12 excons
l != 0 <-> E. a E. b l = a : b
13 elArraySne0
l e. Array A (suc n) -> l != 0
14 12, 13 sylib
l e. Array A (suc n) -> E. a E. b l = a : b
15 11, 14 ax_mp
l e. Array A (suc n) /\ E. a E. b l = a : b <-> l e. Array A (suc n)
16 10, 15 ax_mp
l e. Array A (suc n) <-> E. a E. b (a e. A /\ b e. Array A n /\ l = a : b)

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)