Theorem dmsn ≪ | index | src | ≫ 

theorem dmsn (x y: nat): $ Dom (sn (x, y)) == sn x $;
StepHypRefExpression
1 bitr 
(a1 e. Dom (sn (x, y)) <-> E. a2 a1, a2 e. sn (x, y)) -> (E. a2 a1, a2 e. sn (x, y) <-> a1 e. sn x) -> (a1 e. Dom (sn (x, y)) <-> a1 e. sn x)
2 eldm 
a1 e. Dom (sn (x, y)) <-> E. a2 a1, a2 e. sn (x, y)
3 1, 2 ax_mp 
(E. a2 a1, a2 e. sn (x, y) <-> a1 e. sn x) -> (a1 e. Dom (sn (x, y)) <-> a1 e. sn x)
4 bitr4 
(E. a2 a1, a2 e. sn (x, y) <-> E. a2 (a2 = y /\ a1 = x)) -> (a1 e. sn x <-> E. a2 (a2 = y /\ a1 = x)) -> (E. a2 a1, a2 e. sn (x, y) <-> a1 e. sn x)
5 bitr 
(a1, a2 e. sn (x, y) <-> a1, a2 = x, y) -> (a1, a2 = x, y <-> a2 = y /\ a1 = x) -> (a1, a2 e. sn (x, y) <-> a2 = y /\ a1 = x)
6 elsn 
a1, a2 e. sn (x, y) <-> a1, a2 = x, y
7 5, 6 ax_mp 
(a1, a2 = x, y <-> a2 = y /\ a1 = x) -> (a1, a2 e. sn (x, y) <-> a2 = y /\ a1 = x)
8 bitr 
(a1, a2 = x, y <-> a1 = x /\ a2 = y) -> (a1 = x /\ a2 = y <-> a2 = y /\ a1 = x) -> (a1, a2 = x, y <-> a2 = y /\ a1 = x)
9 prth 
a1, a2 = x, y <-> a1 = x /\ a2 = y
10 8, 9 ax_mp 
(a1 = x /\ a2 = y <-> a2 = y /\ a1 = x) -> (a1, a2 = x, y <-> a2 = y /\ a1 = x)
11 ancomb 
a1 = x /\ a2 = y <-> a2 = y /\ a1 = x
12 10, 11 ax_mp 
a1, a2 = x, y <-> a2 = y /\ a1 = x
13 7, 12 ax_mp 
a1, a2 e. sn (x, y) <-> a2 = y /\ a1 = x
14 13 exeqi 
E. a2 a1, a2 e. sn (x, y) <-> E. a2 (a2 = y /\ a1 = x)
15 4, 14 ax_mp 
(a1 e. sn x <-> E. a2 (a2 = y /\ a1 = x)) -> (E. a2 a1, a2 e. sn (x, y) <-> a1 e. sn x)
16 bitr4 
(a1 e. sn x <-> a1 = x) -> (E. a2 (a2 = y /\ a1 = x) <-> a1 = x) -> (a1 e. sn x <-> E. a2 (a2 = y /\ a1 = x))
17 elsn 
a1 e. sn x <-> a1 = x
18 16, 17 ax_mp 
(E. a2 (a2 = y /\ a1 = x) <-> a1 = x) -> (a1 e. sn x <-> E. a2 (a2 = y /\ a1 = x))
19 biidd 
a2 = y -> (a1 = x <-> a1 = x)
20 19 exeqe 
E. a2 (a2 = y /\ a1 = x) <-> a1 = x
21 18, 20 ax_mp 
a1 e. sn x <-> E. a2 (a2 = y /\ a1 = x)
22 15, 21 ax_mp 
E. a2 a1, a2 e. sn (x, y) <-> a1 e. sn x
23 3, 22 ax_mp 
a1 e. Dom (sn (x, y)) <-> a1 e. sn x
24 23 ax_gen 
A. a1 (a1 e. Dom (sn (x, y)) <-> a1 e. sn x)
25 24 conv eqs 
Dom (sn (x, y)) == sn x

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)