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

Theorem frfi 9284
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 5591 . . . 4 (𝑥 = ∅ → (𝑅 Po 𝑥𝑅 Po ∅))
2 freq2 5646 . . . 4 (𝑥 = ∅ → (𝑅 Fr 𝑥𝑅 Fr ∅))
31, 2imbi12d 344 . . 3 (𝑥 = ∅ → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po ∅ → 𝑅 Fr ∅)))
4 poeq2 5591 . . . 4 (𝑥 = 𝑦 → (𝑅 Po 𝑥𝑅 Po 𝑦))
5 freq2 5646 . . . 4 (𝑥 = 𝑦 → (𝑅 Fr 𝑥𝑅 Fr 𝑦))
64, 5imbi12d 344 . . 3 (𝑥 = 𝑦 → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po 𝑦𝑅 Fr 𝑦)))
7 poeq2 5591 . . . 4 (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Po 𝑥𝑅 Po (𝑦 ∪ {𝑤})))
8 freq2 5646 . . . 4 (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Fr 𝑥𝑅 Fr (𝑦 ∪ {𝑤})))
97, 8imbi12d 344 . . 3 (𝑥 = (𝑦 ∪ {𝑤}) → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤}))))
10 poeq2 5591 . . . 4 (𝑥 = 𝐴 → (𝑅 Po 𝑥𝑅 Po 𝐴))
11 freq2 5646 . . . 4 (𝑥 = 𝐴 → (𝑅 Fr 𝑥𝑅 Fr 𝐴))
1210, 11imbi12d 344 . . 3 (𝑥 = 𝐴 → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po 𝐴𝑅 Fr 𝐴)))
13 fr0 5654 . . . 4 𝑅 Fr ∅
1413a1i 11 . . 3 (𝑅 Po ∅ → 𝑅 Fr ∅)
15 ssun1 4171 . . . . . . 7 𝑦 ⊆ (𝑦 ∪ {𝑤})
16 poss 5589 . . . . . . 7 (𝑦 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦))
1715, 16ax-mp 5 . . . . . 6 (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦)
1817imim1i 63 . . . . 5 ((𝑅 Po 𝑦𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr 𝑦))
19 uncom 4152 . . . . . . . . . . . 12 (𝑦 ∪ {𝑤}) = ({𝑤} ∪ 𝑦)
2019sseq2i 4010 . . . . . . . . . . 11 (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ 𝑥 ⊆ ({𝑤} ∪ 𝑦))
21 ssundif 4486 . . . . . . . . . . 11 (𝑥 ⊆ ({𝑤} ∪ 𝑦) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
2220, 21bitri 274 . . . . . . . . . 10 (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
2322anbi1i 624 . . . . . . . . 9 ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) ↔ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅))
24 breq1 5150 . . . . . . . . . . . . . 14 (𝑣 = 𝑧 → (𝑣𝑅𝑤𝑧𝑅𝑤))
2524cbvrexvw 3235 . . . . . . . . . . . . 13 (∃𝑣𝑥 𝑣𝑅𝑤 ↔ ∃𝑧𝑥 𝑧𝑅𝑤)
26 simpllr 774 . . . . . . . . . . . . . . . . 17 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑅 Fr 𝑦)
27 simplrl 775 . . . . . . . . . . . . . . . . 17 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (𝑥 ∖ {𝑤}) ⊆ 𝑦)
28 poss 5589 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑥))
2928impcom 408 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑥 ⊆ (𝑦 ∪ {𝑤})) → 𝑅 Po 𝑥)
3022, 29sylan2br 595 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → 𝑅 Po 𝑥)
3130ad2ant2r 745 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → 𝑅 Po 𝑥)
32 simpr1 1194 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧𝑥)
33 simpr2 1195 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧𝑅𝑤)
34 poirr 5599 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Po 𝑥𝑤𝑥) → ¬ 𝑤𝑅𝑤)
35343ad2antr3 1190 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → ¬ 𝑤𝑅𝑤)
36 nbrne2 5167 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧𝑅𝑤 ∧ ¬ 𝑤𝑅𝑤) → 𝑧𝑤)
3733, 35, 36syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧𝑤)
38 eldifsn 4789 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (𝑥 ∖ {𝑤}) ↔ (𝑧𝑥𝑧𝑤))
3932, 37, 38sylanbrc 583 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
4031, 39sylan 580 . . . . . . . . . . . . . . . . . 18 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
4140ne0d 4334 . . . . . . . . . . . . . . . . 17 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (𝑥 ∖ {𝑤}) ≠ ∅)
42 difss 4130 . . . . . . . . . . . . . . . . . 18 (𝑥 ∖ {𝑤}) ⊆ 𝑥
43 vex 3478 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
4443difexi 5327 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∖ {𝑤}) ∈ V
45 fri 5635 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 ∖ {𝑤}) ∈ V ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
4644, 45mpanl1 698 . . . . . . . . . . . . . . . . . 18 ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
47 ssrexv 4050 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {𝑤}) ⊆ 𝑥 → (∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
4842, 46, 47mpsyl 68 . . . . . . . . . . . . . . . . 17 ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
4926, 27, 41, 48syl12anc 835 . . . . . . . . . . . . . . . 16 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
50 breq1 5150 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑧 → (𝑣𝑅𝑢𝑧𝑅𝑢))
5150notbid 317 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑧 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑧𝑅𝑢))
5251rspcv 3608 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ (𝑥 ∖ {𝑤}) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
5339, 52syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
5453adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
55 simplr2 1216 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑧𝑅𝑤)
56 simpll 765 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑅 Po 𝑥)
57 simplr1 1215 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑧𝑥)
58 simplr3 1217 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑤𝑥)
59 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑢𝑥)
60 potr 5600 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑤𝑥𝑢𝑥)) → ((𝑧𝑅𝑤𝑤𝑅𝑢) → 𝑧𝑅𝑢))
6156, 57, 58, 59, 60syl13anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → ((𝑧𝑅𝑤𝑤𝑅𝑢) → 𝑧𝑅𝑢))
6255, 61mpand 693 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (𝑤𝑅𝑢𝑧𝑅𝑢))
6362con3d 152 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (¬ 𝑧𝑅𝑢 → ¬ 𝑤𝑅𝑢))
64 vex 3478 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 ∈ V
65 breq1 5150 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑤 → (𝑣𝑅𝑢𝑤𝑅𝑢))
6665notbid 317 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢))
6764, 66ralsn 4684 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢)
6863, 67syl6ibr 251 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (¬ 𝑧𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
6954, 68syld 47 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
70 ralun 4191 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ∧ ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢) → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢)
7170ex 413 . . . . . . . . . . . . . . . . . . . 20 (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
7269, 71sylcom 30 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
73 difsnid 4812 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑥 → ((𝑥 ∖ {𝑤}) ∪ {𝑤}) = 𝑥)
7473raleqdv 3325 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑥 → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
7558, 74syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
7672, 75sylibd 238 . . . . . . . . . . . . . . . . . 18 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
7776reximdva 3168 . . . . . . . . . . . . . . . . 17 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
7831, 77sylan 580 . . . . . . . . . . . . . . . 16 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
7949, 78mpd 15 . . . . . . . . . . . . . . 15 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)
80793exp2 1354 . . . . . . . . . . . . . 14 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (𝑧𝑥 → (𝑧𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))))
8180rexlimdv 3153 . . . . . . . . . . . . 13 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (∃𝑧𝑥 𝑧𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
8225, 81biimtrid 241 . . . . . . . . . . . 12 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (∃𝑣𝑥 𝑣𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
83 ralnex 3072 . . . . . . . . . . . . 13 (∀𝑣𝑥 ¬ 𝑣𝑅𝑤 ↔ ¬ ∃𝑣𝑥 𝑣𝑅𝑤)
84 breq2 5151 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑤 → (𝑣𝑅𝑢𝑣𝑅𝑤))
8584notbid 317 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝑤))
8685ralbidv 3177 . . . . . . . . . . . . . . 15 (𝑢 = 𝑤 → (∀𝑣𝑥 ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑤))
8786rspcev 3612 . . . . . . . . . . . . . 14 ((𝑤𝑥 ∧ ∀𝑣𝑥 ¬ 𝑣𝑅𝑤) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)
8887expcom 414 . . . . . . . . . . . . 13 (∀𝑣𝑥 ¬ 𝑣𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
8983, 88sylbir 234 . . . . . . . . . . . 12 (¬ ∃𝑣𝑥 𝑣𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
9082, 89pm2.61d1 180 . . . . . . . . . . 11 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
91 difsn 4800 . . . . . . . . . . . 12 𝑤𝑥 → (𝑥 ∖ {𝑤}) = 𝑥)
9248expr 457 . . . . . . . . . . . . . . . 16 ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
93 neeq1 3003 . . . . . . . . . . . . . . . . 17 ((𝑥 ∖ {𝑤}) = 𝑥 → ((𝑥 ∖ {𝑤}) ≠ ∅ ↔ 𝑥 ≠ ∅))
94 raleq 3322 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {𝑤}) = 𝑥 → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
9594rexbidv 3178 . . . . . . . . . . . . . . . . 17 ((𝑥 ∖ {𝑤}) = 𝑥 → (∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
9693, 95imbi12d 344 . . . . . . . . . . . . . . . 16 ((𝑥 ∖ {𝑤}) = 𝑥 → (((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢) ↔ (𝑥 ≠ ∅ → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
9792, 96syl5ibcom 244 . . . . . . . . . . . . . . 15 ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) = 𝑥 → (𝑥 ≠ ∅ → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
9897com23 86 . . . . . . . . . . . . . 14 ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
9998adantll 712 . . . . . . . . . . . . 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, 103biimtrid 241 . . . . . . . 8 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
105104alrimiv 1930 . . . . . . 7 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
106 df-fr 5630 . . . . . . 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 9160 . 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 1087  wal 1539   = wceq 1541  wcel 2106  wne 2940  wral 3061  wrex 3070  Vcvv 3474  cdif 3944  cun 3945  wss 3947  c0 4321  {csn 4627   class class class wbr 5147   Po wpo 5585   Fr wfr 5627  Fincfn 8935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-om 7852  df-en 8936  df-fin 8939
This theorem is referenced by:  fimax2g  9285  wofi  9288  fimin2g  9488  isfin1-3  10377
  Copyright terms: Public domain W3C validator