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

Theorem dfon2 30941
 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 5644 . 2 On = {𝑥 ∣ Ord 𝑥}
2 tz7.7 5666 . . . . . . . . 9 ((Ord 𝑥 ∧ Tr 𝑦) → (𝑦𝑥 ↔ (𝑦𝑥𝑦𝑥)))
3 df-pss 3556 . . . . . . . . 9 (𝑦𝑥 ↔ (𝑦𝑥𝑦𝑥))
42, 3syl6bbr 277 . . . . . . . 8 ((Ord 𝑥 ∧ Tr 𝑦) → (𝑦𝑥𝑦𝑥))
54exbiri 650 . . . . . . 7 (Ord 𝑥 → (Tr 𝑦 → (𝑦𝑥𝑦𝑥)))
65com23 84 . . . . . 6 (Ord 𝑥 → (𝑦𝑥 → (Tr 𝑦𝑦𝑥)))
76impd 446 . . . . 5 (Ord 𝑥 → ((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥))
87alrimiv 1842 . . . 4 (Ord 𝑥 → ∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥))
9 vex 3176 . . . . . . 7 𝑥 ∈ V
10 dfon2lem3 30934 . . . . . . 7 (𝑥 ∈ V → (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (Tr 𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧𝑧)))
119, 10ax-mp 5 . . . . . 6 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (Tr 𝑥 ∧ ∀𝑧𝑥 ¬ 𝑧𝑧))
1211simpld 474 . . . . 5 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → Tr 𝑥)
139dfon2lem7 30938 . . . . . . . 8 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → (𝑡𝑥 → ∀𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡)))
1413ralrimiv 2948 . . . . . . 7 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡))
15 dfon2lem9 30940 . . . . . . . 8 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → E Fr 𝑥)
16 psseq2 3657 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑧 → (𝑢𝑡𝑢𝑧))
1716anbi1d 737 . . . . . . . . . . . . . . 15 (𝑡 = 𝑧 → ((𝑢𝑡 ∧ Tr 𝑢) ↔ (𝑢𝑧 ∧ Tr 𝑢)))
18 elequ2 1991 . . . . . . . . . . . . . . 15 (𝑡 = 𝑧 → (𝑢𝑡𝑢𝑧))
1917, 18imbi12d 333 . . . . . . . . . . . . . 14 (𝑡 = 𝑧 → (((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ((𝑢𝑧 ∧ Tr 𝑢) → 𝑢𝑧)))
2019albidv 1836 . . . . . . . . . . . . 13 (𝑡 = 𝑧 → (∀𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ∀𝑢((𝑢𝑧 ∧ Tr 𝑢) → 𝑢𝑧)))
21 psseq1 3656 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑣 → (𝑢𝑧𝑣𝑧))
22 treq 4686 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑣 → (Tr 𝑢 ↔ Tr 𝑣))
2321, 22anbi12d 743 . . . . . . . . . . . . . . 15 (𝑢 = 𝑣 → ((𝑢𝑧 ∧ Tr 𝑢) ↔ (𝑣𝑧 ∧ Tr 𝑣)))
24 elequ1 1984 . . . . . . . . . . . . . . 15 (𝑢 = 𝑣 → (𝑢𝑧𝑣𝑧))
2523, 24imbi12d 333 . . . . . . . . . . . . . 14 (𝑢 = 𝑣 → (((𝑢𝑧 ∧ Tr 𝑢) → 𝑢𝑧) ↔ ((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧)))
2625cbvalv 2261 . . . . . . . . . . . . 13 (∀𝑢((𝑢𝑧 ∧ Tr 𝑢) → 𝑢𝑧) ↔ ∀𝑣((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧))
2720, 26syl6bb 275 . . . . . . . . . . . 12 (𝑡 = 𝑧 → (∀𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ∀𝑣((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧)))
2827rspccv 3279 . . . . . . . . . . 11 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → (𝑧𝑥 → ∀𝑣((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧)))
29 psseq2 3657 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑤 → (𝑢𝑡𝑢𝑤))
3029anbi1d 737 . . . . . . . . . . . . . . 15 (𝑡 = 𝑤 → ((𝑢𝑡 ∧ Tr 𝑢) ↔ (𝑢𝑤 ∧ Tr 𝑢)))
31 elequ2 1991 . . . . . . . . . . . . . . 15 (𝑡 = 𝑤 → (𝑢𝑡𝑢𝑤))
3230, 31imbi12d 333 . . . . . . . . . . . . . 14 (𝑡 = 𝑤 → (((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ((𝑢𝑤 ∧ Tr 𝑢) → 𝑢𝑤)))
3332albidv 1836 . . . . . . . . . . . . 13 (𝑡 = 𝑤 → (∀𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ∀𝑢((𝑢𝑤 ∧ Tr 𝑢) → 𝑢𝑤)))
34 psseq1 3656 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑦 → (𝑢𝑤𝑦𝑤))
35 treq 4686 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑦 → (Tr 𝑢 ↔ Tr 𝑦))
3634, 35anbi12d 743 . . . . . . . . . . . . . . 15 (𝑢 = 𝑦 → ((𝑢𝑤 ∧ Tr 𝑢) ↔ (𝑦𝑤 ∧ Tr 𝑦)))
37 elequ1 1984 . . . . . . . . . . . . . . 15 (𝑢 = 𝑦 → (𝑢𝑤𝑦𝑤))
3836, 37imbi12d 333 . . . . . . . . . . . . . 14 (𝑢 = 𝑦 → (((𝑢𝑤 ∧ Tr 𝑢) → 𝑢𝑤) ↔ ((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤)))
3938cbvalv 2261 . . . . . . . . . . . . 13 (∀𝑢((𝑢𝑤 ∧ Tr 𝑢) → 𝑢𝑤) ↔ ∀𝑦((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤))
4033, 39syl6bb 275 . . . . . . . . . . . 12 (𝑡 = 𝑤 → (∀𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) ↔ ∀𝑦((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤)))
4140rspccv 3279 . . . . . . . . . . 11 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → (𝑤𝑥 → ∀𝑦((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤)))
4228, 41anim12d 584 . . . . . . . . . 10 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → ((𝑧𝑥𝑤𝑥) → (∀𝑣((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧) ∧ ∀𝑦((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤))))
43 vex 3176 . . . . . . . . . . 11 𝑧 ∈ V
44 vex 3176 . . . . . . . . . . 11 𝑤 ∈ V
4543, 44dfon2lem5 30936 . . . . . . . . . 10 ((∀𝑣((𝑣𝑧 ∧ Tr 𝑣) → 𝑣𝑧) ∧ ∀𝑦((𝑦𝑤 ∧ Tr 𝑦) → 𝑦𝑤)) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
4642, 45syl6 34 . . . . . . . . 9 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → ((𝑧𝑥𝑤𝑥) → (𝑧𝑤𝑧 = 𝑤𝑤𝑧)))
4746ralrimivv 2953 . . . . . . . 8 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
4815, 47jca 553 . . . . . . 7 (∀𝑡𝑥𝑢((𝑢𝑡 ∧ Tr 𝑢) → 𝑢𝑡) → ( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧)))
4914, 48syl 17 . . . . . 6 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → ( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧)))
50 dfwe2 6873 . . . . . . 7 ( E We 𝑥 ↔ ( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧 E 𝑤𝑧 = 𝑤𝑤 E 𝑧)))
51 epel 4952 . . . . . . . . . 10 (𝑧 E 𝑤𝑧𝑤)
52 biid 250 . . . . . . . . . 10 (𝑧 = 𝑤𝑧 = 𝑤)
53 epel 4952 . . . . . . . . . 10 (𝑤 E 𝑧𝑤𝑧)
5451, 52, 533orbi123i 1245 . . . . . . . . 9 ((𝑧 E 𝑤𝑧 = 𝑤𝑤 E 𝑧) ↔ (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
55542ralbii 2964 . . . . . . . 8 (∀𝑧𝑥𝑤𝑥 (𝑧 E 𝑤𝑧 = 𝑤𝑤 E 𝑧) ↔ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧))
5655anbi2i 726 . . . . . . 7 (( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧 E 𝑤𝑧 = 𝑤𝑤 E 𝑧)) ↔ ( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧)))
5750, 56bitri 263 . . . . . 6 ( E We 𝑥 ↔ ( E Fr 𝑥 ∧ ∀𝑧𝑥𝑤𝑥 (𝑧𝑤𝑧 = 𝑤𝑤𝑧)))
5849, 57sylibr 223 . . . . 5 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → E We 𝑥)
59 df-ord 5643 . . . . 5 (Ord 𝑥 ↔ (Tr 𝑥 ∧ E We 𝑥))
6012, 58, 59sylanbrc 695 . . . 4 (∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥) → Ord 𝑥)
618, 60impbii 198 . . 3 (Ord 𝑥 ↔ ∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥))
6261abbii 2726 . 2 {𝑥 ∣ Ord 𝑥} = {𝑥 ∣ ∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)}
631, 62eqtri 2632 1 On = {𝑥 ∣ ∀𝑦((𝑦𝑥 ∧ Tr 𝑦) → 𝑦𝑥)}
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∨ w3o 1030  ∀wal 1473   = wceq 1475   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  Vcvv 3173   ⊆ wss 3540   ⊊ wpss 3541   class class class wbr 4583  Tr wtr 4680   E cep 4947   Fr wfr 4994   We wwe 4996  Ord word 5639  Oncon0 5640 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-ord 5643  df-on 5644  df-suc 5646 This theorem is referenced by:  dfon3  31169
 Copyright terms: Public domain W3C validator