Mathbox for Richard Penner < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  harval3 Structured version   Visualization version   GIF version

Theorem harval3 40415
 Description: (har‘𝐴) is the least cardinal that is greater than 𝐴. (Contributed by RP, 4-Nov-2023.)
Assertion
Ref Expression
harval3 (𝐴 ∈ dom card → (har‘𝐴) = {𝑥 ∈ ran card ∣ 𝐴𝑥})
Distinct variable group:   𝑥,𝐴

Proof of Theorem harval3
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 harval2 9428 . 2 (𝐴 ∈ dom card → (har‘𝐴) = {𝑦 ∈ On ∣ 𝐴𝑦})
2 vex 3445 . . . . . 6 𝑥 ∈ V
32a1i 11 . . . . 5 (𝐴 ∈ dom card → 𝑥 ∈ V)
4 elrncard 40414 . . . . . . . . 9 (𝑥 ∈ ran card ↔ (𝑥 ∈ On ∧ ∀𝑦𝑥 ¬ 𝑦𝑥))
54simplbi 501 . . . . . . . 8 (𝑥 ∈ ran card → 𝑥 ∈ On)
65anim1i 617 . . . . . . 7 ((𝑥 ∈ ran card ∧ 𝐴𝑥) → (𝑥 ∈ On ∧ 𝐴𝑥))
7 eleq1 2877 . . . . . . . 8 (𝑦 = 𝑥 → (𝑦 ∈ On ↔ 𝑥 ∈ On))
8 breq2 5038 . . . . . . . 8 (𝑦 = 𝑥 → (𝐴𝑦𝐴𝑥))
97, 8anbi12d 633 . . . . . . 7 (𝑦 = 𝑥 → ((𝑦 ∈ On ∧ 𝐴𝑦) ↔ (𝑥 ∈ On ∧ 𝐴𝑥)))
106, 9syl5ibr 249 . . . . . 6 (𝑦 = 𝑥 → ((𝑥 ∈ ran card ∧ 𝐴𝑥) → (𝑦 ∈ On ∧ 𝐴𝑦)))
1110adantl 485 . . . . 5 ((𝐴 ∈ dom card ∧ 𝑦 = 𝑥) → ((𝑥 ∈ ran card ∧ 𝐴𝑥) → (𝑦 ∈ On ∧ 𝐴𝑦)))
12 ssidd 3940 . . . . 5 (𝐴 ∈ dom card → 𝑥𝑥)
133, 11, 12intabssd 40398 . . . 4 (𝐴 ∈ dom card → {𝑦 ∣ (𝑦 ∈ On ∧ 𝐴𝑦)} ⊆ {𝑥 ∣ (𝑥 ∈ ran card ∧ 𝐴𝑥)})
14 vex 3445 . . . . . . 7 𝑦 ∈ V
1514inex1 5189 . . . . . 6 (𝑦 ∩ (card‘𝑦)) ∈ V
1615a1i 11 . . . . 5 (𝐴 ∈ dom card → (𝑦 ∩ (card‘𝑦)) ∈ V)
17 oncardid 9387 . . . . . . . . . . . 12 (𝑦 ∈ On → (card‘𝑦) ≈ 𝑦)
1817ensymd 8561 . . . . . . . . . . 11 (𝑦 ∈ On → 𝑦 ≈ (card‘𝑦))
19 sdomentr 8653 . . . . . . . . . . . 12 ((𝐴𝑦𝑦 ≈ (card‘𝑦)) → 𝐴 ≺ (card‘𝑦))
2019a1i 11 . . . . . . . . . . 11 (𝑦 ∈ On → ((𝐴𝑦𝑦 ≈ (card‘𝑦)) → 𝐴 ≺ (card‘𝑦)))
2118, 20mpan2d 693 . . . . . . . . . 10 (𝑦 ∈ On → (𝐴𝑦𝐴 ≺ (card‘𝑦)))
22 df-card 9370 . . . . . . . . . . . 12 card = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦𝑥})
2322funmpt2 6371 . . . . . . . . . . 11 Fun card
24 onenon 9380 . . . . . . . . . . 11 (𝑦 ∈ On → 𝑦 ∈ dom card)
25 fvelrn 6831 . . . . . . . . . . 11 ((Fun card ∧ 𝑦 ∈ dom card) → (card‘𝑦) ∈ ran card)
2623, 24, 25sylancr 590 . . . . . . . . . 10 (𝑦 ∈ On → (card‘𝑦) ∈ ran card)
2721, 26jctild 529 . . . . . . . . 9 (𝑦 ∈ On → (𝐴𝑦 → ((card‘𝑦) ∈ ran card ∧ 𝐴 ≺ (card‘𝑦))))
2827adantl 485 . . . . . . . 8 ((𝑥 = (𝑦 ∩ (card‘𝑦)) ∧ 𝑦 ∈ On) → (𝐴𝑦 → ((card‘𝑦) ∈ ran card ∧ 𝐴 ≺ (card‘𝑦))))
29 simpl 486 . . . . . . . . . 10 ((𝑥 = (𝑦 ∩ (card‘𝑦)) ∧ 𝑦 ∈ On) → 𝑥 = (𝑦 ∩ (card‘𝑦)))
30 cardonle 9388 . . . . . . . . . . . 12 (𝑦 ∈ On → (card‘𝑦) ⊆ 𝑦)
3130adantl 485 . . . . . . . . . . 11 ((𝑥 = (𝑦 ∩ (card‘𝑦)) ∧ 𝑦 ∈ On) → (card‘𝑦) ⊆ 𝑦)
32 sseqin2 4145 . . . . . . . . . . 11 ((card‘𝑦) ⊆ 𝑦 ↔ (𝑦 ∩ (card‘𝑦)) = (card‘𝑦))
3331, 32sylib 221 . . . . . . . . . 10 ((𝑥 = (𝑦 ∩ (card‘𝑦)) ∧ 𝑦 ∈ On) → (𝑦 ∩ (card‘𝑦)) = (card‘𝑦))
3429, 33eqtrd 2833 . . . . . . . . 9 ((𝑥 = (𝑦 ∩ (card‘𝑦)) ∧ 𝑦 ∈ On) → 𝑥 = (card‘𝑦))
35 eleq1 2877 . . . . . . . . . 10 (𝑥 = (card‘𝑦) → (𝑥 ∈ ran card ↔ (card‘𝑦) ∈ ran card))
36 breq2 5038 . . . . . . . . . 10 (𝑥 = (card‘𝑦) → (𝐴𝑥𝐴 ≺ (card‘𝑦)))
3735, 36anbi12d 633 . . . . . . . . 9 (𝑥 = (card‘𝑦) → ((𝑥 ∈ ran card ∧ 𝐴𝑥) ↔ ((card‘𝑦) ∈ ran card ∧ 𝐴 ≺ (card‘𝑦))))
3834, 37syl 17 . . . . . . . 8 ((𝑥 = (𝑦 ∩ (card‘𝑦)) ∧ 𝑦 ∈ On) → ((𝑥 ∈ ran card ∧ 𝐴𝑥) ↔ ((card‘𝑦) ∈ ran card ∧ 𝐴 ≺ (card‘𝑦))))
3928, 38sylibrd 262 . . . . . . 7 ((𝑥 = (𝑦 ∩ (card‘𝑦)) ∧ 𝑦 ∈ On) → (𝐴𝑦 → (𝑥 ∈ ran card ∧ 𝐴𝑥)))
4039expimpd 457 . . . . . 6 (𝑥 = (𝑦 ∩ (card‘𝑦)) → ((𝑦 ∈ On ∧ 𝐴𝑦) → (𝑥 ∈ ran card ∧ 𝐴𝑥)))
4140adantl 485 . . . . 5 ((𝐴 ∈ dom card ∧ 𝑥 = (𝑦 ∩ (card‘𝑦))) → ((𝑦 ∈ On ∧ 𝐴𝑦) → (𝑥 ∈ ran card ∧ 𝐴𝑥)))
42 inss1 4158 . . . . . 6 (𝑦 ∩ (card‘𝑦)) ⊆ 𝑦
4342a1i 11 . . . . 5 (𝐴 ∈ dom card → (𝑦 ∩ (card‘𝑦)) ⊆ 𝑦)
4416, 41, 43intabssd 40398 . . . 4 (𝐴 ∈ dom card → {𝑥 ∣ (𝑥 ∈ ran card ∧ 𝐴𝑥)} ⊆ {𝑦 ∣ (𝑦 ∈ On ∧ 𝐴𝑦)})
4513, 44eqssd 3934 . . 3 (𝐴 ∈ dom card → {𝑦 ∣ (𝑦 ∈ On ∧ 𝐴𝑦)} = {𝑥 ∣ (𝑥 ∈ ran card ∧ 𝐴𝑥)})
46 df-rab 3115 . . . 4 {𝑦 ∈ On ∣ 𝐴𝑦} = {𝑦 ∣ (𝑦 ∈ On ∧ 𝐴𝑦)}
4746inteqi 4846 . . 3 {𝑦 ∈ On ∣ 𝐴𝑦} = {𝑦 ∣ (𝑦 ∈ On ∧ 𝐴𝑦)}
48 df-rab 3115 . . . 4 {𝑥 ∈ ran card ∣ 𝐴𝑥} = {𝑥 ∣ (𝑥 ∈ ran card ∧ 𝐴𝑥)}
4948inteqi 4846 . . 3 {𝑥 ∈ ran card ∣ 𝐴𝑥} = {𝑥 ∣ (𝑥 ∈ ran card ∧ 𝐴𝑥)}
5045, 47, 493eqtr4g 2858 . 2 (𝐴 ∈ dom card → {𝑦 ∈ On ∣ 𝐴𝑦} = {𝑥 ∈ ran card ∣ 𝐴𝑥})
511, 50eqtrd 2833 1 (𝐴 ∈ dom card → (har‘𝐴) = {𝑥 ∈ ran card ∣ 𝐴𝑥})
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {cab 2776  ∀wral 3106  {crab 3110  Vcvv 3442   ∩ cin 3882   ⊆ wss 3883  ∩ cint 4842   class class class wbr 5034  dom cdm 5523  ran crn 5524  Oncon0 6166  Fun wfun 6326  ‘cfv 6332   ≈ cen 8507   ≺ csdm 8509  harchar 9022  cardccrd 9366 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-isom 6341  df-riota 7103  df-wrecs 7948  df-recs 8009  df-er 8290  df-en 8511  df-dom 8512  df-sdom 8513  df-oi 8976  df-har 9023  df-card 9370 This theorem is referenced by:  harval3on  40416
 Copyright terms: Public domain W3C validator