Theorem nnacda 6088

Description: The cardinal and ordinal sums of finite ordinals are equal. (Contributed by Paul Chapman, 11-Apr-2009.)

Assertion

Ref	Expression
nnacda	|- ((A e. om /\ B e. om) -> (card` (A +c B)) = (A +o B))

Proof of Theorem nnacda

Step	Hyp	Ref	Expression
1		opreq2 4890	. . . . . . 7 |- (y = (/) -> (x +c y) = (x +c (/)))
2	1	fveq2d 4685	. . . . . 6 |- (y = (/) -> (card` (x +c y)) = (card` (x +c (/))))
3		opreq2 4890	. . . . . 6 |- (y = (/) -> (x +o y) = (x +o (/)))
4	2, 3	eqeq12d 1899	. . . . 5 |- (y = (/) -> ((card` (x +c y)) = (x +o y) <-> (card` (x +c (/))) = (x +o (/))))
5		opreq2 4890	. . . . . . 7 |- (y = z -> (x +c y) = (x +c z))
6	5	fveq2d 4685	. . . . . 6 |- (y = z -> (card` (x +c y)) = (card` (x +c z)))
7		opreq2 4890	. . . . . 6 |- (y = z -> (x +o y) = (x +o z))
8	6, 7	eqeq12d 1899	. . . . 5 |- (y = z -> ((card` (x +c y)) = (x +o y) <-> (card` (x +c z)) = (x +o z)))
9		opreq2 4890	. . . . . . 7 |- (y = suc z -> (x +c y) = (x +c suc z))
10	9	fveq2d 4685	. . . . . 6 |- (y = suc z -> (card` (x +c y)) = (card` (x +c suc z)))
11		opreq2 4890	. . . . . 6 |- (y = suc z -> (x +o y) = (x +o suc z))
12	10, 11	eqeq12d 1899	. . . . 5 |- (y = suc z -> ((card` (x +c y)) = (x +o y) <-> (card` (x +c suc z)) = (x +o suc z)))
13		cardnn 5870	. . . . . . 7 |- (x e. om -> (card` x) = x)
14		visset 2295	. . . . . . . . 9 |- x e. _V
15	14	cda0en 6075	. . . . . . . 8 |- (x +c (/)) ~~ x
16		oprex 4907	. . . . . . . . 9 |- (x +c (/)) e. _V
17		carden 5981	. . . . . . . . 9 |- (((x +c (/)) e. _V /\ x e. _V) -> ((card` (x +c (/))) = (card` x) <-> (x +c (/)) ~~ x))
18	16, 14, 17	mp2an 761	. . . . . . . 8 |- ((card` (x +c (/))) = (card` x) <-> (x +c (/)) ~~ x)
19	15, 18	mpbir 207	. . . . . . 7 |- (card` (x +c (/))) = (card` x)
20	13, 19	syl5eq 1940	. . . . . 6 |- (x e. om -> (card` (x +c (/))) = x)
21		nna0 5275	. . . . . 6 |- (x e. om -> (x +o (/)) = x)
22	20, 21	eqtr4d 1928	. . . . 5 |- (x e. om -> (card` (x +c (/))) = (x +o (/)))
23		visset 2295	. . . . . . . . . . . . . . 15 |- z e. _V
24	23	cda1en 6076	. . . . . . . . . . . . . 14 |- (z +c 1o) ~~ suc (card` z)
25		cardnn 5870	. . . . . . . . . . . . . . . 16 |- (z e. om -> (card` z) = z)
26		suceq 3729	. . . . . . . . . . . . . . . 16 |- ((card` z) = z -> suc (card` z) = suc z)
27	25, 26	syl 12	. . . . . . . . . . . . . . 15 |- (z e. om -> suc (card` z) = suc z)
28	27	breq2d 3350	. . . . . . . . . . . . . 14 |- (z e. om -> ((z +c 1o) ~~ suc (card` z) <-> (z +c 1o) ~~ suc z))
29	24, 28	mpbii 210	. . . . . . . . . . . . 13 |- (z e. om -> (z +c 1o) ~~ suc z)
30	14	enref 5450	. . . . . . . . . . . . . 14 |- x ~~ x
31		oprex 4907	. . . . . . . . . . . . . . 15 |- (z +c 1o) e. _V
32	23	sucex 3892	. . . . . . . . . . . . . . 15 |- suc z e. _V
33	14, 14, 31, 32	cdaen 6073	. . . . . . . . . . . . . 14 |- ((x ~~ x /\ (z +c 1o) ~~ suc z) -> (x +c (z +c 1o)) ~~ (x +c suc z))
34	30, 33	mpan 759	. . . . . . . . . . . . 13 |- ((z +c 1o) ~~ suc z -> (x +c (z +c 1o)) ~~ (x +c suc z))
35		1onn 5310	. . . . . . . . . . . . . . . 16 |- 1o e. om
36	35	elisseti 2301	. . . . . . . . . . . . . . 15 |- 1o e. _V
37	14, 23, 36	cdaassen 6080	. . . . . . . . . . . . . 14 |- ((x +c z) +c 1o) ~~ (x +c (z +c 1o))
38		entr 5473	. . . . . . . . . . . . . 14 |- ((((x +c z) +c 1o) ~~ (x +c (z +c 1o)) /\ (x +c (z +c 1o)) ~~ (x +c suc z)) -> ((x +c z) +c 1o) ~~ (x +c suc z))
39	37, 38	mpan 759	. . . . . . . . . . . . 13 |- ((x +c (z +c 1o)) ~~ (x +c suc z) -> ((x +c z) +c 1o) ~~ (x +c suc z))
40	29, 34, 39	3syl 24	. . . . . . . . . . . 12 |- (z e. om -> ((x +c z) +c 1o) ~~ (x +c suc z))
41		oprex 4907	. . . . . . . . . . . . 13 |- (x +c suc z) e. _V
42	41	ensym 5471	. . . . . . . . . . . 12 |- (((x +c z) +c 1o) ~~ (x +c suc z) -> (x +c suc z) ~~ ((x +c z) +c 1o))
43		oprex 4907	. . . . . . . . . . . . . 14 |- (x +c z) e. _V
44	43	cda1en 6076	. . . . . . . . . . . . 13 |- ((x +c z) +c 1o) ~~ suc (card` (x +c z))
45		entr 5473	. . . . . . . . . . . . 13 |- (((x +c suc z) ~~ ((x +c z) +c 1o) /\ ((x +c z) +c 1o) ~~ suc (card` (x +c z))) -> (x +c suc z) ~~ suc (card` (x +c z)))
46	44, 45	mpan2 760	. . . . . . . . . . . 12 |- ((x +c suc z) ~~ ((x +c z) +c 1o) -> (x +c suc z) ~~ suc (card` (x +c z)))
47	40, 42, 46	3syl 24	. . . . . . . . . . 11 |- (z e. om -> (x +c suc z) ~~ suc (card` (x +c z)))
48	47	3ad2ant2 898	. . . . . . . . . 10 |- ((x e. om /\ z e. om /\ (card` (x +c z)) = (x +o z)) -> (x +c suc z) ~~ suc (card` (x +c z)))
49		suceq 3729	. . . . . . . . . . . . 13 |- ((card` (x +c z)) = (x +o z) -> suc (card` (x +c z)) = suc (x +o z))
50	49	3ad2ant3 899	. . . . . . . . . . . 12 |- ((x e. om /\ z e. om /\ (card` (x +c z)) = (x +o z)) -> suc (card` (x +c z)) = suc (x +o z))
51		nnasuc 5277	. . . . . . . . . . . . 13 |- ((x e. om /\ z e. om) -> (x +o suc z) = suc (x +o z))
52	51	3adant3 896	. . . . . . . . . . . 12 |- ((x e. om /\ z e. om /\ (card` (x +c z)) = (x +o z)) -> (x +o suc z) = suc (x +o z))
53	50, 52	eqtr4d 1928	. . . . . . . . . . 11 |- ((x e. om /\ z e. om /\ (card` (x +c z)) = (x +o z)) -> suc (card` (x +c z)) = (x +o suc z))
54	53	breq2d 3350	. . . . . . . . . 10 |- ((x e. om /\ z e. om /\ (card` (x +c z)) = (x +o z)) -> ((x +c suc z) ~~ suc (card` (x +c z)) <-> (x +c suc z) ~~ (x +o suc z)))
55	48, 54	mpbid 212	. . . . . . . . 9 |- ((x e. om /\ z e. om /\ (card` (x +c z)) = (x +o z)) -> (x +c suc z) ~~ (x +o suc z))
56		oprex 4907	. . . . . . . . . 10 |- (x +o suc z) e. _V
57		carden 5981	. . . . . . . . . 10 |- (((x +c suc z) e. _V /\ (x +o suc z) e. _V) -> ((card` (x +c suc z)) = (card` (x +o suc z)) <-> (x +c suc z) ~~ (x +o suc z)))
58	41, 56, 57	mp2an 761	. . . . . . . . 9 |- ((card` (x +c suc z)) = (card` (x +o suc z)) <-> (x +c suc z) ~~ (x +o suc z))
59	55, 58	sylibr 217	. . . . . . . 8 |- ((x e. om /\ z e. om /\ (card` (x +c z)) = (x +o z)) -> (card` (x +c suc z)) = (card` (x +o suc z)))
60		nnacl 5281	. . . . . . . . . . 11 |- ((x e. om /\ suc z e. om) -> (x +o suc z) e. om)
61		peano2b 3968	. . . . . . . . . . 11 |- (z e. om <-> suc z e. om)
62	60, 61	sylan2b 501	. . . . . . . . . 10 |- ((x e. om /\ z e. om) -> (x +o suc z) e. om)
63		cardnn 5870	. . . . . . . . . 10 |- ((x +o suc z) e. om -> (card` (x +o suc z)) = (x +o suc z))
64	62, 63	syl 12	. . . . . . . . 9 |- ((x e. om /\ z e. om) -> (card` (x +o suc z)) = (x +o suc z))
65	64	3adant3 896	. . . . . . . 8 |- ((x e. om /\ z e. om /\ (card` (x +c z)) = (x +o z)) -> (card` (x +o suc z)) = (x +o suc z))
66	59, 65	eqtrd 1925	. . . . . . 7 |- ((x e. om /\ z e. om /\ (card` (x +c z)) = (x +o z)) -> (card` (x +c suc z)) = (x +o suc z))
67	66	3expia 1069	. . . . . 6 |- ((x e. om /\ z e. om) -> ((card` (x +c z)) = (x +o z) -> (card` (x +c suc z)) = (x +o suc z)))
68	67	expcom 403	. . . . 5 |- (z e. om -> (x e. om -> ((card` (x +c z)) = (x +o z) -> (card` (x +c suc z)) = (x +o suc z))))
69	4, 8, 12, 22, 68	finds2 3981	. . . 4 |- (y e. om -> (x e. om -> (card` (x +c y)) = (x +o y)))
70	69	impcom 378	. . 3 |- ((x e. om /\ y e. om) -> (card` (x +c y)) = (x +o y))
71	70	rgen2a 2160	. 2 |- A.x e. om A.y e. om (card` (x +c y)) = (x +o y)
72		opreq1 4889	. . . . 5 |- (x = A -> (x +c y) = (A +c y))
73	72	fveq2d 4685	. . . 4 |- (x = A -> (card` (x +c y)) = (card` (A +c y)))
74		opreq1 4889	. . . 4 |- (x = A -> (x +o y) = (A +o y))
75	73, 74	eqeq12d 1899	. . 3 |- (x = A -> ((card` (x +c y)) = (x +o y) <-> (card` (A +c y)) = (A +o y)))
76		opreq2 4890	. . . . 5 |- (y = B -> (A +c y) = (A +c B))
77	76	fveq2d 4685	. . . 4 |- (y = B -> (card` (A +c y)) = (card` (A +c B)))
78		opreq2 4890	. . . 4 |- (y = B -> (A +o y) = (A +o B))
79	77, 78	eqeq12d 1899	. . 3 |- (y = B -> ((card` (A +c y)) = (A +o y) <-> (card` (A +c B)) = (A +o B)))
80	75, 79	rcla42v 2384	. 2 |- ((A e. om /\ B e. om) -> (A.x e. om A.y e. om (card` (x +c y)) = (x +o y) -> (card` (A +c B)) = (A +o B)))
81	71, 80	mpi 55	1 |- ((A e. om /\ B e. om) -> (card` (A +c B)) = (A +o B))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292  (/)c0 2875   class class class wbr 3338  suc csuc 3659  omcom 3949  ` cfv 3998  (class class class)co 4884  1oc1o 5172   +o coa 5174   ~~ cen 5423  cardccrd 5859   +c ccda 6065

This theorem is referenced by:  nnaun 6089

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-ac 5906

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-dom 5428  df-sdom 5429  df-card 5862  df-cda 6066

Copyright terms: Public domain