# Metamath Proof Explorer

## Theorem cardaleph

Description: Given any transfinite cardinal number A , there is exactly one aleph that is equal to it. Here we compute that alephexplicitly. (Contributed by NM, 9-Nov-2003) (Revised by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion cardaleph ${⊢}\left(\mathrm{\omega }\subseteq {A}\wedge \mathrm{card}\left({A}\right)={A}\right)\to {A}=\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)$

### Proof

Step Hyp Ref Expression
1 cardon ${⊢}\mathrm{card}\left({A}\right)\in \mathrm{On}$
2 eleq1 ${⊢}\mathrm{card}\left({A}\right)={A}\to \left(\mathrm{card}\left({A}\right)\in \mathrm{On}↔{A}\in \mathrm{On}\right)$
3 1 2 mpbii ${⊢}\mathrm{card}\left({A}\right)={A}\to {A}\in \mathrm{On}$
4 alephle ${⊢}{A}\in \mathrm{On}\to {A}\subseteq \aleph \left({A}\right)$
5 fveq2 ${⊢}{x}={A}\to \aleph \left({x}\right)=\aleph \left({A}\right)$
6 5 sseq2d ${⊢}{x}={A}\to \left({A}\subseteq \aleph \left({x}\right)↔{A}\subseteq \aleph \left({A}\right)\right)$
7 6 rspcev ${⊢}\left({A}\in \mathrm{On}\wedge {A}\subseteq \aleph \left({A}\right)\right)\to \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{A}\subseteq \aleph \left({x}\right)$
8 4 7 mpdan ${⊢}{A}\in \mathrm{On}\to \exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{A}\subseteq \aleph \left({x}\right)$
9 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
10 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\aleph$
11 nfrab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}$
12 11 nfint ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}$
13 10 12 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)$
14 9 13 nfss ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}\subseteq \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)$
15 fveq2 ${⊢}{x}=\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\to \aleph \left({x}\right)=\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)$
16 15 sseq2d ${⊢}{x}=\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\to \left({A}\subseteq \aleph \left({x}\right)↔{A}\subseteq \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
17 14 16 onminsb ${⊢}\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{A}\subseteq \aleph \left({x}\right)\to {A}\subseteq \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)$
18 3 8 17 3syl ${⊢}\mathrm{card}\left({A}\right)={A}\to {A}\subseteq \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)$
19 18 a1i ${⊢}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \to \left(\mathrm{card}\left({A}\right)={A}\to {A}\subseteq \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
20 fveq2 ${⊢}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \to \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)=\aleph \left(\varnothing \right)$
21 aleph0 ${⊢}\aleph \left(\varnothing \right)=\mathrm{\omega }$
22 20 21 syl6eq ${⊢}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \to \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)=\mathrm{\omega }$
23 22 sseq1d ${⊢}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \to \left(\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\subseteq {A}↔\mathrm{\omega }\subseteq {A}\right)$
24 23 biimprd ${⊢}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \to \left(\mathrm{\omega }\subseteq {A}\to \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\subseteq {A}\right)$
25 19 24 anim12d ${⊢}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \to \left(\left(\mathrm{card}\left({A}\right)={A}\wedge \mathrm{\omega }\subseteq {A}\right)\to \left({A}\subseteq \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\wedge \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\subseteq {A}\right)\right)$
26 eqss ${⊢}{A}=\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)↔\left({A}\subseteq \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\wedge \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\subseteq {A}\right)$
27 25 26 syl6ibr ${⊢}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \to \left(\left(\mathrm{card}\left({A}\right)={A}\wedge \mathrm{\omega }\subseteq {A}\right)\to {A}=\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
28 27 com12 ${⊢}\left(\mathrm{card}\left({A}\right)={A}\wedge \mathrm{\omega }\subseteq {A}\right)\to \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \to {A}=\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
29 28 ancoms ${⊢}\left(\mathrm{\omega }\subseteq {A}\wedge \mathrm{card}\left({A}\right)={A}\right)\to \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \to {A}=\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
30 fveq2 ${⊢}{x}={y}\to \aleph \left({x}\right)=\aleph \left({y}\right)$
31 30 sseq2d ${⊢}{x}={y}\to \left({A}\subseteq \aleph \left({x}\right)↔{A}\subseteq \aleph \left({y}\right)\right)$
32 31 onnminsb ${⊢}{y}\in \mathrm{On}\to \left({y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\to ¬{A}\subseteq \aleph \left({y}\right)\right)$
33 vex ${⊢}{y}\in \mathrm{V}$
34 33 sucid ${⊢}{y}\in \mathrm{suc}{y}$
35 eleq2 ${⊢}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\to \left({y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}↔{y}\in \mathrm{suc}{y}\right)$
36 34 35 mpbiri ${⊢}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\to {y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}$
37 32 36 impel ${⊢}\left({y}\in \mathrm{On}\wedge \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\right)\to ¬{A}\subseteq \aleph \left({y}\right)$
38 37 adantl ${⊢}\left(\mathrm{card}\left({A}\right)={A}\wedge \left({y}\in \mathrm{On}\wedge \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\right)\right)\to ¬{A}\subseteq \aleph \left({y}\right)$
39 fveq2 ${⊢}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\to \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)=\aleph \left(\mathrm{suc}{y}\right)$
40 alephsuc ${⊢}{y}\in \mathrm{On}\to \aleph \left(\mathrm{suc}{y}\right)=\mathrm{har}\left(\aleph \left({y}\right)\right)$
41 39 40 sylan9eqr ${⊢}\left({y}\in \mathrm{On}\wedge \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\right)\to \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)=\mathrm{har}\left(\aleph \left({y}\right)\right)$
42 41 eleq2d ${⊢}\left({y}\in \mathrm{On}\wedge \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\right)\to \left({A}\in \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)↔{A}\in \mathrm{har}\left(\aleph \left({y}\right)\right)\right)$
43 42 biimpd ${⊢}\left({y}\in \mathrm{On}\wedge \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\right)\to \left({A}\in \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to {A}\in \mathrm{har}\left(\aleph \left({y}\right)\right)\right)$
44 elharval ${⊢}{A}\in \mathrm{har}\left(\aleph \left({y}\right)\right)↔\left({A}\in \mathrm{On}\wedge {A}\preccurlyeq \aleph \left({y}\right)\right)$
45 44 simprbi ${⊢}{A}\in \mathrm{har}\left(\aleph \left({y}\right)\right)\to {A}\preccurlyeq \aleph \left({y}\right)$
46 onenon ${⊢}{A}\in \mathrm{On}\to {A}\in \mathrm{dom}\mathrm{card}$
47 3 46 syl ${⊢}\mathrm{card}\left({A}\right)={A}\to {A}\in \mathrm{dom}\mathrm{card}$
48 alephon ${⊢}\aleph \left({y}\right)\in \mathrm{On}$
49 onenon ${⊢}\aleph \left({y}\right)\in \mathrm{On}\to \aleph \left({y}\right)\in \mathrm{dom}\mathrm{card}$
50 48 49 ax-mp ${⊢}\aleph \left({y}\right)\in \mathrm{dom}\mathrm{card}$
51 carddom2 ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \aleph \left({y}\right)\in \mathrm{dom}\mathrm{card}\right)\to \left(\mathrm{card}\left({A}\right)\subseteq \mathrm{card}\left(\aleph \left({y}\right)\right)↔{A}\preccurlyeq \aleph \left({y}\right)\right)$
52 47 50 51 sylancl ${⊢}\mathrm{card}\left({A}\right)={A}\to \left(\mathrm{card}\left({A}\right)\subseteq \mathrm{card}\left(\aleph \left({y}\right)\right)↔{A}\preccurlyeq \aleph \left({y}\right)\right)$
53 sseq1 ${⊢}\mathrm{card}\left({A}\right)={A}\to \left(\mathrm{card}\left({A}\right)\subseteq \mathrm{card}\left(\aleph \left({y}\right)\right)↔{A}\subseteq \mathrm{card}\left(\aleph \left({y}\right)\right)\right)$
54 alephcard ${⊢}\mathrm{card}\left(\aleph \left({y}\right)\right)=\aleph \left({y}\right)$
55 54 sseq2i ${⊢}{A}\subseteq \mathrm{card}\left(\aleph \left({y}\right)\right)↔{A}\subseteq \aleph \left({y}\right)$
56 53 55 syl6bb ${⊢}\mathrm{card}\left({A}\right)={A}\to \left(\mathrm{card}\left({A}\right)\subseteq \mathrm{card}\left(\aleph \left({y}\right)\right)↔{A}\subseteq \aleph \left({y}\right)\right)$
57 52 56 bitr3d ${⊢}\mathrm{card}\left({A}\right)={A}\to \left({A}\preccurlyeq \aleph \left({y}\right)↔{A}\subseteq \aleph \left({y}\right)\right)$
58 45 57 syl5ib ${⊢}\mathrm{card}\left({A}\right)={A}\to \left({A}\in \mathrm{har}\left(\aleph \left({y}\right)\right)\to {A}\subseteq \aleph \left({y}\right)\right)$
59 43 58 sylan9r ${⊢}\left(\mathrm{card}\left({A}\right)={A}\wedge \left({y}\in \mathrm{On}\wedge \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\right)\right)\to \left({A}\in \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to {A}\subseteq \aleph \left({y}\right)\right)$
60 38 59 mtod ${⊢}\left(\mathrm{card}\left({A}\right)={A}\wedge \left({y}\in \mathrm{On}\wedge \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\right)\right)\to ¬{A}\in \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)$
61 60 rexlimdvaa ${⊢}\mathrm{card}\left({A}\right)={A}\to \left(\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\to ¬{A}\in \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
62 onintrab2 ${⊢}\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{A}\subseteq \aleph \left({x}\right)↔\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\in \mathrm{On}$
63 8 62 sylib ${⊢}{A}\in \mathrm{On}\to \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\in \mathrm{On}$
64 onelon ${⊢}\left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\in \mathrm{On}\wedge {y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to {y}\in \mathrm{On}$
65 63 64 sylan ${⊢}\left({A}\in \mathrm{On}\wedge {y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to {y}\in \mathrm{On}$
66 32 adantld ${⊢}{y}\in \mathrm{On}\to \left(\left({A}\in \mathrm{On}\wedge {y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to ¬{A}\subseteq \aleph \left({y}\right)\right)$
67 65 66 mpcom ${⊢}\left({A}\in \mathrm{On}\wedge {y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to ¬{A}\subseteq \aleph \left({y}\right)$
68 48 onelssi ${⊢}{A}\in \aleph \left({y}\right)\to {A}\subseteq \aleph \left({y}\right)$
69 67 68 nsyl ${⊢}\left({A}\in \mathrm{On}\wedge {y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to ¬{A}\in \aleph \left({y}\right)$
70 69 nrexdv ${⊢}{A}\in \mathrm{On}\to ¬\exists {y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\phantom{\rule{.4em}{0ex}}{A}\in \aleph \left({y}\right)$
71 70 adantr ${⊢}\left({A}\in \mathrm{On}\wedge \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to ¬\exists {y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\phantom{\rule{.4em}{0ex}}{A}\in \aleph \left({y}\right)$
72 alephlim ${⊢}\left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\in \mathrm{On}\wedge \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)=\bigcup _{{y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}}\aleph \left({y}\right)$
73 63 72 sylan ${⊢}\left({A}\in \mathrm{On}\wedge \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)=\bigcup _{{y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}}\aleph \left({y}\right)$
74 73 eleq2d ${⊢}\left({A}\in \mathrm{On}\wedge \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to \left({A}\in \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)↔{A}\in \bigcup _{{y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}}\aleph \left({y}\right)\right)$
75 eliun ${⊢}{A}\in \bigcup _{{y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}}\aleph \left({y}\right)↔\exists {y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\phantom{\rule{.4em}{0ex}}{A}\in \aleph \left({y}\right)$
76 74 75 syl6bb ${⊢}\left({A}\in \mathrm{On}\wedge \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to \left({A}\in \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)↔\exists {y}\in \bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\phantom{\rule{.4em}{0ex}}{A}\in \aleph \left({y}\right)\right)$
77 71 76 mtbird ${⊢}\left({A}\in \mathrm{On}\wedge \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to ¬{A}\in \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)$
78 77 ex ${⊢}{A}\in \mathrm{On}\to \left(\mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\to ¬{A}\in \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
79 3 78 syl ${⊢}\mathrm{card}\left({A}\right)={A}\to \left(\mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\to ¬{A}\in \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
80 61 79 jaod ${⊢}\mathrm{card}\left({A}\right)={A}\to \left(\left(\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\vee \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to ¬{A}\in \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
81 8 17 syl ${⊢}{A}\in \mathrm{On}\to {A}\subseteq \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)$
82 alephon ${⊢}\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\in \mathrm{On}$
83 onsseleq ${⊢}\left({A}\in \mathrm{On}\wedge \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\in \mathrm{On}\right)\to \left({A}\subseteq \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)↔\left({A}\in \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\vee {A}=\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)\right)$
84 82 83 mpan2 ${⊢}{A}\in \mathrm{On}\to \left({A}\subseteq \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)↔\left({A}\in \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\vee {A}=\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)\right)$
85 81 84 mpbid ${⊢}{A}\in \mathrm{On}\to \left({A}\in \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\vee {A}=\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
86 85 ord ${⊢}{A}\in \mathrm{On}\to \left(¬{A}\in \aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to {A}=\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
87 3 80 86 sylsyld ${⊢}\mathrm{card}\left({A}\right)={A}\to \left(\left(\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\vee \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to {A}=\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
88 87 adantl ${⊢}\left(\mathrm{\omega }\subseteq {A}\wedge \mathrm{card}\left({A}\right)={A}\right)\to \left(\left(\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\vee \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\to {A}=\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
89 eloni ${⊢}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\in \mathrm{On}\to \mathrm{Ord}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}$
90 ordzsl ${⊢}\mathrm{Ord}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}↔\left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \vee \exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\vee \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)$
91 3orass ${⊢}\left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \vee \exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\vee \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)↔\left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \vee \left(\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\vee \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
92 90 91 bitri ${⊢}\mathrm{Ord}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}↔\left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \vee \left(\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\vee \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
93 89 92 sylib ${⊢}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\in \mathrm{On}\to \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \vee \left(\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\vee \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
94 3 63 93 3syl ${⊢}\mathrm{card}\left({A}\right)={A}\to \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \vee \left(\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\vee \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
95 94 adantl ${⊢}\left(\mathrm{\omega }\subseteq {A}\wedge \mathrm{card}\left({A}\right)={A}\right)\to \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\varnothing \vee \left(\exists {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}=\mathrm{suc}{y}\vee \mathrm{Lim}\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)\right)$
96 29 88 95 mpjaod ${⊢}\left(\mathrm{\omega }\subseteq {A}\wedge \mathrm{card}\left({A}\right)={A}\right)\to {A}=\aleph \left(\bigcap \left\{{x}\in \mathrm{On}|{A}\subseteq \aleph \left({x}\right)\right\}\right)$