Theorem nnsucsssuc 6547

Description: Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucsssucr 4542, but the forward direction, for all ordinals, implies excluded middle as seen as onsucsssucexmid 4560. (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 3203	. . . . . 6 |- ( x = A -> ( x C_ B <-> A C_ B ) )
2		suceq 4434	. . . . . . 7 |- ( x = A -> suc x = suc A )
3	2	sseq1d 3209	. . . . . 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 3203	. . . . . 6 |- ( x = (/) -> ( x C_ B <-> (/) C_ B ) )
7		suceq 4434	. . . . . . 7 |- ( x = (/) -> suc x = suc (/) )
8	7	sseq1d 3209	. . . . . 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 3203	. . . . . 6 |- ( x = y -> ( x C_ B <-> y C_ B ) )
11		suceq 4434	. . . . . . 7 |- ( x = y -> suc x = suc y )
12	11	sseq1d 3209	. . . . . 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 3203	. . . . . 6 |- ( x = suc y -> ( x C_ B <-> suc y C_ B ) )
15		suceq 4434	. . . . . . 7 |- ( x = suc y -> suc x = suc suc y )
16	15	sseq1d 3209	. . . . . 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 4629	. . . . . . . . 9 |- ( B e. om -> suc B =/= (/) )
19	18	neneqd 2385	. . . . . . . 8 |- ( B e. om -> -. suc B = (/) )
20		peano2 4628	. . . . . . . . . 10 |- ( B e. om -> suc B e. om )
21		0elnn 4652	. . . . . . . . . 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 4645	. . . . . . . 8 |- ( B e. om -> Ord B )
26		ordsucim 4533	. . . . . . . 8 |- ( Ord B -> Ord suc B )
27		0ex 4157	. . . . . . . . 9 |- (/) e. _V
28		ordelsuc 4538	. . . . . . . . 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 4538	. . . . . . . . . . 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 6546	. . . . . . . . . 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 4628	. . . . . . . . . 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 4538	. . . . . . . . 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 4634	. . . 4 |- ( x e. om -> ( B e. om -> ( x C_ B -> suc x C_ suc B ) ) )
52	5, 51	vtoclga 2827	. . 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 4643	. . 3 |- ( A e. om -> A e. On )
55		onsucsssucr 4542	. . 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 3154   (/)c0 3447   Ord word 4394   Oncon0 4395   suc csuc 4397   omcom 4623

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 4148  ax-nul 4156  ax-pow 4204  ax-pr 4239  ax-un 4465  ax-iinf 4621

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 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3448  df-pw 3604  df-sn 3625  df-pr 3626  df-uni 3837  df-int 3872  df-tr 4129  df-iord 4398  df-on 4400  df-suc 4403  df-iom 4624

This theorem is referenced by:  nnaword  6566  ennnfonelemk  12560  ennnfonelemkh  12572