Theorem indstr ≪ | index | src | ≫

theorem indstr (G: wff) {x y: nat} (a: nat y) (px: wff x) (pa py: wff y):
  $ x = a -> (px <-> pa) $ >
  $ x = y -> (px <-> py) $ >
  $ G /\ A. x (x < y -> px) -> py $ >
  $ G -> pa $;

Step	Hyp	Ref	Expression
1		ltsucid	a < suc a
2		lteq1	x = a -> (x < suc a <-> a < suc a)
3		hyp ha	x = a -> (px <-> pa)
4	2, 3	imeqd	x = a -> (x < suc a -> px <-> a < suc a -> pa)
5	4	eale	A. x (x < suc a -> px) -> a < suc a -> pa
6	1, 5	mpi	A. x (x < suc a -> px) -> pa
7		id	z = suc a -> z = suc a
8	7	lteq2d	z = suc a -> (x < z <-> x < suc a)
9	8	imeq1d	z = suc a -> (x < z -> px <-> x < suc a -> px)
10	9	aleqd	z = suc a -> (A. x (x < z -> px) <-> A. x (x < suc a -> px))
11		id	z = 0 -> z = 0
12	11	lteq2d	z = 0 -> (x < z <-> x < 0)
13	12	imeq1d	z = 0 -> (x < z -> px <-> x < 0 -> px)
14	13	aleqd	z = 0 -> (A. x (x < z -> px) <-> A. x (x < 0 -> px))
15		id	z = y -> z = y
16	15	lteq2d	z = y -> (x < z <-> x < y)
17	16	imeq1d	z = y -> (x < z -> px <-> x < y -> px)
18	17	aleqd	z = y -> (A. x (x < z -> px) <-> A. x (x < y -> px))
19		id	z = suc y -> z = suc y
20	19	lteq2d	z = suc y -> (x < z <-> x < suc y)
21	20	imeq1d	z = suc y -> (x < z -> px <-> x < suc y -> px)
22	21	aleqd	z = suc y -> (A. x (x < z -> px) <-> A. x (x < suc y -> px))
23		absurd	~x < 0 -> x < 0 -> px
24		lt02	~x < 0
25	23, 24	ax_mp	x < 0 -> px
26	25	ax_gen	A. x (x < 0 -> px)
27	26	a1i	G -> A. x (x < 0 -> px)
28		hyp h	G /\ A. x (x < y -> px) -> py
29		hyp hy	x = y -> (px <-> py)
30	29	bi2d	x = y -> py -> px
31	30	com12	py -> x = y -> px
32	31	iald	py -> A. x (x = y -> px)
33	28, 32	rsyl	G /\ A. x (x < y -> px) -> A. x (x = y -> px)
34		bitr3	(x <= y <-> x < suc y) -> (x <= y <-> x < y \/ x = y) -> (x < suc y <-> x < y \/ x = y)
35		leltsuc	x <= y <-> x < suc y
36	34, 35	ax_mp	(x <= y <-> x < y \/ x = y) -> (x < suc y <-> x < y \/ x = y)
37		leloe	x <= y <-> x < y \/ x = y
38	36, 37	ax_mp	x < suc y <-> x < y \/ x = y
39	38	bi1i	x < suc y -> x < y \/ x = y
40	39	imim1i	(x < y \/ x = y -> px) -> x < suc y -> px
41		eor	(x < y -> px) -> (x = y -> px) -> x < y \/ x = y -> px
42	40, 41	syl6	(x < y -> px) -> (x = y -> px) -> x < suc y -> px
43	42	al2imi	A. x (x < y -> px) -> A. x (x = y -> px) -> A. x (x < suc y -> px)
44	43	anwr	G /\ A. x (x < y -> px) -> A. x (x = y -> px) -> A. x (x < suc y -> px)
45	33, 44	mpd	G /\ A. x (x < y -> px) -> A. x (x < suc y -> px)
46	10, 14, 18, 22, 27, 45	indd	G -> A. x (x < suc a -> px)
47	6, 46	syl	G -> pa

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_peano (peano1, peano2, peano5, addeq, add0, addS)