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

Theorem ondomon 9073
Description: The collection of ordinal numbers dominated by a set is an ordinal number. (In general, not all collections of ordinal numbers are ordinal.) Theorem 56 of [Suppes] p. 227. This theorem can be proved (with a longer proof) without the Axiom of Choice; see hartogs 8142. (Contributed by NM, 7-Nov-2003.) (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
ondomon (𝐴𝑉 → {𝑥 ∈ On ∣ 𝑥𝐴} ∈ On)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem ondomon
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 onelon 5499 . . . . . . . . . . . 12 ((𝑧 ∈ On ∧ 𝑦𝑧) → 𝑦 ∈ On)
2 vex 3069 . . . . . . . . . . . . 13 𝑧 ∈ V
3 onelss 5516 . . . . . . . . . . . . . 14 (𝑧 ∈ On → (𝑦𝑧𝑦𝑧))
43imp 438 . . . . . . . . . . . . 13 ((𝑧 ∈ On ∧ 𝑦𝑧) → 𝑦𝑧)
5 ssdomg 7698 . . . . . . . . . . . . 13 (𝑧 ∈ V → (𝑦𝑧𝑦𝑧))
62, 4, 5mpsyl 65 . . . . . . . . . . . 12 ((𝑧 ∈ On ∧ 𝑦𝑧) → 𝑦𝑧)
71, 6jca 547 . . . . . . . . . . 11 ((𝑧 ∈ On ∧ 𝑦𝑧) → (𝑦 ∈ On ∧ 𝑦𝑧))
8 domtr 7706 . . . . . . . . . . . . 13 ((𝑦𝑧𝑧𝐴) → 𝑦𝐴)
98anim2i 585 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ (𝑦𝑧𝑧𝐴)) → (𝑦 ∈ On ∧ 𝑦𝐴))
109anassrs 669 . . . . . . . . . . 11 (((𝑦 ∈ On ∧ 𝑦𝑧) ∧ 𝑧𝐴) → (𝑦 ∈ On ∧ 𝑦𝐴))
117, 10sylan 481 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑦𝑧) ∧ 𝑧𝐴) → (𝑦 ∈ On ∧ 𝑦𝐴))
1211exp31 621 . . . . . . . . 9 (𝑧 ∈ On → (𝑦𝑧 → (𝑧𝐴 → (𝑦 ∈ On ∧ 𝑦𝐴))))
1312com12 32 . . . . . . . 8 (𝑦𝑧 → (𝑧 ∈ On → (𝑧𝐴 → (𝑦 ∈ On ∧ 𝑦𝐴))))
1413impd 440 . . . . . . 7 (𝑦𝑧 → ((𝑧 ∈ On ∧ 𝑧𝐴) → (𝑦 ∈ On ∧ 𝑦𝐴)))
15 breq1 4437 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
1615elrab 3220 . . . . . . 7 (𝑧 ∈ {𝑥 ∈ On ∣ 𝑥𝐴} ↔ (𝑧 ∈ On ∧ 𝑧𝐴))
17 breq1 4437 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
1817elrab 3220 . . . . . . 7 (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥𝐴} ↔ (𝑦 ∈ On ∧ 𝑦𝐴))
1914, 16, 183imtr4g 280 . . . . . 6 (𝑦𝑧 → (𝑧 ∈ {𝑥 ∈ On ∣ 𝑥𝐴} → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥𝐴}))
2019imp 438 . . . . 5 ((𝑦𝑧𝑧 ∈ {𝑥 ∈ On ∣ 𝑥𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥𝐴})
2120gen2 1699 . . . 4 𝑦𝑧((𝑦𝑧𝑧 ∈ {𝑥 ∈ On ∣ 𝑥𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥𝐴})
22 dftr2 4532 . . . 4 (Tr {𝑥 ∈ On ∣ 𝑥𝐴} ↔ ∀𝑦𝑧((𝑦𝑧𝑧 ∈ {𝑥 ∈ On ∣ 𝑥𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥𝐴}))
2321, 22mpbir 216 . . 3 Tr {𝑥 ∈ On ∣ 𝑥𝐴}
24 ssrab2 3536 . . 3 {𝑥 ∈ On ∣ 𝑥𝐴} ⊆ On
25 ordon 6686 . . 3 Ord On
26 trssord 5491 . . 3 ((Tr {𝑥 ∈ On ∣ 𝑥𝐴} ∧ {𝑥 ∈ On ∣ 𝑥𝐴} ⊆ On ∧ Ord On) → Ord {𝑥 ∈ On ∣ 𝑥𝐴})
2723, 24, 25, 26mp3an 1406 . 2 Ord {𝑥 ∈ On ∣ 𝑥𝐴}
28 elex 3075 . . . . . 6 (𝐴𝑉𝐴 ∈ V)
29 canth2g 7810 . . . . . . . . 9 (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
30 domsdomtr 7791 . . . . . . . . 9 ((𝑥𝐴𝐴 ≺ 𝒫 𝐴) → 𝑥 ≺ 𝒫 𝐴)
3129, 30sylan2 484 . . . . . . . 8 ((𝑥𝐴𝐴 ∈ V) → 𝑥 ≺ 𝒫 𝐴)
3231expcom 444 . . . . . . 7 (𝐴 ∈ V → (𝑥𝐴𝑥 ≺ 𝒫 𝐴))
3332ralrimivw 2845 . . . . . 6 (𝐴 ∈ V → ∀𝑥 ∈ On (𝑥𝐴𝑥 ≺ 𝒫 𝐴))
3428, 33syl 17 . . . . 5 (𝐴𝑉 → ∀𝑥 ∈ On (𝑥𝐴𝑥 ≺ 𝒫 𝐴))
35 ss2rab 3527 . . . . 5 ({𝑥 ∈ On ∣ 𝑥𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ↔ ∀𝑥 ∈ On (𝑥𝐴𝑥 ≺ 𝒫 𝐴))
3634, 35sylibr 219 . . . 4 (𝐴𝑉 → {𝑥 ∈ On ∣ 𝑥𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴})
37 pwexg 4626 . . . . . 6 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
38 numth3 8985 . . . . . 6 (𝒫 𝐴 ∈ V → 𝒫 𝐴 ∈ dom card)
39 cardval2 8510 . . . . . 6 (𝒫 𝐴 ∈ dom card → (card‘𝒫 𝐴) = {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴})
4037, 38, 393syl 18 . . . . 5 (𝐴𝑉 → (card‘𝒫 𝐴) = {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴})
41 fvex 5937 . . . . 5 (card‘𝒫 𝐴) ∈ V
4240, 41syl6eqelr 2592 . . . 4 (𝐴𝑉 → {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ∈ V)
43 ssexg 4582 . . . 4 (({𝑥 ∈ On ∣ 𝑥𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ∧ {𝑥 ∈ On ∣ 𝑥 ≺ 𝒫 𝐴} ∈ V) → {𝑥 ∈ On ∣ 𝑥𝐴} ∈ V)
4436, 42, 43syl2anc 682 . . 3 (𝐴𝑉 → {𝑥 ∈ On ∣ 𝑥𝐴} ∈ V)
45 elong 5482 . . 3 ({𝑥 ∈ On ∣ 𝑥𝐴} ∈ V → ({𝑥 ∈ On ∣ 𝑥𝐴} ∈ On ↔ Ord {𝑥 ∈ On ∣ 𝑥𝐴}))
4644, 45syl 17 . 2 (𝐴𝑉 → ({𝑥 ∈ On ∣ 𝑥𝐴} ∈ On ↔ Ord {𝑥 ∈ On ∣ 𝑥𝐴}))
4727, 46mpbiri 243 1 (𝐴𝑉 → {𝑥 ∈ On ∣ 𝑥𝐴} ∈ On)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 191  wa 378  wal 1466   = wceq 1468  wcel 1937  wral 2791  {crab 2795  Vcvv 3066  wss 3426  𝒫 cpw 3978   class class class wbr 4434  Tr wtr 4530  dom cdm 4880  Ord word 5473  Oncon0 5474  cfv 5633  cdom 7650  csdm 7651  cardccrd 8454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-rep 4548  ax-sep 4558  ax-nul 4567  ax-pow 4619  ax-pr 4680  ax-un 6659  ax-ac2 8978
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3068  df-sbc 3292  df-csb 3386  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-int 4265  df-iun 4309  df-br 4435  df-opab 4494  df-mpt 4495  df-tr 4531  df-eprel 4791  df-id 4795  df-po 4801  df-so 4802  df-fr 4839  df-se 4840  df-we 4841  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-pred 5431  df-ord 5477  df-on 5478  df-suc 5480  df-iota 5597  df-fun 5635  df-fn 5636  df-f 5637  df-f1 5638  df-fo 5639  df-f1o 5640  df-fv 5641  df-isom 5642  df-riota 6325  df-wrecs 7105  df-recs 7167  df-er 7440  df-en 7653  df-dom 7654  df-sdom 7655  df-card 8458  df-ac 8632
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator