Theorem pseteqd ≪ | index | src | ≫ 

theorem pseteqd (_G: wff) (_a1 _a2: nat):
  $ _G -> _a1 = _a2 $ >
  $ _G -> pset _a1 == pset _a2 $;
StepHypRefExpression
1 hyp _ah 
_G -> _a1 = _a2
2 1 fsteqd 
_G -> fst _a1 = fst _a2
3 2 lteq2d 
_G -> (0 < fst _a1 <-> 0 < fst _a2)
4 1 sndeqd 
_G -> snd _a1 = snd _a2
5 4 lteq2d 
_G -> (0 < snd _a1 <-> 0 < snd _a2)
6 3, 5 aneqd 
_G -> (0 < fst _a1 /\ 0 < snd _a1 <-> 0 < fst _a2 /\ 0 < snd _a2)
7 2 dvdeq2d 
_G -> (x || fst _a1 <-> x || fst _a2)
8 7 imeq2d 
_G -> (0 < x /\ x <= n -> x || fst _a1 <-> 0 < x /\ x <= n -> x || fst _a2)
9 8 aleqd 
_G -> (A. x (0 < x /\ x <= n -> x || fst _a1) <-> A. x (0 < x /\ x <= n -> x || fst _a2))
10 6, 9 aneqd 
_G -> (0 < fst _a1 /\ 0 < snd _a1 /\ A. x (0 < x /\ x <= n -> x || fst _a1) <-> 0 < fst _a2 /\ 0 < snd _a2 /\ A. x (0 < x /\ x <= n -> x || fst _a2))
11 2 muleq1d 
_G -> fst _a1 * suc n = fst _a2 * suc n
12 11 suceqd 
_G -> suc (fst _a1 * suc n) = suc (fst _a2 * suc n)
13 12, 4 dvdeqd 
_G -> (suc (fst _a1 * suc n) || snd _a1 <-> suc (fst _a2 * suc n) || snd _a2)
14 10, 13 aneqd 
_G ->
  (0 < fst _a1 /\ 0 < snd _a1 /\ A. x (0 < x /\ x <= n -> x || fst _a1) /\ suc (fst _a1 * suc n) || snd _a1 <->
    0 < fst _a2 /\ 0 < snd _a2 /\ A. x (0 < x /\ x <= n -> x || fst _a2) /\ suc (fst _a2 * suc n) || snd _a2)
15 14 abeqd 
_G ->
  {n | 0 < fst _a1 /\ 0 < snd _a1 /\ A. x (0 < x /\ x <= n -> x || fst _a1) /\ suc (fst _a1 * suc n) || snd _a1} ==
    {n | 0 < fst _a2 /\ 0 < snd _a2 /\ A. x (0 < x /\ x <= n -> x || fst _a2) /\ suc (fst _a2 * suc n) || snd _a2}
16 15 conv pset 
_G -> pset _a1 == pset _a2

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 (peano2, addeq, muleq)