Theorem elex2 ≪ | index | src | ≫ 

theorem elex2 (R: set) (l1 l2: nat) {n x y: nat}:
  $ l1, l2 e. ex2 R <->
    len l1 = len l2 /\
      E. n E. x E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R) $;
StepHypRefExpression
1 id 
_1 = l1 -> _1 = l1
2 1 anwl 
_1 = l1 /\ _2 = l2 -> _1 = l1
3 2 leneqd 
_1 = l1 /\ _2 = l2 -> len _1 = len l1
4 id 
_2 = l2 -> _2 = l2
5 4 anwr 
_1 = l1 /\ _2 = l2 -> _2 = l2
6 5 leneqd 
_1 = l1 /\ _2 = l2 -> len _2 = len l2
7 3, 6 eqeqd 
_1 = l1 /\ _2 = l2 -> (len _1 = len _2 <-> len l1 = len l2)
8 2 ntheq2d 
_1 = l1 /\ _2 = l2 -> nth n _1 = nth n l1
9 8 eqeq1d 
_1 = l1 /\ _2 = l2 -> (nth n _1 = suc x <-> nth n l1 = suc x)
10 5 ntheq2d 
_1 = l1 /\ _2 = l2 -> nth n _2 = nth n l2
11 10 eqeq1d 
_1 = l1 /\ _2 = l2 -> (nth n _2 = suc y <-> nth n l2 = suc y)
12 9, 11 aneqd 
_1 = l1 /\ _2 = l2 -> (nth n _1 = suc x /\ nth n _2 = suc y <-> nth n l1 = suc x /\ nth n l2 = suc y)
13 12 aneq1d 
_1 = l1 /\ _2 = l2 -> (nth n _1 = suc x /\ nth n _2 = suc y /\ x, y e. R <-> nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R)
14 13 exeqd 
_1 = l1 /\ _2 = l2 -> (E. y (nth n _1 = suc x /\ nth n _2 = suc y /\ x, y e. R) <-> E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R))
15 14 exeqd 
_1 = l1 /\ _2 = l2 -> (E. x E. y (nth n _1 = suc x /\ nth n _2 = suc y /\ x, y e. R) <-> E. x E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R))
16 15 exeqd 
_1 = l1 /\ _2 = l2 ->
  (E. n E. x E. y (nth n _1 = suc x /\ nth n _2 = suc y /\ x, y e. R) <-> E. n E. x E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R))
17 7, 16 aneqd 
_1 = l1 /\ _2 = l2 ->
  (len _1 = len _2 /\ E. n E. x E. y (nth n _1 = suc x /\ nth n _2 = suc y /\ x, y e. R) <->
    len l1 = len l2 /\ E. n E. x E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R))
18 17 elabed 
_1 = l1 ->
  (l2 e. {_2 | len _1 = len _2 /\ E. n E. x E. y (nth n _1 = suc x /\ nth n _2 = suc y /\ x, y e. R)} <->
    len l1 = len l2 /\ E. n E. x E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R))
19 18 elsabe 
l1, l2 e. S\ _1, {_2 | len _1 = len _2 /\ E. n E. x E. y (nth n _1 = suc x /\ nth n _2 = suc y /\ x, y e. R)} <->
  len l1 = len l2 /\ E. n E. x E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R)
20 19 conv ex2 
l1, l2 e. ex2 R <-> len l1 = len l2 /\ E. n E. x E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R)

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)