Theorem ex2ssg ≪ | index | src | ≫ 

theorem ex2ssg (R S: set) (l1 l2: nat) {x y: nat}:
  $ A. x A. y (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) ->
    l1, l2 e. ex2 R ->
    l1, l2 e. ex2 S $;
StepHypRefExpression
1 elex2 
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)
2 elex2 
l1, l2 e. ex2 S <-> len l1 = len l2 /\ E. n E. x E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. S)
3 1, 2 imeqi 
l1, l2 e. ex2 R -> l1, l2 e. ex2 S <->
  len l1 = len l2 /\ E. n E. x E. y (nth n l1 = suc x /\ nth n l2 = 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. S)
4 exim 
A. x (E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R) -> E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. S)) ->
  E. x E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R) ->
  E. x E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. S)
5 exim 
A. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R -> nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. S) ->
  E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R) ->
  E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. S)
6 anim2a 
(nth n l1 = suc x /\ nth n l2 = suc y -> x, y e. R -> x, y e. S) ->
  nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R ->
  nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. S
7 imim1 
(nth n l1 = suc x /\ nth n l2 = suc y -> x IN l1 /\ y IN l2) ->
  (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) ->
  nth n l1 = suc x /\ nth n l2 = suc y ->
  x, y e. R ->
  x, y e. S
8 anim 
(nth n l1 = suc x -> x IN l1) -> (nth n l2 = suc y -> y IN l2) -> nth n l1 = suc x /\ nth n l2 = suc y -> x IN l1 /\ y IN l2
9 nthlmem 
nth n l1 = suc x -> x IN l1
10 8, 9 ax_mp 
(nth n l2 = suc y -> y IN l2) -> nth n l1 = suc x /\ nth n l2 = suc y -> x IN l1 /\ y IN l2
11 nthlmem 
nth n l2 = suc y -> y IN l2
12 10, 11 ax_mp 
nth n l1 = suc x /\ nth n l2 = suc y -> x IN l1 /\ y IN l2
13 7, 12 ax_mp 
(x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) -> nth n l1 = suc x /\ nth n l2 = suc y -> x, y e. R -> x, y e. S
14 6, 13 syl 
(x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) -> nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R -> nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. S
15 14 alimi 
A. y (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) ->
  A. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R -> nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. S)
16 5, 15 syl 
A. y (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) ->
  E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R) ->
  E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. S)
17 16 alimi 
A. x A. y (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) ->
  A. x (E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R) -> E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. S))
18 4, 17 syl 
A. x A. y (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) ->
  E. x E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R) ->
  E. x E. y (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. S)
19 18 eximd 
A. x A. y (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) ->
  E. n E. x E. y (nth n l1 = suc x /\ nth n l2 = 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. S)
20 19 anim2d 
A. x A. y (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) ->
  len l1 = len l2 /\ E. n E. x E. y (nth n l1 = suc x /\ nth n l2 = 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. S)
21 3, 20 sylibr 
A. x A. y (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) -> l1, l2 e. ex2 R -> l1, l2 e. ex2 S

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)