Metamath Proof Explorer

Theorem nummin

Description: Every nonempty class of numerable sets has a minimal element. (Contributed by BTernaryTau, 18-Jul-2024)

Ref Expression
Assertion nummin 
|- ( ( A C_ dom card /\ A =/= (/) ) -> E. x e. A Pred ( ~< , A , x ) = (/) )

Proof

Step Hyp Ref Expression
1 cardf2 
 |-  card : { z | E. y e. On y ~~ z } --> On
2 ffun 
 |-  ( card : { z | E. y e. On y ~~ z } --> On -> Fun card )
3 2 funfnd 
 |-  ( card : { z | E. y e. On y ~~ z } --> On -> card Fn dom card )
4 1 3 ax-mp 
 |-  card Fn dom card
5 fnimaeq0 
 |-  ( ( card Fn dom card /\ A C_ dom card ) -> ( ( card " A ) = (/) <-> A = (/) ) )
6 4 5 mpan 
 |-  ( A C_ dom card -> ( ( card " A ) = (/) <-> A = (/) ) )
7 6 necon3bid 
 |-  ( A C_ dom card -> ( ( card " A ) =/= (/) <-> A =/= (/) ) )
8 7 biimprd 
 |-  ( A C_ dom card -> ( A =/= (/) -> ( card " A ) =/= (/) ) )
9 8 imdistani 
 |-  ( ( A C_ dom card /\ A =/= (/) ) -> ( A C_ dom card /\ ( card " A ) =/= (/) ) )
10 fimass 
 |-  ( card : { z | E. y e. On y ~~ z } --> On -> ( card " A ) C_ On )
11 1 10 ax-mp 
 |-  ( card " A ) C_ On
12 onssmin 
 |-  ( ( ( card " A ) C_ On /\ ( card " A ) =/= (/) ) -> E. z e. ( card " A ) A. y e. ( card " A ) z C_ y )
13 11 12 mpan 
 |-  ( ( card " A ) =/= (/) -> E. z e. ( card " A ) A. y e. ( card " A ) z C_ y )
14 ssel 
 |-  ( ( card " A ) C_ On -> ( z e. ( card " A ) -> z e. On ) )
15 ssel 
 |-  ( ( card " A ) C_ On -> ( y e. ( card " A ) -> y e. On ) )
16 14 15 anim12d 
 |-  ( ( card " A ) C_ On -> ( ( z e. ( card " A ) /\ y e. ( card " A ) ) -> ( z e. On /\ y e. On ) ) )
17 11 16 ax-mp 
 |-  ( ( z e. ( card " A ) /\ y e. ( card " A ) ) -> ( z e. On /\ y e. On ) )
18 ontri1 
 |-  ( ( z e. On /\ y e. On ) -> ( z C_ y <-> -. y e. z ) )
19 17 18 syl 
 |-  ( ( z e. ( card " A ) /\ y e. ( card " A ) ) -> ( z C_ y <-> -. y e. z ) )
20 epel 
 |-  ( y _E z <-> y e. z )
21 20 notbii 
 |-  ( -. y _E z <-> -. y e. z )
22 19 21 bitr4di 
 |-  ( ( z e. ( card " A ) /\ y e. ( card " A ) ) -> ( z C_ y <-> -. y _E z ) )
23 22 rgen2 
 |-  A. z e. ( card " A ) A. y e. ( card " A ) ( z C_ y <-> -. y _E z )
24 r19.29r 
 |-  ( ( E. z e. ( card " A ) A. y e. ( card " A ) z C_ y /\ A. z e. ( card " A ) A. y e. ( card " A ) ( z C_ y <-> -. y _E z ) ) -> E. z e. ( card " A ) ( A. y e. ( card " A ) z C_ y /\ A. y e. ( card " A ) ( z C_ y <-> -. y _E z ) ) )
25 13 23 24 sylancl 
 |-  ( ( card " A ) =/= (/) -> E. z e. ( card " A ) ( A. y e. ( card " A ) z C_ y /\ A. y e. ( card " A ) ( z C_ y <-> -. y _E z ) ) )
26 r19.26 
 |-  ( A. y e. ( card " A ) ( z C_ y /\ ( z C_ y <-> -. y _E z ) ) <-> ( A. y e. ( card " A ) z C_ y /\ A. y e. ( card " A ) ( z C_ y <-> -. y _E z ) ) )
27 bicom1 
 |-  ( ( z C_ y <-> -. y _E z ) -> ( -. y _E z <-> z C_ y ) )
28 27 biimparc 
 |-  ( ( z C_ y /\ ( z C_ y <-> -. y _E z ) ) -> -. y _E z )
29 28 ralimi 
 |-  ( A. y e. ( card " A ) ( z C_ y /\ ( z C_ y <-> -. y _E z ) ) -> A. y e. ( card " A ) -. y _E z )
30 26 29 sylbir 
 |-  ( ( A. y e. ( card " A ) z C_ y /\ A. y e. ( card " A ) ( z C_ y <-> -. y _E z ) ) -> A. y e. ( card " A ) -. y _E z )
31 30 reximi 
 |-  ( E. z e. ( card " A ) ( A. y e. ( card " A ) z C_ y /\ A. y e. ( card " A ) ( z C_ y <-> -. y _E z ) ) -> E. z e. ( card " A ) A. y e. ( card " A ) -. y _E z )
32 25 31 syl 
 |-  ( ( card " A ) =/= (/) -> E. z e. ( card " A ) A. y e. ( card " A ) -. y _E z )
33 32 adantl 
 |-  ( ( A C_ dom card /\ ( card " A ) =/= (/) ) -> E. z e. ( card " A ) A. y e. ( card " A ) -. y _E z )
34 breq2 
 |-  ( z = ( card ` x ) -> ( y _E z <-> y _E ( card ` x ) ) )
35 34 notbid 
 |-  ( z = ( card ` x ) -> ( -. y _E z <-> -. y _E ( card ` x ) ) )
36 35 ralbidv 
 |-  ( z = ( card ` x ) -> ( A. y e. ( card " A ) -. y _E z <-> A. y e. ( card " A ) -. y _E ( card ` x ) ) )
37 36 rexima 
 |-  ( ( card Fn dom card /\ A C_ dom card ) -> ( E. z e. ( card " A ) A. y e. ( card " A ) -. y _E z <-> E. x e. A A. y e. ( card " A ) -. y _E ( card ` x ) ) )
38 4 37 mpan 
 |-  ( A C_ dom card -> ( E. z e. ( card " A ) A. y e. ( card " A ) -. y _E z <-> E. x e. A A. y e. ( card " A ) -. y _E ( card ` x ) ) )
39 38 adantr 
 |-  ( ( A C_ dom card /\ ( card " A ) =/= (/) ) -> ( E. z e. ( card " A ) A. y e. ( card " A ) -. y _E z <-> E. x e. A A. y e. ( card " A ) -. y _E ( card ` x ) ) )
40 33 39 mpbid 
 |-  ( ( A C_ dom card /\ ( card " A ) =/= (/) ) -> E. x e. A A. y e. ( card " A ) -. y _E ( card ` x ) )
41 fvex 
 |-  ( card ` x ) e. _V
42 41 dfpred3 
 |-  Pred ( _E , ( card " A ) , ( card ` x ) ) = { y e. ( card " A ) | y _E ( card ` x ) }
43 42 eqeq1i 
 |-  ( Pred ( _E , ( card " A ) , ( card ` x ) ) = (/) <-> { y e. ( card " A ) | y _E ( card ` x ) } = (/) )
44 rabeq0 
 |-  ( { y e. ( card " A ) | y _E ( card ` x ) } = (/) <-> A. y e. ( card " A ) -. y _E ( card ` x ) )
45 43 44 bitri 
 |-  ( Pred ( _E , ( card " A ) , ( card ` x ) ) = (/) <-> A. y e. ( card " A ) -. y _E ( card ` x ) )
46 45 rexbii 
 |-  ( E. x e. A Pred ( _E , ( card " A ) , ( card ` x ) ) = (/) <-> E. x e. A A. y e. ( card " A ) -. y _E ( card ` x ) )
47 40 46 sylibr 
 |-  ( ( A C_ dom card /\ ( card " A ) =/= (/) ) -> E. x e. A Pred ( _E , ( card " A ) , ( card ` x ) ) = (/) )
48 9 47 syl 
 |-  ( ( A C_ dom card /\ A =/= (/) ) -> E. x e. A Pred ( _E , ( card " A ) , ( card ` x ) ) = (/) )
49 ssel2 
 |-  ( ( A C_ dom card /\ x e. A ) -> x e. dom card )
50 cardpred 
 |-  ( ( A C_ dom card /\ x e. dom card ) -> Pred ( _E , ( card " A ) , ( card ` x ) ) = ( card " Pred ( ~< , A , x ) ) )
51 50 eqeq1d 
 |-  ( ( A C_ dom card /\ x e. dom card ) -> ( Pred ( _E , ( card " A ) , ( card ` x ) ) = (/) <-> ( card " Pred ( ~< , A , x ) ) = (/) ) )
52 predss 
 |-  Pred ( ~< , A , x ) C_ A
53 sstr 
 |-  ( ( Pred ( ~< , A , x ) C_ A /\ A C_ dom card ) -> Pred ( ~< , A , x ) C_ dom card )
54 52 53 mpan 
 |-  ( A C_ dom card -> Pred ( ~< , A , x ) C_ dom card )
55 fnimaeq0 
 |-  ( ( card Fn dom card /\ Pred ( ~< , A , x ) C_ dom card ) -> ( ( card " Pred ( ~< , A , x ) ) = (/) <-> Pred ( ~< , A , x ) = (/) ) )
56 4 54 55 sylancr 
 |-  ( A C_ dom card -> ( ( card " Pred ( ~< , A , x ) ) = (/) <-> Pred ( ~< , A , x ) = (/) ) )
57 56 adantr 
 |-  ( ( A C_ dom card /\ x e. dom card ) -> ( ( card " Pred ( ~< , A , x ) ) = (/) <-> Pred ( ~< , A , x ) = (/) ) )
58 51 57 bitrd 
 |-  ( ( A C_ dom card /\ x e. dom card ) -> ( Pred ( _E , ( card " A ) , ( card ` x ) ) = (/) <-> Pred ( ~< , A , x ) = (/) ) )
59 49 58 syldan 
 |-  ( ( A C_ dom card /\ x e. A ) -> ( Pred ( _E , ( card " A ) , ( card ` x ) ) = (/) <-> Pred ( ~< , A , x ) = (/) ) )
60 59 rexbidva 
 |-  ( A C_ dom card -> ( E. x e. A Pred ( _E , ( card " A ) , ( card ` x ) ) = (/) <-> E. x e. A Pred ( ~< , A , x ) = (/) ) )
61 60 adantr 
 |-  ( ( A C_ dom card /\ A =/= (/) ) -> ( E. x e. A Pred ( _E , ( card " A ) , ( card ` x ) ) = (/) <-> E. x e. A Pred ( ~< , A , x ) = (/) ) )
62 48 61 mpbid 
 |-  ( ( A C_ dom card /\ A =/= (/) ) -> E. x e. A Pred ( ~< , A , x ) = (/) )