Metamath Proof Explorer

Theorem finminlem

Description: A useful lemma about finite sets. If a property holds for a finite set, it holds for a minimal set. (Contributed by Jeff Hankins, 4-Dec-2009)

Ref Expression
Hypothesis finminlem.1 
|- ( x = y -> ( ph <-> ps ) )
Assertion finminlem 
|- ( E. x e. Fin ph -> E. x ( ph /\ A. y ( ( y C_ x /\ ps ) -> x = y ) ) )

Proof

Step Hyp Ref Expression
1 finminlem.1 
 |-  ( x = y -> ( ph <-> ps ) )
2 nfe1 
 |-  F/ x E. x ( x ~~ n /\ ph )
3 nfcv 
 |-  F/_ x _om
4 2 3 nfrabw 
 |-  F/_ x { n e. _om | E. x ( x ~~ n /\ ph ) }
5 nfcv 
 |-  F/_ x (/)
6 4 5 nfne 
 |-  F/ x { n e. _om | E. x ( x ~~ n /\ ph ) } =/= (/)
7 isfi 
 |-  ( x e. Fin <-> E. m e. _om x ~~ m )
8 19.8a 
 |-  ( ( x ~~ m /\ ph ) -> E. x ( x ~~ m /\ ph ) )
9 8 anim2i 
 |-  ( ( m e. _om /\ ( x ~~ m /\ ph ) ) -> ( m e. _om /\ E. x ( x ~~ m /\ ph ) ) )
10 9 3impb 
 |-  ( ( m e. _om /\ x ~~ m /\ ph ) -> ( m e. _om /\ E. x ( x ~~ m /\ ph ) ) )
11 breq2 
 |-  ( n = m -> ( x ~~ n <-> x ~~ m ) )
12 11 anbi1d 
 |-  ( n = m -> ( ( x ~~ n /\ ph ) <-> ( x ~~ m /\ ph ) ) )
13 12 exbidv 
 |-  ( n = m -> ( E. x ( x ~~ n /\ ph ) <-> E. x ( x ~~ m /\ ph ) ) )
14 13 elrab 
 |-  ( m e. { n e. _om | E. x ( x ~~ n /\ ph ) } <-> ( m e. _om /\ E. x ( x ~~ m /\ ph ) ) )
15 10 14 sylibr 
 |-  ( ( m e. _om /\ x ~~ m /\ ph ) -> m e. { n e. _om | E. x ( x ~~ n /\ ph ) } )
16 15 ne0d 
 |-  ( ( m e. _om /\ x ~~ m /\ ph ) -> { n e. _om | E. x ( x ~~ n /\ ph ) } =/= (/) )
17 16 3exp 
 |-  ( m e. _om -> ( x ~~ m -> ( ph -> { n e. _om | E. x ( x ~~ n /\ ph ) } =/= (/) ) ) )
18 17 rexlimiv 
 |-  ( E. m e. _om x ~~ m -> ( ph -> { n e. _om | E. x ( x ~~ n /\ ph ) } =/= (/) ) )
19 7 18 sylbi 
 |-  ( x e. Fin -> ( ph -> { n e. _om | E. x ( x ~~ n /\ ph ) } =/= (/) ) )
20 6 19 rexlimi 
 |-  ( E. x e. Fin ph -> { n e. _om | E. x ( x ~~ n /\ ph ) } =/= (/) )
21 epweon 
 |-  _E We On
22 ssrab2 
 |-  { n e. _om | E. x ( x ~~ n /\ ph ) } C_ _om
23 omsson 
 |-  _om C_ On
24 22 23 sstri 
 |-  { n e. _om | E. x ( x ~~ n /\ ph ) } C_ On
25 wefrc 
 |-  ( ( _E We On /\ { n e. _om | E. x ( x ~~ n /\ ph ) } C_ On /\ { n e. _om | E. x ( x ~~ n /\ ph ) } =/= (/) ) -> E. m e. { n e. _om | E. x ( x ~~ n /\ ph ) } ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) )
26 21 24 25 mp3an12 
 |-  ( { n e. _om | E. x ( x ~~ n /\ ph ) } =/= (/) -> E. m e. { n e. _om | E. x ( x ~~ n /\ ph ) } ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) )
27 nfv 
 |-  F/ x m e. _om
28 nfcv 
 |-  F/_ x m
29 4 28 nfin 
 |-  F/_ x ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m )
30 29 nfeq1 
 |-  F/ x ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/)
31 27 30 nfan 
 |-  F/ x ( m e. _om /\ ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) )
32 simprr 
 |-  ( ( ( m e. _om /\ ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) ) /\ ( x ~~ m /\ ph ) ) -> ph )
33 sspss 
 |-  ( y C_ x <-> ( y C. x \/ y = x ) )
34 rspe 
 |-  ( ( m e. _om /\ x ~~ m ) -> E. m e. _om x ~~ m )
35 pssss 
 |-  ( y C. x -> y C_ x )
36 ssfi 
 |-  ( ( x e. Fin /\ y C_ x ) -> y e. Fin )
37 35 36 sylan2 
 |-  ( ( x e. Fin /\ y C. x ) -> y e. Fin )
38 37 ex 
 |-  ( x e. Fin -> ( y C. x -> y e. Fin ) )
39 7 38 sylbir 
 |-  ( E. m e. _om x ~~ m -> ( y C. x -> y e. Fin ) )
40 34 39 syl 
 |-  ( ( m e. _om /\ x ~~ m ) -> ( y C. x -> y e. Fin ) )
41 40 adantrr 
 |-  ( ( m e. _om /\ ( x ~~ m /\ ph ) ) -> ( y C. x -> y e. Fin ) )
42 41 adantrr 
 |-  ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) -> ( y C. x -> y e. Fin ) )
43 isfi 
 |-  ( y e. Fin <-> E. k e. _om y ~~ k )
44 simprll 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( ( k e. _om /\ y ~~ k ) /\ y C. x ) ) -> k e. _om )
45 simprlr 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( ( k e. _om /\ y ~~ k ) /\ y C. x ) ) -> y ~~ k )
46 simplrr 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( ( k e. _om /\ y ~~ k ) /\ y C. x ) ) -> ps )
47 vex 
 |-  y e. _V
48 breq1 
 |-  ( x = y -> ( x ~~ k <-> y ~~ k ) )
49 48 1 anbi12d 
 |-  ( x = y -> ( ( x ~~ k /\ ph ) <-> ( y ~~ k /\ ps ) ) )
50 47 49 spcev 
 |-  ( ( y ~~ k /\ ps ) -> E. x ( x ~~ k /\ ph ) )
51 45 46 50 syl2anc 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( ( k e. _om /\ y ~~ k ) /\ y C. x ) ) -> E. x ( x ~~ k /\ ph ) )
52 34 7 sylibr 
 |-  ( ( m e. _om /\ x ~~ m ) -> x e. Fin )
53 52 adantrr 
 |-  ( ( m e. _om /\ ( x ~~ m /\ ph ) ) -> x e. Fin )
54 53 adantrr 
 |-  ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) -> x e. Fin )
55 54 adantr 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( k e. _om /\ y ~~ k ) ) -> x e. Fin )
56 php3 
 |-  ( ( x e. Fin /\ y C. x ) -> y ~< x )
57 56 ex 
 |-  ( x e. Fin -> ( y C. x -> y ~< x ) )
58 55 57 syl 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( k e. _om /\ y ~~ k ) ) -> ( y C. x -> y ~< x ) )
59 vex 
 |-  k e. _V
60 ssdomg 
 |-  ( k e. _V -> ( m C_ k -> m ~<_ k ) )
61 59 60 ax-mp 
 |-  ( m C_ k -> m ~<_ k )
62 endomtr 
 |-  ( ( x ~~ m /\ m ~<_ k ) -> x ~<_ k )
63 62 ex 
 |-  ( x ~~ m -> ( m ~<_ k -> x ~<_ k ) )
64 63 ad2antrr 
 |-  ( ( ( x ~~ m /\ ph ) /\ ps ) -> ( m ~<_ k -> x ~<_ k ) )
65 64 ad2antlr 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( k e. _om /\ y ~~ k ) ) -> ( m ~<_ k -> x ~<_ k ) )
66 ensym 
 |-  ( y ~~ k -> k ~~ y )
67 domentr 
 |-  ( ( x ~<_ k /\ k ~~ y ) -> x ~<_ y )
68 66 67 sylan2 
 |-  ( ( x ~<_ k /\ y ~~ k ) -> x ~<_ y )
69 68 expcom 
 |-  ( y ~~ k -> ( x ~<_ k -> x ~<_ y ) )
70 69 ad2antll 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( k e. _om /\ y ~~ k ) ) -> ( x ~<_ k -> x ~<_ y ) )
71 65 70 syld 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( k e. _om /\ y ~~ k ) ) -> ( m ~<_ k -> x ~<_ y ) )
72 61 71 syl5 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( k e. _om /\ y ~~ k ) ) -> ( m C_ k -> x ~<_ y ) )
73 domnsym 
 |-  ( x ~<_ y -> -. y ~< x )
74 73 con2i 
 |-  ( y ~< x -> -. x ~<_ y )
75 72 74 nsyli 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( k e. _om /\ y ~~ k ) ) -> ( y ~< x -> -. m C_ k ) )
76 58 75 syld 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( k e. _om /\ y ~~ k ) ) -> ( y C. x -> -. m C_ k ) )
77 76 impr 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( ( k e. _om /\ y ~~ k ) /\ y C. x ) ) -> -. m C_ k )
78 nnord 
 |-  ( m e. _om -> Ord m )
79 78 ad2antrr 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( ( k e. _om /\ y ~~ k ) /\ y C. x ) ) -> Ord m )
80 nnord 
 |-  ( k e. _om -> Ord k )
81 80 adantr 
 |-  ( ( k e. _om /\ y ~~ k ) -> Ord k )
82 81 ad2antrl 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( ( k e. _om /\ y ~~ k ) /\ y C. x ) ) -> Ord k )
83 ordtri1 
 |-  ( ( Ord m /\ Ord k ) -> ( m C_ k <-> -. k e. m ) )
84 83 con2bid 
 |-  ( ( Ord m /\ Ord k ) -> ( k e. m <-> -. m C_ k ) )
85 79 82 84 syl2anc 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( ( k e. _om /\ y ~~ k ) /\ y C. x ) ) -> ( k e. m <-> -. m C_ k ) )
86 77 85 mpbird 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( ( k e. _om /\ y ~~ k ) /\ y C. x ) ) -> k e. m )
87 44 51 86 jca31 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( ( k e. _om /\ y ~~ k ) /\ y C. x ) ) -> ( ( k e. _om /\ E. x ( x ~~ k /\ ph ) ) /\ k e. m ) )
88 elin 
 |-  ( k e. ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) <-> ( k e. { n e. _om | E. x ( x ~~ n /\ ph ) } /\ k e. m ) )
89 breq2 
 |-  ( n = k -> ( x ~~ n <-> x ~~ k ) )
90 89 anbi1d 
 |-  ( n = k -> ( ( x ~~ n /\ ph ) <-> ( x ~~ k /\ ph ) ) )
91 90 exbidv 
 |-  ( n = k -> ( E. x ( x ~~ n /\ ph ) <-> E. x ( x ~~ k /\ ph ) ) )
92 91 elrab 
 |-  ( k e. { n e. _om | E. x ( x ~~ n /\ ph ) } <-> ( k e. _om /\ E. x ( x ~~ k /\ ph ) ) )
93 92 anbi1i 
 |-  ( ( k e. { n e. _om | E. x ( x ~~ n /\ ph ) } /\ k e. m ) <-> ( ( k e. _om /\ E. x ( x ~~ k /\ ph ) ) /\ k e. m ) )
94 88 93 bitri 
 |-  ( k e. ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) <-> ( ( k e. _om /\ E. x ( x ~~ k /\ ph ) ) /\ k e. m ) )
95 87 94 sylibr 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( ( k e. _om /\ y ~~ k ) /\ y C. x ) ) -> k e. ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) )
96 95 ne0d 
 |-  ( ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) /\ ( ( k e. _om /\ y ~~ k ) /\ y C. x ) ) -> ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) =/= (/) )
97 96 exp44 
 |-  ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) -> ( k e. _om -> ( y ~~ k -> ( y C. x -> ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) =/= (/) ) ) ) )
98 97 rexlimdv 
 |-  ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) -> ( E. k e. _om y ~~ k -> ( y C. x -> ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) =/= (/) ) ) )
99 43 98 syl5bi 
 |-  ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) -> ( y e. Fin -> ( y C. x -> ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) =/= (/) ) ) )
100 99 com23 
 |-  ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) -> ( y C. x -> ( y e. Fin -> ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) =/= (/) ) ) )
101 42 100 mpdd 
 |-  ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) -> ( y C. x -> ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) =/= (/) ) )
102 101 necon2bd 
 |-  ( ( m e. _om /\ ( ( x ~~ m /\ ph ) /\ ps ) ) -> ( ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) -> -. y C. x ) )
103 102 ex 
 |-  ( m e. _om -> ( ( ( x ~~ m /\ ph ) /\ ps ) -> ( ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) -> -. y C. x ) ) )
104 103 com23 
 |-  ( m e. _om -> ( ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) -> ( ( ( x ~~ m /\ ph ) /\ ps ) -> -. y C. x ) ) )
105 104 imp31 
 |-  ( ( ( m e. _om /\ ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) ) /\ ( ( x ~~ m /\ ph ) /\ ps ) ) -> -. y C. x )
106 105 pm2.21d 
 |-  ( ( ( m e. _om /\ ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) ) /\ ( ( x ~~ m /\ ph ) /\ ps ) ) -> ( y C. x -> x = y ) )
107 equcomi 
 |-  ( y = x -> x = y )
108 107 a1i 
 |-  ( ( ( m e. _om /\ ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) ) /\ ( ( x ~~ m /\ ph ) /\ ps ) ) -> ( y = x -> x = y ) )
109 106 108 jaod 
 |-  ( ( ( m e. _om /\ ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) ) /\ ( ( x ~~ m /\ ph ) /\ ps ) ) -> ( ( y C. x \/ y = x ) -> x = y ) )
110 33 109 syl5bi 
 |-  ( ( ( m e. _om /\ ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) ) /\ ( ( x ~~ m /\ ph ) /\ ps ) ) -> ( y C_ x -> x = y ) )
111 110 expr 
 |-  ( ( ( m e. _om /\ ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) ) /\ ( x ~~ m /\ ph ) ) -> ( ps -> ( y C_ x -> x = y ) ) )
112 111 com23 
 |-  ( ( ( m e. _om /\ ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) ) /\ ( x ~~ m /\ ph ) ) -> ( y C_ x -> ( ps -> x = y ) ) )
113 112 impd 
 |-  ( ( ( m e. _om /\ ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) ) /\ ( x ~~ m /\ ph ) ) -> ( ( y C_ x /\ ps ) -> x = y ) )
114 113 alrimiv 
 |-  ( ( ( m e. _om /\ ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) ) /\ ( x ~~ m /\ ph ) ) -> A. y ( ( y C_ x /\ ps ) -> x = y ) )
115 32 114 jca 
 |-  ( ( ( m e. _om /\ ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) ) /\ ( x ~~ m /\ ph ) ) -> ( ph /\ A. y ( ( y C_ x /\ ps ) -> x = y ) ) )
116 115 ex 
 |-  ( ( m e. _om /\ ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) ) -> ( ( x ~~ m /\ ph ) -> ( ph /\ A. y ( ( y C_ x /\ ps ) -> x = y ) ) ) )
117 31 116 eximd 
 |-  ( ( m e. _om /\ ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) ) -> ( E. x ( x ~~ m /\ ph ) -> E. x ( ph /\ A. y ( ( y C_ x /\ ps ) -> x = y ) ) ) )
118 117 impancom 
 |-  ( ( m e. _om /\ E. x ( x ~~ m /\ ph ) ) -> ( ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) -> E. x ( ph /\ A. y ( ( y C_ x /\ ps ) -> x = y ) ) ) )
119 14 118 sylbi 
 |-  ( m e. { n e. _om | E. x ( x ~~ n /\ ph ) } -> ( ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) -> E. x ( ph /\ A. y ( ( y C_ x /\ ps ) -> x = y ) ) ) )
120 119 rexlimiv 
 |-  ( E. m e. { n e. _om | E. x ( x ~~ n /\ ph ) } ( { n e. _om | E. x ( x ~~ n /\ ph ) } i^i m ) = (/) -> E. x ( ph /\ A. y ( ( y C_ x /\ ps ) -> x = y ) ) )
121 20 26 120 3syl 
 |-  ( E. x e. Fin ph -> E. x ( ph /\ A. y ( ( y C_ x /\ ps ) -> x = y ) ) )