Theorem peano5 2394

Description: The induction postulate: any class containing zero and closed under the successor operation contains all natural numbers. One of Peano's 5 postulates for arithmetic. Proposition 7.30(5) of [TakeutiZaring] p. 43.

Assertion

Ref	Expression
peano5	|- (((/) e. A /\ A.x e. om (x e. A -> suc x e. A)) -> om (_ A)

Distinct variable group(s):   x,A

Proof of Theorem peano5

Step	Hyp	Ref	Expression
1		eldifn 1592	. . . . . 6 |- (y e. (om \ A) -> -. y e. A)
2	1	adantl 305	. . . . 5 |- ((((/) e. A /\ A.x e. om (x e. A -> suc x e. A)) /\ y e. (om \ A)) -> -. y e. A)
3		nnsuc 2389	. . . . . . . . . 10 |- ((y e. om /\ -. y = (/)) -> E.x e. om y = suc x)
4		eldifi 1591	. . . . . . . . . . 11 |- (y e. (om \ A) -> y e. om)
5	4	adantl 305	. . . . . . . . . 10 |- (((/) e. A /\ y e. (om \ A)) -> y e. om)
6		elndif 1593	. . . . . . . . . . . 12 |- ((/) e. A -> -. (/) e. (om \ A))
7		eleq1 1149	. . . . . . . . . . . . . . 15 |- (y = (/) -> (y e. (om \ A) <-> (/) e. (om \ A)))
8	7	biimpcd 137	. . . . . . . . . . . . . 14 |- (y e. (om \ A) -> (y = (/) -> (/) e. (om \ A)))
9	8	con3d 87	. . . . . . . . . . . . 13 |- (y e. (om \ A) -> (-. (/) e. (om \ A) -> -. y = (/)))
10	9	com12 13	. . . . . . . . . . . 12 |- (-. (/) e. (om \ A) -> (y e. (om \ A) -> -. y = (/)))
11	6, 10	syl 12	. . . . . . . . . . 11 |- ((/) e. A -> (y e. (om \ A) -> -. y = (/)))
12	11	imp 277	. . . . . . . . . 10 |- (((/) e. A /\ y e. (om \ A)) -> -. y = (/))
13	3, 5, 12	sylanc 361	. . . . . . . . 9 |- (((/) e. A /\ y e. (om \ A)) -> E.x e. om y = suc x)
14	13	adantlr 310	. . . . . . . 8 |- ((((/) e. A /\ A.x e. om (x e. A -> suc x e. A)) /\ y e. (om \ A)) -> E.x e. om y = suc x)
15	14	adantr 306	. . . . . . 7 |- (((((/) e. A /\ A.x e. om (x e. A -> suc x e. A)) /\ y e. (om \ A)) /\ ((om \ A) i^i y) = (/)) -> E.x e. om y = suc x)
16		hbra1 1237	. . . . . . . . . . . 12 |- (A.x e. om (x e. A -> suc x e. A) -> A.xA.x e. om (x e. A -> suc x e. A))
17		ax-17 925	. . . . . . . . . . . 12 |- ((y e. (om \ A) /\ ((om \ A) i^i y) = (/)) -> A.x(y e. (om \ A) /\ ((om \ A) i^i y) = (/)))
18	16, 17	hban 704	. . . . . . . . . . 11 |- ((A.x e. om (x e. A -> suc x e. A) /\ (y e. (om \ A) /\ ((om \ A) i^i y) = (/))) -> A.x(A.x e. om (x e. A -> suc x e. A) /\ (y e. (om \ A) /\ ((om \ A) i^i y) = (/))))
19		ax-17 925	. . . . . . . . . . 11 |- (y e. A -> A.x y e. A)
20		ra4 1243	. . . . . . . . . . . 12 |- (A.x e. om (x e. A -> suc x e. A) -> (x e. om -> (x e. A -> suc x e. A)))
21		visset 1350	. . . . . . . . . . . . . . . . . . 19 |- x e. V
22	21	sucid 2304	. . . . . . . . . . . . . . . . . 18 |- x e. suc x
23		eleq2 1150	. . . . . . . . . . . . . . . . . 18 |- (y = suc x -> (x e. y <-> x e. suc x))
24	22, 23	mpbiri 169	. . . . . . . . . . . . . . . . 17 |- (y = suc x -> x e. y)
25		eleq1 1149	. . . . . . . . . . . . . . . . . . 19 |- (y = suc x -> (y e. om <-> suc x e. om))
26		peano2b 2388	. . . . . . . . . . . . . . . . . . 19 |- (x e. om <-> suc x e. om)
27	25, 26	syl6bbr 416	. . . . . . . . . . . . . . . . . 18 |- (y = suc x -> (y e. om <-> x e. om))
28		neldif 1594	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. om /\ -. x e. (om \ A)) -> x e. A)
29		minel 1743	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. y /\ ((om \ A) i^i y) = (/)) -> -. x e. (om \ A))
30	28, 29	sylan2 346	. . . . . . . . . . . . . . . . . . 19 |- ((x e. om /\ (x e. y /\ ((om \ A) i^i y) = (/))) -> x e. A)
31	30	exp32 294	. . . . . . . . . . . . . . . . . 18 |- (x e. om -> (x e. y -> (((om \ A) i^i y) = (/) -> x e. A)))
32	27, 31	syl6bi 187	. . . . . . . . . . . . . . . . 17 |- (y = suc x -> (y e. om -> (x e. y -> (((om \ A) i^i y) = (/) -> x e. A))))
33	24, 32	mpid 48	. . . . . . . . . . . . . . . 16 |- (y = suc x -> (y e. om -> (((om \ A) i^i y) = (/) -> x e. A)))
34	33, 4	syl5 22	. . . . . . . . . . . . . . 15 |- (y = suc x -> (y e. (om \ A) -> (((om \ A) i^i y) = (/) -> x e. A)))
35	34	imp3a 279	. . . . . . . . . . . . . 14 |- (y = suc x -> ((y e. (om \ A) /\ ((om \ A) i^i y) = (/)) -> x e. A))
36		eleq1a 1158	. . . . . . . . . . . . . . 15 |- (suc x e. A -> (y = suc x -> y e. A))
37	36	com12 13	. . . . . . . . . . . . . 14 |- (y = suc x -> (suc x e. A -> y e. A))
38	35, 37	syl34d 29	. . . . . . . . . . . . 13 |- (y = suc x -> ((x e. A -> suc x e. A) -> ((y e. (om \ A) /\ ((om \ A) i^i y) = (/)) -> y e. A)))
39	38	com13 33	. . . . . . . . . . . 12 |- ((y e. (om \ A) /\ ((om \ A) i^i y) = (/)) -> ((x e. A -> suc x e. A) -> (y = suc x -> y e. A)))
40	20, 39	sylan9 359	. . . . . . . . . . 11 |- ((A.x e. om (x e. A -> suc x e. A) /\ (y e. (om \ A) /\ ((om \ A) i^i y) = (/))) -> (x e. om -> (y = suc x -> y e. A)))
41	18, 19, 40	r19.23ad 1285	. . . . . . . . . 10 |- ((A.x e. om (x e. A -> suc x e. A) /\ (y e. (om \ A) /\ ((om \ A) i^i y) = (/))) -> (E.x e. om y = suc x -> y e. A))
42	41	exp32 294	. . . . . . . . 9 |- (A.x e. om (x e. A -> suc x e. A) -> (y e. (om \ A) -> (((om \ A) i^i y) = (/) -> (E.x e. om y = suc x -> y e. A))))
43	42	a1i 7	. . . . . . . 8 |- ((/) e. A -> (A.x e. om (x e. A -> suc x e. A) -> (y e. (om \ A) -> (((om \ A) i^i y) = (/) -> (E.x e. om y = suc x -> y e. A)))))
44	43	imp41 286	. . . . . . 7 |- (((((/) e. A /\ A.x e. om (x e. A -> suc x e. A)) /\ y e. (om \ A)) /\ ((om \ A) i^i y) = (/)) -> (E.x e. om y = suc x -> y e. A))
45	15, 44	mpd 46	. . . . . 6 |- (((((/) e. A /\ A.x e. om (x e. A -> suc x e. A)) /\ y e. (om \ A)) /\ ((om \ A) i^i y) = (/)) -> y e. A)
46	45	exp 291	. . . . 5 |- ((((/) e. A /\ A.x e. om (x e. A -> suc x e. A)) /\ y e. (om \ A)) -> (((om \ A) i^i y) = (/) -> y e. A))
47	2, 46	mtod 95	. . . 4 |- ((((/) e. A /\ A.x e. om (x e. A -> suc x e. A)) /\ y e. (om \ A)) -> -. ((om \ A) i^i y) = (/))
48	47	nrexdv 1271	. . 3 |- (((/) e. A /\ A.x e. om (x e. A -> suc x e. A)) -> -. E.y e. (om \ A)((om \ A) i^i y) = (/))
49		difss 1596	. . . 4 |- (om \ A) (_ om
50		ordom 2382	. . . . 5 |- Ord om
51		tz7.5 2220	. . . . 5 |- ((Ord om /\ ((om \ A) (_ om /\ -. (om \ A) = (/))) -> E.y e. (om \ A)((om \ A) i^i y) = (/))
52	50, 51	mpan 518	. . . 4 |- (((om \ A) (_ om /\ -. (om \ A) = (/)) -> E.y e. (om \ A)((om \ A) i^i y) = (/))
53	49, 52	mpan 518	. . 3 |- (-. (om \ A) = (/) -> E.y e. (om \ A)((om \ A) i^i y) = (/))
54	48, 53	nsyl2 103	. 2 |- (((/) e. A /\ A.x e. om (x e. A -> suc x e. A)) -> (om \ A) = (/))
55		ssdif0 1748	. 2 |- (om (_ A <-> (om \ A) = (/))
56	54, 55	sylibr 175	1 |- (((/) e. A /\ A.x e. om (x e. A -> suc x e. A)) -> om (_ A)

Syntax hints:  -. wn 1   -> wi 2   /\ wa 196   e. wel 803   = wceq 1091   e. wcel 1092  A.wral 1201  E.wrex 1202   \ cdif 1484   i^i cin 1486   (_ wss 1487  (/)c0 1707  Ord word 2198  suc csuc 2201  omcom 2372

This theorem is referenced by:  find 2396  finds 2397  finds2 2399  omex 3475  dfom3 3477

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373

metamath.org