Metamath Proof Explorer


Theorem frfi

Description: A partial order is well-founded on a finite set. (Contributed by Jeff Madsen, 18-Jun-2010) (Proof shortened by Mario Carneiro, 29-Jan-2014)

Ref Expression
Assertion frfi R Po A A Fin R Fr A

Proof

Step Hyp Ref Expression
1 poeq2 x = R Po x R Po
2 freq2 x = R Fr x R Fr
3 1 2 imbi12d x = R Po x R Fr x R Po R Fr
4 poeq2 x = y R Po x R Po y
5 freq2 x = y R Fr x R Fr y
6 4 5 imbi12d x = y R Po x R Fr x R Po y R Fr y
7 poeq2 x = y w R Po x R Po y w
8 freq2 x = y w R Fr x R Fr y w
9 7 8 imbi12d x = y w R Po x R Fr x R Po y w R Fr y w
10 poeq2 x = A R Po x R Po A
11 freq2 x = A R Fr x R Fr A
12 10 11 imbi12d x = A R Po x R Fr x R Po A R Fr A
13 fr0 R Fr
14 13 a1i R Po R Fr
15 ssun1 y y w
16 poss y y w R Po y w R Po y
17 15 16 ax-mp R Po y w R Po y
18 17 imim1i R Po y R Fr y R Po y w R Fr y
19 uncom y w = w y
20 19 sseq2i x y w x w y
21 ssundif x w y x w y
22 20 21 bitri x y w x w y
23 22 anbi1i x y w x x w y x
24 breq1 v = z v R w z R w
25 24 cbvrexvw v x v R w z x z R w
26 simpllr R Po y w R Fr y x w y x z x z R w w x R Fr y
27 simplrl R Po y w R Fr y x w y x z x z R w w x x w y
28 poss x y w R Po y w R Po x
29 28 impcom R Po y w x y w R Po x
30 22 29 sylan2br R Po y w x w y R Po x
31 30 ad2ant2r R Po y w R Fr y x w y x R Po x
32 simpr1 R Po x z x z R w w x z x
33 simpr2 R Po x z x z R w w x z R w
34 poirr R Po x w x ¬ w R w
35 34 3ad2antr3 R Po x z x z R w w x ¬ w R w
36 nbrne2 z R w ¬ w R w z w
37 33 35 36 syl2anc R Po x z x z R w w x z w
38 eldifsn z x w z x z w
39 32 37 38 sylanbrc R Po x z x z R w w x z x w
40 31 39 sylan R Po y w R Fr y x w y x z x z R w w x z x w
41 40 ne0d R Po y w R Fr y x w y x z x z R w w x x w
42 difss x w x
43 vex x V
44 43 difexi x w V
45 fri x w V R Fr y x w y x w u x w v x w ¬ v R u
46 44 45 mpanl1 R Fr y x w y x w u x w v x w ¬ v R u
47 ssrexv x w x u x w v x w ¬ v R u u x v x w ¬ v R u
48 42 46 47 mpsyl R Fr y x w y x w u x v x w ¬ v R u
49 26 27 41 48 syl12anc R Po y w R Fr y x w y x z x z R w w x u x v x w ¬ v R u
50 breq1 v = z v R u z R u
51 50 notbid v = z ¬ v R u ¬ z R u
52 51 rspcv z x w v x w ¬ v R u ¬ z R u
53 39 52 syl R Po x z x z R w w x v x w ¬ v R u ¬ z R u
54 53 adantr R Po x z x z R w w x u x v x w ¬ v R u ¬ z R u
55 simplr2 R Po x z x z R w w x u x z R w
56 simpll R Po x z x z R w w x u x R Po x
57 simplr1 R Po x z x z R w w x u x z x
58 simplr3 R Po x z x z R w w x u x w x
59 simpr R Po x z x z R w w x u x u x
60 potr R Po x z x w x u x z R w w R u z R u
61 56 57 58 59 60 syl13anc R Po x z x z R w w x u x z R w w R u z R u
62 55 61 mpand R Po x z x z R w w x u x w R u z R u
63 62 con3d R Po x z x z R w w x u x ¬ z R u ¬ w R u
64 vex w V
65 breq1 v = w v R u w R u
66 65 notbid v = w ¬ v R u ¬ w R u
67 64 66 ralsn v w ¬ v R u ¬ w R u
68 63 67 syl6ibr R Po x z x z R w w x u x ¬ z R u v w ¬ v R u
69 54 68 syld R Po x z x z R w w x u x v x w ¬ v R u v w ¬ v R u
70 ralun v x w ¬ v R u v w ¬ v R u v x w w ¬ v R u
71 70 ex v x w ¬ v R u v w ¬ v R u v x w w ¬ v R u
72 69 71 sylcom R Po x z x z R w w x u x v x w ¬ v R u v x w w ¬ v R u
73 difsnid w x x w w = x
74 73 raleqdv w x v x w w ¬ v R u v x ¬ v R u
75 58 74 syl R Po x z x z R w w x u x v x w w ¬ v R u v x ¬ v R u
76 72 75 sylibd R Po x z x z R w w x u x v x w ¬ v R u v x ¬ v R u
77 76 reximdva R Po x z x z R w w x u x v x w ¬ v R u u x v x ¬ v R u
78 31 77 sylan R Po y w R Fr y x w y x z x z R w w x u x v x w ¬ v R u u x v x ¬ v R u
79 49 78 mpd R Po y w R Fr y x w y x z x z R w w x u x v x ¬ v R u
80 79 3exp2 R Po y w R Fr y x w y x z x z R w w x u x v x ¬ v R u
81 80 rexlimdv R Po y w R Fr y x w y x z x z R w w x u x v x ¬ v R u
82 25 81 syl5bi R Po y w R Fr y x w y x v x v R w w x u x v x ¬ v R u
83 ralnex v x ¬ v R w ¬ v x v R w
84 breq2 u = w v R u v R w
85 84 notbid u = w ¬ v R u ¬ v R w
86 85 ralbidv u = w v x ¬ v R u v x ¬ v R w
87 86 rspcev w x v x ¬ v R w u x v x ¬ v R u
88 87 expcom v x ¬ v R w w x u x v x ¬ v R u
89 83 88 sylbir ¬ v x v R w w x u x v x ¬ v R u
90 82 89 pm2.61d1 R Po y w R Fr y x w y x w x u x v x ¬ v R u
91 difsn ¬ w x x w = x
92 48 expr R Fr y x w y x w u x v x w ¬ v R u
93 neeq1 x w = x x w x
94 raleq x w = x v x w ¬ v R u v x ¬ v R u
95 94 rexbidv x w = x u x v x w ¬ v R u u x v x ¬ v R u
96 93 95 imbi12d x w = x x w u x v x w ¬ v R u x u x v x ¬ v R u
97 92 96 syl5ibcom R Fr y x w y x w = x x u x v x ¬ v R u
98 97 com23 R Fr y x w y x x w = x u x v x ¬ v R u
99 98 adantll R Po y w R Fr y x w y x x w = x u x v x ¬ v R u
100 99 impr R Po y w R Fr y x w y x x w = x u x v x ¬ v R u
101 91 100 syl5 R Po y w R Fr y x w y x ¬ w x u x v x ¬ v R u
102 90 101 pm2.61d R Po y w R Fr y x w y x u x v x ¬ v R u
103 102 ex R Po y w R Fr y x w y x u x v x ¬ v R u
104 23 103 syl5bi R Po y w R Fr y x y w x u x v x ¬ v R u
105 104 alrimiv R Po y w R Fr y x x y w x u x v x ¬ v R u
106 df-fr R Fr y w x x y w x u x v x ¬ v R u
107 105 106 sylibr R Po y w R Fr y R Fr y w
108 107 ex R Po y w R Fr y R Fr y w
109 18 108 sylcom R Po y R Fr y R Po y w R Fr y w
110 109 a1i y Fin R Po y R Fr y R Po y w R Fr y w
111 3 6 9 12 14 110 findcard2 A Fin R Po A R Fr A
112 111 impcom R Po A A Fin R Fr A