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	⊢ ((ω ⊆ A ∧ (card ‘A) = A) → A = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}))

Distinct variable group(s):   x,A

Proof of Theorem cardaleph

Step	Hyp	Ref	Expression
1		cardon 3634	. . . . 5 ⊢ (card ‘A) ∈ On
2		eleq1 1149	. . . . 5 ⊢ ((card ‘A) = A → ((card ‘A) ∈ On ↔ A ∈ On))
3	1, 2	mpbii 168	. . . 4 ⊢ ((card ‘A) = A → A ∈ On)
4		alephle 3689	. . . . . 6 ⊢ (A ∈ On → A ⊆ (ℵ ‘A))
5		fveq2 2832	. . . . . . . 8 ⊢ (x = A → (ℵ ‘x) = (ℵ ‘A))
6	5	sseq2d 1528	. . . . . . 7 ⊢ (x = A → (A ⊆ (ℵ ‘x) ↔ A ⊆ (ℵ ‘A)))
7	6	rcla4ev 1403	. . . . . 6 ⊢ ((A ∈ On ∧ A ⊆ (ℵ ‘A)) → ∃x ∈ On A ⊆ (ℵ ‘x))
8	4, 7	mpdan 527	. . . . 5 ⊢ (A ∈ On → ∃x ∈ On A ⊆ (ℵ ‘x))
9		onintrab2 2269	. . . . 5 ⊢ (∃x ∈ On A ⊆ (ℵ ‘x) ↔ ∩{x ∈ On∣A ⊆ (ℵ ‘x)} ∈ On)
10	8, 9	sylib 173	. . . 4 ⊢ (A ∈ On → ∩{x ∈ On∣A ⊆ (ℵ ‘x)} ∈ On)
11		eloni 2209	. . . . 5 ⊢ (∩{x ∈ On∣A ⊆ (ℵ ‘x)} ∈ On → Ord ∩{x ∈ On∣A ⊆ (ℵ ‘x)})
12		ordzsl 2366	. . . . . 6 ⊢ (Ord ∩{x ∈ On∣A ⊆ (ℵ ‘x)} ↔ (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ ∨ ∃y ∈ On ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y ∨ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)}))
13		3orass 584	. . . . . 6 ⊢ ((∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ ∨ ∃y ∈ On ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y ∨ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ↔ (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ ∨ (∃y ∈ On ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y ∨ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
14	12, 13	bitr 151	. . . . 5 ⊢ (Ord ∩{x ∈ On∣A ⊆ (ℵ ‘x)} ↔ (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ ∨ (∃y ∈ On ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y ∨ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
15	11, 14	sylib 173	. . . 4 ⊢ (∩{x ∈ On∣A ⊆ (ℵ ‘x)} ∈ On → (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ ∨ (∃y ∈ On ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y ∨ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
16	3, 10, 15	3syl 21	. . 3 ⊢ ((card ‘A) = A → (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ ∨ (∃y ∈ On ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y ∨ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
17	16	adantl 305	. 2 ⊢ ((ω ⊆ A ∧ (card ‘A) = A) → (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ ∨ (∃y ∈ On ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y ∨ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
18		ax-17 925	. . . . . . . . . . 11 ⊢ (y ∈ A → ∀x y ∈ A)
19		ax-17 925	. . . . . . . . . . . 12 ⊢ (y ∈ ℵ → ∀x y ∈ ℵ)
20		hbrab1 1310	. . . . . . . . . . . . 13 ⊢ (y ∈ {x ∈ On∣A ⊆ (ℵ ‘x)} → ∀x y ∈ {x ∈ On∣A ⊆ (ℵ ‘x)})
21	20	hbint 1975	. . . . . . . . . . . 12 ⊢ (y ∈ ∩{x ∈ On∣A ⊆ (ℵ ‘x)} → ∀x y ∈ ∩{x ∈ On∣A ⊆ (ℵ ‘x)})
22	19, 21	hbfv 2837	. . . . . . . . . . 11 ⊢ (y ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → ∀x y ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}))
23	18, 22	hbss 1501	. . . . . . . . . 10 ⊢ (A ⊆ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → ∀x A ⊆ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}))
24		fveq2 2832	. . . . . . . . . . 11 ⊢ (x = ∩{x ∈ On∣A ⊆ (ℵ ‘x)} → (ℵ ‘x) = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}))
25	24	sseq2d 1528	. . . . . . . . . 10 ⊢ (x = ∩{x ∈ On∣A ⊆ (ℵ ‘x)} → (A ⊆ (ℵ ‘x) ↔ A ⊆ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
26	23, 25	onminsb 2264	. . . . . . . . 9 ⊢ (∃x ∈ On A ⊆ (ℵ ‘x) → A ⊆ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}))
27	3, 8, 26	3syl 21	. . . . . . . 8 ⊢ ((card ‘A) = A → A ⊆ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}))
28	27	a1i 7	. . . . . . 7 ⊢ (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ → ((card ‘A) = A → A ⊆ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
29		fveq2 2832	. . . . . . . . . 10 ⊢ (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ → (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) = (ℵ ‘∅))
30		aleph0 3669	. . . . . . . . . 10 ⊢ (ℵ ‘∅) = ω
31	29, 30	syl6eq 1140	. . . . . . . . 9 ⊢ (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ → (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) = ω)
32	31	sseq1d 1527	. . . . . . . 8 ⊢ (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ → ((ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ⊆ A ↔ ω ⊆ A))
33	32	biimprd 136	. . . . . . 7 ⊢ (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ → (ω ⊆ A → (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ⊆ A))
34	28, 33	anim12d 431	. . . . . 6 ⊢ (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ → (((card ‘A) = A ∧ ω ⊆ A) → (A ⊆ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ∧ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ⊆ A)))
35		eqss 1516	. . . . . 6 ⊢ (A = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ↔ (A ⊆ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ∧ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ⊆ A))
36	34, 35	syl6ibr 186	. . . . 5 ⊢ (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ → (((card ‘A) = A ∧ ω ⊆ A) → A = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
37	36	com12 13	. . . 4 ⊢ (((card ‘A) = A ∧ ω ⊆ A) → (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ → A = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
38	37	ancoms 334	. . 3 ⊢ ((ω ⊆ A ∧ (card ‘A) = A) → (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ → A = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
39		fveq2 2832	. . . . . . . . . . . . . 14 ⊢ (x = y → (ℵ ‘x) = (ℵ ‘y))
40	39	sseq2d 1528	. . . . . . . . . . . . 13 ⊢ (x = y → (A ⊆ (ℵ ‘x) ↔ A ⊆ (ℵ ‘y)))
41	40	onnminsb 2271	. . . . . . . . . . . 12 ⊢ (y ∈ On → (y ∈ ∩{x ∈ On∣A ⊆ (ℵ ‘x)} → ¬ A ⊆ (ℵ ‘y)))
42		visset 1350	. . . . . . . . . . . . . 14 ⊢ y ∈ V
43	42	sucid 2304	. . . . . . . . . . . . 13 ⊢ y ∈ suc y
44		eleq2 1150	. . . . . . . . . . . . 13 ⊢ (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y → (y ∈ ∩{x ∈ On∣A ⊆ (ℵ ‘x)} ↔ y ∈ suc y))
45	43, 44	mpbiri 169	. . . . . . . . . . . 12 ⊢ (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y → y ∈ ∩{x ∈ On∣A ⊆ (ℵ ‘x)})
46	41, 45	syl5 22	. . . . . . . . . . 11 ⊢ (y ∈ On → (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y → ¬ A ⊆ (ℵ ‘y)))
47	46	imp 277	. . . . . . . . . 10 ⊢ ((y ∈ On ∧ ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y) → ¬ A ⊆ (ℵ ‘y))
48	47	adantl 305	. . . . . . . . 9 ⊢ (((card ‘A) = A ∧ (y ∈ On ∧ ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y)) → ¬ A ⊆ (ℵ ‘y))
49		fveq2 2832	. . . . . . . . . . . . 13 ⊢ (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y → (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) = (ℵ ‘suc y))
50		alephsuc 3672	. . . . . . . . . . . . 13 ⊢ (y ∈ On → (ℵ ‘suc y) = ∩{x ∈ On∣(ℵ ‘y) ≺ x})
51	49, 50	sylan9eqr 1145	. . . . . . . . . . . 12 ⊢ ((y ∈ On ∧ ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y) → (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) = ∩{x ∈ On∣(ℵ ‘y) ≺ x})
52	51	eleq2d 1156	. . . . . . . . . . 11 ⊢ ((y ∈ On ∧ ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y) → (A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ↔ A ∈ ∩{x ∈ On∣(ℵ ‘y) ≺ x}))
53	52	biimpd 135	. . . . . . . . . 10 ⊢ ((y ∈ On ∧ ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y) → (A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → A ∈ ∩{x ∈ On∣(ℵ ‘y) ≺ x}))
54		breq2 2066	. . . . . . . . . . . . . . 15 ⊢ (x = A → ((ℵ ‘y) ≺ x ↔ (ℵ ‘y) ≺ A))
55	54	onnminsb 2271	. . . . . . . . . . . . . 14 ⊢ (A ∈ On → (A ∈ ∩{x ∈ On∣(ℵ ‘y) ≺ x} → ¬ (ℵ ‘y) ≺ A))
56		fvex 2838	. . . . . . . . . . . . . . 15 ⊢ (ℵ ‘y) ∈ V
57		domtri 3644	. . . . . . . . . . . . . . 15 ⊢ ((A ∈ On ∧ (ℵ ‘y) ∈ V) → (A ≼ (ℵ ‘y) ↔ ¬ (ℵ ‘y) ≺ A))
58	56, 57	mpan2 519	. . . . . . . . . . . . . 14 ⊢ (A ∈ On → (A ≼ (ℵ ‘y) ↔ ¬ (ℵ ‘y) ≺ A))
59	55, 58	sylibrd 179	. . . . . . . . . . . . 13 ⊢ (A ∈ On → (A ∈ ∩{x ∈ On∣(ℵ ‘y) ≺ x} → A ≼ (ℵ ‘y)))
60		carddom 3642	. . . . . . . . . . . . . 14 ⊢ ((A ∈ On ∧ (ℵ ‘y) ∈ V) → ((card ‘A) ⊆ (card ‘(ℵ ‘y)) ↔ A ≼ (ℵ ‘y)))
61	56, 60	mpan2 519	. . . . . . . . . . . . 13 ⊢ (A ∈ On → ((card ‘A) ⊆ (card ‘(ℵ ‘y)) ↔ A ≼ (ℵ ‘y)))
62	59, 61	sylibrd 179	. . . . . . . . . . . 12 ⊢ (A ∈ On → (A ∈ ∩{x ∈ On∣(ℵ ‘y) ≺ x} → (card ‘A) ⊆ (card ‘(ℵ ‘y))))
63	3, 62	syl 12	. . . . . . . . . . 11 ⊢ ((card ‘A) = A → (A ∈ ∩{x ∈ On∣(ℵ ‘y) ≺ x} → (card ‘A) ⊆ (card ‘(ℵ ‘y))))
64		sseq1 1521	. . . . . . . . . . . 12 ⊢ ((card ‘A) = A → ((card ‘A) ⊆ (card ‘(ℵ ‘y)) ↔ A ⊆ (card ‘(ℵ ‘y))))
65		alephcard 3673	. . . . . . . . . . . . 13 ⊢ (card ‘(ℵ ‘y)) = (ℵ ‘y)
66	65	sseq2i 1525	. . . . . . . . . . . 12 ⊢ (A ⊆ (card ‘(ℵ ‘y)) ↔ A ⊆ (ℵ ‘y))
67	64, 66	syl6bb 414	. . . . . . . . . . 11 ⊢ ((card ‘A) = A → ((card ‘A) ⊆ (card ‘(ℵ ‘y)) ↔ A ⊆ (ℵ ‘y)))
68	63, 67	sylibd 177	. . . . . . . . . 10 ⊢ ((card ‘A) = A → (A ∈ ∩{x ∈ On∣(ℵ ‘y) ≺ x} → A ⊆ (ℵ ‘y)))
69	53, 68	sylan9r 360	. . . . . . . . 9 ⊢ (((card ‘A) = A ∧ (y ∈ On ∧ ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y)) → (A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → A ⊆ (ℵ ‘y)))
70	48, 69	mtod 95	. . . . . . . 8 ⊢ (((card ‘A) = A ∧ (y ∈ On ∧ ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y)) → ¬ A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}))
71	70	exp32 294	. . . . . . 7 ⊢ ((card ‘A) = A → (y ∈ On → (∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y → ¬ A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}))))
72	71	r19.23adv 1286	. . . . . 6 ⊢ ((card ‘A) = A → (∃y ∈ On ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y → ¬ A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
73		onelon 2223	. . . . . . . . . . . . . 14 ⊢ ((∩{x ∈ On∣A ⊆ (ℵ ‘x)} ∈ On ∧ y ∈ ∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → y ∈ On)
74	73, 10	sylan 343	. . . . . . . . . . . . 13 ⊢ ((A ∈ On ∧ y ∈ ∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → y ∈ On)
75	41	adantld 307	. . . . . . . . . . . . 13 ⊢ (y ∈ On → ((A ∈ On ∧ y ∈ ∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → ¬ A ⊆ (ℵ ‘y)))
76	74, 75	mpcom 49	. . . . . . . . . . . 12 ⊢ ((A ∈ On ∧ y ∈ ∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → ¬ A ⊆ (ℵ ‘y))
77		alephon 3671	. . . . . . . . . . . . 13 ⊢ (ℵ ‘y) ∈ On
78	77	onelss 2348	. . . . . . . . . . . 12 ⊢ (A ∈ (ℵ ‘y) → A ⊆ (ℵ ‘y))
79	76, 78	nsyl 102	. . . . . . . . . . 11 ⊢ ((A ∈ On ∧ y ∈ ∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → ¬ A ∈ (ℵ ‘y))
80	79	nrexdv 1271	. . . . . . . . . 10 ⊢ (A ∈ On → ¬ ∃y ∈ ∩ {x ∈ On∣A ⊆ (ℵ ‘x)}A ∈ (ℵ ‘y))
81	80	adantr 306	. . . . . . . . 9 ⊢ ((A ∈ On ∧ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → ¬ ∃y ∈ ∩ {x ∈ On∣A ⊆ (ℵ ‘x)}A ∈ (ℵ ‘y))
82		alephlim 3670	. . . . . . . . . . . 12 ⊢ ((∩{x ∈ On∣A ⊆ (ℵ ‘x)} ∈ On ∧ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) = ∪y ∈ ∩ {x ∈ On∣A ⊆ (ℵ ‘x)} (ℵ ‘y))
83	82, 10	sylan 343	. . . . . . . . . . 11 ⊢ ((A ∈ On ∧ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) = ∪y ∈ ∩ {x ∈ On∣A ⊆ (ℵ ‘x)} (ℵ ‘y))
84	83	eleq2d 1156	. . . . . . . . . 10 ⊢ ((A ∈ On ∧ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → (A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ↔ A ∈ ∪y ∈ ∩ {x ∈ On∣A ⊆ (ℵ ‘x)} (ℵ ‘y)))
85		eliun 1998	. . . . . . . . . 10 ⊢ (A ∈ ∪y ∈ ∩ {x ∈ On∣A ⊆ (ℵ ‘x)} (ℵ ‘y) ↔ ∃y ∈ ∩ {x ∈ On∣A ⊆ (ℵ ‘x)}A ∈ (ℵ ‘y))
86	84, 85	syl6bb 414	. . . . . . . . 9 ⊢ ((A ∈ On ∧ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → (A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ↔ ∃y ∈ ∩ {x ∈ On∣A ⊆ (ℵ ‘x)}A ∈ (ℵ ‘y)))
87	81, 86	mtbird 537	. . . . . . . 8 ⊢ ((A ∈ On ∧ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → ¬ A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}))
88	87	exp 291	. . . . . . 7 ⊢ (A ∈ On → (Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)} → ¬ A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
89	3, 88	syl 12	. . . . . 6 ⊢ ((card ‘A) = A → (Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)} → ¬ A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
90	72, 89	jaod 329	. . . . 5 ⊢ ((card ‘A) = A → ((∃y ∈ On ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y ∨ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → ¬ A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
91	8, 26	syl 12	. . . . . . . 8 ⊢ (A ∈ On → A ⊆ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}))
92		alephon 3671	. . . . . . . . 9 ⊢ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ∈ On
93		onsseleq 2254	. . . . . . . . 9 ⊢ ((A ∈ On ∧ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ∈ On) → (A ⊆ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ↔ (A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ∨ A = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}))))
94	92, 93	mpan2 519	. . . . . . . 8 ⊢ (A ∈ On → (A ⊆ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ↔ (A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ∨ A = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}))))
95	91, 94	mpbid 170	. . . . . . 7 ⊢ (A ∈ On → (A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) ∨ A = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
96	95	ord 202	. . . . . 6 ⊢ (A ∈ On → (¬ A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → A = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
97	3, 96	syl 12	. . . . 5 ⊢ ((card ‘A) = A → (¬ A ∈ (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → A = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
98	90, 97	syld 27	. . . 4 ⊢ ((card ‘A) = A → ((∃y ∈ On ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y ∨ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → A = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
99	98	adantl 305	. . 3 ⊢ ((ω ⊆ A ∧ (card ‘A) = A) → ((∃y ∈ On ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y ∨ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)}) → A = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
100	38, 99	jaod 329	. 2 ⊢ ((ω ⊆ A ∧ (card ‘A) = A) → ((∩{x ∈ On∣A ⊆ (ℵ ‘x)} = ∅ ∨ (∃y ∈ On ∩{x ∈ On∣A ⊆ (ℵ ‘x)} = suc y ∨ Lim ∩{x ∈ On∣A ⊆ (ℵ ‘x)})) → A = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)})))
101	17, 100	mpd 46	1 ⊢ ((ω ⊆ A ∧ (card ‘A) = A) → A = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196   ∨ w3o 580   = weq 797   = wceq 1091   ∈ wcel 1092  ∃wrex 1202  {crab 1204  Vcvv 1348   ⊆ wss 1487  ∅c0 1707  ∩cint 1965  ∪ciun 1994   class class class wbr 2054  Ord word 2198  Oncon0 2199  Lim wlim 2200  suc csuc 2201  ωcom 2372   ‘cfv 2422   ≼ cdom 3272   ≺ csdm 3273  cardccrd 3620  ℵcale 3621

This theorem is referenced by:  cardalephex 3691

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-inf 1079  ax-ac 1080

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-iun 1996  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-rdg 2970  df-er 3200  df-en 3274  df-dom 3275  df-sdom 3276  df-card 3623  df-aleph 3624

metamath.org