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		eqidd	z = suc a -> x = x
8		id	z = suc a -> z = suc a
9	7, 8	lteqd	z = suc a -> (x < z <-> x < suc a)
10		biidd	z = suc a -> (px <-> px)
11	9, 10	imeqd	z = suc a -> (x < z -> px <-> x < suc a -> px)
12	11	aleqd	z = suc a -> (A. x (x < z -> px) <-> A. x (x < suc a -> px))
13		eqidd	z = 0 -> x = x
14		id	z = 0 -> z = 0
15	13, 14	lteqd	z = 0 -> (x < z <-> x < 0)
16		biidd	z = 0 -> (px <-> px)
17	15, 16	imeqd	z = 0 -> (x < z -> px <-> x < 0 -> px)
18	17	aleqd	z = 0 -> (A. x (x < z -> px) <-> A. x (x < 0 -> px))
19		eqidd	z = y -> x = x
20		id	z = y -> z = y
21	19, 20	lteqd	z = y -> (x < z <-> x < y)
22		biidd	z = y -> (px <-> px)
23	21, 22	imeqd	z = y -> (x < z -> px <-> x < y -> px)
24	23	aleqd	z = y -> (A. x (x < z -> px) <-> A. x (x < y -> px))
25		eqidd	z = suc y -> x = x
26		id	z = suc y -> z = suc y
27	25, 26	lteqd	z = suc y -> (x < z <-> x < suc y)
28		biidd	z = suc y -> (px <-> px)
29	27, 28	imeqd	z = suc y -> (x < z -> px <-> x < suc y -> px)
30	29	aleqd	z = suc y -> (A. x (x < z -> px) <-> A. x (x < suc y -> px))
31		absurd	~x < 0 -> x < 0 -> px
32		lt02	~x < 0
33	31, 32	ax_mp	x < 0 -> px
34	33	ax_gen	A. x (x < 0 -> px)
35	34	a1i	G -> A. x (x < 0 -> px)
36		hyp h	G /\ A. x (x < y -> px) -> py
37		hyp hy	x = y -> (px <-> py)
38	37	bi2d	x = y -> py -> px
39	38	com12	py -> x = y -> px
40	39	iald	py -> A. x (x = y -> px)
41	36, 40	rsyl	G /\ A. x (x < y -> px) -> A. x (x = y -> px)
42		bitr3	(x <= y <-> x < suc y) -> (x <= y <-> x < y \/ x = y) -> (x < suc y <-> x < y \/ x = y)
43		leltsuc	x <= y <-> x < suc y
44	42, 43	ax_mp	(x <= y <-> x < y \/ x = y) -> (x < suc y <-> x < y \/ x = y)
45		leloe	x <= y <-> x < y \/ x = y
46	44, 45	ax_mp	x < suc y <-> x < y \/ x = y
47	46	bi1i	x < suc y -> x < y \/ x = y
48	47	imim1i	(x < y \/ x = y -> px) -> x < suc y -> px
49		eor	(x < y -> px) -> (x = y -> px) -> x < y \/ x = y -> px
50	48, 49	syl6	(x < y -> px) -> (x = y -> px) -> x < suc y -> px
51	50	al2imi	A. x (x < y -> px) -> A. x (x = y -> px) -> A. x (x < suc y -> px)
52	51	anwr	G /\ A. x (x < y -> px) -> A. x (x = y -> px) -> A. x (x < suc y -> px)
53	41, 52	mpd	G /\ A. x (x < y -> px) -> A. x (x < suc y -> px)
54	12, 18, 24, 30, 35, 53	indd	G -> A. x (x < suc a -> px)
55	6, 54	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)