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

Theorem dfwe2 7709
Description: Alternate definition of well-ordering. Definition 6.24(2) of [TakeutiZaring] p. 30. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
Assertion
Ref Expression
dfwe2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
Distinct variable groups:   𝑥,𝑦,𝑅   𝑥,𝐴,𝑦

Proof of Theorem dfwe2
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-we 5591 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
2 df-so 5547 . . . 4 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
3 simpr 486 . . . . 5 ((𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))
4 ax-1 6 . . . . . . . . . . . . . . 15 (𝑥𝑅𝑧 → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
54a1i 11 . . . . . . . . . . . . . 14 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → (𝑥𝑅𝑧 → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
6 fr2nr 5612 . . . . . . . . . . . . . . . . 17 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴)) → ¬ (𝑥𝑅𝑦𝑦𝑅𝑥))
763adantr3 1172 . . . . . . . . . . . . . . . 16 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ¬ (𝑥𝑅𝑦𝑦𝑅𝑥))
8 breq2 5110 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (𝑦𝑅𝑥𝑦𝑅𝑧))
98anbi2d 630 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → ((𝑥𝑅𝑦𝑦𝑅𝑥) ↔ (𝑥𝑅𝑦𝑦𝑅𝑧)))
109notbid 318 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (¬ (𝑥𝑅𝑦𝑦𝑅𝑥) ↔ ¬ (𝑥𝑅𝑦𝑦𝑅𝑧)))
117, 10syl5ibcom 244 . . . . . . . . . . . . . . 15 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → (𝑥 = 𝑧 → ¬ (𝑥𝑅𝑦𝑦𝑅𝑧)))
12 pm2.21 123 . . . . . . . . . . . . . . 15 (¬ (𝑥𝑅𝑦𝑦𝑅𝑧) → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
1311, 12syl6 35 . . . . . . . . . . . . . 14 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → (𝑥 = 𝑧 → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
14 fr3nr 7707 . . . . . . . . . . . . . . . . 17 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ¬ (𝑥𝑅𝑦𝑦𝑅𝑧𝑧𝑅𝑥))
15 df-3an 1090 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑅𝑦𝑦𝑅𝑧𝑧𝑅𝑥) ↔ ((𝑥𝑅𝑦𝑦𝑅𝑧) ∧ 𝑧𝑅𝑥))
1615biimpri 227 . . . . . . . . . . . . . . . . . 18 (((𝑥𝑅𝑦𝑦𝑅𝑧) ∧ 𝑧𝑅𝑥) → (𝑥𝑅𝑦𝑦𝑅𝑧𝑧𝑅𝑥))
1716ancoms 460 . . . . . . . . . . . . . . . . 17 ((𝑧𝑅𝑥 ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) → (𝑥𝑅𝑦𝑦𝑅𝑧𝑧𝑅𝑥))
1814, 17nsyl 140 . . . . . . . . . . . . . . . 16 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ¬ (𝑧𝑅𝑥 ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
1918pm2.21d 121 . . . . . . . . . . . . . . 15 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ((𝑧𝑅𝑥 ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧))
2019expd 417 . . . . . . . . . . . . . 14 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → (𝑧𝑅𝑥 → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
215, 13, 203jaod 1429 . . . . . . . . . . . . 13 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ((𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥) → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
22 frirr 5611 . . . . . . . . . . . . . 14 ((𝑅 Fr 𝐴𝑥𝐴) → ¬ 𝑥𝑅𝑥)
23223ad2antr1 1189 . . . . . . . . . . . . 13 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ¬ 𝑥𝑅𝑥)
2421, 23jctild 527 . . . . . . . . . . . 12 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ((𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
2524ex 414 . . . . . . . . . . 11 (𝑅 Fr 𝐴 → ((𝑥𝐴𝑦𝐴𝑧𝐴) → ((𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))))
2625a2d 29 . . . . . . . . . 10 (𝑅 Fr 𝐴 → (((𝑥𝐴𝑦𝐴𝑧𝐴) → (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥)) → ((𝑥𝐴𝑦𝐴𝑧𝐴) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))))
2726alimdv 1920 . . . . . . . . 9 (𝑅 Fr 𝐴 → (∀𝑧((𝑥𝐴𝑦𝐴𝑧𝐴) → (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥)) → ∀𝑧((𝑥𝐴𝑦𝐴𝑧𝐴) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))))
28272alimdv 1922 . . . . . . . 8 (𝑅 Fr 𝐴 → (∀𝑥𝑦𝑧((𝑥𝐴𝑦𝐴𝑧𝐴) → (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥)) → ∀𝑥𝑦𝑧((𝑥𝐴𝑦𝐴𝑧𝐴) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))))
29 r3al 3194 . . . . . . . 8 (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥) ↔ ∀𝑥𝑦𝑧((𝑥𝐴𝑦𝐴𝑧𝐴) → (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥)))
30 r3al 3194 . . . . . . . 8 (∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥𝑦𝑧((𝑥𝐴𝑦𝐴𝑧𝐴) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
3128, 29, 303imtr4g 296 . . . . . . 7 (𝑅 Fr 𝐴 → (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥) → ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
32 breq2 5110 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑥𝑅𝑦𝑥𝑅𝑧))
33 equequ2 2030 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑥 = 𝑦𝑥 = 𝑧))
34 breq1 5109 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑦𝑅𝑥𝑧𝑅𝑥))
3532, 33, 343orbi123d 1436 . . . . . . . . . 10 (𝑦 = 𝑧 → ((𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥)))
3635ralidmw 4466 . . . . . . . . 9 (∀𝑦𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))
3735cbvralvw 3226 . . . . . . . . . 10 (∀𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑧𝐴 (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥))
3837ralbii 3097 . . . . . . . . 9 (∀𝑦𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑦𝐴𝑧𝐴 (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥))
3936, 38bitr3i 277 . . . . . . . 8 (∀𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑦𝐴𝑧𝐴 (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥))
4039ralbii 3097 . . . . . . 7 (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥))
41 df-po 5546 . . . . . . 7 (𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
4231, 40, 413imtr4g 296 . . . . . 6 (𝑅 Fr 𝐴 → (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → 𝑅 Po 𝐴))
4342ancrd 553 . . . . 5 (𝑅 Fr 𝐴 → (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
443, 43impbid2 225 . . . 4 (𝑅 Fr 𝐴 → ((𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) ↔ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
452, 44bitrid 283 . . 3 (𝑅 Fr 𝐴 → (𝑅 Or 𝐴 ↔ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
4645pm5.32i 576 . 2 ((𝑅 Fr 𝐴𝑅 Or 𝐴) ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
471, 46bitri 275 1 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  w3o 1087  w3a 1088  wal 1540  wcel 2107  wral 3065   class class class wbr 5106   Po wpo 5544   Or wor 5545   Fr wfr 5586   We wwe 5588
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-br 5107  df-po 5546  df-so 5547  df-fr 5589  df-we 5591
This theorem is referenced by:  epweonALT  7711  f1oweALT  7906  dford2  9557  fpwwe2lem11  10578  fpwwe2lem12  10579  dfon2  34370  fnwe2  41383
  Copyright terms: Public domain W3C validator