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

Theorem cardf2 8807
Description: The cardinality function is a function with domain the well-orderable sets. Assuming AC, this is the universe. (Contributed by Mario Carneiro, 6-Jun-2013.) (Revised by Mario Carneiro, 20-Sep-2014.)
Assertion
Ref Expression
cardf2 card:{𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥}⟶On
Distinct variable group:   𝑥,𝑦

Proof of Theorem cardf2
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-card 8803 . . . 4 card = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦𝑥})
21funmpt2 5965 . . 3 Fun card
3 rabab 3254 . . . 4 {𝑥 ∈ V ∣ {𝑦 ∈ On ∣ 𝑦𝑥} ∈ V} = {𝑥 {𝑦 ∈ On ∣ 𝑦𝑥} ∈ V}
41dmmpt 5668 . . . 4 dom card = {𝑥 ∈ V ∣ {𝑦 ∈ On ∣ 𝑦𝑥} ∈ V}
5 intexrab 4853 . . . . 5 (∃𝑦 ∈ On 𝑦𝑥 {𝑦 ∈ On ∣ 𝑦𝑥} ∈ V)
65abbii 2768 . . . 4 {𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥} = {𝑥 {𝑦 ∈ On ∣ 𝑦𝑥} ∈ V}
73, 4, 63eqtr4i 2683 . . 3 dom card = {𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥}
8 df-fn 5929 . . 3 (card Fn {𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥} ↔ (Fun card ∧ dom card = {𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥}))
92, 7, 8mpbir2an 975 . 2 card Fn {𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥}
10 simpr 476 . . . . . . . . 9 ((𝑧 ∈ V ∧ 𝑤 = {𝑦 ∈ On ∣ 𝑦𝑧}) → 𝑤 = {𝑦 ∈ On ∣ 𝑦𝑧})
11 vex 3234 . . . . . . . . 9 𝑤 ∈ V
1210, 11syl6eqelr 2739 . . . . . . . 8 ((𝑧 ∈ V ∧ 𝑤 = {𝑦 ∈ On ∣ 𝑦𝑧}) → {𝑦 ∈ On ∣ 𝑦𝑧} ∈ V)
13 intex 4850 . . . . . . . 8 ({𝑦 ∈ On ∣ 𝑦𝑧} ≠ ∅ ↔ {𝑦 ∈ On ∣ 𝑦𝑧} ∈ V)
1412, 13sylibr 224 . . . . . . 7 ((𝑧 ∈ V ∧ 𝑤 = {𝑦 ∈ On ∣ 𝑦𝑧}) → {𝑦 ∈ On ∣ 𝑦𝑧} ≠ ∅)
15 rabn0 3991 . . . . . . 7 ({𝑦 ∈ On ∣ 𝑦𝑧} ≠ ∅ ↔ ∃𝑦 ∈ On 𝑦𝑧)
1614, 15sylib 208 . . . . . 6 ((𝑧 ∈ V ∧ 𝑤 = {𝑦 ∈ On ∣ 𝑦𝑧}) → ∃𝑦 ∈ On 𝑦𝑧)
17 vex 3234 . . . . . . 7 𝑧 ∈ V
18 breq2 4689 . . . . . . . 8 (𝑥 = 𝑧 → (𝑦𝑥𝑦𝑧))
1918rexbidv 3081 . . . . . . 7 (𝑥 = 𝑧 → (∃𝑦 ∈ On 𝑦𝑥 ↔ ∃𝑦 ∈ On 𝑦𝑧))
2017, 19elab 3382 . . . . . 6 (𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥} ↔ ∃𝑦 ∈ On 𝑦𝑧)
2116, 20sylibr 224 . . . . 5 ((𝑧 ∈ V ∧ 𝑤 = {𝑦 ∈ On ∣ 𝑦𝑧}) → 𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥})
22 ssrab2 3720 . . . . . . 7 {𝑦 ∈ On ∣ 𝑦𝑧} ⊆ On
23 oninton 7042 . . . . . . 7 (({𝑦 ∈ On ∣ 𝑦𝑧} ⊆ On ∧ {𝑦 ∈ On ∣ 𝑦𝑧} ≠ ∅) → {𝑦 ∈ On ∣ 𝑦𝑧} ∈ On)
2422, 14, 23sylancr 696 . . . . . 6 ((𝑧 ∈ V ∧ 𝑤 = {𝑦 ∈ On ∣ 𝑦𝑧}) → {𝑦 ∈ On ∣ 𝑦𝑧} ∈ On)
2510, 24eqeltrd 2730 . . . . 5 ((𝑧 ∈ V ∧ 𝑤 = {𝑦 ∈ On ∣ 𝑦𝑧}) → 𝑤 ∈ On)
2621, 25jca 553 . . . 4 ((𝑧 ∈ V ∧ 𝑤 = {𝑦 ∈ On ∣ 𝑦𝑧}) → (𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥} ∧ 𝑤 ∈ On))
2726ssopab2i 5032 . . 3 {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ V ∧ 𝑤 = {𝑦 ∈ On ∣ 𝑦𝑧})} ⊆ {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥} ∧ 𝑤 ∈ On)}
28 df-card 8803 . . . 4 card = (𝑧 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦𝑧})
29 df-mpt 4763 . . . 4 (𝑧 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦𝑧}) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ V ∧ 𝑤 = {𝑦 ∈ On ∣ 𝑦𝑧})}
3028, 29eqtri 2673 . . 3 card = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ V ∧ 𝑤 = {𝑦 ∈ On ∣ 𝑦𝑧})}
31 df-xp 5149 . . 3 ({𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥} × On) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥} ∧ 𝑤 ∈ On)}
3227, 30, 313sstr4i 3677 . 2 card ⊆ ({𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥} × On)
33 dff2 6411 . 2 (card:{𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥}⟶On ↔ (card Fn {𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥} ∧ card ⊆ ({𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥} × On)))
349, 32, 33mpbir2an 975 1 card:{𝑥 ∣ ∃𝑦 ∈ On 𝑦𝑥}⟶On
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1523  wcel 2030  {cab 2637  wne 2823  wrex 2942  {crab 2945  Vcvv 3231  wss 3607  c0 3948   cint 4507   class class class wbr 4685  {copab 4745  cmpt 4762   × cxp 5141  dom cdm 5143  Oncon0 5761  Fun wfun 5920   Fn wfn 5921  wf 5922  cen 7994  cardccrd 8799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-ord 5764  df-on 5765  df-fun 5928  df-fn 5929  df-f 5930  df-card 8803
This theorem is referenced by:  cardon  8808  isnum2  8809  cardf  9410  smobeth  9446  hashkf  13159  hashgval  13160
  Copyright terms: Public domain W3C validator