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

Theorem cardcf 10188
Description: Cofinality is a cardinal number. Proposition 11.11 of [TakeutiZaring] p. 103. (Contributed by NM, 24-Apr-2004.) (Revised by Mario Carneiro, 15-Sep-2013.)
Assertion
Ref Expression
cardcf (cardβ€˜(cfβ€˜π΄)) = (cfβ€˜π΄)

Proof of Theorem cardcf
Dummy variables π‘₯ 𝑦 𝑧 𝑀 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cfval 10183 . . . 4 (𝐴 ∈ On β†’ (cfβ€˜π΄) = ∩ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))})
2 vex 3449 . . . . . . . . 9 𝑣 ∈ V
3 eqeq1 2740 . . . . . . . . . . 11 (π‘₯ = 𝑣 β†’ (π‘₯ = (cardβ€˜π‘¦) ↔ 𝑣 = (cardβ€˜π‘¦)))
43anbi1d 630 . . . . . . . . . 10 (π‘₯ = 𝑣 β†’ ((π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀)) ↔ (𝑣 = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))))
54exbidv 1924 . . . . . . . . 9 (π‘₯ = 𝑣 β†’ (βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀)) ↔ βˆƒπ‘¦(𝑣 = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))))
62, 5elab 3630 . . . . . . . 8 (𝑣 ∈ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))} ↔ βˆƒπ‘¦(𝑣 = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀)))
7 fveq2 6842 . . . . . . . . . . . 12 (𝑣 = (cardβ€˜π‘¦) β†’ (cardβ€˜π‘£) = (cardβ€˜(cardβ€˜π‘¦)))
8 cardidm 9895 . . . . . . . . . . . 12 (cardβ€˜(cardβ€˜π‘¦)) = (cardβ€˜π‘¦)
97, 8eqtrdi 2792 . . . . . . . . . . 11 (𝑣 = (cardβ€˜π‘¦) β†’ (cardβ€˜π‘£) = (cardβ€˜π‘¦))
10 eqeq2 2748 . . . . . . . . . . 11 (𝑣 = (cardβ€˜π‘¦) β†’ ((cardβ€˜π‘£) = 𝑣 ↔ (cardβ€˜π‘£) = (cardβ€˜π‘¦)))
119, 10mpbird 256 . . . . . . . . . 10 (𝑣 = (cardβ€˜π‘¦) β†’ (cardβ€˜π‘£) = 𝑣)
1211adantr 481 . . . . . . . . 9 ((𝑣 = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀)) β†’ (cardβ€˜π‘£) = 𝑣)
1312exlimiv 1933 . . . . . . . 8 (βˆƒπ‘¦(𝑣 = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀)) β†’ (cardβ€˜π‘£) = 𝑣)
146, 13sylbi 216 . . . . . . 7 (𝑣 ∈ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))} β†’ (cardβ€˜π‘£) = 𝑣)
15 cardon 9880 . . . . . . 7 (cardβ€˜π‘£) ∈ On
1614, 15eqeltrrdi 2846 . . . . . 6 (𝑣 ∈ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))} β†’ 𝑣 ∈ On)
1716ssriv 3948 . . . . 5 {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))} βŠ† On
18 fvex 6855 . . . . . . 7 (cfβ€˜π΄) ∈ V
191, 18eqeltrrdi 2846 . . . . . 6 (𝐴 ∈ On β†’ ∩ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))} ∈ V)
20 intex 5294 . . . . . 6 ({π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))} β‰  βˆ… ↔ ∩ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))} ∈ V)
2119, 20sylibr 233 . . . . 5 (𝐴 ∈ On β†’ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))} β‰  βˆ…)
22 onint 7725 . . . . 5 (({π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))} βŠ† On ∧ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))} β‰  βˆ…) β†’ ∩ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))} ∈ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))})
2317, 21, 22sylancr 587 . . . 4 (𝐴 ∈ On β†’ ∩ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))} ∈ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))})
241, 23eqeltrd 2837 . . 3 (𝐴 ∈ On β†’ (cfβ€˜π΄) ∈ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))})
25 fveq2 6842 . . . . 5 (𝑣 = (cfβ€˜π΄) β†’ (cardβ€˜π‘£) = (cardβ€˜(cfβ€˜π΄)))
26 id 22 . . . . 5 (𝑣 = (cfβ€˜π΄) β†’ 𝑣 = (cfβ€˜π΄))
2725, 26eqeq12d 2752 . . . 4 (𝑣 = (cfβ€˜π΄) β†’ ((cardβ€˜π‘£) = 𝑣 ↔ (cardβ€˜(cfβ€˜π΄)) = (cfβ€˜π΄)))
2827, 14vtoclga 3534 . . 3 ((cfβ€˜π΄) ∈ {π‘₯ ∣ βˆƒπ‘¦(π‘₯ = (cardβ€˜π‘¦) ∧ (𝑦 βŠ† 𝐴 ∧ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘€ ∈ 𝑦 𝑧 βŠ† 𝑀))} β†’ (cardβ€˜(cfβ€˜π΄)) = (cfβ€˜π΄))
2924, 28syl 17 . 2 (𝐴 ∈ On β†’ (cardβ€˜(cfβ€˜π΄)) = (cfβ€˜π΄))
30 cff 10184 . . . . . 6 cf:On⟢On
3130fdmi 6680 . . . . 5 dom cf = On
3231eleq2i 2829 . . . 4 (𝐴 ∈ dom cf ↔ 𝐴 ∈ On)
33 ndmfv 6877 . . . 4 (Β¬ 𝐴 ∈ dom cf β†’ (cfβ€˜π΄) = βˆ…)
3432, 33sylnbir 330 . . 3 (Β¬ 𝐴 ∈ On β†’ (cfβ€˜π΄) = βˆ…)
35 card0 9894 . . . 4 (cardβ€˜βˆ…) = βˆ…
36 fveq2 6842 . . . 4 ((cfβ€˜π΄) = βˆ… β†’ (cardβ€˜(cfβ€˜π΄)) = (cardβ€˜βˆ…))
37 id 22 . . . 4 ((cfβ€˜π΄) = βˆ… β†’ (cfβ€˜π΄) = βˆ…)
3835, 36, 373eqtr4a 2802 . . 3 ((cfβ€˜π΄) = βˆ… β†’ (cardβ€˜(cfβ€˜π΄)) = (cfβ€˜π΄))
3934, 38syl 17 . 2 (Β¬ 𝐴 ∈ On β†’ (cardβ€˜(cfβ€˜π΄)) = (cfβ€˜π΄))
4029, 39pm2.61i 182 1 (cardβ€˜(cfβ€˜π΄)) = (cfβ€˜π΄)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   ∧ wa 396   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106  {cab 2713   β‰  wne 2943  βˆ€wral 3064  βˆƒwrex 3073  Vcvv 3445   βŠ† wss 3910  βˆ…c0 4282  βˆ© cint 4907  dom cdm 5633  Oncon0 6317  β€˜cfv 6496  cardccrd 9871  cfccf 9873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-er 8648  df-en 8884  df-card 9875  df-cf 9877
This theorem is referenced by:  cfon  10191  winacard  10628
  Copyright terms: Public domain W3C validator