Theorem all2S1 ≪ | index | src | ≫ 

theorem all2S1 (R: set) (a: nat) {b: nat} (l1 l2: nat) {l2_: nat}:
  $ a : l1, l2 e. all2 R <->
    E. b E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R)) $;
StepHypRefExpression
1 bitr3 
(E. b E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R <-> a : l1, l2 e. all2 R) ->
  (E. b E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R <-> E. b E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R))) ->
  (a : l1, l2 e. all2 R <-> E. b E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R)))
2 bian1a 
(a : l1, l2 e. all2 R -> E. b E. l2_ l2 = b : l2_) -> (E. b E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R <-> a : l1, l2 e. all2 R)
3 excons 
l2 != 0 <-> E. b E. l2_ l2 = b : l2_
4 noteq 
(len l2 = 0 <-> l2 = 0) -> (~len l2 = 0 <-> ~l2 = 0)
5 4 conv ne 
(len l2 = 0 <-> l2 = 0) -> (~len l2 = 0 <-> l2 != 0)
6 leneq0 
len l2 = 0 <-> l2 = 0
7 5, 6 ax_mp 
~len l2 = 0 <-> l2 != 0
8 peano1 
suc (len l1) != 0
9 lenS 
len (a : l1) = suc (len l1)
10 all2len 
a : l1, l2 e. all2 R -> len (a : l1) = len l2
11 9, 10 syl5eqr 
a : l1, l2 e. all2 R -> suc (len l1) = len l2
12 11 neeq1d 
a : l1, l2 e. all2 R -> (suc (len l1) != 0 <-> len l2 != 0)
13 12 conv ne 
a : l1, l2 e. all2 R -> (suc (len l1) != 0 <-> ~len l2 = 0)
14 8, 13 mpbii 
a : l1, l2 e. all2 R -> ~len l2 = 0
15 7, 14 sylib 
a : l1, l2 e. all2 R -> l2 != 0
16 3, 15 sylib 
a : l1, l2 e. all2 R -> E. b E. l2_ l2 = b : l2_
17 2, 16 ax_mp 
E. b E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R <-> a : l1, l2 e. all2 R
18 1, 17 ax_mp 
(E. b E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R <-> E. b E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R))) ->
  (a : l1, l2 e. all2 R <-> E. b E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R)))
19 bitr3 
(E. b (E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R) <-> E. b E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R) ->
  (E. b (E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R) <-> E. b E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R))) ->
  (E. b E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R <-> E. b E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R)))
20 exan2 
E. b (E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R) <-> E. b E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R
21 19, 20 ax_mp 
(E. b (E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R) <-> E. b E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R))) ->
  (E. b E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R <-> E. b E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R)))
22 bitr3 
(E. l2_ (l2 = b : l2_ /\ a : l1, l2 e. all2 R) <-> E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R) ->
  (E. l2_ (l2 = b : l2_ /\ a : l1, l2 e. all2 R) <-> E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R))) ->
  (E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R <-> E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R)))
23 exan2 
E. l2_ (l2 = b : l2_ /\ a : l1, l2 e. all2 R) <-> E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R
24 22, 23 ax_mp 
(E. l2_ (l2 = b : l2_ /\ a : l1, l2 e. all2 R) <-> E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R))) ->
  (E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R <-> E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R)))
25 aneq2a 
(l2 = b : l2_ -> (a : l1, l2 e. all2 R <-> a, b e. R /\ l1, l2_ e. all2 R)) ->
  (l2 = b : l2_ /\ a : l1, l2 e. all2 R <-> l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R))
26 all2S 
a : l1, b : l2_ e. all2 R <-> a, b e. R /\ l1, l2_ e. all2 R
27 preq2 
l2 = b : l2_ -> a : l1, l2 = a : l1, b : l2_
28 27 eleq1d 
l2 = b : l2_ -> (a : l1, l2 e. all2 R <-> a : l1, b : l2_ e. all2 R)
29 26, 28 syl6bb 
l2 = b : l2_ -> (a : l1, l2 e. all2 R <-> a, b e. R /\ l1, l2_ e. all2 R)
30 25, 29 ax_mp 
l2 = b : l2_ /\ a : l1, l2 e. all2 R <-> l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R)
31 30 exeqi 
E. l2_ (l2 = b : l2_ /\ a : l1, l2 e. all2 R) <-> E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R))
32 24, 31 ax_mp 
E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R <-> E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R))
33 32 exeqi 
E. b (E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R) <-> E. b E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R))
34 21, 33 ax_mp 
E. b E. l2_ l2 = b : l2_ /\ a : l1, l2 e. all2 R <-> E. b E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 R))
35 18, 34 ax_mp 
a : l1, l2 e. all2 R <-> E. b E. l2_ (l2 = b : l2_ /\ (a, b e. R /\ l1, l2_ e. all2 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)