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φψ
Assertion finminlem xFinφxφyyxψx=y

Proof

Step Hyp Ref Expression
1 finminlem.1 x=yφψ
2 nfe1 xxxnφ
3 nfcv _xω
4 2 3 nfrabw _xnω|xxnφ
5 nfcv _x
6 4 5 nfne xnω|xxnφ
7 isfi xFinmωxm
8 19.8a xmφxxmφ
9 8 anim2i mωxmφmωxxmφ
10 9 3impb mωxmφmωxxmφ
11 breq2 n=mxnxm
12 11 anbi1d n=mxnφxmφ
13 12 exbidv n=mxxnφxxmφ
14 13 elrab mnω|xxnφmωxxmφ
15 10 14 sylibr mωxmφmnω|xxnφ
16 15 ne0d mωxmφnω|xxnφ
17 16 3exp mωxmφnω|xxnφ
18 17 rexlimiv mωxmφnω|xxnφ
19 7 18 sylbi xFinφnω|xxnφ
20 6 19 rexlimi xFinφnω|xxnφ
21 epweon EWeOn
22 ssrab2 nω|xxnφω
23 omsson ωOn
24 22 23 sstri nω|xxnφOn
25 wefrc EWeOnnω|xxnφOnnω|xxnφmnω|xxnφnω|xxnφm=
26 21 24 25 mp3an12 nω|xxnφmnω|xxnφnω|xxnφm=
27 nfv xmω
28 nfcv _xm
29 4 28 nfin _xnω|xxnφm
30 29 nfeq1 xnω|xxnφm=
31 27 30 nfan xmωnω|xxnφm=
32 simprr mωnω|xxnφm=xmφφ
33 sspss yxyxy=x
34 rspe mωxmmωxm
35 pssss yxyx
36 ssfi xFinyxyFin
37 35 36 sylan2 xFinyxyFin
38 37 ex xFinyxyFin
39 7 38 sylbir mωxmyxyFin
40 34 39 syl mωxmyxyFin
41 40 adantrr mωxmφyxyFin
42 41 adantrr mωxmφψyxyFin
43 isfi yFinkωyk
44 simprll mωxmφψkωykyxkω
45 simprlr mωxmφψkωykyxyk
46 simplrr mωxmφψkωykyxψ
47 vex yV
48 breq1 x=yxkyk
49 48 1 anbi12d x=yxkφykψ
50 47 49 spcev ykψxxkφ
51 45 46 50 syl2anc mωxmφψkωykyxxxkφ
52 34 7 sylibr mωxmxFin
53 52 adantrr mωxmφxFin
54 53 adantrr mωxmφψxFin
55 54 adantr mωxmφψkωykxFin
56 php3 xFinyxyx
57 56 ex xFinyxyx
58 55 57 syl mωxmφψkωykyxyx
59 vex kV
60 ssdomg kVmkmk
61 59 60 ax-mp mkmk
62 endomtr xmmkxk
63 62 ex xmmkxk
64 63 ad2antrr xmφψmkxk
65 64 ad2antlr mωxmφψkωykmkxk
66 ensym ykky
67 domentr xkkyxy
68 66 67 sylan2 xkykxy
69 68 expcom ykxkxy
70 69 ad2antll mωxmφψkωykxkxy
71 65 70 syld mωxmφψkωykmkxy
72 61 71 syl5 mωxmφψkωykmkxy
73 domnsym xy¬yx
74 73 con2i yx¬xy
75 72 74 nsyli mωxmφψkωykyx¬mk
76 58 75 syld mωxmφψkωykyx¬mk
77 76 impr mωxmφψkωykyx¬mk
78 nnord mωOrdm
79 78 ad2antrr mωxmφψkωykyxOrdm
80 nnord kωOrdk
81 80 adantr kωykOrdk
82 81 ad2antrl mωxmφψkωykyxOrdk
83 ordtri1 OrdmOrdkmk¬km
84 83 con2bid OrdmOrdkkm¬mk
85 79 82 84 syl2anc mωxmφψkωykyxkm¬mk
86 77 85 mpbird mωxmφψkωykyxkm
87 44 51 86 jca31 mωxmφψkωykyxkωxxkφkm
88 elin knω|xxnφmknω|xxnφkm
89 breq2 n=kxnxk
90 89 anbi1d n=kxnφxkφ
91 90 exbidv n=kxxnφxxkφ
92 91 elrab knω|xxnφkωxxkφ
93 92 anbi1i knω|xxnφkmkωxxkφkm
94 88 93 bitri knω|xxnφmkωxxkφkm
95 87 94 sylibr mωxmφψkωykyxknω|xxnφm
96 95 ne0d mωxmφψkωykyxnω|xxnφm
97 96 exp44 mωxmφψkωykyxnω|xxnφm
98 97 rexlimdv mωxmφψkωykyxnω|xxnφm
99 43 98 syl5bi mωxmφψyFinyxnω|xxnφm
100 99 com23 mωxmφψyxyFinnω|xxnφm
101 42 100 mpdd mωxmφψyxnω|xxnφm
102 101 necon2bd mωxmφψnω|xxnφm=¬yx
103 102 ex mωxmφψnω|xxnφm=¬yx
104 103 com23 mωnω|xxnφm=xmφψ¬yx
105 104 imp31 mωnω|xxnφm=xmφψ¬yx
106 105 pm2.21d mωnω|xxnφm=xmφψyxx=y
107 equcomi y=xx=y
108 107 a1i mωnω|xxnφm=xmφψy=xx=y
109 106 108 jaod mωnω|xxnφm=xmφψyxy=xx=y
110 33 109 syl5bi mωnω|xxnφm=xmφψyxx=y
111 110 expr mωnω|xxnφm=xmφψyxx=y
112 111 com23 mωnω|xxnφm=xmφyxψx=y
113 112 impd mωnω|xxnφm=xmφyxψx=y
114 113 alrimiv mωnω|xxnφm=xmφyyxψx=y
115 32 114 jca mωnω|xxnφm=xmφφyyxψx=y
116 115 ex mωnω|xxnφm=xmφφyyxψx=y
117 31 116 eximd mωnω|xxnφm=xxmφxφyyxψx=y
118 117 impancom mωxxmφnω|xxnφm=xφyyxψx=y
119 14 118 sylbi mnω|xxnφnω|xxnφm=xφyyxψx=y
120 119 rexlimiv mnω|xxnφnω|xxnφm=xφyyxψx=y
121 20 26 120 3syl xFinφxφyyxψx=y