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