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 
|- ( A e. V -> ( card ` |^| { x e. On | A ~< x } ) = |^| { x e. On | A ~< x } )

Proof

Step Hyp Ref Expression
1 numthcor 
 |-  ( A e. V -> E. x e. On A ~< x )
2 onintrab2 
 |-  ( E. x e. On A ~< x <-> |^| { x e. On | A ~< x } e. On )
3 1 2 sylib 
 |-  ( A e. V -> |^| { x e. On | A ~< x } e. On )
4 onelon 
 |-  ( ( |^| { x e. On | A ~< x } e. On /\ y e. |^| { x e. On | A ~< x } ) -> y e. On )
5 4 ex 
 |-  ( |^| { x e. On | A ~< x } e. On -> ( y e. |^| { x e. On | A ~< x } -> y e. On ) )
6 3 5 syl 
 |-  ( A e. V -> ( y e. |^| { x e. On | A ~< x } -> y e. On ) )
7 breq2 
 |-  ( x = y -> ( A ~< x <-> A ~< y ) )
8 7 onnminsb 
 |-  ( y e. On -> ( y e. |^| { x e. On | A ~< x } -> -. A ~< y ) )
9 6 8 syli 
 |-  ( A e. V -> ( y e. |^| { x e. On | A ~< x } -> -. A ~< y ) )
10 vex 
 |-  y e. _V
11 domtri 
 |-  ( ( y e. _V /\ A e. V ) -> ( y ~<_ A <-> -. A ~< y ) )
12 10 11 mpan 
 |-  ( A e. V -> ( y ~<_ A <-> -. A ~< y ) )
13 9 12 sylibrd 
 |-  ( A e. V -> ( y e. |^| { x e. On | A ~< x } -> y ~<_ A ) )
14 nfcv 
 |-  F/_ x A
15 nfcv 
 |-  F/_ x ~<
16 nfrab1 
 |-  F/_ x { x e. On | A ~< x }
17 16 nfint 
 |-  F/_ x |^| { x e. On | A ~< x }
18 14 15 17 nfbr 
 |-  F/ x A ~< |^| { x e. On | A ~< x }
19 breq2 
 |-  ( x = |^| { x e. On | A ~< x } -> ( A ~< x <-> A ~< |^| { x e. On | A ~< x } ) )
20 18 19 onminsb 
 |-  ( E. x e. On A ~< x -> A ~< |^| { x e. On | A ~< x } )
21 1 20 syl 
 |-  ( A e. V -> A ~< |^| { x e. On | A ~< x } )
22 13 21 jctird 
 |-  ( A e. V -> ( y e. |^| { x e. On | A ~< x } -> ( y ~<_ A /\ A ~< |^| { x e. On | A ~< x } ) ) )
23 domsdomtr 
 |-  ( ( y ~<_ A /\ A ~< |^| { x e. On | A ~< x } ) -> y ~< |^| { x e. On | A ~< x } )
24 22 23 syl6 
 |-  ( A e. V -> ( y e. |^| { x e. On | A ~< x } -> y ~< |^| { x e. On | A ~< x } ) )
25 24 ralrimiv 
 |-  ( A e. V -> A. y e. |^| { x e. On | A ~< x } y ~< |^| { x e. On | A ~< x } )
26 iscard 
 |-  ( ( card ` |^| { x e. On | A ~< x } ) = |^| { x e. On | A ~< x } <-> ( |^| { x e. On | A ~< x } e. On /\ A. y e. |^| { x e. On | A ~< x } y ~< |^| { x e. On | A ~< x } ) )
27 3 25 26 sylanbrc 
 |-  ( A e. V -> ( card ` |^| { x e. On | A ~< x } ) = |^| { x e. On | A ~< x } )