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 ( ( 𝑅 Po 𝐴𝐴 ∈ Fin ) → 𝑅 Fr 𝐴 )

Proof

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