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

Theorem cfeq0 9330
Description: Only the ordinal zero has cofinality zero. (Contributed by NM, 24-Apr-2004.) (Revised by Mario Carneiro, 12-Feb-2013.)
Assertion
Ref Expression
cfeq0 (𝐴 ∈ On → ((cf‘𝐴) = ∅ ↔ 𝐴 = ∅))

Proof of Theorem cfeq0
Dummy variables 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cfval 9321 . . . 4 (𝐴 ∈ On → (cf‘𝐴) = {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))})
21eqeq1d 2766 . . 3 (𝐴 ∈ On → ((cf‘𝐴) = ∅ ↔ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))} = ∅))
3 vex 3352 . . . . . . . . 9 𝑣 ∈ V
4 eqeq1 2768 . . . . . . . . . . 11 (𝑥 = 𝑣 → (𝑥 = (card‘𝑦) ↔ 𝑣 = (card‘𝑦)))
54anbi1d 623 . . . . . . . . . 10 (𝑥 = 𝑣 → ((𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)) ↔ (𝑣 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))))
65exbidv 2016 . . . . . . . . 9 (𝑥 = 𝑣 → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)) ↔ ∃𝑦(𝑣 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))))
73, 6elab 3503 . . . . . . . 8 (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))} ↔ ∃𝑦(𝑣 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)))
8 fveq2 6374 . . . . . . . . . . . 12 (𝑣 = (card‘𝑦) → (card‘𝑣) = (card‘(card‘𝑦)))
9 cardidm 9035 . . . . . . . . . . . 12 (card‘(card‘𝑦)) = (card‘𝑦)
108, 9syl6eq 2814 . . . . . . . . . . 11 (𝑣 = (card‘𝑦) → (card‘𝑣) = (card‘𝑦))
11 eqeq2 2775 . . . . . . . . . . 11 (𝑣 = (card‘𝑦) → ((card‘𝑣) = 𝑣 ↔ (card‘𝑣) = (card‘𝑦)))
1210, 11mpbird 248 . . . . . . . . . 10 (𝑣 = (card‘𝑦) → (card‘𝑣) = 𝑣)
1312adantr 472 . . . . . . . . 9 ((𝑣 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)) → (card‘𝑣) = 𝑣)
1413exlimiv 2025 . . . . . . . 8 (∃𝑦(𝑣 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)) → (card‘𝑣) = 𝑣)
157, 14sylbi 208 . . . . . . 7 (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))} → (card‘𝑣) = 𝑣)
16 cardon 9020 . . . . . . 7 (card‘𝑣) ∈ On
1715, 16syl6eqelr 2852 . . . . . 6 (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))} → 𝑣 ∈ On)
1817ssriv 3764 . . . . 5 {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))} ⊆ On
19 onint0 7193 . . . . 5 ({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))} ⊆ On → ( {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))} = ∅ ↔ ∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))}))
2018, 19ax-mp 5 . . . 4 ( {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))} = ∅ ↔ ∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))})
21 0ex 4949 . . . . . 6 ∅ ∈ V
22 eqeq1 2768 . . . . . . . 8 (𝑥 = ∅ → (𝑥 = (card‘𝑦) ↔ ∅ = (card‘𝑦)))
2322anbi1d 623 . . . . . . 7 (𝑥 = ∅ → ((𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)) ↔ (∅ = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))))
2423exbidv 2016 . . . . . 6 (𝑥 = ∅ → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)) ↔ ∃𝑦(∅ = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))))
2521, 24elab 3503 . . . . 5 (∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))} ↔ ∃𝑦(∅ = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)))
26 onss 7187 . . . . . . . . . . 11 (𝐴 ∈ On → 𝐴 ⊆ On)
27 sstr 3768 . . . . . . . . . . . 12 ((𝑦𝐴𝐴 ⊆ On) → 𝑦 ⊆ On)
2827ancoms 450 . . . . . . . . . . 11 ((𝐴 ⊆ On ∧ 𝑦𝐴) → 𝑦 ⊆ On)
2926, 28sylan 575 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝑦𝐴) → 𝑦 ⊆ On)
30293adant2 1161 . . . . . . . . 9 ((𝐴 ∈ On ∧ ∅ = (card‘𝑦) ∧ 𝑦𝐴) → 𝑦 ⊆ On)
31303adant3r 1231 . . . . . . . 8 ((𝐴 ∈ On ∧ ∅ = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)) → 𝑦 ⊆ On)
32 simp2 1167 . . . . . . . 8 ((𝐴 ∈ On ∧ ∅ = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)) → ∅ = (card‘𝑦))
33 simp3 1168 . . . . . . . 8 ((𝐴 ∈ On ∧ ∅ = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)) → (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))
34 eqcom 2771 . . . . . . . . . . . 12 (∅ = (card‘𝑦) ↔ (card‘𝑦) = ∅)
35 vex 3352 . . . . . . . . . . . . . 14 𝑦 ∈ V
36 onssnum 9113 . . . . . . . . . . . . . 14 ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom card)
3735, 36mpan 681 . . . . . . . . . . . . 13 (𝑦 ⊆ On → 𝑦 ∈ dom card)
38 cardnueq0 9040 . . . . . . . . . . . . 13 (𝑦 ∈ dom card → ((card‘𝑦) = ∅ ↔ 𝑦 = ∅))
3937, 38syl 17 . . . . . . . . . . . 12 (𝑦 ⊆ On → ((card‘𝑦) = ∅ ↔ 𝑦 = ∅))
4034, 39syl5bb 274 . . . . . . . . . . 11 (𝑦 ⊆ On → (∅ = (card‘𝑦) ↔ 𝑦 = ∅))
4140biimpa 468 . . . . . . . . . 10 ((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) → 𝑦 = ∅)
42 sseq1 3785 . . . . . . . . . . . 12 (𝑦 = ∅ → (𝑦𝐴 ↔ ∅ ⊆ 𝐴))
43 rexeq 3286 . . . . . . . . . . . . 13 (𝑦 = ∅ → (∃𝑤𝑦 𝑧𝑤 ↔ ∃𝑤 ∈ ∅ 𝑧𝑤))
4443ralbidv 3132 . . . . . . . . . . . 12 (𝑦 = ∅ → (∀𝑧𝐴𝑤𝑦 𝑧𝑤 ↔ ∀𝑧𝐴𝑤 ∈ ∅ 𝑧𝑤))
4542, 44anbi12d 624 . . . . . . . . . . 11 (𝑦 = ∅ → ((𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤) ↔ (∅ ⊆ 𝐴 ∧ ∀𝑧𝐴𝑤 ∈ ∅ 𝑧𝑤)))
4645biimpa 468 . . . . . . . . . 10 ((𝑦 = ∅ ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)) → (∅ ⊆ 𝐴 ∧ ∀𝑧𝐴𝑤 ∈ ∅ 𝑧𝑤))
4741, 46sylan 575 . . . . . . . . 9 (((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)) → (∅ ⊆ 𝐴 ∧ ∀𝑧𝐴𝑤 ∈ ∅ 𝑧𝑤))
48 rex0 4101 . . . . . . . . . . . . . 14 ¬ ∃𝑤 ∈ ∅ 𝑧𝑤
4948rgenw 3070 . . . . . . . . . . . . 13 𝑧𝐴 ¬ ∃𝑤 ∈ ∅ 𝑧𝑤
50 r19.2z 4218 . . . . . . . . . . . . 13 ((𝐴 ≠ ∅ ∧ ∀𝑧𝐴 ¬ ∃𝑤 ∈ ∅ 𝑧𝑤) → ∃𝑧𝐴 ¬ ∃𝑤 ∈ ∅ 𝑧𝑤)
5149, 50mpan2 682 . . . . . . . . . . . 12 (𝐴 ≠ ∅ → ∃𝑧𝐴 ¬ ∃𝑤 ∈ ∅ 𝑧𝑤)
52 rexnal 3140 . . . . . . . . . . . 12 (∃𝑧𝐴 ¬ ∃𝑤 ∈ ∅ 𝑧𝑤 ↔ ¬ ∀𝑧𝐴𝑤 ∈ ∅ 𝑧𝑤)
5351, 52sylib 209 . . . . . . . . . . 11 (𝐴 ≠ ∅ → ¬ ∀𝑧𝐴𝑤 ∈ ∅ 𝑧𝑤)
5453necon4ai 2967 . . . . . . . . . 10 (∀𝑧𝐴𝑤 ∈ ∅ 𝑧𝑤𝐴 = ∅)
5554adantl 473 . . . . . . . . 9 ((∅ ⊆ 𝐴 ∧ ∀𝑧𝐴𝑤 ∈ ∅ 𝑧𝑤) → 𝐴 = ∅)
5647, 55syl 17 . . . . . . . 8 (((𝑦 ⊆ On ∧ ∅ = (card‘𝑦)) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)) → 𝐴 = ∅)
5731, 32, 33, 56syl21anc 866 . . . . . . 7 ((𝐴 ∈ On ∧ ∅ = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)) → 𝐴 = ∅)
58573expib 1152 . . . . . 6 (𝐴 ∈ On → ((∅ = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)) → 𝐴 = ∅))
5958exlimdv 2028 . . . . 5 (𝐴 ∈ On → (∃𝑦(∅ = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤)) → 𝐴 = ∅))
6025, 59syl5bi 233 . . . 4 (𝐴 ∈ On → (∅ ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))} → 𝐴 = ∅))
6120, 60syl5bi 233 . . 3 (𝐴 ∈ On → ( {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦𝐴 ∧ ∀𝑧𝐴𝑤𝑦 𝑧𝑤))} = ∅ → 𝐴 = ∅))
622, 61sylbid 231 . 2 (𝐴 ∈ On → ((cf‘𝐴) = ∅ → 𝐴 = ∅))
63 fveq2 6374 . . 3 (𝐴 = ∅ → (cf‘𝐴) = (cf‘∅))
64 cf0 9325 . . 3 (cf‘∅) = ∅
6563, 64syl6eq 2814 . 2 (𝐴 = ∅ → (cf‘𝐴) = ∅)
6662, 65impbid1 216 1 (𝐴 ∈ On → ((cf‘𝐴) = ∅ ↔ 𝐴 = ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wex 1874  wcel 2155  {cab 2750  wne 2936  wral 3054  wrex 3055  Vcvv 3349  wss 3731  c0 4078   cint 4632  dom cdm 5276  Oncon0 5907  cfv 6067  cardccrd 9011  cfccf 9013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-wrecs 7609  df-recs 7671  df-er 7946  df-en 8160  df-dom 8161  df-card 9015  df-cf 9017
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator