Theorem nnsucsssuc 6269

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

Assertion

Ref	Expression
nnsucsssuc	|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> suc A C_ suc B ) )

Proof of Theorem nnsucsssuc

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

Step	Hyp	Ref	Expression
1		sseq1 3050	. . . . . 6 |- ( x = A -> ( x C_ B <-> A C_ B ) )
2		suceq 4240	. . . . . . 7 |- ( x = A -> suc x = suc A )
3	2	sseq1d 3056	. . . . . 6 |- ( x = A -> ( suc x C_ suc B <-> suc A C_ suc B ) )
4	1, 3	imbi12d 233	. . . . 5 |- ( x = A -> ( ( x C_ B -> suc x C_ suc B ) <-> ( A C_ B -> suc A C_ suc B ) ) )
5	4	imbi2d 229	. . . 4 |- ( x = A -> ( ( B e. om -> ( x C_ B -> suc x C_ suc B ) ) <-> ( B e. om -> ( A C_ B -> suc A C_ suc B ) ) ) )
6		sseq1 3050	. . . . . 6 |- ( x = (/) -> ( x C_ B <-> (/) C_ B ) )
7		suceq 4240	. . . . . . 7 |- ( x = (/) -> suc x = suc (/) )
8	7	sseq1d 3056	. . . . . 6 |- ( x = (/) -> ( suc x C_ suc B <-> suc (/) C_ suc B ) )
9	6, 8	imbi12d 233	. . . . 5 |- ( x = (/) -> ( ( x C_ B -> suc x C_ suc B ) <-> ( (/) C_ B -> suc (/) C_ suc B ) ) )
10		sseq1 3050	. . . . . 6 |- ( x = y -> ( x C_ B <-> y C_ B ) )
11		suceq 4240	. . . . . . 7 |- ( x = y -> suc x = suc y )
12	11	sseq1d 3056	. . . . . 6 |- ( x = y -> ( suc x C_ suc B <-> suc y C_ suc B ) )
13	10, 12	imbi12d 233	. . . . 5 |- ( x = y -> ( ( x C_ B -> suc x C_ suc B ) <-> ( y C_ B -> suc y C_ suc B ) ) )
14		sseq1 3050	. . . . . 6 |- ( x = suc y -> ( x C_ B <-> suc y C_ B ) )
15		suceq 4240	. . . . . . 7 |- ( x = suc y -> suc x = suc suc y )
16	15	sseq1d 3056	. . . . . 6 |- ( x = suc y -> ( suc x C_ suc B <-> suc suc y C_ suc B ) )
17	14, 16	imbi12d 233	. . . . 5 |- ( x = suc y -> ( ( x C_ B -> suc x C_ suc B ) <-> ( suc y C_ B -> suc suc y C_ suc B ) ) )
18		peano3 4426	. . . . . . . . 9 |- ( B e. om -> suc B =/= (/) )
19	18	neneqd 2277	. . . . . . . 8 |- ( B e. om -> -. suc B = (/) )
20		peano2 4425	. . . . . . . . . 10 |- ( B e. om -> suc B e. om )
21		0elnn 4447	. . . . . . . . . 10 |- ( suc B e. om -> ( suc B = (/) \/ (/) e. suc B ) )
22	20, 21	syl 14	. . . . . . . . 9 |- ( B e. om -> ( suc B = (/) \/ (/) e. suc B ) )
23	22	ord 679	. . . . . . . 8 |- ( B e. om -> ( -. suc B = (/) -> (/) e. suc B ) )
24	19, 23	mpd 13	. . . . . . 7 |- ( B e. om -> (/) e. suc B )
25		nnord 4441	. . . . . . . 8 |- ( B e. om -> Ord B )
26		ordsucim 4332	. . . . . . . 8 |- ( Ord B -> Ord suc B )
27		0ex 3974	. . . . . . . . 9 |- (/) e. _V
28		ordelsuc 4337	. . . . . . . . 9 |- ( ( (/) e. _V /\ Ord suc B ) -> ( (/) e. suc B <-> suc (/) C_ suc B ) )
29	27, 28	mpan 416	. . . . . . . 8 |- ( Ord suc B -> ( (/) e. suc B <-> suc (/) C_ suc B ) )
30	25, 26, 29	3syl 17	. . . . . . 7 |- ( B e. om -> ( (/) e. suc B <-> suc (/) C_ suc B ) )
31	24, 30	mpbid 146	. . . . . 6 |- ( B e. om -> suc (/) C_ suc B )
32	31	a1d 22	. . . . 5 |- ( B e. om -> ( (/) C_ B -> suc (/) C_ suc B ) )
33		simp3 946	. . . . . . . . . 10 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> suc y C_ B )
34		simp1l 968	. . . . . . . . . . 11 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> y e. om )
35		simp1r 969	. . . . . . . . . . . 12 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> B e. om )
36	35, 25	syl 14	. . . . . . . . . . 11 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> Ord B )
37		ordelsuc 4337	. . . . . . . . . . 11 |- ( ( y e. om /\ Ord B ) -> ( y e. B <-> suc y C_ B ) )
38	34, 36, 37	syl2anc 404	. . . . . . . . . 10 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> ( y e. B <-> suc y C_ B ) )
39	33, 38	mpbird 166	. . . . . . . . 9 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> y e. B )
40		nnsucelsuc 6268	. . . . . . . . . 10 |- ( B e. om -> ( y e. B <-> suc y e. suc B ) )
41	35, 40	syl 14	. . . . . . . . 9 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> ( y e. B <-> suc y e. suc B ) )
42	39, 41	mpbid 146	. . . . . . . 8 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> suc y e. suc B )
43		peano2 4425	. . . . . . . . . 10 |- ( y e. om -> suc y e. om )
44	34, 43	syl 14	. . . . . . . . 9 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> suc y e. om )
45	36, 26	syl 14	. . . . . . . . 9 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> Ord suc B )
46		ordelsuc 4337	. . . . . . . . 9 |- ( ( suc y e. om /\ Ord suc B ) -> ( suc y e. suc B <-> suc suc y C_ suc B ) )
47	44, 45, 46	syl2anc 404	. . . . . . . 8 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> ( suc y e. suc B <-> suc suc y C_ suc B ) )
48	42, 47	mpbid 146	. . . . . . 7 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> suc suc y C_ suc B )
49	48	3expia 1146	. . . . . 6 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) ) -> ( suc y C_ B -> suc suc y C_ suc B ) )
50	49	exp31 357	. . . . 5 |- ( y e. om -> ( B e. om -> ( ( y C_ B -> suc y C_ suc B ) -> ( suc y C_ B -> suc suc y C_ suc B ) ) ) )
51	9, 13, 17, 32, 50	finds2 4431	. . . 4 |- ( x e. om -> ( B e. om -> ( x C_ B -> suc x C_ suc B ) ) )
52	5, 51	vtoclga 2688	. . 3 |- ( A e. om -> ( B e. om -> ( A C_ B -> suc A C_ suc B ) ) )
53	52	imp 123	. 2 |- ( ( A e. om /\ B e. om ) -> ( A C_ B -> suc A C_ suc B ) )
54		nnon 4439	. . 3 |- ( A e. om -> A e. On )
55		onsucsssucr 4341	. . 3 |- ( ( A e. On /\ Ord B ) -> ( suc A C_ suc B -> A C_ B ) )
56	54, 25, 55	syl2an 284	. 2 |- ( ( A e. om /\ B e. om ) -> ( suc A C_ suc B -> A C_ B ) )
57	53, 56	impbid 128	1 |- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> suc A C_ suc B ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   \/ wo 665   /\ w3a 925   = wceq 1290   e. wcel 1439   _Vcvv 2622   C_ wss 3002   (/)c0 3289   Ord word 4200   Oncon0 4201   suc csuc 4203   omcom 4420

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3965  ax-nul 3973  ax-pow 4017  ax-pr 4047  ax-un 4271  ax-iinf 4418

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rex 2366  df-v 2624  df-dif 3004  df-un 3006  df-in 3008  df-ss 3015  df-nul 3290  df-pw 3437  df-sn 3458  df-pr 3459  df-uni 3662  df-int 3697  df-tr 3945  df-iord 4204  df-on 4206  df-suc 4209  df-iom 4421

This theorem is referenced by:  nnaword  6286