Theorem elobind ≪ | index | src | ≫

theorem elobind (F: set) (n x: nat) {y: nat}:
  $ x e. obind n F <-> E. y (n = suc y /\ x e. F @ y) $;

Step	Hyp	Ref	Expression
1		binth	~x e. 0 -> ~E. y (0 = suc y /\ x e. F @ y) -> (x e. 0 <-> E. y (0 = suc y /\ x e. F @ y))
2		nel0	~x e. 0
3	1, 2	ax_mp	~E. y (0 = suc y /\ x e. F @ y) -> (x e. 0 <-> E. y (0 = suc y /\ x e. F @ y))
4		eqcom	0 = suc y -> suc y = 0
5	4	anwl	0 = suc y /\ x e. F @ y -> suc y = 0
6		peano1	suc y != 0
7	6	conv ne	~suc y = 0
8	5, 7	mt	~(0 = suc y /\ x e. F @ y)
9	8	nexi	~E. y (0 = suc y /\ x e. F @ y)
10	3, 9	ax_mp	x e. 0 <-> E. y (0 = suc y /\ x e. F @ y)
11		obind0	obind 0 F = 0
12		obindeq1	n = 0 -> obind n F = obind 0 F
13	11, 12	syl6eq	n = 0 -> obind n F = 0
14	13	elneq2d	n = 0 -> (x e. obind n F <-> x e. 0)
15		eqeq1	n = 0 -> (n = suc y <-> 0 = suc y)
16	15	aneq1d	n = 0 -> (n = suc y /\ x e. F @ y <-> 0 = suc y /\ x e. F @ y)
17	16	exeqd	n = 0 -> (E. y (n = suc y /\ x e. F @ y) <-> E. y (0 = suc y /\ x e. F @ y))
18	14, 17	bieqd	n = 0 -> (x e. obind n F <-> E. y (n = suc y /\ x e. F @ y) <-> (x e. 0 <-> E. y (0 = suc y /\ x e. F @ y)))
19	10, 18	mpbiri	n = 0 -> (x e. obind n F <-> E. y (n = suc y /\ x e. F @ y))
20		exsuc	n != 0 <-> E. a1 n = suc a1
21	20	conv ne	~n = 0 <-> E. a1 n = suc a1
22		bicom	(E. y (y = a1 /\ x e. F @ y) <-> x e. F @ a1) -> (x e. F @ a1 <-> E. y (y = a1 /\ x e. F @ y))
23		appeq2	y = a1 -> F @ y = F @ a1
24	23	elneq2d	y = a1 -> (x e. F @ y <-> x e. F @ a1)
25	24	exeqe	E. y (y = a1 /\ x e. F @ y) <-> x e. F @ a1
26	22, 25	ax_mp	x e. F @ a1 <-> E. y (y = a1 /\ x e. F @ y)
27		obindS	obind (suc a1) F = F @ a1
28		obindeq1	n = suc a1 -> obind n F = obind (suc a1) F
29	27, 28	syl6eq	n = suc a1 -> obind n F = F @ a1
30	29	elneq2d	n = suc a1 -> (x e. obind n F <-> x e. F @ a1)
31		eqcomb	a1 = y <-> y = a1
32		peano2	suc a1 = suc y <-> a1 = y
33		eqeq1	n = suc a1 -> (n = suc y <-> suc a1 = suc y)
34	32, 33	syl6bb	n = suc a1 -> (n = suc y <-> a1 = y)
35	31, 34	syl6bb	n = suc a1 -> (n = suc y <-> y = a1)
36	35	aneq1d	n = suc a1 -> (n = suc y /\ x e. F @ y <-> y = a1 /\ x e. F @ y)
37	36	exeqd	n = suc a1 -> (E. y (n = suc y /\ x e. F @ y) <-> E. y (y = a1 /\ x e. F @ y))
38	30, 37	bieqd	n = suc a1 -> (x e. obind n F <-> E. y (n = suc y /\ x e. F @ y) <-> (x e. F @ a1 <-> E. y (y = a1 /\ x e. F @ y)))
39	26, 38	mpbiri	n = suc a1 -> (x e. obind n F <-> E. y (n = suc y /\ x e. F @ y))
40	39	eex	E. a1 n = suc a1 -> (x e. obind n F <-> E. y (n = suc y /\ x e. F @ y))
41	21, 40	sylbi	~n = 0 -> (x e. obind n F <-> E. y (n = suc y /\ x e. F @ y))
42	19, 41	cases	x e. obind n F <-> E. y (n = suc y /\ x e. F @ y)

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)