Theorem nnsucelsuc 6252

Description: Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucelsucr 4325, but the forward direction, for all ordinals, implies excluded middle as seen as onsucelsucexmid 4346. (Contributed by Jim Kingdon, 25-Aug-2019.)

Assertion

Ref	Expression
nnsucelsuc	|- ( B e. om -> ( A e. B <-> suc A e. suc B ) )

Proof of Theorem nnsucelsuc

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2151	. . . 4 |- ( x = (/) -> ( A e. x <-> A e. (/) ) )
2		suceq 4229	. . . . 5 |- ( x = (/) -> suc x = suc (/) )
3	2	eleq2d 2157	. . . 4 |- ( x = (/) -> ( suc A e. suc x <-> suc A e. suc (/) ) )
4	1, 3	imbi12d 232	. . 3 |- ( x = (/) -> ( ( A e. x -> suc A e. suc x ) <-> ( A e. (/) -> suc A e. suc (/) ) ) )
5		eleq2 2151	. . . 4 |- ( x = y -> ( A e. x <-> A e. y ) )
6		suceq 4229	. . . . 5 |- ( x = y -> suc x = suc y )
7	6	eleq2d 2157	. . . 4 |- ( x = y -> ( suc A e. suc x <-> suc A e. suc y ) )
8	5, 7	imbi12d 232	. . 3 |- ( x = y -> ( ( A e. x -> suc A e. suc x ) <-> ( A e. y -> suc A e. suc y ) ) )
9		eleq2 2151	. . . 4 |- ( x = suc y -> ( A e. x <-> A e. suc y ) )
10		suceq 4229	. . . . 5 |- ( x = suc y -> suc x = suc suc y )
11	10	eleq2d 2157	. . . 4 |- ( x = suc y -> ( suc A e. suc x <-> suc A e. suc suc y ) )
12	9, 11	imbi12d 232	. . 3 |- ( x = suc y -> ( ( A e. x -> suc A e. suc x ) <-> ( A e. suc y -> suc A e. suc suc y ) ) )
13		eleq2 2151	. . . 4 |- ( x = B -> ( A e. x <-> A e. B ) )
14		suceq 4229	. . . . 5 |- ( x = B -> suc x = suc B )
15	14	eleq2d 2157	. . . 4 |- ( x = B -> ( suc A e. suc x <-> suc A e. suc B ) )
16	13, 15	imbi12d 232	. . 3 |- ( x = B -> ( ( A e. x -> suc A e. suc x ) <-> ( A e. B -> suc A e. suc B ) ) )
17		noel 3290	. . . 4 |- -. A e. (/)
18	17	pm2.21i 610	. . 3 |- ( A e. (/) -> suc A e. suc (/) )
19		elsuci 4230	. . . . . . . 8 |- ( A e. suc y -> ( A e. y \/ A = y ) )
20	19	adantl 271	. . . . . . 7 |- ( ( ( A e. y -> suc A e. suc y ) /\ A e. suc y ) -> ( A e. y \/ A = y ) )
21		simpl 107	. . . . . . . 8 |- ( ( ( A e. y -> suc A e. suc y ) /\ A e. suc y ) -> ( A e. y -> suc A e. suc y ) )
22		suceq 4229	. . . . . . . . 9 |- ( A = y -> suc A = suc y )
23	22	a1i 9	. . . . . . . 8 |- ( ( ( A e. y -> suc A e. suc y ) /\ A e. suc y ) -> ( A = y -> suc A = suc y ) )
24	21, 23	orim12d 735	. . . . . . 7 |- ( ( ( A e. y -> suc A e. suc y ) /\ A e. suc y ) -> ( ( A e. y \/ A = y ) -> ( suc A e. suc y \/ suc A = suc y ) ) )
25	20, 24	mpd 13	. . . . . 6 |- ( ( ( A e. y -> suc A e. suc y ) /\ A e. suc y ) -> ( suc A e. suc y \/ suc A = suc y ) )
26		vex 2622	. . . . . . . 8 |- y e. _V
27	26	sucex 4316	. . . . . . 7 |- suc y e. _V
28	27	elsuc2 4234	. . . . . 6 |- ( suc A e. suc suc y <-> ( suc A e. suc y \/ suc A = suc y ) )
29	25, 28	sylibr 132	. . . . 5 |- ( ( ( A e. y -> suc A e. suc y ) /\ A e. suc y ) -> suc A e. suc suc y )
30	29	ex 113	. . . 4 |- ( ( A e. y -> suc A e. suc y ) -> ( A e. suc y -> suc A e. suc suc y ) )
31	30	a1i 9	. . 3 |- ( y e. om -> ( ( A e. y -> suc A e. suc y ) -> ( A e. suc y -> suc A e. suc suc y ) ) )
32	4, 8, 12, 16, 18, 31	finds 4415	. 2 |- ( B e. om -> ( A e. B -> suc A e. suc B ) )
33		nnon 4424	. . 3 |- ( B e. om -> B e. On )
34		onsucelsucr 4325	. . 3 |- ( B e. On -> ( suc A e. suc B -> A e. B ) )
35	33, 34	syl 14	. 2 |- ( B e. om -> ( suc A e. suc B -> A e. B ) )
36	32, 35	impbid 127	1 |- ( B e. om -> ( A e. B <-> suc A e. suc B ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   \/ wo 664   = wceq 1289   e. wcel 1438   (/)c0 3286   Oncon0 4190   suc csuc 4192   omcom 4405

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3957  ax-nul 3965  ax-pow 4009  ax-pr 4036  ax-un 4260  ax-iinf 4403

This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-dif 3001  df-un 3003  df-in 3005  df-ss 3012  df-nul 3287  df-pw 3431  df-sn 3452  df-pr 3453  df-uni 3654  df-int 3689  df-tr 3937  df-iord 4193  df-on 4195  df-suc 4198  df-iom 4406

This theorem is referenced by:  nnsucsssuc  6253  nntri3or  6254  nnsucuniel  6256  nnaordi  6265