This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrdi ⊢ ( ( ( 𝑅 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 biimtrid ⊢ ( ( ( 𝑅 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 biimtrid ⊢ ( ( 𝑅 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 𝐴 )