Theorem cardaleph 4868

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 (_ A /\ (card` A) = A) -> A = (aleph` |^|{x e. On | A (_ (aleph` x)}))

Distinct variable group:   x,A

Proof of Theorem cardaleph

Step	Hyp	Ref	Expression
1		cardon 4810	. . . . 5 |- (card` A) e. On
2		eleq1 1532	. . . . 5 |- ((card` A) = A -> ((card` A) e. On <-> A e. On))
3	1, 2	mpbii 193	. . . 4 |- ((card` A) = A -> A e. On)
4		alephle 4867	. . . . . 6 |- (A e. On -> A (_ (aleph` A))
5		fveq2 3719	. . . . . . . 8 |- (x = A -> (aleph` x) = (aleph` A))
6	5	sseq2d 2086	. . . . . . 7 |- (x = A -> (A (_ (aleph` x) <-> A (_ (aleph` A)))
7	6	rcla4ev 1874	. . . . . 6 |- ((A e. On /\ A (_ (aleph` A)) -> E.x e. On A (_ (aleph` x))
8	4, 7	mpdan 703	. . . . 5 |- (A e. On -> E.x e. On A (_ (aleph` x))
9		onintrab2 3010	. . . . 5 |- (E.x e. On A (_ (aleph` x) <-> |^|{x e. On | A (_ (aleph` x)} e. On)
10	8, 9	sylib 198	. . . 4 |- (A e. On -> |^|{x e. On | A (_ (aleph` x)} e. On)
11		eloni 2954	. . . . 5 |- (|^|{x e. On | A (_ (aleph` x)} e. On -> Ord |^|{x e. On | A (_ (aleph` x)})
12		ordzsl 3112	. . . . . 6 |- (Ord |^|{x e. On | A (_ (aleph` x)} <-> (|^|{x e. On | A (_ (aleph` x)} = (/) \/ E.y e. On |^|{x e. On | A (_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A (_ (aleph` x)}))
13		3orass 777	. . . . . 6 |- ((|^|{x e. On | A (_ (aleph` x)} = (/) \/ E.y e. On |^|{x e. On | A (_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A (_ (aleph` x)}) <-> (|^|{x e. On | A (_ (aleph` x)} = (/) \/ (E.y e. On |^|{x e. On | A (_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A (_ (aleph` x)})))
14	12, 13	bitr 173	. . . . 5 |- (Ord |^|{x e. On | A (_ (aleph` x)} <-> (|^|{x e. On | A (_ (aleph` x)} = (/) \/ (E.y e. On |^|{x e. On | A (_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A (_ (aleph` x)})))
15	11, 14	sylib 198	. . . 4 |- (|^|{x e. On | A (_ (aleph` x)} e. On -> (|^|{x e. On | A (_ (aleph` x)} = (/) \/ (E.y e. On |^|{x e. On | A (_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A (_ (aleph` x)})))
16	3, 10, 15	3syl 20	. . 3 |- ((card` A) = A -> (|^|{x e. On | A (_ (aleph` x)} = (/) \/ (E.y e. On |^|{x e. On | A (_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A (_ (aleph` x)})))
17	16	adantl 388	. 2 |- ((om (_ A /\ (card` A) = A) -> (|^|{x e. On | A (_ (aleph` x)} = (/) \/ (E.y e. On |^|{x e. On | A (_ (aleph` x)} = suc y \/ Lim |^|{x e. On | A (_ (aleph` x)})))
18		ax-17 970	. . . . . . . . . . 11 |- (y e. A -> A.x y e. A)
19		ax-17 970	. . . . . . . . . . . 12 |- (y e. aleph -> A.x y e. aleph)
20		hbrab1 1770	. . . . . . . . . . . . 13 |- (y e. {x e. On | A (_ (aleph` x)} -> A.x y e. {x e. On | A (_ (aleph` x)})
21	20	hbint 2539	. . . . . . . . . . . 12 |- (y e. |^|{x e. On | A (_ (aleph` x)} -> A.x y e. |^|{x e. On | A (_ (aleph` x)})
22	19, 21	hbfv 3724	. . . . . . . . . . 11 |- (y e. (aleph` |^|{x e. On | A (_ (aleph` x)}) -> A.x y e. (aleph` |^|{x e. On | A (_ (aleph` x)}))
23	18, 22	hbss 2059	. . . . . . . . . 10 |- (A (_ (aleph` |^|{x e. On | A (_ (aleph` x)}) -> A.x A (_ (aleph` |^|{x e. On | A (_ (aleph` x)}))
24		fveq2 3719	. . . . . . . . . . 11 |- (x = |^|{x e. On | A (_ (aleph` x)} -> (aleph` x) = (aleph` |^|{x e. On | A (_ (aleph` x)}))
25	24	sseq2d 2086	. . . . . . . . . 10 |- (x = |^|{x e. On | A (_ (aleph` x)} -> (A (_ (aleph` x) <-> A (_ (aleph` |^|{x e. On | A (_ (aleph` x)})))
26	23, 25	onminsb 3005	. . . . . . . . 9 |- (E.x e. On A (_ (aleph` x) -> A (_ (aleph` |^|{x e. On | A (_ (aleph` x)}))
27	3, 8, 26	3syl 20	. . . . . . . 8 |- ((card` A) = A -> A (_ (aleph` |^|{x e. On | A (_ (aleph` x)}))
28	27	a1i 8	. . . . . . 7 |- (|^|{x e. On | A (_ (aleph` x)} = (/) -> ((card` A) = A -> A (_ (aleph` |^|{x e. On | A (_ (aleph` x)})))
29		fveq2 3719	. . . . . . . . . 10 |- (|^|{x e. On | A (_ (aleph` x)} = (/) -> (aleph` |^|{x e. On | A (_ (aleph` x)}) = (aleph` (/)))
30		aleph0 4846	. . . . . . . . . 10 |- (aleph` (/)) = om
31	29, 30	syl6eq 1521	. . . . . . . . 9 |- (|^|{x e. On | A (_ (aleph` x)} = (/) -> (aleph` |^|{x e. On | A (_ (aleph` x)}) = om)
32	31	sseq1d 2085	. . . . . . . 8 |- (|^|{x e. On | A (_ (aleph` x)} = (/) -> ((aleph` |^|{x e. On | A (_ (aleph` x)}) (_ A <-> om (_ A))
33	32	biimprd 154	. . . . . . 7 |- (|^|{x e. On | A (_ (aleph` x)} = (/) -> (om (_ A -> (aleph` |^|{x e. On | A (_ (aleph` x)}) (_ A))
34	28, 33	anim12d 557	. . . . . 6 |- (|^|{x e. On | A (_ (aleph` x)} = (/) -> (((card` A) = A /\ om (_ A) -> (A (_ (aleph` |^|{x e. On | A (_ (aleph` x)}) /\ (aleph` |^|{x e. On | A (_ (aleph` x)}) (_ A)))
35		eqss 2074	. . . . . 6 |- (A = (aleph` |^|{x e. On | A (_ (aleph` x)}) <-> (A (_ (aleph` |^|{x e. On | A (_ (aleph` x)}) /\ (aleph` |^|{x e. On | A (_ (aleph` x)}) (_ A))
36	34, 35	syl6ibr 213	. . . . 5 |- (|^|{x e. On | A (_ (aleph` x)} = (/) -> (((card` A) = A /\ om (_ A) -> A = (aleph` |^|{x e. On | A (_ (aleph` x)})))
37	36	com12 11	. . . 4 |- (((card` A) = A /\ om (_ A) -> (|^|{x e. On | A (_ (aleph` x)} = (/) -> A = (aleph` |^|{x e. On | A (_ (aleph` x)})))
38	37	ancoms 436	. . 3 |- ((om (_ A /\ (card` A) = A) -> (|^|{x e. On | A (_ (aleph` x)} = (/) -> A = (aleph` |^|{x e. On | A (_ (aleph` x)})))
39		fveq2 3719	. . . . . . . . . . . . . 14 |- (x = y -> (aleph` x) = (aleph` y))
40	39	sseq2d 2086	. . . . . . . . . . . . 13 |- (x = y -> (A (_ (aleph` x) <-> A (_ (aleph` y)))
41	40	onnminsb 3012	. . . . . . . . . . . 12 |- (y e. On -> (y e. |^|{x e. On | A (_ (aleph` x)} -> -. A (_ (aleph` y)))
42		visset 1810	. . . . . . . . . . . . . 14 |- y e. V
43	42	sucid 3047	. . . . . . . . . . . . 13 |- y e. suc y
44		eleq2 1533	. . . . . . . . . . . . 13 |- (|^|{x e. On | A (_ (aleph` x)} = suc y -> (y e. |^|{x e. On | A (_ (aleph` x)} <-> y e. suc y))
45	43, 44	mpbiri 194	. . . . . . . . . . . 12 |- (|^|{x e. On | A (_ (aleph` x)} = suc y -> y e. |^|{x e. On | A (_ (aleph` x)})
46	41, 45	syl5 21	. . . . . . . . . . 11 |- (y e. On -> (|^|{x e. On | A (_ (aleph` x)} = suc y -> -. A (_ (aleph` y)))
47	46	imp 350	. . . . . . . . . 10 |- ((y e. On /\ |^|{x e. On | A (_ (aleph` x)} = suc y) -> -. A (_ (aleph` y))
48	47	adantl 388	. . . . . . . . 9 |- (((card` A) = A /\ (y e. On /\ |^|{x e. On | A (_ (aleph` x)} = suc y)) -> -. A (_ (aleph` y))
49		fveq2 3719	. . . . . . . . . . . . 13 |- (|^|{x e. On | A (_ (aleph` x)} = suc y -> (aleph` |^|{x e. On | A (_ (aleph` x)}) = (aleph` suc y))
50		alephsuc 4849	. . . . . . . . . . . . 13 |- (<