Theorem cardaleph 3690

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(s):   x,A

Proof of Theorem cardaleph

Step	Hyp	Ref	Expression
1		cardon 3634	. . . . 5 |- (card` A) e. On
2		eleq1 1149	. . . . 5 |- ((card` A) = A -> ((card` A) e. On <-> A e. On))
3	1, 2	mpbii 168	. . . 4 |- ((card` A) = A -> A e. On)
4		alephle 3689	. . . . . 6 |- (A e. On -> A (_ (aleph` A))
5		fveq2 2832	. . . . . . . 8 |- (x = A -> (aleph` x) = (aleph` A))
6	5	sseq2d 1528	. . . . . . 7 |- (x = A -> (A (_ (aleph` x) <-> A (_ (aleph` A)))
7	6	rcla4ev 1403	. . . . . 6 |- ((A e. On /\ A (_ (aleph` A)) -> E.x e. On A (_ (aleph` x))
8	4, 7	mpdan 527	. . . . 5 |- (A e. On -> E.x e. On A (_ (aleph` x))
9		onintrab2 2269	. . . . 5 |- (E.x e. On A (_ (aleph` x) <-> |^|{x e. On | A (_ (aleph` x)} e. On)
10	8, 9	sylib 173	. . . 4 |- (A e. On -> |^|{x e. On | A (_ (aleph` x)} e. On)
11		eloni 2209	. . . . 5 |- (|^|{x e. On | A (_ (aleph` x)} e. On -> Ord |^|{x e. On | A (_ (aleph` x)})
12		ordzsl 2366	. . . . . 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 584	. . . . . 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 151	. . . . 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 173	. . . 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 21	. . 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 305	. 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 925	. . . . . . . . . . 11 |- (y e. A -> A.x y e. A)
19		ax-17 925	. . . . . . . . . . . 12 |- (y e. aleph -> A.x y e. aleph)
20		hbrab1 1310	. . . . . . . . . . . . 13 |- (y e. {x e. On | A (_ (aleph` x)} -> A.x y e. {x e. On | A (_ (aleph` x)})
21	20	hbint 1975	. . . . . . . . . . . 12 |- (y e. |^|{x e. On | A (_ (aleph` x)} -> A.x y e. |^|{x e. On | A (_ (aleph` x)})
22	19, 21	hbfv 2837	. . . . . . . . . . 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 1501	. . . . . . . . . 10 |- (A (_ (aleph` |^|{x e. On | A (_ (aleph` x)}) -> A.x A (_ (aleph` |^|{x e. On | A (_ (aleph` x)}))
24		fveq2 2832	. . . . . . . . . . 11 |- (x = |^|{x e. On | A (_ (aleph` x)} -> (aleph` x) = (aleph` |^|{x e. On | A (_ (aleph` x)}))
25	24	sseq2d 1528	. . . . . . . . . 10 |- (x = |^|{x e. On | A (_ (aleph` x)} -> (A (_ (aleph` x) <-> A (_ (aleph` |^|{x e. On | A (_ (aleph` x)})))
26	23, 25	onminsb 2264	. . . . . . . . 9 |- (E.x e. On A (_ (aleph` x) -> A (_ (aleph` |^|{x e. On | A (_ (aleph` x)}))
27	3, 8, 26	3syl 21	. . . . . . . 8 |- ((card` A) = A -> A (_ (aleph` |^|{x e. On | A (_ (aleph` x)}))
28	27	a1i 7	. . . . . . 7 |- (|^|{x e. On | A (_ (aleph` x)} = (/) -> ((card` A) = A -> A (_ (aleph` |^|{x e. On | A (_ (aleph` x)})))
29		fveq2 2832	. . . . . . . . . 10 |- (|^|{x e. On | A (_ (aleph` x)} = (/) -> (aleph` |^|{x e. On | A (_ (aleph` x)}) = (aleph` (/)))
30		aleph0 3669	. . . . . . . . . 10 |- (aleph` (/)) = om
31	29, 30	syl6eq 1140	. . . . . . . . 9 |- (|^|{x e. On | A (_ (aleph` x)} = (/) -> (aleph` |^|{x e. On | A (_ (aleph` x)}) = om)
32	31	sseq1d 1527	. . . . . . . 8 |- (|^|{x e. On | A (_ (aleph` x)} = (/) -> ((aleph` |^|{x e. On | A (_ (aleph` x)}) (_ A <-> om (_ A))
33	32	biimprd 136	. . . . . . 7 |- (|^|{x e. On | A (_ (aleph` x)} = (/) -> (om (_ A -> (aleph` |^|{x e. On | A (_ (aleph` x)}) (_ A))
34	28, 33	anim12d 431	. . . . . 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 1516	. . . . . 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 186	. . . . 5 |- (|^|{x e. On | A (_ (aleph` x)} = (/) -> (((card` A) = A /\ om (_ A) -> A = (aleph` |^|{x e. On | A (_ (aleph` x)})))
37	36	com12 13	. . . 4 |- (((card` A) = A /\ om (_ A) -> (|^|{x e. On | A (_ (aleph` x)} = (/) -> A = (aleph` |^|{x e. On | A (_ (aleph` x)})))
38	37	ancoms 334	. . 3 |- ((om (_ A /\ (card` A) = A) -> (|^|{x e. On | A (_ (aleph` x)} = (/) -> A = (aleph` |^|{x e. On | A (_ (aleph` x)})))
39		fveq2 2832	. . . . . . . . . . . . . 14 |- (x = y -> (aleph` x) = (aleph` y))
40	39	sseq2d 1528	. . . . . . . . . . . . 13 |- (x = y -> (A (_ (aleph` x) <-> A (_ (aleph` y)))
41	40	onnminsb 2271	. . . . . . . . . . . 12 |- (y e. On -> (y e. |^|{x e. On | A (_ (aleph` x)} -> -. A (_ (aleph` y)))
42		visset 1350	. . . . . . . . . . . . . 14 |- y e. V
43	42	sucid 2304	. . . . . . . . . . . . 13 |- y e. suc y
44		eleq2 1150	. . . . . . . . . . . . 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 169	. . . . . . . . . . . 12 |- (|^|{x e. On | A (_ (aleph` x)} = suc y -> y e. |^|{x e. On | A (_ (aleph` x)})
46	41, 45	syl5 22	. . . . . . . . . . 11 |- (y e. On -> (|^|{x e. On | A (_ (aleph` x)} = suc y -> -. A (_ (aleph` y)))
47	46	imp 277	. . . . . . . . . 10 |- ((y e. On /\ |^|{x e. On | A (_ (aleph` x)} = suc y) -> -. A (_ (aleph` y))
48	47	adantl 305	. . . . . . . . 9 |- (((card` A) = A /\ (y e. On /\ |^|{x e. On | A (_ (aleph` x)} = suc y)) -> -. A (_ (aleph` y))
49		fveq2 2832	. . . . . . . . . . . . 13 |- (|^|{x e. On | A (_ (aleph` x)} = suc y -> (aleph` |^|{x e. On | A (_ (aleph` x)}) = (aleph` suc y))
50		alephsuc 3672	. . . . . . . . . . . . 13 |- (y e. On -> (aleph` suc y) = |^|{x e. On | (aleph` y) ~< x})
51	49, 50	sylan9eqr 1145	. . . . . . . . . . . 12 |- ((y e. On /\ |^|{x e. On | A (_ (aleph` x)} = suc y) -> (aleph` |^|