MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frfi Structured version   Visualization version   GIF version

Theorem frfi 8757
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.)
Assertion
Ref Expression
frfi ((𝑅 Po 𝐴𝐴 ∈ Fin) → 𝑅 Fr 𝐴)

Proof of Theorem frfi
Dummy variables 𝑢 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 poeq2 5477 . . . 4 (𝑥 = ∅ → (𝑅 Po 𝑥𝑅 Po ∅))
2 freq2 5525 . . . 4 (𝑥 = ∅ → (𝑅 Fr 𝑥𝑅 Fr ∅))
31, 2imbi12d 346 . . 3 (𝑥 = ∅ → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po ∅ → 𝑅 Fr ∅)))
4 poeq2 5477 . . . 4 (𝑥 = 𝑦 → (𝑅 Po 𝑥𝑅 Po 𝑦))
5 freq2 5525 . . . 4 (𝑥 = 𝑦 → (𝑅 Fr 𝑥𝑅 Fr 𝑦))
64, 5imbi12d 346 . . 3 (𝑥 = 𝑦 → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po 𝑦𝑅 Fr 𝑦)))
7 poeq2 5477 . . . 4 (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Po 𝑥𝑅 Po (𝑦 ∪ {𝑤})))
8 freq2 5525 . . . 4 (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Fr 𝑥𝑅 Fr (𝑦 ∪ {𝑤})))
97, 8imbi12d 346 . . 3 (𝑥 = (𝑦 ∪ {𝑤}) → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤}))))
10 poeq2 5477 . . . 4 (𝑥 = 𝐴 → (𝑅 Po 𝑥𝑅 Po 𝐴))
11 freq2 5525 . . . 4 (𝑥 = 𝐴 → (𝑅 Fr 𝑥𝑅 Fr 𝐴))
1210, 11imbi12d 346 . . 3 (𝑥 = 𝐴 → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po 𝐴𝑅 Fr 𝐴)))
13 fr0 5533 . . . 4 𝑅 Fr ∅
1413a1i 11 . . 3 (𝑅 Po ∅ → 𝑅 Fr ∅)
15 ssun1 4152 . . . . . . 7 𝑦 ⊆ (𝑦 ∪ {𝑤})
16 poss 5475 . . . . . . 7 (𝑦 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦))
1715, 16ax-mp 5 . . . . . 6 (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦)
1817imim1i 63 . . . . 5 ((𝑅 Po 𝑦𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr 𝑦))
19 uncom 4133 . . . . . . . . . . . 12 (𝑦 ∪ {𝑤}) = ({𝑤} ∪ 𝑦)
2019sseq2i 4000 . . . . . . . . . . 11 (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ 𝑥 ⊆ ({𝑤} ∪ 𝑦))
21 ssundif 4436 . . . . . . . . . . 11 (𝑥 ⊆ ({𝑤} ∪ 𝑦) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
2220, 21bitri 276 . . . . . . . . . 10 (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
2322anbi1i 623 . . . . . . . . 9 ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) ↔ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅))
24 breq1 5066 . . . . . . . . . . . . . 14 (𝑣 = 𝑧 → (𝑣𝑅𝑤𝑧𝑅𝑤))
2524cbvrexvw 3456 . . . . . . . . . . . . 13 (∃𝑣𝑥 𝑣𝑅𝑤 ↔ ∃𝑧𝑥 𝑧𝑅𝑤)
26 simpllr 772 . . . . . . . . . . . . . . . . 17 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑅 Fr 𝑦)
27 simplrl 773 . . . . . . . . . . . . . . . . 17 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (𝑥 ∖ {𝑤}) ⊆ 𝑦)
28 poss 5475 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑥))
2928impcom 408 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑥 ⊆ (𝑦 ∪ {𝑤})) → 𝑅 Po 𝑥)
3022, 29sylan2br 594 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → 𝑅 Po 𝑥)
3130ad2ant2r 743 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → 𝑅 Po 𝑥)
32 simpr1 1188 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧𝑥)
33 simpr2 1189 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧𝑅𝑤)
34 poirr 5484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Po 𝑥𝑤𝑥) → ¬ 𝑤𝑅𝑤)
35343ad2antr3 1184 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → ¬ 𝑤𝑅𝑤)
36 nbrne2 5083 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧𝑅𝑤 ∧ ¬ 𝑤𝑅𝑤) → 𝑧𝑤)
3733, 35, 36syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧𝑤)
38 eldifsn 4718 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (𝑥 ∖ {𝑤}) ↔ (𝑧𝑥𝑧𝑤))
3932, 37, 38sylanbrc 583 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
4031, 39sylan 580 . . . . . . . . . . . . . . . . . 18 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
4140ne0d 4305 . . . . . . . . . . . . . . . . 17 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (𝑥 ∖ {𝑤}) ≠ ∅)
42 difss 4112 . . . . . . . . . . . . . . . . . 18 (𝑥 ∖ {𝑤}) ⊆ 𝑥
43 vex 3503 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
4443difexi 5229 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∖ {𝑤}) ∈ V
45 fri 5516 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 ∖ {𝑤}) ∈ V ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
4644, 45mpanl1 696 . . . . . . . . . . . . . . . . . 18 ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
47 ssrexv 4038 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {𝑤}) ⊆ 𝑥 → (∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
4842, 46, 47mpsyl 68 . . . . . . . . . . . . . . . . 17 ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
4926, 27, 41, 48syl12anc 834 . . . . . . . . . . . . . . . 16 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
50 breq1 5066 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑧 → (𝑣𝑅𝑢𝑧𝑅𝑢))
5150notbid 319 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑧 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑧𝑅𝑢))
5251rspcv 3622 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ (𝑥 ∖ {𝑤}) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
5339, 52syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
5453adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
55 simplr2 1210 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑧𝑅𝑤)
56 simpll 763 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑅 Po 𝑥)
57 simplr1 1209 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑧𝑥)
58 simplr3 1211 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑤𝑥)
59 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑢𝑥)
60 potr 5485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑤𝑥𝑢𝑥)) → ((𝑧𝑅𝑤𝑤𝑅𝑢) → 𝑧𝑅𝑢))
6156, 57, 58, 59, 60syl13anc 1366 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → ((𝑧𝑅𝑤𝑤𝑅𝑢) → 𝑧𝑅𝑢))
6255, 61mpand 691 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (𝑤𝑅𝑢𝑧𝑅𝑢))
6362con3d 155 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (¬ 𝑧𝑅𝑢 → ¬ 𝑤𝑅𝑢))
64 vex 3503 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 ∈ V
65 breq1 5066 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑤 → (𝑣𝑅𝑢𝑤𝑅𝑢))
6665notbid 319 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢))
6764, 66ralsn 4618 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢)
6863, 67syl6ibr 253 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (¬ 𝑧𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
6954, 68syld 47 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
70 ralun 4172 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ∧ ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢) → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢)
7170ex 413 . . . . . . . . . . . . . . . . . . . 20 (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
7269, 71sylcom 30 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
73 difsnid 4742 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑥 → ((𝑥 ∖ {𝑤}) ∪ {𝑤}) = 𝑥)
7473raleqdv 3421 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑥 → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
7558, 74syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
7672, 75sylibd 240 . . . . . . . . . . . . . . . . . 18 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
7776reximdva 3279 . . . . . . . . . . . . . . . . 17 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
7831, 77sylan 580 . . . . . . . . . . . . . . . 16 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
7949, 78mpd 15 . . . . . . . . . . . . . . 15 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)
80793exp2 1348 . . . . . . . . . . . . . 14 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (𝑧𝑥 → (𝑧𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))))
8180rexlimdv 3288 . . . . . . . . . . . . 13 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (∃𝑧𝑥 𝑧𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
8225, 81syl5bi 243 . . . . . . . . . . . 12 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (∃𝑣𝑥 𝑣𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
83 ralnex 3241 . . . . . . . . . . . . 13 (∀𝑣𝑥 ¬ 𝑣𝑅𝑤 ↔ ¬ ∃𝑣𝑥 𝑣𝑅𝑤)
84 breq2 5067 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑤 → (𝑣𝑅𝑢𝑣𝑅𝑤))
8584notbid 319 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝑤))
8685ralbidv 3202 . . . . . . . . . . . . . . 15 (𝑢 = 𝑤 → (∀𝑣𝑥 ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑤))
8786rspcev 3627 . . . . . . . . . . . . . 14 ((𝑤𝑥 ∧ ∀𝑣𝑥 ¬ 𝑣𝑅𝑤) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)
8887expcom 414 . . . . . . . . . . . . 13 (∀𝑣𝑥 ¬ 𝑣𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
8983, 88sylbir 236 . . . . . . . . . . . 12 (¬ ∃𝑣𝑥 𝑣𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
9082, 89pm2.61d1 181 . . . . . . . . . . 11 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
91 difsn 4730 . . . . . . . . . . . 12 𝑤𝑥 → (𝑥 ∖ {𝑤}) = 𝑥)
9248expr 457 . . . . . . . . . . . . . . . 16 ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
93 neeq1 3083 . . . . . . . . . . . . . . . . 17 ((𝑥 ∖ {𝑤}) = 𝑥 → ((𝑥 ∖ {𝑤}) ≠ ∅ ↔ 𝑥 ≠ ∅))
94 raleq 3411 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {𝑤}) = 𝑥 → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
9594rexbidv 3302 . . . . . . . . . . . . . . . . 17 ((𝑥 ∖ {𝑤}) = 𝑥 → (∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
9693, 95imbi12d 346 . . . . . . . . . . . . . . . 16 ((𝑥 ∖ {𝑤}) = 𝑥 → (((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢) ↔ (𝑥 ≠ ∅ → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
9792, 96syl5ibcom 246 . . . . . . . . . . . . . . 15 ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) = 𝑥 → (𝑥 ≠ ∅ → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
9897com23 86 . . . . . . . . . . . . . 14 ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
9998adantll 710 . . . . . . . . . . . . 13 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
10099impr 455 . . . . . . . . . . . 12 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
10191, 100syl5 34 . . . . . . . . . . 11 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (¬ 𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
10290, 101pm2.61d 180 . . . . . . . . . 10 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)
103102ex 413 . . . . . . . . 9 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → (((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
10423, 103syl5bi 243 . . . . . . . 8 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
105104alrimiv 1921 . . . . . . 7 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
106 df-fr 5513 . . . . . . 7 (𝑅 Fr (𝑦 ∪ {𝑤}) ↔ ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
107105, 106sylibr 235 . . . . . 6 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → 𝑅 Fr (𝑦 ∪ {𝑤}))
108107ex 413 . . . . 5 (𝑅 Po (𝑦 ∪ {𝑤}) → (𝑅 Fr 𝑦𝑅 Fr (𝑦 ∪ {𝑤})))
10918, 108sylcom 30 . . . 4 ((𝑅 Po 𝑦𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤})))
110109a1i 11 . . 3 (𝑦 ∈ Fin → ((𝑅 Po 𝑦𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤}))))
1113, 6, 9, 12, 14, 110findcard2 8752 . 2 (𝐴 ∈ Fin → (𝑅 Po 𝐴𝑅 Fr 𝐴))
112111impcom 408 1 ((𝑅 Po 𝐴𝐴 ∈ Fin) → 𝑅 Fr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1081  wal 1528   = wceq 1530  wcel 2107  wne 3021  wral 3143  wrex 3144  Vcvv 3500  cdif 3937  cun 3938  wss 3940  c0 4295  {csn 4564   class class class wbr 5063   Po wpo 5471   Fr wfr 5510  Fincfn 8503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-om 7574  df-1o 8098  df-er 8284  df-en 8504  df-fin 8507
This theorem is referenced by:  fimax2g  8758  wofi  8761  fimin2g  8955  isfin1-3  9802
  Copyright terms: Public domain W3C validator