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

Theorem frfi 8373
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 5192 . . . 4 (𝑥 = ∅ → (𝑅 Po 𝑥𝑅 Po ∅))
2 freq2 5238 . . . 4 (𝑥 = ∅ → (𝑅 Fr 𝑥𝑅 Fr ∅))
31, 2imbi12d 333 . . 3 (𝑥 = ∅ → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po ∅ → 𝑅 Fr ∅)))
4 poeq2 5192 . . . 4 (𝑥 = 𝑦 → (𝑅 Po 𝑥𝑅 Po 𝑦))
5 freq2 5238 . . . 4 (𝑥 = 𝑦 → (𝑅 Fr 𝑥𝑅 Fr 𝑦))
64, 5imbi12d 333 . . 3 (𝑥 = 𝑦 → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po 𝑦𝑅 Fr 𝑦)))
7 poeq2 5192 . . . 4 (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Po 𝑥𝑅 Po (𝑦 ∪ {𝑤})))
8 freq2 5238 . . . 4 (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Fr 𝑥𝑅 Fr (𝑦 ∪ {𝑤})))
97, 8imbi12d 333 . . 3 (𝑥 = (𝑦 ∪ {𝑤}) → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤}))))
10 poeq2 5192 . . . 4 (𝑥 = 𝐴 → (𝑅 Po 𝑥𝑅 Po 𝐴))
11 freq2 5238 . . . 4 (𝑥 = 𝐴 → (𝑅 Fr 𝑥𝑅 Fr 𝐴))
1210, 11imbi12d 333 . . 3 (𝑥 = 𝐴 → ((𝑅 Po 𝑥𝑅 Fr 𝑥) ↔ (𝑅 Po 𝐴𝑅 Fr 𝐴)))
13 fr0 5246 . . . 4 𝑅 Fr ∅
1413a1i 11 . . 3 (𝑅 Po ∅ → 𝑅 Fr ∅)
15 ssun1 3920 . . . . . . 7 𝑦 ⊆ (𝑦 ∪ {𝑤})
16 poss 5190 . . . . . . 7 (𝑦 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦))
1715, 16ax-mp 5 . . . . . 6 (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦)
1817imim1i 63 . . . . 5 ((𝑅 Po 𝑦𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr 𝑦))
19 uncom 3901 . . . . . . . . . . . 12 (𝑦 ∪ {𝑤}) = ({𝑤} ∪ 𝑦)
2019sseq2i 3772 . . . . . . . . . . 11 (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ 𝑥 ⊆ ({𝑤} ∪ 𝑦))
21 ssundif 4197 . . . . . . . . . . 11 (𝑥 ⊆ ({𝑤} ∪ 𝑦) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
2220, 21bitri 264 . . . . . . . . . 10 (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦)
2322anbi1i 733 . . . . . . . . 9 ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) ↔ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅))
24 breq1 4808 . . . . . . . . . . . . . 14 (𝑣 = 𝑧 → (𝑣𝑅𝑤𝑧𝑅𝑤))
2524cbvrexv 3312 . . . . . . . . . . . . 13 (∃𝑣𝑥 𝑣𝑅𝑤 ↔ ∃𝑧𝑥 𝑧𝑅𝑤)
26 simpllr 817 . . . . . . . . . . . . . . . . 17 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑅 Fr 𝑦)
27 simplrl 819 . . . . . . . . . . . . . . . . 17 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (𝑥 ∖ {𝑤}) ⊆ 𝑦)
28 poss 5190 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑥))
2928impcom 445 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑥 ⊆ (𝑦 ∪ {𝑤})) → 𝑅 Po 𝑥)
3022, 29sylan2br 494 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → 𝑅 Po 𝑥)
3130ad2ant2r 800 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → 𝑅 Po 𝑥)
32 simpr1 1234 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧𝑥)
33 simpr2 1236 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧𝑅𝑤)
34 poirr 5199 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Po 𝑥𝑤𝑥) → ¬ 𝑤𝑅𝑤)
35343ad2antr3 1206 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → ¬ 𝑤𝑅𝑤)
36 nbrne2 4825 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧𝑅𝑤 ∧ ¬ 𝑤𝑅𝑤) → 𝑧𝑤)
3733, 35, 36syl2anc 696 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧𝑤)
38 eldifsn 4463 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (𝑥 ∖ {𝑤}) ↔ (𝑧𝑥𝑧𝑤))
3932, 37, 38sylanbrc 701 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
4031, 39sylan 489 . . . . . . . . . . . . . . . . . 18 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤}))
41 ne0i 4065 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (𝑥 ∖ {𝑤}) → (𝑥 ∖ {𝑤}) ≠ ∅)
4240, 41syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (𝑥 ∖ {𝑤}) ≠ ∅)
43 difss 3881 . . . . . . . . . . . . . . . . . 18 (𝑥 ∖ {𝑤}) ⊆ 𝑥
44 vex 3344 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
45 difexg 4961 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ V → (𝑥 ∖ {𝑤}) ∈ V)
4644, 45ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∖ {𝑤}) ∈ V
47 fri 5229 . . . . . . . . . . . . . . . . . . 19 ((((𝑥 ∖ {𝑤}) ∈ V ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
4846, 47mpanl1 718 . . . . . . . . . . . . . . . . . 18 ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
49 ssrexv 3809 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {𝑤}) ⊆ 𝑥 → (∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
5043, 48, 49mpsyl 68 . . . . . . . . . . . . . . . . 17 ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
5126, 27, 42, 50syl12anc 1475 . . . . . . . . . . . . . . . 16 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)
52 breq1 4808 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 = 𝑧 → (𝑣𝑅𝑢𝑧𝑅𝑢))
5352notbid 307 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑧 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑧𝑅𝑢))
5453rspcv 3446 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ∈ (𝑥 ∖ {𝑤}) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
5539, 54syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
5655adantr 472 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢))
57 simplr2 1263 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑧𝑅𝑤)
58 simpll 807 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑅 Po 𝑥)
59 simplr1 1261 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑧𝑥)
60 simplr3 1265 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑤𝑥)
61 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → 𝑢𝑥)
62 potr 5200 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑤𝑥𝑢𝑥)) → ((𝑧𝑅𝑤𝑤𝑅𝑢) → 𝑧𝑅𝑢))
6358, 59, 60, 61, 62syl13anc 1479 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → ((𝑧𝑅𝑤𝑤𝑅𝑢) → 𝑧𝑅𝑢))
6457, 63mpand 713 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (𝑤𝑅𝑢𝑧𝑅𝑢))
6564con3d 148 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (¬ 𝑧𝑅𝑢 → ¬ 𝑤𝑅𝑢))
66 vex 3344 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 ∈ V
67 breq1 4808 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = 𝑤 → (𝑣𝑅𝑢𝑤𝑅𝑢))
6867notbid 307 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢))
6966, 68ralsn 4367 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢)
7065, 69syl6ibr 242 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (¬ 𝑧𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
7156, 70syld 47 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢))
72 ralun 3939 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ∧ ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢) → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢)
7372ex 449 . . . . . . . . . . . . . . . . . . . 20 (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
7471, 73sylcom 30 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢))
75 difsnid 4487 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑥 → ((𝑥 ∖ {𝑤}) ∪ {𝑤}) = 𝑥)
7675raleqdv 3284 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑥 → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
7760, 76syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
7874, 77sylibd 229 . . . . . . . . . . . . . . . . . 18 (((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) ∧ 𝑢𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
7978reximdva 3156 . . . . . . . . . . . . . . . . 17 ((𝑅 Po 𝑥 ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
8031, 79sylan 489 . . . . . . . . . . . . . . . 16 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → (∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
8151, 80mpd 15 . . . . . . . . . . . . . . 15 ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) ∧ (𝑧𝑥𝑧𝑅𝑤𝑤𝑥)) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)
82813exp2 1448 . . . . . . . . . . . . . 14 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (𝑧𝑥 → (𝑧𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))))
8382rexlimdv 3169 . . . . . . . . . . . . 13 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (∃𝑧𝑥 𝑧𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
8425, 83syl5bi 232 . . . . . . . . . . . 12 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (∃𝑣𝑥 𝑣𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
85 ralnex 3131 . . . . . . . . . . . . 13 (∀𝑣𝑥 ¬ 𝑣𝑅𝑤 ↔ ¬ ∃𝑣𝑥 𝑣𝑅𝑤)
86 breq2 4809 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑤 → (𝑣𝑅𝑢𝑣𝑅𝑤))
8786notbid 307 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝑤))
8887ralbidv 3125 . . . . . . . . . . . . . . 15 (𝑢 = 𝑤 → (∀𝑣𝑥 ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑤))
8988rspcev 3450 . . . . . . . . . . . . . 14 ((𝑤𝑥 ∧ ∀𝑣𝑥 ¬ 𝑣𝑅𝑤) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)
9089expcom 450 . . . . . . . . . . . . 13 (∀𝑣𝑥 ¬ 𝑣𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
9185, 90sylbir 225 . . . . . . . . . . . 12 (¬ ∃𝑣𝑥 𝑣𝑅𝑤 → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
9284, 91pm2.61d1 171 . . . . . . . . . . 11 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
93 difsn 4474 . . . . . . . . . . . 12 𝑤𝑥 → (𝑥 ∖ {𝑤}) = 𝑥)
9450expr 644 . . . . . . . . . . . . . . . 16 ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢))
95 neeq1 2995 . . . . . . . . . . . . . . . . 17 ((𝑥 ∖ {𝑤}) = 𝑥 → ((𝑥 ∖ {𝑤}) ≠ ∅ ↔ 𝑥 ≠ ∅))
96 raleq 3278 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∖ {𝑤}) = 𝑥 → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣𝑥 ¬ 𝑣𝑅𝑢))
9796rexbidv 3191 . . . . . . . . . . . . . . . . 17 ((𝑥 ∖ {𝑤}) = 𝑥 → (∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
9895, 97imbi12d 333 . . . . . . . . . . . . . . . 16 ((𝑥 ∖ {𝑤}) = 𝑥 → (((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢𝑥𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢) ↔ (𝑥 ≠ ∅ → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
9994, 98syl5ibcom 235 . . . . . . . . . . . . . . 15 ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) = 𝑥 → (𝑥 ≠ ∅ → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
10099com23 86 . . . . . . . . . . . . . 14 ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
101100adantll 752 . . . . . . . . . . . . 13 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)))
102101impr 650 . . . . . . . . . . . 12 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
10393, 102syl5 34 . . . . . . . . . . 11 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → (¬ 𝑤𝑥 → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
10492, 103pm2.61d 170 . . . . . . . . . 10 (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅)) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢)
105104ex 449 . . . . . . . . 9 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → (((𝑥 ∖ {𝑤}) ⊆ 𝑦𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
10623, 105syl5bi 232 . . . . . . . 8 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
107106alrimiv 2005 . . . . . . 7 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
108 df-fr 5226 . . . . . . 7 (𝑅 Fr (𝑦 ∪ {𝑤}) ↔ ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢𝑥𝑣𝑥 ¬ 𝑣𝑅𝑢))
109107, 108sylibr 224 . . . . . 6 ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → 𝑅 Fr (𝑦 ∪ {𝑤}))
110109ex 449 . . . . 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 8368 . 2 (𝐴 ∈ Fin → (𝑅 Po 𝐴𝑅 Fr 𝐴))
114113impcom 445 1 ((𝑅 Po 𝐴𝐴 ∈ Fin) → 𝑅 Fr 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072  wal 1630   = wceq 1632  wcel 2140  wne 2933  wral 3051  wrex 3052  Vcvv 3341  cdif 3713  cun 3714  wss 3716  c0 4059  {csn 4322   class class class wbr 4805   Po wpo 5186   Fr wfr 5223  Fincfn 8124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-sbc 3578  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-pss 3732  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-tp 4327  df-op 4329  df-uni 4590  df-br 4806  df-opab 4866  df-tr 4906  df-id 5175  df-eprel 5180  df-po 5188  df-so 5189  df-fr 5226  df-we 5228  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-ord 5888  df-on 5889  df-lim 5890  df-suc 5891  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-om 7233  df-1o 7731  df-er 7914  df-en 8125  df-fin 8128
This theorem is referenced by:  fimax2g  8374  wofi  8377  fimin2g  8571  isfin1-3  9421
  Copyright terms: Public domain W3C validator