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

Theorem frfi 8156
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 5004 . . . 4 (𝑥 = ∅ → (𝑅 Po 𝑥𝑅 Po ∅))
2 freq2 5050 . . . 4 (𝑥 = ∅ → (𝑅 Fr 𝑥𝑅 Fr ∅))
31, 2imbi12d 334 . . 3 (𝑥 = ∅ → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po ∅ → 𝑅 Fr ∅)))
4 poeq2 5004 . . . 4 (𝑥 = 𝑦 → (𝑅 Po 𝑥𝑅 Po 𝑦))
5 freq2 5050 . . . 4 (𝑥 = 𝑦 → (𝑅 Fr 𝑥𝑅 Fr 𝑦))
64, 5imbi12d 334 . . 3 (𝑥 = 𝑦 → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po 𝑦𝑅 Fr 𝑦)))
7 poeq2 5004 . . . 4 (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Po 𝑥𝑅 Po (𝑦 ∪ {𝑤})))
8 freq2 5050 . . . 4 (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Fr 𝑥𝑅 Fr (𝑦 ∪ {𝑤})))
97, 8imbi12d 334 . . 3 (𝑥 = (𝑦 ∪ {𝑤}) → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤}))))
10 poeq2 5004 . . . 4 (𝑥 = 𝐴 → (𝑅 Po 𝑥𝑅 Po 𝐴))
11 freq2 5050 . . . 4 (𝑥 = 𝐴 → (𝑅 Fr 𝑥𝑅 Fr 𝐴))
1210, 11imbi12d 334 . . 3 (𝑥 = 𝐴 → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po 𝐴𝑅 Fr 𝐴)))
13 fr0 5058 . . . 4 𝑅 Fr ∅
1413a1i 11 . . 3 (𝑅 Po ∅ → 𝑅 Fr ∅)
15 ssun1 3759 . . . . . . 7 𝑦 ⊆ (𝑦 ∪ {𝑤})
16 poss 5002 . . . . . . 7 (𝑦 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦))
1715, 16ax-mp 5 . . . . . 6 (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦)
1817imim1i 63 . . . . 5 ((𝑅 Po 𝑦𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr 𝑦))
19 uncom 3740 . . . . . . . . . . . 12 (𝑦 ∪ {𝑤}) = ({𝑤} ∪ 𝑦)
2019sseq2i 3614 . . . . . . . . . . 11 (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ 𝑥 ⊆ ({𝑤} ∪ 𝑦))
21 ssundif 4029 . . . . . . . . . . 11 (𝑥 ⊆ ({𝑤} ∪ 𝑦) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
2220, 21bitri 264 . . . . . . . . . 10 (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
2322anbi1i 730 . . . . . . . . 9 ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) ↔ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅))
24 breq1 4621 . . . . . . . . . . . . . 14 (𝑣 = 𝑧 → (𝑣𝑅𝑤𝑧𝑅𝑤))
2524cbvrexv 3163 . . . . . . . . . . . . 13 (∃𝑣𝑥 𝑣𝑅𝑤 ↔ ∃𝑧𝑥 𝑧𝑅𝑤)
26 simpllr 798 . . . . . . . . . . . . . . . . 17 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑅 Fr 𝑦)
27 simplrl 799 . . . . . . . . . . . . . . . . 17 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (𝑥 ∖ {𝑤}) ⊆ 𝑦)
28 poss 5002 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑥))
2928impcom 446 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑥 ⊆ (𝑦 ∪ {𝑤})) → 𝑅 Po 𝑥)
3022, 29sylan2br 493 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → 𝑅 Po 𝑥)
3130ad2ant2r 782 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → 𝑅 Po 𝑥)
32 simpr1 1065 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧𝑥)
33 simpr2 1066 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧𝑅𝑤)
34 poirr 5011 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Po 𝑥𝑤𝑥) → ¬ 𝑤𝑅𝑤)
35343ad2antr3 1226 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → ¬ 𝑤𝑅𝑤)
36 nbrne2 4638 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧𝑅𝑤 ∧ ¬ 𝑤𝑅𝑤) → 𝑧𝑤)
3733, 35, 36syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧𝑤)
38 eldifsn 4292 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (𝑥 ∖ {𝑤}) ↔ (𝑧𝑥𝑧𝑤))
3932, 37, 38sylanbrc 697 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
4031, 39sylan 488 . . . . . . . . . . . . . . . . . 18 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
41 ne0i 3902 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (𝑥 ∖ {𝑤}) → (𝑥 ∖ {𝑤}) ≠ ∅)
4240, 41syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (𝑥 ∖ {𝑤}) ≠ ∅)
43 difss 3720 . . . . . . . . . . . . . . . . . 18 (𝑥 ∖ {𝑤}) ⊆ 𝑥
44 vex 3192 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
45 difexg 4773 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ V → (𝑥 ∖ {𝑤}) ∈ V)
4644, 45ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∖ {𝑤}) ∈ V
47 fri 5041 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 ∖ {𝑤}) ∈ V ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
4846, 47mpanl1 715 . . . . . . . . . . . . . . . . . 18 ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
49 ssrexv 3651 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {𝑤}) ⊆ 𝑥 → (∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
5043, 48, 49mpsyl 68 . . . . . . . . . . . . . . . . 17 ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
5126, 27, 42, 50syl12anc 1321 . . . . . . . . . . . . . . . 16 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
52 breq1 4621 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑧 → (𝑣𝑅𝑢𝑧𝑅𝑢))
5352notbid 308 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑧 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑧𝑅𝑢))
5453rspcv 3294 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ (𝑥 ∖ {𝑤}) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
5539, 54syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
5655adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
57 simplr2 1102 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑧𝑅𝑤)
58 simpll 789 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑅 Po 𝑥)
59 simplr1 1101 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑧𝑥)
60 simplr3 1103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑤𝑥)
61 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑢𝑥)
62 potr 5012 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑤𝑥𝑢𝑥)) → ((𝑧𝑅𝑤𝑤𝑅𝑢) → 𝑧𝑅𝑢))
6358, 59, 60, 61, 62syl13anc 1325 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → ((𝑧𝑅𝑤𝑤𝑅𝑢) → 𝑧𝑅𝑢))
6457, 63mpand 710 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (𝑤𝑅𝑢𝑧𝑅𝑢))
6564con3d 148 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (¬ 𝑧𝑅𝑢 → ¬ 𝑤𝑅𝑢))
66 vex 3192 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 ∈ V
67 breq1 4621 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑤 → (𝑣𝑅𝑢𝑤𝑅𝑢))
6867notbid 308 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢))
6966, 68ralsn 4198 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢)
7065, 69syl6ibr 242 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (¬ 𝑧𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
7156, 70syld 47 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
72 ralun 3778 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ∧ ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢) → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢)
7372ex 450 . . . . . . . . . . . . . . . . . . . 20 (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
7471, 73sylcom 30 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
75 difsnid 4315 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑥 → ((𝑥 ∖ {𝑤}) ∪ {𝑤}) = 𝑥)
7675raleqdv 3136 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑥 → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
7760, 76syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
7874, 77sylibd 229 . . . . . . . . . . . . . . . . . 18 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
7978reximdva 3012 . . . . . . . . . . . . . . . . 17 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
8031, 79sylan 488 . . . . . . . . . . . . . . . 16 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
8151, 80mpd 15 . . . . . . . . . . . . . . 15 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)
82813exp2 1282 . . . . . . . . . . . . . 14 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (𝑧𝑥 → (𝑧𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))))
8382rexlimdv 3024 . . . . . . . . . . . . 13 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (∃𝑧𝑥 𝑧𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
8425, 83syl5bi 232 . . . . . . . . . . . 12 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (∃𝑣𝑥 𝑣𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
85 ralnex 2987 . . . . . . . . . . . . 13 (∀𝑣𝑥 ¬ 𝑣𝑅𝑤 ↔ ¬ ∃𝑣𝑥 𝑣𝑅𝑤)
86 breq2 4622 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑤 → (𝑣𝑅𝑢𝑣𝑅𝑤))
8786notbid 308 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝑤))
8887ralbidv 2981 . . . . . . . . . . . . . . 15 (𝑢 = 𝑤 → (∀𝑣𝑥 ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑤))
8988rspcev 3298 . . . . . . . . . . . . . 14 ((𝑤𝑥 ∧ ∀𝑣𝑥 ¬ 𝑣𝑅𝑤) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)
9089expcom 451 . . . . . . . . . . . . 13 (∀𝑣𝑥 ¬ 𝑣𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
9185, 90sylbir 225 . . . . . . . . . . . 12 (¬ ∃𝑣𝑥 𝑣𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
9284, 91pm2.61d1 171 . . . . . . . . . . 11 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
93 difsn 4302 . . . . . . . . . . . 12 𝑤𝑥 → (𝑥 ∖ {𝑤}) = 𝑥)
9450expr 642 . . . . . . . . . . . . . . . 16 ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
95 neeq1 2852 . . . . . . . . . . . . . . . . 17 ((𝑥 ∖ {𝑤}) = 𝑥 → ((𝑥 ∖ {𝑤}) ≠ ∅ ↔ 𝑥 ≠ ∅))
96 raleq 3130 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {𝑤}) = 𝑥 → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
9796rexbidv 3046 . . . . . . . . . . . . . . . . 17 ((𝑥 ∖ {𝑤}) = 𝑥 → (∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
9895, 97imbi12d 334 . . . . . . . . . . . . . . . 16 ((𝑥 ∖ {𝑤}) = 𝑥 → (((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢) ↔ (𝑥 ≠ ∅ → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
9994, 98syl5ibcom 235 . . . . . . . . . . . . . . 15 ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) = 𝑥 → (𝑥 ≠ ∅ → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
10099com23 86 . . . . . . . . . . . . . 14 ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
101100adantll 749 . . . . . . . . . . . . 13 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
102101impr 648 . . . . . . . . . . . 12 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
10393, 102syl5 34 . . . . . . . . . . 11 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (¬ 𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
10492, 103pm2.61d 170 . . . . . . . . . 10 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)
105104ex 450 . . . . . . . . 9 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → (((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
10623, 105syl5bi 232 . . . . . . . 8 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
107106alrimiv 1852 . . . . . . 7 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
108 df-fr 5038 . . . . . . 7 (𝑅 Fr (𝑦 ∪ {𝑤}) ↔ ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
109107, 108sylibr 224 . . . . . 6 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → 𝑅 Fr (𝑦 ∪ {𝑤}))
110109ex 450 . . . . 5 (𝑅 Po (𝑦 ∪ {𝑤}) → (𝑅 Fr 𝑦𝑅 Fr (𝑦 ∪ {𝑤})))
11118, 110sylcom 30 . . . 4 ((𝑅 Po 𝑦𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤})))
112111a1i 11 . . 3 (𝑦 ∈ Fin → ((𝑅 Po 𝑦𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤}))))
1133, 6, 9, 12, 14, 112findcard2 8151 . 2 (𝐴 ∈ Fin → (𝑅 Po 𝐴𝑅 Fr 𝐴))
114113impcom 446 1 ((𝑅 Po 𝐴𝐴 ∈ Fin) → 𝑅 Fr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036  wal 1478   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  Vcvv 3189  cdif 3556  cun 3557  wss 3559  c0 3896  {csn 4153   class class class wbr 4618   Po wpo 4998   Fr wfr 5035  Fincfn 7906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-om 7020  df-1o 7512  df-er 7694  df-en 7907  df-fin 7910
This theorem is referenced by:  fimax2g  8157  wofi  8160  fimin2g  8354  isfin1-3  9159
  Copyright terms: Public domain W3C validator