Theorem cardaleph 6033

Description: Given any transfinite cardinal number A, there is exactly one aleph that is equal to it. Here we compute that aleph explicitly.

Assertion

Ref	Expression
cardaleph	|- ((om C_ A /\ (card` A) = A) -> A = (aleph` |^|{x e. On | A C_ (aleph` x)}))

Distinct variable group:   x,A

Proof of Theorem cardaleph

Step	Hyp	Ref	Expression
1		cardon 5976	. . . . 5 |- (card` A) e. On
2		eleq1 1957	. . . . 5 |- ((card` A) = A -> ((card` A) e. On <-> A e. On))
3	1, 2	mpbii 210	. . . 4 |- ((card` A) = A -> A e. On)
4		alephle 6032	. . . . . 6 |- (A e. On -> A C_ (aleph` A))
5		fveq2 4681	. . . . . . . 8 |- (x = A -> (aleph` x) = (aleph` A))
6	5	sseq2d 2645	. . . . . . 7 |- (x = A -> (A C_ (aleph` x) <-> A C_ (aleph` A)))
7	6	rcla4ev 2381	. . . . . 6 |- ((A e. On /\ A C_ (aleph` A)) -> E.x e. On A C_ (aleph` x))
8	4, 7	mpdan 768	. . . . 5 |- (A e. On -> E.x e. On A C_ (aleph` x))
9		onintrab2 3883	. . . . 5 |- (E.x e. On A C_ (aleph` x) <-> |^|{x e. On | A C_ (aleph` x)} e. On)
10	8, 9	sylib 215	. . . 4 |- (A e. On -> |^|{x e. On | A C_ (aleph` x)} e. On)
11		eloni 3667	. . . . 5 |- (|^|{x e. On | A C_ (aleph` x)} e. On -> Ord |^|{x e. On | A C_ (aleph` x)})
12		ordzsl 3927	. . . . . 6 |- (Ord |^|{x e. On | A C_ (aleph` x)} <-> (|^|{x e. On | A C_ (aleph` x)} = (/) \/ E.y e. On |^|{x e. On | A C_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A C_ (aleph` x)}))
13		3orass 861	. . . . . 6 |- ((|^|{x e. On | A C_ (aleph` x)} = (/) \/ E.y e. On |^|{x e. On | A C_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A C_ (aleph` x)}) <-> (|^|{x e. On | A C_ (aleph` x)} = (/) \/ (E.y e. On |^|{x e. On | A C_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A C_ (aleph` x)})))
14	12, 13	bitri 190	. . . . 5 |- (Ord |^|{x e. On | A C_ (aleph` x)} <-> (|^|{x e. On | A C_ (aleph` x)} = (/) \/ (E.y e. On |^|{x e. On | A C_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A C_ (aleph` x)})))
15	11, 14	sylib 215	. . . 4 |- (|^|{x e. On | A C_ (aleph` x)} e. On -> (|^|{x e. On | A C_ (aleph` x)} = (/) \/ (E.y e. On |^|{x e. On | A C_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A C_ (aleph` x)})))
16	3, 10, 15	3syl 24	. . 3 |- ((card` A) = A -> (|^|{x e. On | A C_ (aleph` x)} = (/) \/ (E.y e. On |^|{x e. On | A C_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A C_ (aleph` x)})))
17	16	adantl 424	. 2 |- ((om C_ A /\ (card` A) = A) -> (|^|{x e. On | A C_ (aleph` x)} = (/) \/ (E.y e. On |^|{x e. On | A C_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A C_ (aleph` x)})))
18		ax-17 1317	. . . . . . . . . . 11 |- (y e. A -> A.x y e. A)
19		ax-17 1317	. . . . . . . . . . . 12 |- (y e. aleph -> A.x y e. aleph)
20		hbrab1 2257	. . . . . . . . . . . . 13 |- (y e. {x e. On | A C_ (aleph` x)} -> A.x y e. {x e. On | A C_ (aleph` x)})
21	20	hbint 3225	. . . . . . . . . . . 12 |- (y e. |^|{x e. On | A C_ (aleph` x)} -> A.x y e. |^|{x e. On | A C_ (aleph` x)})
22	19, 21	hbfv 4686	. . . . . . . . . . 11 |- (y e. (aleph` |^|{x e. On | A C_ (aleph` x)}) -> A.x y e. (aleph` |^|{x e. On | A C_ (aleph` x)}))
23	18, 22	hbss 2614	. . . . . . . . . 10 |- (A C_ (aleph` |^|{x e. On | A C_ (aleph` x)}) -> A.x A C_ (aleph` |^|{x e. On | A C_ (aleph` x)}))
24		fveq2 4681	. . . . . . . . . . 11 |- (x = |^|{x e. On | A C_ (aleph` x)} -> (aleph` x) = (aleph` |^|{x e. On | A C_ (aleph` x)}))
25	24	sseq2d 2645	. . . . . . . . . 10 |- (x = |^|{x e. On | A C_ (aleph` x)} -> (A C_ (aleph` x) <-> A C_ (aleph` |^|{x e. On | A C_ (aleph` x)})))
26	23, 25	onminsb 3879	. . . . . . . . 9 |- (E.x e. On A C_ (aleph` x) -> A C_ (aleph` |^|{x e. On | A C_ (aleph` x)}))
27	3, 8, 26	3syl 24	. . . . . . . 8 |- ((card` A) = A -> A C_ (aleph` |^|{x e. On | A C_ (aleph` x)}))
28	27	a1i 8	. . . . . . 7 |- (|^|{x e. On | A C_ (aleph` x)} = (/) -> ((card` A) = A -> A C_ (aleph` |^|{x e. On | A C_ (aleph` x)})))
29		fveq2 4681	. . . . . . . . . 10 |- (|^|{x e. On | A C_ (aleph` x)} = (/) -> (aleph` |^|{x e. On | A C_ (aleph` x)}) = (aleph` (/)))
30		aleph0 5874	. . . . . . . . . 10 |- (aleph` (/)) = om
31	29, 30	syl6eq 1944	. . . . . . . . 9 |- (|^|{x e. On | A C_ (aleph` x)} = (/) -> (aleph` |^|{x e. On | A C_ (aleph` x)}) = om)
32	31	sseq1d 2644	. . . . . . . 8 |- (|^|{x e. On | A C_ (aleph` x)} = (/) -> ((aleph` |^|{x e. On | A C_ (aleph` x)}) C_ A <-> om C_ A))
33	32	biimprd 171	. . . . . . 7 |- (|^|{x e. On | A C_ (aleph` x)} = (/) -> (om C_ A -> (aleph` |^|{x e. On | A C_ (aleph` x)}) C_ A))
34	28, 33	anim12d 617	. . . . . 6 |- (|^|{x e. On | A C_ (aleph` x)} = (/) -> (((card` A) = A /\ om C_ A) -> (A C_ (aleph` |^|{x e. On | A C_ (aleph` x)}) /\ (aleph` |^|{x e. On | A C_ (aleph` x)}) C_ A)))
35		eqss 2631	. . . . . 6 |- (A = (aleph` |^|{x e. On | A C_ (aleph` x)}) <-> (A C_ (aleph` |^|{x e. On | A C_ (aleph` x)}) /\ (aleph` |^|{x e. On | A C_ (aleph` x)}) C_ A))
36	34, 35	syl6ibr 230	. . . . 5 |- (|^|{x e. On | A C_ (aleph` x)} = (/) -> (((card` A) = A /\ om C_ A) -> A = (aleph` |^|{x e. On | A C_ (aleph` x)})))
37	36	com12 14	. . . 4 |- (((card` A) = A /\ om C_ A) -> (|^|{x e. On | A C_ (aleph` x)} = (/) -> A = (aleph` |^|{x e. On | A C_ (aleph` x)})))
38	37	ancoms 484	. . 3 |- ((om C_ A /\ (card` A) = A) -> (|^|{x e. On | A C_ (aleph` x)} = (/) -> A = (aleph` |^|{x e. On | A C_ (aleph` x)})))
39		fveq2 4681	. . . . . . . . . . . . . 14 |- (x = y -> (aleph` x) = (aleph` y))
40	39	sseq2d 2645	. . . . . . . . . . . . 13 |- (x = y -> (A C_ (aleph` x) <-> A C_ (aleph` y)))
41	40	onnminsb 3885	. . . . . . . . . . . 12 |- (y e. On -> (y e. |^|{x e. On | A C_ (aleph` x)} -> -. A C_ (aleph` y)))
42		visset 2295	. . . . . . . . . . . . . 14 |- y e. _V
43	42	sucid 3744	. . . . . . . . . . . . 13 |- y e. suc y
44		eleq2 1958	. . . . . . . . . . . . 13 |- (|^|{x e. On | A C_ (aleph` x)} = suc y -> (y e. |^|{x e. On | A C_ (aleph` x)} <-> y e. suc y))
45	43, 44	mpbiri 211	. . . . . . . . . . . 12 |- (|^|{x e. On | A C_ (aleph` x)} = suc y -> y e. |^|{x e. On | A C_ (aleph` x)})
46	41, 45	syl5 20	. . . . . . . . . . 11 |- (y e. On -> (|^|{x e. On | A C_ (aleph` x)} = suc y -> -. A C_ (aleph` y)))
47	46	imp 377	. . . . . . . . . 10 |- ((y e. On /\ |^|{x e. On | A C_ (aleph` x)} = suc y) -> -. A C_ (aleph` y))
48	47	adantl 424	. . . . . . . . 9 |- (((card` A) = A /\ (y e. On /\ |^|{x e. On | A C_ (aleph` x)} = suc y)) -> -. A C_ (aleph` y))
49		fveq2 4681	. . . . . . . . . . . . 13 |- (|^|{x e. On | A C_ (aleph` x)} = suc y -> (aleph` |^|{x e. On | A C_ (aleph` x)}) = (aleph` suc y))
50		alephsuc 6014	. . . . . . . . . . . . 13 |- (y e. On -> (aleph` suc y) = |^|{x e. On | (aleph` y) ~< x})
51	49, 50	sylan9eqr 1951	. . . . . . . . . . . 12 |- ((y e. On /\ |^|{x e. On | A C_ (aleph` x)} = suc y) -> (aleph` |^|{x e. On | A C_ (aleph` x)}) = |^|{x e. On | (aleph` y) ~< x})
52	51	eleq2d 1964	. . . . . . . . . . 11 |- ((y e. On /\ |^|{x e. On | A C_ (aleph` x)} = suc y) -> (A e. (aleph` |^|{x e. On | A C_ (aleph` x)}) <-> A e. |^|{x e. On | (aleph` y) ~< x}))
53	52	biimpd 170	. . . . . . . . . 10 |- ((y e. On /\ |^|{x e. On | A C_ (aleph` x)} = suc y) -> (A e. (aleph` |^|{x e. On | A C_ (aleph` x)}) -> A e. |^|{x e. On | (aleph` y) ~< x}))
54		breq2 3342	. . . . . . . . . . . . . . 15 |- (x = A -> ((aleph` y) ~< x <-> (aleph` y) ~< A))
55	54	onnminsb 3885	. . . . . . . . . . . . . 14 |- (A e. On -> (A e. |^|{x e. On | (aleph` y) ~< x} -> -. (aleph` y) ~< A))
56		fvex 4689	. . . . . . . . . . . . . . 15 |- (aleph` y) e. _V
57		domtri 5989	. . . . . . . . . . . . . . 15 |- ((A e. On /\ (aleph` y) e. _V) -> (A ~<_ (aleph` y) <-> -. (aleph` y) ~< A))
58	56, 57	mpan2 760	. . . . . . . . . . . . . 14 |- (A e. On -> (A ~<_ (aleph` y) <-> -. (aleph` y) ~< A))
59	55, 58	sylibrd 221	. . . . . . . . . . . . 13 |- (A e. On -> (A e. |^|{x e. On | (aleph` y) ~< x} -> A ~<_ (aleph` y)))
60		carddom 5987	. . . . . . . . . . . . . 14 |- ((A e. On /\ (aleph` y) e. _V) -> ((card` A) C_ (card` (aleph` y)) <-> A ~<_ (aleph` y)))
61	56, 60	mpan2 760	. . . . . . . . . . . . 13 |- (A e. On -> ((card` A) C_ (card` (aleph` y)) <-> A ~<_ (aleph` y)))
62	59, 61	sylibrd 221	. . . . . . . . . . . 12 |- (A e. On -> (A e. |^|{x e. On | (aleph` y) ~< x} -> (card` A) C_ (card` (aleph` y))))
63	3, 62	syl 12	. . . . . . . . . . 11 |- ((card` A) = A -> (A e. |^|{x e. On | (aleph` y) ~< x} -> (card` A) C_ (card` (aleph` y))))
64		sseq1 2637	. . . . . . . . . . . 12 |- ((card` A) = A -> ((card` A) C_ (card` (aleph` y)) <-> A C_ (card` (aleph` y))))
65		alephcard 6015	. . . . . . . . . . . . 13 |- (card` (aleph` y)) = (aleph` y)
66	65	sseq2i 2642	. . . . . . . . . . . 12 |- (A C_ (card` (aleph` y)) <-> A C_ (aleph` y))
67	64, 66	syl6bb 595	. . . . . . . . . . 11 |- ((card` A) = A -> ((card` A) C_ (card` (aleph` y)) <-> A C_ (aleph` y)))
68	63, 67	sylibd 219	. . . . . . . . . 10 |- ((card` A) = A -> (A e. |^|{x e. On | (aleph` y) ~< x} -> A C_ (aleph` y)))
69	53, 68	sylan9r 519	. . . . . . . . 9 |- (((card` A) = A /\ (y e. On /\ |^|{x e. On | A C_ (aleph` x)} = suc y)) -> (A e. (aleph` |^|{x e. On | A C_ (aleph` x)}) -> A C_ (aleph` y)))
70	48, 69	mtod 123	. . . . . . . 8 |- (((card` A) = A /\ (y e. On /\ |^|{x e. On | A C_ (aleph` x)} = suc y)) -> -. A e. (aleph` |^|{x e. On | A C_ (aleph` x)}))
71	70	exp32 408	. . . . . . 7 |- ((card` A) = A -> (y e. On -> (|^|{x e. On | A C_ (aleph` x)} = suc y -> -. A e. (aleph` |^|{x e. On | A C_ (aleph` x)}))))
72	71	r19.23adv 2215	. . . . . 6 |- ((card` A) = A -> (E.y e. On |^|{x e. On | A C_ (aleph` x)} = suc y -> -. A e. (aleph` |^|{x e. On | A C_ (aleph` x)})))
73		onelon 3683	. . . . . . . . . . . . . 14 |- ((|^|{x e. On | A C_ (aleph` x)} e. On /\ y e. |^|{x e. On | A C_ (aleph` x)}) -> y e. On)
74	73, 10	sylan 497	. . . . . . . . . . . . 13 |- ((A e. On /\ y e. |^|{x e. On | A C_ (aleph` x)}) -> y e. On)
75	41	adantld 426	. . . . . . . . . . . . 13 |- (y e. On -> ((A e. On /\ y e. |^|{x e. On | A C_ (aleph` x)}) -> -. A C_ (aleph` y)))
76	74, 75	mpcom 60	. . . . . . . . . . . 12 |- ((A e. On /\ y e. |^|{x e. On | A C_ (aleph` x)}) -> -. A C_ (aleph` y))
77		alephon 5876	. . . . . . . . . . . . 13 |- (aleph` y) e. On
78	77	onelssi 3778	. . . . . . . . . . . 12 |- (A e. (aleph` y) -> A C_ (aleph` y))
79	76, 78	nsyl 131	. . . . . . . . . . 11 |- ((A e. On /\ y e. |^|{x e. On | A C_ (aleph` x)}) -> -. A e. (aleph` y))
80	79	nrexdv 2193	. . . . . . . . . 10 |- (A e. On -> -. E.y e. |^|{x e. On | A C_ (aleph` x)}A e. (aleph` y))
81	80	adantr 425	. . . . . . . . 9 |- ((A e. On /\ Lim |^|{x e. On | A C_ (aleph` x)}) -> -. E.y e. |^|{x e. On | A C_ (aleph` x)}A e. (aleph` y))
82		alephlim 5875	. . . . . . . . . . . 12 |- ((|^|{x e. On | A C_ (aleph` x)} e. On /\ Lim |^|{x e. On | A C_ (aleph` x)}) -> (aleph` |^|{x e. On | A C_ (aleph` x)}) = U_y e. |^|{x e. On | A C_ (aleph` x)} (aleph` y))
83	82, 10	sylan 497	. . . . . . . . . . 11 |- ((A e. On /\ Lim |^|{x e. On | A C_ (aleph` x)}) -> (aleph` |^|{x e. On | A C_ (aleph` x)}) = U_y e. |^|{x e. On | A C_ (aleph` x)} (aleph` y))
84	83	eleq2d 1964	. . . . . . . . . 10 |- ((A e. On /\ Lim |^|{x e. On | A C_ (aleph` x)}) -> (A e. (aleph` |^|{x e. On | A C_ (aleph` x)}) <-> A e. U_y e. |^|{x e. On | A C_ (aleph` x)} (aleph` y)))
85		eliun 3259	. . . . . . . . . 10 |- (A e. U_y e. |^|{x e. On | A C_ (aleph` x)} (aleph` y) <-> E.y e. |^|{x e. On | A C_ (aleph` x)}A e. (aleph` y))
86	84, 85	syl6bb 595	. . . . . . . . 9 |- ((A e. On /\ Lim |^|{x e. On | A C_ (aleph` x)}) -> (A e. (aleph` |^|{x e. On | A C_ (aleph` x)}) <-> E.y e. |^|{x e. On | A C_ (aleph` x)}A e. (aleph` y)))
87	81, 86	mtbird 783	. . . . . . . 8 |- ((A e. On /\ Lim |^|{x e. On | A C_ (aleph` x)}) -> -. A e. (aleph` |^|{x e. On | A C_ (aleph` x)}))
88	87	ex 402	. . . . . . 7 |- (A e. On -> (Lim |^|{x e. On | A C_ (aleph` x)} -> -. A e. (aleph` |^|{x e. On | A C_ (aleph` x)})))
89	3, 88	syl 12	. . . . . 6 |- ((card` A) = A -> (Lim |^|{x e. On | A C_ (aleph` x)} -> -. A e. (aleph` |^|{x e. On | A C_ (aleph` x)})))
90	72, 89	jaod 469	. . . . 5 |- ((card` A) = A -> ((E.y e. On |^|{x e. On | A C_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A C_ (aleph` x)}) -> -. A e. (aleph` |^|{x e. On | A C_ (aleph` x)})))
91	8, 26	syl 12	. . . . . . 7 |- (A e. On -> A C_ (aleph` |^|{x e. On | A C_ (aleph` x)}))
92		alephon 5876	. . . . . . . 8 |- (aleph` |^|{x e. On | A C_ (aleph` x)}) e. On
93		onsseleq 3704	. . . . . . . 8 |- ((A e. On /\ (aleph` |^|{x e. On | A C_ (aleph` x)}) e. On) -> (A C_ (aleph` |^|{x e. On | A C_ (aleph` x)}) <-> (A e. (aleph` |^|{x e. On | A C_ (aleph` x)}) \/ A = (aleph` |^|{x e. On | A C_ (aleph` x)}))))
94	92, 93	mpan2 760	. . . . . . 7 |- (A e. On -> (A C_ (aleph` |^|{x e. On | A C_ (aleph` x)}) <-> (A e. (aleph` |^|{x e. On | A C_ (aleph` x)}) \/ A = (aleph` |^|{x e. On | A C_ (aleph` x)}))))
95	91, 94	mpbid 212	. . . . . 6 |- (A e. On -> (A e. (aleph` |^|{x e. On | A C_ (aleph` x)}) \/ A = (aleph` |^|{x e. On | A C_ (aleph` x)})))
96	95	ord 249	. . . . 5 |- (A e. On -> (-. A e. (aleph` |^|{x e. On | A C_ (aleph` x)}) -> A = (aleph` |^|{x e. On | A C_ (aleph` x)})))
97	3, 90, 96	sylsyld 32	. . . 4 |- ((card` A) = A -> ((E.y e. On |^|{x e. On | A C_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A C_ (aleph` x)}) -> A = (aleph` |^|{x e. On | A C_ (aleph` x)})))
98	97	adantl 424	. . 3 |- ((om C_ A /\ (card` A) = A) -> ((E.y e. On |^|{x e. On | A C_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A C_ (aleph` x)}) -> A = (aleph` |^|{x e. On | A C_ (aleph` x)})))
99	38, 98	jaod 469	. 2 |- ((om C_ A /\ (card` A) = A) -> ((|^|{x e. On | A C_ (aleph` x)} = (/) \/ (E.y e. On |^|{x e. On | A C_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A C_ (aleph` x)})) -> A = (aleph` |^|{x e. On | A C_ (aleph` x)})))
100	17, 99	mpd 29	1 |- ((om C_ A /\ (card` A) = A) -> A = (aleph` |^|{x e. On | A C_ (aleph` x)}))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   \/ w3o 857   = wceq 1298   e. wcel 1300  E.wrex 2106  {crab 2108  _Vcvv 2292   C_ wss 2593  (/)c0 2875  |^|cint 3214  U_ciun 3255   class class class wbr 3338  Ord word 3656  Oncon0 3657  Lim wlim 3658  suc csuc 3659  omcom 3949  ` cfv 3998   ~<_ cdom 5424   ~< csdm 5425  cardccrd 5859  alephcale 5860

This theorem is referenced by:  cardalephex 6034

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-reg 5695  ax-inf2 5731  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-rdg 5140  df-er 5318  df-en 5427  df-dom 5428  df-sdom 5429  df-fin 5430  df-card 5862  df-aleph 5863

Copyright terms: Public domain