Theorem nnsucsssuc 6545

Description: Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucsssucr 4541, but the forward direction, for all ordinals, implies excluded middle as seen as onsucsssucexmid 4559. (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 3202	. . . . . 6 |- ( x = A -> ( x C_ B <-> A C_ B ) )
2		suceq 4433	. . . . . . 7 |- ( x = A -> suc x = suc A )
3	2	sseq1d 3208	. . . . . 6 |- ( x = A -> ( suc x C_ suc B <-> suc A C_ suc B ) )
4	1, 3	imbi12d 234	. . . . 5 |- ( x = A -> ( ( x C_ B -> suc x C_ suc B ) <-> ( A C_ B -> suc A C_ suc B ) ) )
5	4	imbi2d 230	. . . 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 3202	. . . . . 6 |- ( x = (/) -> ( x C_ B <-> (/) C_ B ) )
7		suceq 4433	. . . . . . 7 |- ( x = (/) -> suc x = suc (/) )
8	7	sseq1d 3208	. . . . . 6 |- ( x = (/) -> ( suc x C_ suc B <-> suc (/) C_ suc B ) )
9	6, 8	imbi12d 234	. . . . 5 |- ( x = (/) -> ( ( x C_ B -> suc x C_ suc B ) <-> ( (/) C_ B -> suc (/) C_ suc B ) ) )
10		sseq1 3202	. . . . . 6 |- ( x = y -> ( x C_ B <-> y C_ B ) )
11		suceq 4433	. . . . . . 7 |- ( x = y -> suc x = suc y )
12	11	sseq1d 3208	. . . . . 6 |- ( x = y -> ( suc x C_ suc B <-> suc y C_ suc B ) )
13	10, 12	imbi12d 234	. . . . 5 |- ( x = y -> ( ( x C_ B -> suc x C_ suc B ) <-> ( y C_ B -> suc y C_ suc B ) ) )
14		sseq1 3202	. . . . . 6 |- ( x = suc y -> ( x C_ B <-> suc y C_ B ) )
15		suceq 4433	. . . . . . 7 |- ( x = suc y -> suc x = suc suc y )
16	15	sseq1d 3208	. . . . . 6 |- ( x = suc y -> ( suc x C_ suc B <-> suc suc y C_ suc B ) )
17	14, 16	imbi12d 234	. . . . 5 |- ( x = suc y -> ( ( x C_ B -> suc x C_ suc B ) <-> ( suc y C_ B -> suc suc y C_ suc B ) ) )
18		peano3 4628	. . . . . . . . 9 |- ( B e. om -> suc B =/= (/) )
19	18	neneqd 2385	. . . . . . . 8 |- ( B e. om -> -. suc B = (/) )
20		peano2 4627	. . . . . . . . . 10 |- ( B e. om -> suc B e. om )
21		0elnn 4651	. . . . . . . . . 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 725	. . . . . . . 8 |- ( B e. om -> ( -. suc B = (/) -> (/) e. suc B ) )
24	19, 23	mpd 13	. . . . . . 7 |- ( B e. om -> (/) e. suc B )
25		nnord 4644	. . . . . . . 8 |- ( B e. om -> Ord B )
26		ordsucim 4532	. . . . . . . 8 |- ( Ord B -> Ord suc B )
27		0ex 4156	. . . . . . . . 9 |- (/) e. _V
28		ordelsuc 4537	. . . . . . . . 9 |- ( ( (/) e. _V /\ Ord suc B ) -> ( (/) e. suc B <-> suc (/) C_ suc B ) )
29	27, 28	mpan 424	. . . . . . . 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 147	. . . . . 6 |- ( B e. om -> suc (/) C_ suc B )
32	31	a1d 22	. . . . 5 |- ( B e. om -> ( (/) C_ B -> suc (/) C_ suc B ) )
33		simp3 1001	. . . . . . . . . 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 1023	. . . . . . . . . . 11 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> y e. om )
35		simp1r 1024	. . . . . . . . . . . 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 4537	. . . . . . . . . . 11 |- ( ( y e. om /\ Ord B ) -> ( y e. B <-> suc y C_ B ) )
38	34, 36, 37	syl2anc 411	. . . . . . . . . 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 167	. . . . . . . . 9 |- ( ( ( y e. om /\ B e. om ) /\ ( y C_ B -> suc y C_ suc B ) /\ suc y C_ B ) -> y e. B )
40		nnsucelsuc 6544	. . . . . . . . . 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 147	. . . . . . . 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 4627	. . . . . . . . . 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 4537	. . . . . . . . 9 |- ( ( suc y e. om /\ Ord suc B ) -> ( suc y e. suc B <-> suc suc y C_ suc B ) )
47	44, 45, 46	syl2anc 411	. . . . . . . 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 147	. . . . . . 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 1207	. . . . . 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 364	. . . . 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 4633	. . . 4 |- ( x e. om -> ( B e. om -> ( x C_ B -> suc x C_ suc B ) ) )
52	5, 51	vtoclga 2826	. . 3 |- ( A e. om -> ( B e. om -> ( A C_ B -> suc A C_ suc B ) ) )
53	52	imp 124	. 2 |- ( ( A e. om /\ B e. om ) -> ( A C_ B -> suc A C_ suc B ) )
54		nnon 4642	. . 3 |- ( A e. om -> A e. On )
55		onsucsssucr 4541	. . 3 |- ( ( A e. On /\ Ord B ) -> ( suc A C_ suc B -> A C_ B ) )
56	54, 25, 55	syl2an 289	. 2 |- ( ( A e. om /\ B e. om ) -> ( suc A C_ suc B -> A C_ B ) )
57	53, 56	impbid 129	1 |- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> suc A C_ suc B ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 709   /\ w3a 980   = wceq 1364   e. wcel 2164   _Vcvv 2760   C_ wss 3153   (/)c0 3446   Ord word 4393   Oncon0 4394   suc csuc 4396   omcom 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-iinf 4620

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-ral 2477  df-rex 2478  df-v 2762  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-pw 3603  df-sn 3624  df-pr 3625  df-uni 3836  df-int 3871  df-tr 4128  df-iord 4397  df-on 4399  df-suc 4402  df-iom 4623

This theorem is referenced by:  nnaword  6564  ennnfonelemk  12557  ennnfonelemkh  12569