Theorem all2ssg ≪ | index | src | ≫ 

theorem all2ssg (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. all2 R ->
    l1, l2 e. all2 S $;
StepHypRefExpression
1 elall2 
l1, l2 e. all2 R <-> len l1 = len l2 /\ A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R)
2 elall2 
l1, l2 e. all2 S <-> len l1 = len l2 /\ A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. S)
3 1, 2 imeqi 
l1, l2 e. all2 R -> l1, l2 e. all2 S <->
  len l1 = len l2 /\ A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R) ->
    len l1 = len l2 /\ A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. S)
4 impexp 
x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S <-> x IN l1 -> y IN l2 -> x, y e. R -> x, y e. S
5 imim 
(nth n l1 = suc x -> x IN l1) ->
  ((y IN l2 -> x, y e. R -> x, y e. S) -> (nth n l2 = suc y -> x, y e. R) -> nth n l2 = suc y -> x, y e. S) ->
  (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 l2 = suc y ->
  x, y e. S
6 nthlmem 
nth n l1 = suc x -> x IN l1
7 5, 6 ax_mp 
((y IN l2 -> x, y e. R -> x, y e. S) -> (nth n l2 = suc y -> x, y e. R) -> nth n l2 = suc y -> x, y e. S) ->
  (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 l2 = suc y ->
  x, y e. S
8 imim1 
(nth n l2 = suc y -> y IN l2) -> (y IN l2 -> x, y e. R -> x, y e. S) -> nth n l2 = suc y -> x, y e. R -> x, y e. S
9 nthlmem 
nth n l2 = suc y -> y IN l2
10 8, 9 ax_mp 
(y IN l2 -> x, y e. R -> x, y e. S) -> nth n l2 = suc y -> x, y e. R -> x, y e. S
11 10 a2d 
(y IN l2 -> x, y e. R -> x, y e. S) -> (nth n l2 = suc y -> x, y e. R) -> nth n l2 = suc y -> x, y e. S
12 7, 11 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) -> nth n l2 = suc y -> x, y e. S
13 12 a2d 
(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
14 4, 13 sylbi 
(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 al2imi 
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) ->
  A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. S)
16 15 al2imi 
A. x A. y (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) ->
  A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R) ->
  A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. S)
17 16 alimd 
A. x A. y (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) ->
  A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R) ->
  A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. S)
18 17 anim2d 
A. x A. y (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) ->
  len l1 = len l2 /\ A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R) ->
  len l1 = len l2 /\ A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. S)
19 3, 18 sylibr 
A. x A. y (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) -> l1, l2 e. all2 R -> l1, l2 e. all2 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)