Theorem elpset ≪ | index | src | ≫ 

theorem elpset (m n v: nat) {x: nat}:
  $ n e. pset (m, v) <->
    0 < m /\
      0 < v /\
      A. x (0 < x /\ x <= n -> x || m) /\
      suc (m * suc n) || v $;
StepHypRefExpression
1 fstpr 
fst (m, v) = m
2 1 a1i 
y = n -> fst (m, v) = m
3 2 lteq2d 
y = n -> (0 < fst (m, v) <-> 0 < m)
4 sndpr 
snd (m, v) = v
5 4 a1i 
y = n -> snd (m, v) = v
6 5 lteq2d 
y = n -> (0 < snd (m, v) <-> 0 < v)
7 3, 6 aneqd 
y = n -> (0 < fst (m, v) /\ 0 < snd (m, v) <-> 0 < m /\ 0 < v)
8 lteq2 
x1 = x -> (0 < x1 <-> 0 < x)
9 8 anwr 
y = n /\ x1 = x -> (0 < x1 <-> 0 < x)
10 anr 
y = n /\ x1 = x -> x1 = x
11 anl 
y = n /\ x1 = x -> y = n
12 10, 11 leeqd 
y = n /\ x1 = x -> (x1 <= y <-> x <= n)
13 9, 12 aneqd 
y = n /\ x1 = x -> (0 < x1 /\ x1 <= y <-> 0 < x /\ x <= n)
14 1 a1i 
y = n /\ x1 = x -> fst (m, v) = m
15 10, 14 dvdeqd 
y = n /\ x1 = x -> (x1 || fst (m, v) <-> x || m)
16 13, 15 imeqd 
y = n /\ x1 = x -> (0 < x1 /\ x1 <= y -> x1 || fst (m, v) <-> 0 < x /\ x <= n -> x || m)
17 16 cbvald 
y = n -> (A. x1 (0 < x1 /\ x1 <= y -> x1 || fst (m, v)) <-> A. x (0 < x /\ x <= n -> x || m))
18 7, 17 aneqd 
y = n -> (0 < fst (m, v) /\ 0 < snd (m, v) /\ A. x1 (0 < x1 /\ x1 <= y -> x1 || fst (m, v)) <-> 0 < m /\ 0 < v /\ A. x (0 < x /\ x <= n -> x || m))
19 suceq 
y = n -> suc y = suc n
20 2, 19 muleqd 
y = n -> fst (m, v) * suc y = m * suc n
21 20 suceqd 
y = n -> suc (fst (m, v) * suc y) = suc (m * suc n)
22 21, 5 dvdeqd 
y = n -> (suc (fst (m, v) * suc y) || snd (m, v) <-> suc (m * suc n) || v)
23 18, 22 aneqd 
y = n ->
  (0 < fst (m, v) /\ 0 < snd (m, v) /\ A. x1 (0 < x1 /\ x1 <= y -> x1 || fst (m, v)) /\ suc (fst (m, v) * suc y) || snd (m, v) <->
    0 < m /\ 0 < v /\ A. x (0 < x /\ x <= n -> x || m) /\ suc (m * suc n) || v)
24 23 elabe 
n e. {y | 0 < fst (m, v) /\ 0 < snd (m, v) /\ A. x1 (0 < x1 /\ x1 <= y -> x1 || fst (m, v)) /\ suc (fst (m, v) * suc y) || snd (m, v)} <->
  0 < m /\ 0 < v /\ A. x (0 < x /\ x <= n -> x || m) /\ suc (m * suc n) || v
25 24 conv pset 
n e. pset (m, v) <-> 0 < m /\ 0 < v /\ A. x (0 < x /\ x <= n -> x || m) /\ suc (m * suc n) || v

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)