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 eqidd 
_1 = l1 /\ _2 = l2 -> n = n
9 8, 2 ntheqd 
_1 = l1 /\ _2 = l2 -> nth n _1 = nth n l1
10 eqidd 
_1 = l1 /\ _2 = l2 -> suc x = suc x
11 9, 10 eqeqd 
_1 = l1 /\ _2 = l2 -> (nth n _1 = suc x <-> nth n l1 = suc x)
12 8, 5 ntheqd 
_1 = l1 /\ _2 = l2 -> nth n _2 = nth n l2
13 eqidd 
_1 = l1 /\ _2 = l2 -> suc y = suc y
14 12, 13 eqeqd 
_1 = l1 /\ _2 = l2 -> (nth n _2 = suc y <-> nth n l2 = suc y)
15 11, 14 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)
16 biidd 
_1 = l1 /\ _2 = l2 -> (x, y e. R <-> x, y e. R)
17 15, 16 aneqd 
_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)
18 17 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))
19 18 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))
20 19 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))
21 7, 20 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))
22 21 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))
23 22 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)
24 23 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)