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

Theorem frfi 9059
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 5507 . . . 4 (𝑥 = ∅ → (𝑅 Po 𝑥𝑅 Po ∅))
2 freq2 5560 . . . 4 (𝑥 = ∅ → (𝑅 Fr 𝑥𝑅 Fr ∅))
31, 2imbi12d 345 . . 3 (𝑥 = ∅ → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po ∅ → 𝑅 Fr ∅)))
4 poeq2 5507 . . . 4 (𝑥 = 𝑦 → (𝑅 Po 𝑥𝑅 Po 𝑦))
5 freq2 5560 . . . 4 (𝑥 = 𝑦 → (𝑅 Fr 𝑥𝑅 Fr 𝑦))
64, 5imbi12d 345 . . 3 (𝑥 = 𝑦 → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po 𝑦𝑅 Fr 𝑦)))
7 poeq2 5507 . . . 4 (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Po 𝑥𝑅 Po (𝑦 ∪ {𝑤})))
8 freq2 5560 . . . 4 (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Fr 𝑥𝑅 Fr (𝑦 ∪ {𝑤})))
97, 8imbi12d 345 . . 3 (𝑥 = (𝑦 ∪ {𝑤}) → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤}))))
10 poeq2 5507 . . . 4 (𝑥 = 𝐴 → (𝑅 Po 𝑥𝑅 Po 𝐴))
11 freq2 5560 . . . 4 (𝑥 = 𝐴 → (𝑅 Fr 𝑥𝑅 Fr 𝐴))
1210, 11imbi12d 345 . . 3 (𝑥 = 𝐴 → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po 𝐴𝑅 Fr 𝐴)))
13 fr0 5568 . . . 4 𝑅 Fr ∅
1413a1i 11 . . 3 (𝑅 Po ∅ → 𝑅 Fr ∅)
15 ssun1 4106 . . . . . . 7 𝑦 ⊆ (𝑦 ∪ {𝑤})
16 poss 5505 . . . . . . 7 (𝑦 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦))
1715, 16ax-mp 5 . . . . . 6 (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦)
1817imim1i 63 . . . . 5 ((𝑅 Po 𝑦𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr 𝑦))
19 uncom 4087 . . . . . . . . . . . 12 (𝑦 ∪ {𝑤}) = ({𝑤} ∪ 𝑦)
2019sseq2i 3950 . . . . . . . . . . 11 (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ 𝑥 ⊆ ({𝑤} ∪ 𝑦))
21 ssundif 4418 . . . . . . . . . . 11 (𝑥 ⊆ ({𝑤} ∪ 𝑦) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
2220, 21bitri 274 . . . . . . . . . 10 (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
2322anbi1i 624 . . . . . . . . 9 ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) ↔ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅))
24 breq1 5077 . . . . . . . . . . . . . 14 (𝑣 = 𝑧 → (𝑣𝑅𝑤𝑧𝑅𝑤))
2524cbvrexvw 3384 . . . . . . . . . . . . 13 (∃𝑣𝑥 𝑣𝑅𝑤 ↔ ∃𝑧𝑥 𝑧𝑅𝑤)
26 simpllr 773 . . . . . . . . . . . . . . . . 17 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑅 Fr 𝑦)
27 simplrl 774 . . . . . . . . . . . . . . . . 17 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (𝑥 ∖ {𝑤}) ⊆ 𝑦)
28 poss 5505 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑥))
2928impcom 408 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑥 ⊆ (𝑦 ∪ {𝑤})) → 𝑅 Po 𝑥)
3022, 29sylan2br 595 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → 𝑅 Po 𝑥)
3130ad2ant2r 744 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → 𝑅 Po 𝑥)
32 simpr1 1193 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧𝑥)
33 simpr2 1194 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧𝑅𝑤)
34 poirr 5515 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Po 𝑥𝑤𝑥) → ¬ 𝑤𝑅𝑤)
35343ad2antr3 1189 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → ¬ 𝑤𝑅𝑤)
36 nbrne2 5094 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧𝑅𝑤 ∧ ¬ 𝑤𝑅𝑤) → 𝑧𝑤)
3733, 35, 36syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧𝑤)
38 eldifsn 4720 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (𝑥 ∖ {𝑤}) ↔ (𝑧𝑥𝑧𝑤))
3932, 37, 38sylanbrc 583 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
4031, 39sylan 580 . . . . . . . . . . . . . . . . . 18 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
4140ne0d 4269 . . . . . . . . . . . . . . . . 17 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (𝑥 ∖ {𝑤}) ≠ ∅)
42 difss 4066 . . . . . . . . . . . . . . . . . 18 (𝑥 ∖ {𝑤}) ⊆ 𝑥
43 vex 3436 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
4443difexi 5252 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∖ {𝑤}) ∈ V
45 fri 5549 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 ∖ {𝑤}) ∈ V ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
4644, 45mpanl1 697 . . . . . . . . . . . . . . . . . 18 ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
47 ssrexv 3988 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {𝑤}) ⊆ 𝑥 → (∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
4842, 46, 47mpsyl 68 . . . . . . . . . . . . . . . . 17 ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
4926, 27, 41, 48syl12anc 834 . . . . . . . . . . . . . . . 16 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
50 breq1 5077 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑧 → (𝑣𝑅𝑢𝑧𝑅𝑢))
5150notbid 318 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑧 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑧𝑅𝑢))
5251rspcv 3557 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ (𝑥 ∖ {𝑤}) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
5339, 52syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
5453adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
55 simplr2 1215 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑧𝑅𝑤)
56 simpll 764 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑅 Po 𝑥)
57 simplr1 1214 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑧𝑥)
58 simplr3 1216 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑤𝑥)
59 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑢𝑥)
60 potr 5516 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑤𝑥𝑢𝑥)) → ((𝑧𝑅𝑤𝑤𝑅𝑢) → 𝑧𝑅𝑢))
6156, 57, 58, 59, 60syl13anc 1371 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → ((𝑧𝑅𝑤𝑤𝑅𝑢) → 𝑧𝑅𝑢))
6255, 61mpand 692 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (𝑤𝑅𝑢𝑧𝑅𝑢))
6362con3d 152 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (¬ 𝑧𝑅𝑢 → ¬ 𝑤𝑅𝑢))
64 vex 3436 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 ∈ V
65 breq1 5077 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑤 → (𝑣𝑅𝑢𝑤𝑅𝑢))
6665notbid 318 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢))
6764, 66ralsn 4617 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢)
6863, 67syl6ibr 251 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (¬ 𝑧𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
6954, 68syld 47 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
70 ralun 4126 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ∧ ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢) → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢)
7170ex 413 . . . . . . . . . . . . . . . . . . . 20 (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
7269, 71sylcom 30 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
73 difsnid 4743 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑥 → ((𝑥 ∖ {𝑤}) ∪ {𝑤}) = 𝑥)
7473raleqdv 3348 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑥 → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
7558, 74syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
7672, 75sylibd 238 . . . . . . . . . . . . . . . . . 18 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
7776reximdva 3203 . . . . . . . . . . . . . . . . 17 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
7831, 77sylan 580 . . . . . . . . . . . . . . . 16 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
7949, 78mpd 15 . . . . . . . . . . . . . . 15 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)
80793exp2 1353 . . . . . . . . . . . . . 14 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (𝑧𝑥 → (𝑧𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))))
8180rexlimdv 3212 . . . . . . . . . . . . 13 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (∃𝑧𝑥 𝑧𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
8225, 81syl5bi 241 . . . . . . . . . . . 12 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (∃𝑣𝑥 𝑣𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
83 ralnex 3167 . . . . . . . . . . . . 13 (∀𝑣𝑥 ¬ 𝑣𝑅𝑤 ↔ ¬ ∃𝑣𝑥 𝑣𝑅𝑤)
84 breq2 5078 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑤 → (𝑣𝑅𝑢𝑣𝑅𝑤))
8584notbid 318 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝑤))
8685ralbidv 3112 . . . . . . . . . . . . . . 15 (𝑢 = 𝑤 → (∀𝑣𝑥 ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑤))
8786rspcev 3561 . . . . . . . . . . . . . 14 ((𝑤𝑥 ∧ ∀𝑣𝑥 ¬ 𝑣𝑅𝑤) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)
8887expcom 414 . . . . . . . . . . . . 13 (∀𝑣𝑥 ¬ 𝑣𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
8983, 88sylbir 234 . . . . . . . . . . . 12 (¬ ∃𝑣𝑥 𝑣𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
9082, 89pm2.61d1 180 . . . . . . . . . . 11 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
91 difsn 4731 . . . . . . . . . . . 12 𝑤𝑥 → (𝑥 ∖ {𝑤}) = 𝑥)
9248expr 457 . . . . . . . . . . . . . . . 16 ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
93 neeq1 3006 . . . . . . . . . . . . . . . . 17 ((𝑥 ∖ {𝑤}) = 𝑥 → ((𝑥 ∖ {𝑤}) ≠ ∅ ↔ 𝑥 ≠ ∅))
94 raleq 3342 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {𝑤}) = 𝑥 → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
9594rexbidv 3226 . . . . . . . . . . . . . . . . 17 ((𝑥 ∖ {𝑤}) = 𝑥 → (∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
9693, 95imbi12d 345 . . . . . . . . . . . . . . . 16 ((𝑥 ∖ {𝑤}) = 𝑥 → (((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢) ↔ (𝑥 ≠ ∅ → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
9792, 96syl5ibcom 244 . . . . . . . . . . . . . . 15 ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) = 𝑥 → (𝑥 ≠ ∅ → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
9897com23 86 . . . . . . . . . . . . . 14 ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
9998adantll 711 . . . . . . . . . . . . 13 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
10099impr 455 . . . . . . . . . . . 12 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
10191, 100syl5 34 . . . . . . . . . . 11 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (¬ 𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
10290, 101pm2.61d 179 . . . . . . . . . 10 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)
103102ex 413 . . . . . . . . 9 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → (((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
10423, 103syl5bi 241 . . . . . . . 8 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
105104alrimiv 1930 . . . . . . 7 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
106 df-fr 5544 . . . . . . 7 (𝑅 Fr (𝑦 ∪ {𝑤}) ↔ ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
107105, 106sylibr 233 . . . . . 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 8947 . 2 (𝐴 ∈ Fin → (𝑅 Po 𝐴𝑅 Fr 𝐴))
112111impcom 408 1 ((𝑅 Po 𝐴𝐴 ∈ Fin) → 𝑅 Fr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086  wal 1537   = wceq 1539  wcel 2106  wne 2943  wral 3064  wrex 3065  Vcvv 3432  cdif 3884  cun 3885  wss 3887  c0 4256  {csn 4561   class class class wbr 5074   Po wpo 5501   Fr wfr 5541  Fincfn 8733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-om 7713  df-en 8734  df-fin 8737
This theorem is referenced by:  fimax2g  9060  wofi  9063  fimin2g  9256  isfin1-3  10142
  Copyright terms: Public domain W3C validator