Metamath Proof Explorer


Theorem cardmin

Description: The smallest ordinal that strictly dominates a set is a cardinal. (Contributed by NM, 28-Oct-2003) (Revised by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion cardmin AVcardxOn|Ax=xOn|Ax

Proof

Step Hyp Ref Expression
1 numthcor AVxOnAx
2 onintrab2 xOnAxxOn|AxOn
3 1 2 sylib AVxOn|AxOn
4 onelon xOn|AxOnyxOn|AxyOn
5 4 ex xOn|AxOnyxOn|AxyOn
6 3 5 syl AVyxOn|AxyOn
7 breq2 x=yAxAy
8 7 onnminsb yOnyxOn|Ax¬Ay
9 6 8 syli AVyxOn|Ax¬Ay
10 vex yV
11 domtri yVAVyA¬Ay
12 10 11 mpan AVyA¬Ay
13 9 12 sylibrd AVyxOn|AxyA
14 nfcv _xA
15 nfcv _x
16 nfrab1 _xxOn|Ax
17 16 nfint _xxOn|Ax
18 14 15 17 nfbr xAxOn|Ax
19 breq2 x=xOn|AxAxAxOn|Ax
20 18 19 onminsb xOnAxAxOn|Ax
21 1 20 syl AVAxOn|Ax
22 13 21 jctird AVyxOn|AxyAAxOn|Ax
23 domsdomtr yAAxOn|AxyxOn|Ax
24 22 23 syl6 AVyxOn|AxyxOn|Ax
25 24 ralrimiv AVyxOn|AxyxOn|Ax
26 iscard cardxOn|Ax=xOn|AxxOn|AxOnyxOn|AxyxOn|Ax
27 3 25 26 sylanbrc AVcardxOn|Ax=xOn|Ax