Theorem nnsucelsuc 6474

Description: Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucelsucr 4493, but the forward direction, for all ordinals, implies excluded middle as seen as onsucelsucexmid 4515. (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 2235	. . . 4 |- ( x = (/) -> ( A e. x <-> A e. (/) ) )
2		suceq 4388	. . . . 5 |- ( x = (/) -> suc x = suc (/) )
3	2	eleq2d 2241	. . . 4 |- ( x = (/) -> ( suc A e. suc x <-> suc A e. suc (/) ) )
4	1, 3	imbi12d 233	. . 3 |- ( x = (/) -> ( ( A e. x -> suc A e. suc x ) <-> ( A e. (/) -> suc A e. suc (/) ) ) )
5		eleq2 2235	. . . 4 |- ( x = y -> ( A e. x <-> A e. y ) )
6		suceq 4388	. . . . 5 |- ( x = y -> suc x = suc y )
7	6	eleq2d 2241	. . . 4 |- ( x = y -> ( suc A e. suc x <-> suc A e. suc y ) )
8	5, 7	imbi12d 233	. . 3 |- ( x = y -> ( ( A e. x -> suc A e. suc x ) <-> ( A e. y -> suc A e. suc y ) ) )
9		eleq2 2235	. . . 4 |- ( x = suc y -> ( A e. x <-> A e. suc y ) )
10		suceq 4388	. . . . 5 |- ( x = suc y -> suc x = suc suc y )
11	10	eleq2d 2241	. . . 4 |- ( x = suc y -> ( suc A e. suc x <-> suc A e. suc suc y ) )
12	9, 11	imbi12d 233	. . 3 |- ( x = suc y -> ( ( A e. x -> suc A e. suc x ) <-> ( A e. suc y -> suc A e. suc suc y ) ) )
13		eleq2 2235	. . . 4 |- ( x = B -> ( A e. x <-> A e. B ) )
14		suceq 4388	. . . . 5 |- ( x = B -> suc x = suc B )
15	14	eleq2d 2241	. . . 4 |- ( x = B -> ( suc A e. suc x <-> suc A e. suc B ) )
16	13, 15	imbi12d 233	. . 3 |- ( x = B -> ( ( A e. x -> suc A e. suc x ) <-> ( A e. B -> suc A e. suc B ) ) )
17		noel 3419	. . . 4 |- -. A e. (/)
18	17	pm2.21i 642	. . 3 |- ( A e. (/) -> suc A e. suc (/) )
19		elsuci 4389	. . . . . . . 8 |- ( A e. suc y -> ( A e. y \/ A = y ) )
20	19	adantl 275	. . . . . . 7 |- ( ( ( A e. y -> suc A e. suc y ) /\ A e. suc y ) -> ( A e. y \/ A = y ) )
21		simpl 108	. . . . . . . 8 |- ( ( ( A e. y -> suc A e. suc y ) /\ A e. suc y ) -> ( A e. y -> suc A e. suc y ) )
22		suceq 4388	. . . . . . . . 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 782	. . . . . . 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 2734	. . . . . . . 8 |- y e. _V
27	26	sucex 4484	. . . . . . 7 |- suc y e. _V
28	27	elsuc2 4393	. . . . . 6 |- ( suc A e. suc suc y <-> ( suc A e. suc y \/ suc A = suc y ) )
29	25, 28	sylibr 133	. . . . 5 |- ( ( ( A e. y -> suc A e. suc y ) /\ A e. suc y ) -> suc A e. suc suc y )
30	29	ex 114	. . . 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 4585	. 2 |- ( B e. om -> ( A e. B -> suc A e. suc B ) )
33		nnon 4595	. . 3 |- ( B e. om -> B e. On )
34		onsucelsucr 4493	. . 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 128	1 |- ( B e. om -> ( A e. B <-> suc A e. suc B ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   \/ wo 704   = wceq 1349   e. wcel 2142   (/)c0 3415   Oncon0 4349   suc csuc 4351   omcom 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-13 2144  ax-14 2145  ax-ext 2153  ax-sep 4108  ax-nul 4116  ax-pow 4161  ax-pr 4195  ax-un 4419  ax-iinf 4573

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ral 2454  df-rex 2455  df-v 2733  df-dif 3124  df-un 3126  df-in 3128  df-ss 3135  df-nul 3416  df-pw 3569  df-sn 3590  df-pr 3591  df-uni 3798  df-int 3833  df-tr 4089  df-iord 4352  df-on 4354  df-suc 4357  df-iom 4576

This theorem is referenced by:  nnsucsssuc  6475  nntri3or  6476  nnsucuniel  6478  nnaordi  6491  ennnfonelemhom  12374