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

Theorem cardsdomel 9133
Description: A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of [TakeutiZaring] p. 93. (Contributed by Mario Carneiro, 15-Jan-2013.) (Revised by Mario Carneiro, 4-Jun-2015.)
Assertion
Ref Expression
cardsdomel ((𝐴 ∈ On ∧ 𝐵 ∈ dom card) → (𝐴𝐵𝐴 ∈ (card‘𝐵)))

Proof of Theorem cardsdomel
StepHypRef Expression
1 cardid2 9112 . . . . . . 7 (𝐵 ∈ dom card → (card‘𝐵) ≈ 𝐵)
21ensymd 8292 . . . . . 6 (𝐵 ∈ dom card → 𝐵 ≈ (card‘𝐵))
3 sdomentr 8382 . . . . . 6 ((𝐴𝐵𝐵 ≈ (card‘𝐵)) → 𝐴 ≺ (card‘𝐵))
42, 3sylan2 586 . . . . 5 ((𝐴𝐵𝐵 ∈ dom card) → 𝐴 ≺ (card‘𝐵))
5 ssdomg 8287 . . . . . . . 8 (𝐴 ∈ On → ((card‘𝐵) ⊆ 𝐴 → (card‘𝐵) ≼ 𝐴))
6 cardon 9103 . . . . . . . . 9 (card‘𝐵) ∈ On
7 domtriord 8394 . . . . . . . . 9 (((card‘𝐵) ∈ On ∧ 𝐴 ∈ On) → ((card‘𝐵) ≼ 𝐴 ↔ ¬ 𝐴 ≺ (card‘𝐵)))
86, 7mpan 680 . . . . . . . 8 (𝐴 ∈ On → ((card‘𝐵) ≼ 𝐴 ↔ ¬ 𝐴 ≺ (card‘𝐵)))
95, 8sylibd 231 . . . . . . 7 (𝐴 ∈ On → ((card‘𝐵) ⊆ 𝐴 → ¬ 𝐴 ≺ (card‘𝐵)))
109con2d 132 . . . . . 6 (𝐴 ∈ On → (𝐴 ≺ (card‘𝐵) → ¬ (card‘𝐵) ⊆ 𝐴))
11 ontri1 6010 . . . . . . . 8 (((card‘𝐵) ∈ On ∧ 𝐴 ∈ On) → ((card‘𝐵) ⊆ 𝐴 ↔ ¬ 𝐴 ∈ (card‘𝐵)))
126, 11mpan 680 . . . . . . 7 (𝐴 ∈ On → ((card‘𝐵) ⊆ 𝐴 ↔ ¬ 𝐴 ∈ (card‘𝐵)))
1312con2bid 346 . . . . . 6 (𝐴 ∈ On → (𝐴 ∈ (card‘𝐵) ↔ ¬ (card‘𝐵) ⊆ 𝐴))
1410, 13sylibrd 251 . . . . 5 (𝐴 ∈ On → (𝐴 ≺ (card‘𝐵) → 𝐴 ∈ (card‘𝐵)))
154, 14syl5 34 . . . 4 (𝐴 ∈ On → ((𝐴𝐵𝐵 ∈ dom card) → 𝐴 ∈ (card‘𝐵)))
1615expcomd 408 . . 3 (𝐴 ∈ On → (𝐵 ∈ dom card → (𝐴𝐵𝐴 ∈ (card‘𝐵))))
1716imp 397 . 2 ((𝐴 ∈ On ∧ 𝐵 ∈ dom card) → (𝐴𝐵𝐴 ∈ (card‘𝐵)))
18 cardsdomelir 9132 . 2 (𝐴 ∈ (card‘𝐵) → 𝐴𝐵)
1917, 18impbid1 217 1 ((𝐴 ∈ On ∧ 𝐵 ∈ dom card) → (𝐴𝐵𝐴 ∈ (card‘𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wcel 2106  wss 3791   class class class wbr 4886  dom cdm 5355  Oncon0 5976  cfv 6135  cen 8238  cdom 8239  csdm 8240  cardccrd 9094
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-sbc 3652  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-int 4711  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-ord 5979  df-on 5980  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-card 9098
This theorem is referenced by:  iscard  9134  cardval2  9150  infxpenlem  9169  alephnbtwn  9227  alephnbtwn2  9228  alephord2  9232  alephsdom  9242  pwsdompw  9361  inaprc  9993
  Copyright terms: Public domain W3C validator