Metamath Proof Explorer

Theorem cardmin2

Description: The smallest ordinal that strictly dominates a set is a cardinal, if it exists. (Contributed by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion cardmin2 
|- ( E. x e. On A ~< x <-> ( card ` |^| { x e. On | A ~< x } ) = |^| { x e. On | A ~< x } )

Proof

Step Hyp Ref Expression
1 onintrab2 
 |-  ( E. x e. On A ~< x <-> |^| { x e. On | A ~< x } e. On )
2 1 biimpi 
 |-  ( E. x e. On A ~< x -> |^| { x e. On | A ~< x } e. On )
3 2 adantr 
 |-  ( ( E. x e. On A ~< x /\ y e. |^| { x e. On | A ~< x } ) -> |^| { x e. On | A ~< x } e. On )
4 eloni 
 |-  ( |^| { x e. On | A ~< x } e. On -> Ord |^| { x e. On | A ~< x } )
5 ordelss 
 |-  ( ( Ord |^| { x e. On | A ~< x } /\ y e. |^| { x e. On | A ~< x } ) -> y C_ |^| { x e. On | A ~< x } )
6 4 5 sylan 
 |-  ( ( |^| { x e. On | A ~< x } e. On /\ y e. |^| { x e. On | A ~< x } ) -> y C_ |^| { x e. On | A ~< x } )
7 1 6 sylanb 
 |-  ( ( E. x e. On A ~< x /\ y e. |^| { x e. On | A ~< x } ) -> y C_ |^| { x e. On | A ~< x } )
8 ssdomg 
 |-  ( |^| { x e. On | A ~< x } e. On -> ( y C_ |^| { x e. On | A ~< x } -> y ~<_ |^| { x e. On | A ~< x } ) )
9 3 7 8 sylc 
 |-  ( ( E. x e. On A ~< x /\ y e. |^| { x e. On | A ~< x } ) -> y ~<_ |^| { x e. On | A ~< x } )
10 onelon 
 |-  ( ( |^| { x e. On | A ~< x } e. On /\ y e. |^| { x e. On | A ~< x } ) -> y e. On )
11 1 10 sylanb 
 |-  ( ( E. x e. On A ~< x /\ y e. |^| { x e. On | A ~< x } ) -> y e. On )
12 nfcv 
 |-  F/_ x A
13 nfcv 
 |-  F/_ x ~<
14 nfrab1 
 |-  F/_ x { x e. On | A ~< x }
15 14 nfint 
 |-  F/_ x |^| { x e. On | A ~< x }
16 12 13 15 nfbr 
 |-  F/ x A ~< |^| { x e. On | A ~< x }
17 breq2 
 |-  ( x = |^| { x e. On | A ~< x } -> ( A ~< x <-> A ~< |^| { x e. On | A ~< x } ) )
18 16 17 onminsb 
 |-  ( E. x e. On A ~< x -> A ~< |^| { x e. On | A ~< x } )
19 sdomentr 
 |-  ( ( A ~< |^| { x e. On | A ~< x } /\ |^| { x e. On | A ~< x } ~~ y ) -> A ~< y )
20 18 19 sylan 
 |-  ( ( E. x e. On A ~< x /\ |^| { x e. On | A ~< x } ~~ y ) -> A ~< y )
21 breq2 
 |-  ( x = y -> ( A ~< x <-> A ~< y ) )
22 21 elrab 
 |-  ( y e. { x e. On | A ~< x } <-> ( y e. On /\ A ~< y ) )
23 ssrab2 
 |-  { x e. On | A ~< x } C_ On
24 onnmin 
 |-  ( ( { x e. On | A ~< x } C_ On /\ y e. { x e. On | A ~< x } ) -> -. y e. |^| { x e. On | A ~< x } )
25 23 24 mpan 
 |-  ( y e. { x e. On | A ~< x } -> -. y e. |^| { x e. On | A ~< x } )
26 22 25 sylbir 
 |-  ( ( y e. On /\ A ~< y ) -> -. y e. |^| { x e. On | A ~< x } )
27 26 expcom 
 |-  ( A ~< y -> ( y e. On -> -. y e. |^| { x e. On | A ~< x } ) )
28 20 27 syl 
 |-  ( ( E. x e. On A ~< x /\ |^| { x e. On | A ~< x } ~~ y ) -> ( y e. On -> -. y e. |^| { x e. On | A ~< x } ) )
29 28 impancom 
 |-  ( ( E. x e. On A ~< x /\ y e. On ) -> ( |^| { x e. On | A ~< x } ~~ y -> -. y e. |^| { x e. On | A ~< x } ) )
30 29 con2d 
 |-  ( ( E. x e. On A ~< x /\ y e. On ) -> ( y e. |^| { x e. On | A ~< x } -> -. |^| { x e. On | A ~< x } ~~ y ) )
31 30 impancom 
 |-  ( ( E. x e. On A ~< x /\ y e. |^| { x e. On | A ~< x } ) -> ( y e. On -> -. |^| { x e. On | A ~< x } ~~ y ) )
32 11 31 mpd 
 |-  ( ( E. x e. On A ~< x /\ y e. |^| { x e. On | A ~< x } ) -> -. |^| { x e. On | A ~< x } ~~ y )
33 ensym 
 |-  ( y ~~ |^| { x e. On | A ~< x } -> |^| { x e. On | A ~< x } ~~ y )
34 32 33 nsyl 
 |-  ( ( E. x e. On A ~< x /\ y e. |^| { x e. On | A ~< x } ) -> -. y ~~ |^| { x e. On | A ~< x } )
35 brsdom 
 |-  ( y ~< |^| { x e. On | A ~< x } <-> ( y ~<_ |^| { x e. On | A ~< x } /\ -. y ~~ |^| { x e. On | A ~< x } ) )
36 9 34 35 sylanbrc 
 |-  ( ( E. x e. On A ~< x /\ y e. |^| { x e. On | A ~< x } ) -> y ~< |^| { x e. On | A ~< x } )
37 36 ralrimiva 
 |-  ( E. x e. On A ~< x -> A. y e. |^| { x e. On | A ~< x } y ~< |^| { x e. On | A ~< x } )
38 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 } ) )
39 2 37 38 sylanbrc 
 |-  ( E. x e. On A ~< x -> ( card ` |^| { x e. On | A ~< x } ) = |^| { x e. On | A ~< x } )
40 vprc 
 |-  -. _V e. _V
41 inteq 
 |-  ( { x e. On | A ~< x } = (/) -> |^| { x e. On | A ~< x } = |^| (/) )
42 int0 
 |-  |^| (/) = _V
43 41 42 eqtrdi 
 |-  ( { x e. On | A ~< x } = (/) -> |^| { x e. On | A ~< x } = _V )
44 43 eleq1d 
 |-  ( { x e. On | A ~< x } = (/) -> ( |^| { x e. On | A ~< x } e. _V <-> _V e. _V ) )
45 40 44 mtbiri 
 |-  ( { x e. On | A ~< x } = (/) -> -. |^| { x e. On | A ~< x } e. _V )
46 fvex 
 |-  ( card ` |^| { x e. On | A ~< x } ) e. _V
47 eleq1 
 |-  ( ( card ` |^| { x e. On | A ~< x } ) = |^| { x e. On | A ~< x } -> ( ( card ` |^| { x e. On | A ~< x } ) e. _V <-> |^| { x e. On | A ~< x } e. _V ) )
48 46 47 mpbii 
 |-  ( ( card ` |^| { x e. On | A ~< x } ) = |^| { x e. On | A ~< x } -> |^| { x e. On | A ~< x } e. _V )
49 45 48 nsyl 
 |-  ( { x e. On | A ~< x } = (/) -> -. ( card ` |^| { x e. On | A ~< x } ) = |^| { x e. On | A ~< x } )
50 49 necon2ai 
 |-  ( ( card ` |^| { x e. On | A ~< x } ) = |^| { x e. On | A ~< x } -> { x e. On | A ~< x } =/= (/) )
51 rabn0 
 |-  ( { x e. On | A ~< x } =/= (/) <-> E. x e. On A ~< x )
52 50 51 sylib 
 |-  ( ( card ` |^| { x e. On | A ~< x } ) = |^| { x e. On | A ~< x } -> E. x e. On A ~< x )
53 39 52 impbii 
 |-  ( E. x e. On A ~< x <-> ( card ` |^| { x e. On | A ~< x } ) = |^| { x e. On | A ~< x } )