Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dfon2 Structured version   Visualization version   GIF version

Theorem dfon2 31451
Description: On consists of all sets that contain all its transitive proper subsets. This definition comes from J. R. Isbell, "A Definition of Ordinal Numbers," American Mathematical Monthly, vol 67 (1960), pp. 51-52. (Contributed by Scott Fenton, 20-Feb-2011.)
Assertion
Ref Expression
dfon2 On = {𝑥 ∣ ∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)}
Distinct variable group:   𝑥,𝑦

Proof of Theorem dfon2
Dummy variables 𝑧 𝑤 𝑡 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-on 5696 . 2 On = {𝑥 ∣ Ord 𝑥}
2 tz7.7 5718 . . . . . . . . 9 ((Ord 𝑥 ∧ Tr 𝑦) → (𝑦𝑥 ↔ (𝑦𝑥𝑦𝑥)))
3 df-pss 3576 . . . . . . . . 9 (𝑦𝑥 ↔ (𝑦𝑥𝑦𝑥))
42, 3syl6bbr 278 . . . . . . . 8 ((Ord 𝑥 ∧ Tr 𝑦) → (𝑦𝑥𝑦𝑥))
54exbiri 651 . . . . . . 7 (Ord 𝑥 → (Tr 𝑦 → (𝑦𝑥𝑦𝑥)))
65com23 86 . . . . . 6 (Ord 𝑥 → (𝑦𝑥 → (Tr 𝑦𝑦𝑥)))
76impd 447 . . . . 5 (Ord 𝑥 → ((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥))
87alrimiv 1852 . . . 4 (Ord 𝑥 → ∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥))
9 vex 3193 . . . . . . 7 𝑥 ∈ V
10 dfon2lem3 31444 . . . . . . 7 (𝑥 ∈ V → (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (Tr 𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧𝑧)))
119, 10ax-mp 5 . . . . . 6 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (Tr 𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧𝑧))
1211simpld 475 . . . . 5 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → Tr 𝑥)
139dfon2lem7 31448 . . . . . . . 8 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (𝑡𝑥 → ∀𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡)))
1413ralrimiv 2961 . . . . . . 7 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡))
15 dfon2lem9 31450 . . . . . . . 8 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → E Fr 𝑥)
16 psseq2 3679 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑧 → (𝑢𝑡𝑢𝑧))
1716anbi1d 740 . . . . . . . . . . . . . . 15 (𝑡 = 𝑧 → ((𝑢𝑡 ∧ Tr 𝑢) ↔ (𝑢𝑧 ∧ Tr 𝑢)))
18 elequ2 2001 . . . . . . . . . . . . . . 15 (𝑡 = 𝑧 → (𝑢𝑡𝑢𝑧))
1917, 18imbi12d 334 . . . . . . . . . . . . . 14 (𝑡 = 𝑧 → (((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ((𝑢𝑧 ∧ Tr 𝑢) → 𝑢𝑧)))
2019albidv 1846 . . . . . . . . . . . . 13 (𝑡 = 𝑧 → (∀𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ∀𝑢((𝑢𝑧 ∧ Tr 𝑢) → 𝑢𝑧)))
21 psseq1 3678 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑣 → (𝑢𝑧𝑣𝑧))
22 treq 4728 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑣 → (Tr 𝑢 ↔ Tr 𝑣))
2321, 22anbi12d 746 . . . . . . . . . . . . . . 15 (𝑢 = 𝑣 → ((𝑢𝑧 ∧ Tr 𝑢) ↔ (𝑣𝑧 ∧ Tr 𝑣)))
24 elequ1 1994 . . . . . . . . . . . . . . 15 (𝑢 = 𝑣 → (𝑢𝑧𝑣𝑧))
2523, 24imbi12d 334 . . . . . . . . . . . . . 14 (𝑢 = 𝑣 → (((𝑢𝑧 ∧ Tr 𝑢) → 𝑢𝑧) ↔ ((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧)))
2625cbvalv 2272 . . . . . . . . . . . . 13 (∀𝑢((𝑢𝑧 ∧ Tr 𝑢) → 𝑢𝑧) ↔ ∀𝑣((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧))
2720, 26syl6bb 276 . . . . . . . . . . . 12 (𝑡 = 𝑧 → (∀𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ∀𝑣((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧)))
2827rspccv 3296 . . . . . . . . . . 11 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → (𝑧𝑥 → ∀𝑣((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧)))
29 psseq2 3679 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑤 → (𝑢𝑡𝑢𝑤))
3029anbi1d 740 . . . . . . . . . . . . . . 15 (𝑡 = 𝑤 → ((𝑢𝑡 ∧ Tr 𝑢) ↔ (𝑢𝑤 ∧ Tr 𝑢)))
31 elequ2 2001 . . . . . . . . . . . . . . 15 (𝑡 = 𝑤 → (𝑢𝑡𝑢𝑤))
3230, 31imbi12d 334 . . . . . . . . . . . . . 14 (𝑡 = 𝑤 → (((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ((𝑢𝑤 ∧ Tr 𝑢) → 𝑢𝑤)))
3332albidv 1846 . . . . . . . . . . . . 13 (𝑡 = 𝑤 → (∀𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ∀𝑢((𝑢𝑤 ∧ Tr 𝑢) → 𝑢𝑤)))
34 psseq1 3678 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑦 → (𝑢𝑤𝑦𝑤))
35 treq 4728 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑦 → (Tr 𝑢 ↔ Tr 𝑦))
3634, 35anbi12d 746 . . . . . . . . . . . . . . 15 (𝑢 = 𝑦 → ((𝑢𝑤 ∧ Tr 𝑢) ↔ (𝑦𝑤 ∧ Tr 𝑦)))
37 elequ1 1994 . . . . . . . . . . . . . . 15 (𝑢 = 𝑦 → (𝑢𝑤𝑦𝑤))
3836, 37imbi12d 334 . . . . . . . . . . . . . 14 (𝑢 = 𝑦 → (((𝑢𝑤 ∧ Tr 𝑢) → 𝑢𝑤) ↔ ((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤)))
3938cbvalv 2272 . . . . . . . . . . . . 13 (∀𝑢((𝑢𝑤 ∧ Tr 𝑢) → 𝑢𝑤) ↔ ∀𝑦((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤))
4033, 39syl6bb 276 . . . . . . . . . . . 12 (𝑡 = 𝑤 → (∀𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ∀𝑦((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤)))
4140rspccv 3296 . . . . . . . . . . 11 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → (𝑤𝑥 → ∀𝑦((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤)))
4228, 41anim12d 585 . . . . . . . . . 10 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → ((𝑧𝑥𝑤𝑥) → (∀𝑣((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧) ∧ ∀𝑦((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤))))
43 vex 3193 . . . . . . . . . . 11 𝑧 ∈ V
44 vex 3193 . . . . . . . . . . 11 𝑤 ∈ V
4543, 44dfon2lem5 31446 . . . . . . . . . 10 ((∀𝑣((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧) ∧ ∀𝑦((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤)) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
4642, 45syl6 35 . . . . . . . . 9 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → ((𝑧𝑥𝑤𝑥) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧)))
4746ralrimivv 2966 . . . . . . . 8 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
4815, 47jca 554 . . . . . . 7 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → ( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧)))
4914, 48syl 17 . . . . . 6 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧)))
50 dfwe2 6943 . . . . . . 7 ( E We 𝑥 ↔ ( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧 E 𝑤𝑧 = 𝑤𝑤 E 𝑧)))
51 epel 4998 . . . . . . . . . 10 (𝑧 E 𝑤𝑧𝑤)
52 biid 251 . . . . . . . . . 10 (𝑧 = 𝑤𝑧 = 𝑤)
53 epel 4998 . . . . . . . . . 10 (𝑤 E 𝑧𝑤𝑧)
5451, 52, 533orbi123i 1250 . . . . . . . . 9 ((𝑧 E 𝑤𝑧 = 𝑤𝑤 E 𝑧) ↔ (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
55542ralbii 2977 . . . . . . . 8 (∀𝑧𝑥𝑤𝑥 (𝑧 E 𝑤𝑧 = 𝑤𝑤 E 𝑧) ↔ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
5655anbi2i 729 . . . . . . 7 (( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧 E 𝑤𝑧 = 𝑤𝑤 E 𝑧)) ↔ ( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧)))
5750, 56bitri 264 . . . . . 6 ( E We 𝑥 ↔ ( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧)))
5849, 57sylibr 224 . . . . 5 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → E We 𝑥)
59 df-ord 5695 . . . . 5 (Ord 𝑥 ↔ (Tr 𝑥 ∧ E We 𝑥))
6012, 58, 59sylanbrc 697 . . . 4 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → Ord 𝑥)
618, 60impbii 199 . . 3 (Ord 𝑥 ↔ ∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥))
6261abbii 2736 . 2 {𝑥 ∣ Ord 𝑥} = {𝑥 ∣ ∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)}
631, 62eqtri 2643 1 On = {𝑥 ∣ ∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)}
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3o 1035  wal 1478   = wceq 1480  wcel 1987  {cab 2607  wne 2790  wral 2908  Vcvv 3190  wss 3560  wpss 3561   class class class wbr 4623  Tr wtr 4722   E cep 4993   Fr wfr 5040   We wwe 5042  Ord word 5691  Oncon0 5692
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 4751  ax-nul 4759  ax-pr 4877  ax-un 6914
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 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-br 4624  df-opab 4684  df-tr 4723  df-eprel 4995  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-ord 5695  df-on 5696  df-suc 5698
This theorem is referenced by:  dfon3  31694
  Copyright terms: Public domain W3C validator