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 x Fin φ x φ y y x ψ x = y

Proof

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