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

Theorem dfwe2 7211
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 5272 . 2 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
2 df-so 5233 . . . 4 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
3 simpr 473 . . . . 5 ((𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))
4 ax-1 6 . . . . . . . . . . . . . . 15 (𝑥𝑅𝑧 → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
54a1i 11 . . . . . . . . . . . . . 14 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → (𝑥𝑅𝑧 → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
6 fr2nr 5289 . . . . . . . . . . . . . . . . 17 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴)) → ¬ (𝑥𝑅𝑦𝑦𝑅𝑥))
763adantr3 1205 . . . . . . . . . . . . . . . 16 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ¬ (𝑥𝑅𝑦𝑦𝑅𝑥))
8 breq2 4848 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (𝑦𝑅𝑥𝑦𝑅𝑧))
98anbi2d 616 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → ((𝑥𝑅𝑦𝑦𝑅𝑥) ↔ (𝑥𝑅𝑦𝑦𝑅𝑧)))
109notbid 309 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (¬ (𝑥𝑅𝑦𝑦𝑅𝑥) ↔ ¬ (𝑥𝑅𝑦𝑦𝑅𝑧)))
117, 10syl5ibcom 236 . . . . . . . . . . . . . . 15 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → (𝑥 = 𝑧 → ¬ (𝑥𝑅𝑦𝑦𝑅𝑧)))
12 pm2.21 121 . . . . . . . . . . . . . . 15 (¬ (𝑥𝑅𝑦𝑦𝑅𝑧) → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
1311, 12syl6 35 . . . . . . . . . . . . . 14 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → (𝑥 = 𝑧 → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
14 fr3nr 7209 . . . . . . . . . . . . . . . . 17 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ¬ (𝑥𝑅𝑦𝑦𝑅𝑧𝑧𝑅𝑥))
15 df-3an 1102 . . . . . . . . . . . . . . . . . . 19 ((𝑥𝑅𝑦𝑦𝑅𝑧𝑧𝑅𝑥) ↔ ((𝑥𝑅𝑦𝑦𝑅𝑧) ∧ 𝑧𝑅𝑥))
1615biimpri 219 . . . . . . . . . . . . . . . . . 18 (((𝑥𝑅𝑦𝑦𝑅𝑧) ∧ 𝑧𝑅𝑥) → (𝑥𝑅𝑦𝑦𝑅𝑧𝑧𝑅𝑥))
1716ancoms 448 . . . . . . . . . . . . . . . . 17 ((𝑧𝑅𝑥 ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) → (𝑥𝑅𝑦𝑦𝑅𝑧𝑧𝑅𝑥))
1814, 17nsyl 137 . . . . . . . . . . . . . . . 16 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ¬ (𝑧𝑅𝑥 ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)))
1918pm2.21d 119 . . . . . . . . . . . . . . 15 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ((𝑧𝑅𝑥 ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧))
2019expd 402 . . . . . . . . . . . . . 14 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → (𝑧𝑅𝑥 → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
215, 13, 203jaod 1546 . . . . . . . . . . . . 13 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ((𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥) → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
22 frirr 5288 . . . . . . . . . . . . . 14 ((𝑅 Fr 𝐴𝑥𝐴) → ¬ 𝑥𝑅𝑥)
23223ad2antr1 1232 . . . . . . . . . . . . 13 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ¬ 𝑥𝑅𝑥)
2421, 23jctild 517 . . . . . . . . . . . 12 ((𝑅 Fr 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ((𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
2524ex 399 . . . . . . . . . . 11 (𝑅 Fr 𝐴 → ((𝑥𝐴𝑦𝐴𝑧𝐴) → ((𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))))
2625a2d 29 . . . . . . . . . 10 (𝑅 Fr 𝐴 → (((𝑥𝐴𝑦𝐴𝑧𝐴) → (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥)) → ((𝑥𝐴𝑦𝐴𝑧𝐴) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))))
2726alimdv 2007 . . . . . . . . 9 (𝑅 Fr 𝐴 → (∀𝑧((𝑥𝐴𝑦𝐴𝑧𝐴) → (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥)) → ∀𝑧((𝑥𝐴𝑦𝐴𝑧𝐴) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))))
28272alimdv 2009 . . . . . . . 8 (𝑅 Fr 𝐴 → (∀𝑥𝑦𝑧((𝑥𝐴𝑦𝐴𝑧𝐴) → (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥)) → ∀𝑥𝑦𝑧((𝑥𝐴𝑦𝐴𝑧𝐴) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))))
29 r3al 3128 . . . . . . . 8 (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥) ↔ ∀𝑥𝑦𝑧((𝑥𝐴𝑦𝐴𝑧𝐴) → (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥)))
30 r3al 3128 . . . . . . . 8 (∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥𝑦𝑧((𝑥𝐴𝑦𝐴𝑧𝐴) → (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
3128, 29, 303imtr4g 287 . . . . . . 7 (𝑅 Fr 𝐴 → (∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥) → ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
32 ralidm 4270 . . . . . . . . 9 (∀𝑦𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))
33 breq2 4848 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑥𝑅𝑦𝑥𝑅𝑧))
34 equequ2 2122 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑥 = 𝑦𝑥 = 𝑧))
35 breq1 4847 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑦𝑅𝑥𝑧𝑅𝑥))
3633, 34, 353orbi123d 1552 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥)))
3736cbvralv 3360 . . . . . . . . . 10 (∀𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑧𝐴 (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥))
3837ralbii 3168 . . . . . . . . 9 (∀𝑦𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑦𝐴𝑧𝐴 (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥))
3932, 38bitr3i 268 . . . . . . . 8 (∀𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑦𝐴𝑧𝐴 (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥))
4039ralbii 3168 . . . . . . 7 (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑧𝑥 = 𝑧𝑧𝑅𝑥))
41 df-po 5232 . . . . . . 7 (𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
4231, 40, 413imtr4g 287 . . . . . 6 (𝑅 Fr 𝐴 → (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → 𝑅 Po 𝐴))
4342ancrd 543 . . . . 5 (𝑅 Fr 𝐴 → (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
443, 43impbid2 217 . . . 4 (𝑅 Fr 𝐴 → ((𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) ↔ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
452, 44syl5bb 274 . . 3 (𝑅 Fr 𝐴 → (𝑅 Or 𝐴 ↔ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
4645pm5.32i 566 . 2 ((𝑅 Fr 𝐴𝑅 Or 𝐴) ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
471, 46bitri 266 1 (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3o 1099  w3a 1100  wal 1635  wcel 2156  wral 3096   class class class wbr 4844   Po wpo 5230   Or wor 5231   Fr wfr 5267   We wwe 5269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096  ax-un 7179
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-br 4845  df-po 5232  df-so 5233  df-fr 5270  df-we 5272
This theorem is referenced by:  ordon  7212  f1oweALT  7382  dford2  8764  fpwwe2lem12  9748  fpwwe2lem13  9749  dfon2  32017  fnwe2  38124
  Copyright terms: Public domain W3C validator