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

Theorem isnumi 8366
Description: A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
Assertion
Ref Expression
isnumi  |-  ( ( A  e.  On  /\  A  ~~  B )  ->  B  e.  dom  card )

Proof of Theorem isnumi
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 breq1 4376 . . 3  |-  ( x  =  A  ->  (
x  ~~  B  <->  A  ~~  B ) )
21rspcev 3117 . 2  |-  ( ( A  e.  On  /\  A  ~~  B )  ->  E. x  e.  On  x  ~~  B )
3 isnum2 8365 . 2  |-  ( B  e.  dom  card  <->  E. x  e.  On  x  ~~  B
)
42, 3sylibr 217 1  |-  ( ( A  e.  On  /\  A  ~~  B )  ->  B  e.  dom  card )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    e. wcel 1890   E.wrex 2737   class class class wbr 4373   dom cdm 4811   Oncon0 5401    ~~ cen 7552   cardccrd 8355
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pr 4611  ax-un 6570
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3014  df-sbc 3235  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-pss 3387  df-nul 3699  df-if 3849  df-sn 3936  df-pr 3938  df-tp 3940  df-op 3942  df-uni 4168  df-int 4204  df-br 4374  df-opab 4433  df-mpt 4434  df-tr 4469  df-eprel 4722  df-id 4726  df-po 4732  df-so 4733  df-fr 4770  df-we 4772  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-ord 5404  df-on 5405  df-fun 5562  df-fn 5563  df-f 5564  df-en 7556  df-card 8359
This theorem is referenced by:  finnum  8368  onenon  8369  tskwe  8370  xpnum  8371  isnum3  8374  dfac8alem  8446  cdanum  8615  fin67  8811  isfin7-2  8812  gch2  9086  gchacg  9091  znnen  14275  qnnen  14276  met1stc  21546  re2ndc  21829  uniiccdif  22546  dyadmbl  22569  opnmblALT  22572  mbfimaopnlem  22622  aannenlem3  23297  poimirlem32  31973
  Copyright terms: Public domain W3C validator