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 33895
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 6292 . 2 On = {𝑥 ∣ Ord 𝑥}
2 tz7.7 6314 . . . . . . . . 9 ((Ord 𝑥 ∧ Tr 𝑦) → (𝑦𝑥 ↔ (𝑦𝑥𝑦𝑥)))
3 df-pss 3915 . . . . . . . . 9 (𝑦𝑥 ↔ (𝑦𝑥𝑦𝑥))
42, 3bitr4di 288 . . . . . . . 8 ((Ord 𝑥 ∧ Tr 𝑦) → (𝑦𝑥𝑦𝑥))
54exbiri 808 . . . . . . 7 (Ord 𝑥 → (Tr 𝑦 → (𝑦𝑥𝑦𝑥)))
65com23 86 . . . . . 6 (Ord 𝑥 → (𝑦𝑥 → (Tr 𝑦𝑦𝑥)))
76impd 411 . . . . 5 (Ord 𝑥 → ((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥))
87alrimiv 1929 . . . 4 (Ord 𝑥 → ∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥))
9 vex 3444 . . . . . . 7 𝑥 ∈ V
10 dfon2lem3 33888 . . . . . . 7 (𝑥 ∈ V → (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (Tr 𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧𝑧)))
119, 10ax-mp 5 . . . . . 6 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (Tr 𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧𝑧))
1211simpld 495 . . . . 5 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → Tr 𝑥)
139dfon2lem7 33892 . . . . . . . 8 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (𝑡𝑥 → ∀𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡)))
1413ralrimiv 3138 . . . . . . 7 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡))
15 dfon2lem9 33894 . . . . . . . 8 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → E Fr 𝑥)
16 psseq2 4033 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑧 → (𝑢𝑡𝑢𝑧))
1716anbi1d 630 . . . . . . . . . . . . . . 15 (𝑡 = 𝑧 → ((𝑢𝑡 ∧ Tr 𝑢) ↔ (𝑢𝑧 ∧ Tr 𝑢)))
18 elequ2 2120 . . . . . . . . . . . . . . 15 (𝑡 = 𝑧 → (𝑢𝑡𝑢𝑧))
1917, 18imbi12d 344 . . . . . . . . . . . . . 14 (𝑡 = 𝑧 → (((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ((𝑢𝑧 ∧ Tr 𝑢) → 𝑢𝑧)))
2019albidv 1922 . . . . . . . . . . . . 13 (𝑡 = 𝑧 → (∀𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ∀𝑢((𝑢𝑧 ∧ Tr 𝑢) → 𝑢𝑧)))
21 psseq1 4032 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑣 → (𝑢𝑧𝑣𝑧))
22 treq 5211 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑣 → (Tr 𝑢 ↔ Tr 𝑣))
2321, 22anbi12d 631 . . . . . . . . . . . . . . 15 (𝑢 = 𝑣 → ((𝑢𝑧 ∧ Tr 𝑢) ↔ (𝑣𝑧 ∧ Tr 𝑣)))
24 elequ1 2112 . . . . . . . . . . . . . . 15 (𝑢 = 𝑣 → (𝑢𝑧𝑣𝑧))
2523, 24imbi12d 344 . . . . . . . . . . . . . 14 (𝑢 = 𝑣 → (((𝑢𝑧 ∧ Tr 𝑢) → 𝑢𝑧) ↔ ((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧)))
2625cbvalvw 2038 . . . . . . . . . . . . 13 (∀𝑢((𝑢𝑧 ∧ Tr 𝑢) → 𝑢𝑧) ↔ ∀𝑣((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧))
2720, 26bitrdi 286 . . . . . . . . . . . 12 (𝑡 = 𝑧 → (∀𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ∀𝑣((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧)))
2827rspccv 3566 . . . . . . . . . . 11 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → (𝑧𝑥 → ∀𝑣((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧)))
29 psseq2 4033 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑤 → (𝑢𝑡𝑢𝑤))
3029anbi1d 630 . . . . . . . . . . . . . . 15 (𝑡 = 𝑤 → ((𝑢𝑡 ∧ Tr 𝑢) ↔ (𝑢𝑤 ∧ Tr 𝑢)))
31 elequ2 2120 . . . . . . . . . . . . . . 15 (𝑡 = 𝑤 → (𝑢𝑡𝑢𝑤))
3230, 31imbi12d 344 . . . . . . . . . . . . . 14 (𝑡 = 𝑤 → (((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ((𝑢𝑤 ∧ Tr 𝑢) → 𝑢𝑤)))
3332albidv 1922 . . . . . . . . . . . . 13 (𝑡 = 𝑤 → (∀𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ∀𝑢((𝑢𝑤 ∧ Tr 𝑢) → 𝑢𝑤)))
34 psseq1 4032 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑦 → (𝑢𝑤𝑦𝑤))
35 treq 5211 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑦 → (Tr 𝑢 ↔ Tr 𝑦))
3634, 35anbi12d 631 . . . . . . . . . . . . . . 15 (𝑢 = 𝑦 → ((𝑢𝑤 ∧ Tr 𝑢) ↔ (𝑦𝑤 ∧ Tr 𝑦)))
37 elequ1 2112 . . . . . . . . . . . . . . 15 (𝑢 = 𝑦 → (𝑢𝑤𝑦𝑤))
3836, 37imbi12d 344 . . . . . . . . . . . . . 14 (𝑢 = 𝑦 → (((𝑢𝑤 ∧ Tr 𝑢) → 𝑢𝑤) ↔ ((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤)))
3938cbvalvw 2038 . . . . . . . . . . . . 13 (∀𝑢((𝑢𝑤 ∧ Tr 𝑢) → 𝑢𝑤) ↔ ∀𝑦((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤))
4033, 39bitrdi 286 . . . . . . . . . . . 12 (𝑡 = 𝑤 → (∀𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ∀𝑦((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤)))
4140rspccv 3566 . . . . . . . . . . 11 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → (𝑤𝑥 → ∀𝑦((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤)))
4228, 41anim12d 609 . . . . . . . . . 10 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → ((𝑧𝑥𝑤𝑥) → (∀𝑣((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧) ∧ ∀𝑦((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤))))
43 vex 3444 . . . . . . . . . . 11 𝑧 ∈ V
44 vex 3444 . . . . . . . . . . 11 𝑤 ∈ V
4543, 44dfon2lem5 33890 . . . . . . . . . 10 ((∀𝑣((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧) ∧ ∀𝑦((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤)) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
4642, 45syl6 35 . . . . . . . . 9 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → ((𝑧𝑥𝑤𝑥) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧)))
4746ralrimivv 3191 . . . . . . . 8 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
4815, 47jca 512 . . . . . . 7 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → ( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧)))
4914, 48syl 17 . . . . . 6 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧)))
50 dfwe2 7665 . . . . . . 7 ( E We 𝑥 ↔ ( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧 E 𝑤𝑧 = 𝑤𝑤 E 𝑧)))
51 epel 5515 . . . . . . . . . 10 (𝑧 E 𝑤𝑧𝑤)
52 biid 260 . . . . . . . . . 10 (𝑧 = 𝑤𝑧 = 𝑤)
53 epel 5515 . . . . . . . . . 10 (𝑤 E 𝑧𝑤𝑧)
5451, 52, 533orbi123i 1155 . . . . . . . . 9 ((𝑧 E 𝑤𝑧 = 𝑤𝑤 E 𝑧) ↔ (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
55542ralbii 3123 . . . . . . . 8 (∀𝑧𝑥𝑤𝑥 (𝑧 E 𝑤𝑧 = 𝑤𝑤 E 𝑧) ↔ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
5655anbi2i 623 . . . . . . 7 (( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧 E 𝑤𝑧 = 𝑤𝑤 E 𝑧)) ↔ ( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧)))
5750, 56bitri 274 . . . . . 6 ( E We 𝑥 ↔ ( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧)))
5849, 57sylibr 233 . . . . 5 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → E We 𝑥)
59 df-ord 6291 . . . . 5 (Ord 𝑥 ↔ (Tr 𝑥 ∧ E We 𝑥))
6012, 58, 59sylanbrc 583 . . . 4 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → Ord 𝑥)
618, 60impbii 208 . . 3 (Ord 𝑥 ↔ ∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥))
6261abbii 2806 . 2 {𝑥 ∣ Ord 𝑥} = {𝑥 ∣ ∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)}
631, 62eqtri 2764 1 On = {𝑥 ∣ ∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)}
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3o 1085  wal 1538   = wceq 1540  wcel 2105  {cab 2713  wne 2940  wral 3061  Vcvv 3440  wss 3896  wpss 3897   class class class wbr 5086  Tr wtr 5203   E cep 5511   Fr wfr 5559   We wwe 5561  Ord word 6287  Oncon0 6288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pr 5366  ax-un 7629
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3442  df-sbc 3726  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4850  df-int 4892  df-iun 4938  df-iin 4939  df-br 5087  df-opab 5149  df-tr 5204  df-eprel 5512  df-po 5520  df-so 5521  df-fr 5562  df-we 5564  df-ord 6291  df-on 6292  df-suc 6294
This theorem is referenced by:  dfon3  34264
  Copyright terms: Public domain W3C validator