Theorem nnsucsssuc 6094

Description: Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucsssucr 4253, but the forward direction, for all ordinals, implies excluded middle as seen as onsucsssucexmid 4270. (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 3020	. . . . . 6 |- ( x = A -> ( x C_ B <-> A C_ B ) )
2		suceq 4157	. . . . . . 7 |- ( x = A -> suc x = suc A )
3	2	sseq1d 3026	. . . . . 6 |- ( x = A -> ( suc x C_ suc B <-> suc A C_ suc B ) )
4	1, 3	imbi12d 232	. . . . 5 |- ( x = A -> ( ( x C_ B -> suc x C_ suc B ) <-> ( A C_ B -> suc A C_ suc B ) ) )
5	4	imbi2d 228	. . . 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 3020	. . . . . 6 |- ( x = (/) -> ( x C_ B <-> (/) C_ B ) )
7		suceq 4157	. . . . . . 7 |- ( x = (/) -> suc x = suc (/) )
8	7	sseq1d 3026	. . . . . 6 |- ( x = (/) -> ( suc x C_ suc B <-> suc (/) C_ suc B ) )
9	6, 8	imbi12d 232	. . . . 5 |- ( x = (/) -> ( ( x C_ B -> suc x C_ suc B ) <-> ( (/) C_ B -> suc (/) C_ suc B ) ) )
10		sseq1 3020	. . . . . 6 |- ( x = y -> ( x C_ B <-> y C_ B ) )
11		suceq 4157	. . . . . . 7 |- ( x = y -> suc x = suc y )
12	11	sseq1d 3026	. . . . . 6 |- ( x = y -> ( suc x C_ suc B <-> suc y C_ suc B ) )
13	10, 12	imbi12d 232	. . . . 5 |- ( x = y -> ( ( x C_ B -> suc x C_ suc B ) <-> ( y C_ B -> suc y C_ suc B ) ) )
14		sseq1 3020	. . . . . 6 |- ( x = suc y -> ( x C_ B <-> suc y C_ B ) )
15		suceq 4157	. . . . . . 7 |- ( x = suc y -> suc x = suc suc y )
16	15	sseq1d 3026	. . . . . 6 |- ( x = suc y -> ( suc x C_ suc B <-> suc suc y C_ suc B ) )
17	14, 16	imbi12d 232	. . . . 5 |- ( x = suc y -> ( ( x C_ B -> suc x C_ suc B ) <-> ( suc y C_ B -> suc suc y C_ suc B ) ) )
18		peano3 4337	. . . . . . . . 9 |- ( B e. om -> suc B =/= (/) )
19	18	neneqd 2266	. . . . . . . 8 |- ( B e. om -> -. suc B = (/) )
20		peano2 4336	. . . . . . . . . 10 |- ( B e. om -> suc B e. om )
21		0elnn 4358	. . . . . . . . . 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 675	. . . . . . . 8 |- ( B e. om -> ( -. suc B = (/) -> (/) e. suc B ) )
24	19, 23	mpd 13	. . . . . . 7 |- ( B e. om -> (/) e. suc B )
25		nnord 4352	. . . . . . . 8 |- ( B e. om -> Ord B )
26		ordsucim 4244	. . . . . . . 8 |- ( Ord B -> Ord suc B )
27		0ex 3905	. . . . . . . . 9 |- (/) e. _V
28		ordelsuc 4249	. . . . . . . . 9 |- ( ( (/) e. _V /\ Ord suc B ) -> ( (/) e. suc B <-> suc (/) C_ suc B ) )
29	27, 28	mpan 414	. . . . . . . 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 145	. . . . . 6 |- ( B e. om -> suc (/) C_ suc B )
32	31	a1d 22	. . . . 5 |- ( B e. om -> ( (/) C_ B -> suc (/) C_ suc B ) )
33		simp3 940	. . . . . . . . . 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 962	. . . . . . . . . . 11 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> y e. om )
35		simp1r 963	. . . . . . . . . . . 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 4249	. . . . . . . . . . 11 |- ( ( y e. om /\ Ord B ) -> ( y e. B <-> suc y C_ B ) )
38	34, 36, 37	syl2anc 403	. . . . . . . . . 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 165	. . . . . . . . 9 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> y e. B )
40		nnsucelsuc 6093	. . . . . . . . . 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 145	. . . . . . . 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 4336	. . . . . . . . . 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 4249	. . . . . . . . 9 |- ( ( suc y e. om /\ Ord suc B ) -> ( suc y e. suc B <-> suc suc y C_ suc B ) )
47	44, 45, 46	syl2anc 403	. . . . . . . 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 145	. . . . . . 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 1140	. . . . . 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 356	. . . . 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 4342	. . . 4 |- ( x e. om -> ( B e. om -> ( x C_ B -> suc x C_ suc B ) ) )
52	5, 51	vtoclga 2664	. . 3 |- ( A e. om -> ( B e. om -> ( A C_ B -> suc A C_ suc B ) ) )
53	52	imp 122	. 2 |- ( ( A e. om /\ B e. om ) -> ( A C_ B -> suc A C_ suc B ) )
54		nnon 4350	. . 3 |- ( A e. om -> A e. On )
55		onsucsssucr 4253	. . 3 |- ( ( A e. On /\ Ord B ) -> ( suc A C_ suc B -> A C_ B ) )
56	54, 25, 55	syl2an 283	. 2 |- ( ( A e. om /\ B e. om ) -> ( suc A C_ suc B -> A C_ B ) )
57	53, 56	impbid 127	1 |- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> suc A C_ suc B ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 102   <-> wb 103   \/ wo 661   /\ w3a 919   = wceq 1284   e. wcel 1433   _Vcvv 2601   C_ wss 2973   (/)c0 3251   Ord word 4117   Oncon0 4118   suc csuc 4120   omcom 4331

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 576  ax-in2 577  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-13 1444  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-nul 3904  ax-pow 3948  ax-pr 3964  ax-un 4188  ax-iinf 4329

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ne 2246  df-ral 2353  df-rex 2354  df-v 2603  df-dif 2975  df-un 2977  df-in 2979  df-ss 2986  df-nul 3252  df-pw 3384  df-sn 3404  df-pr 3405  df-uni 3602  df-int 3637  df-tr 3876  df-iord 4121  df-on 4123  df-suc 4126  df-iom 4332

This theorem is referenced by:  nnaword  6107