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

Theorem cardmin2 9425
 Description: The smallest ordinal that strictly dominates a set is a cardinal, if it exists. (Contributed by Mario Carneiro, 2-Feb-2013.)
Assertion
Ref Expression
cardmin2 (∃𝑥 ∈ On 𝐴𝑥 ↔ (card‘ {𝑥 ∈ On ∣ 𝐴𝑥}) = {𝑥 ∈ On ∣ 𝐴𝑥})
Distinct variable group:   𝑥,𝐴

Proof of Theorem cardmin2
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 onintrab2 7511 . . . 4 (∃𝑥 ∈ On 𝐴𝑥 {𝑥 ∈ On ∣ 𝐴𝑥} ∈ On)
21biimpi 219 . . 3 (∃𝑥 ∈ On 𝐴𝑥 {𝑥 ∈ On ∣ 𝐴𝑥} ∈ On)
32adantr 484 . . . . . 6 ((∃𝑥 ∈ On 𝐴𝑥𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}) → {𝑥 ∈ On ∣ 𝐴𝑥} ∈ On)
4 eloni 6188 . . . . . . . 8 ( {𝑥 ∈ On ∣ 𝐴𝑥} ∈ On → Ord {𝑥 ∈ On ∣ 𝐴𝑥})
5 ordelss 6194 . . . . . . . 8 ((Ord {𝑥 ∈ On ∣ 𝐴𝑥} ∧ 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}) → 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥})
64, 5sylan 583 . . . . . . 7 (( {𝑥 ∈ On ∣ 𝐴𝑥} ∈ On ∧ 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}) → 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥})
71, 6sylanb 584 . . . . . 6 ((∃𝑥 ∈ On 𝐴𝑥𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}) → 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥})
8 ssdomg 8551 . . . . . 6 ( {𝑥 ∈ On ∣ 𝐴𝑥} ∈ On → (𝑦 {𝑥 ∈ On ∣ 𝐴𝑥} → 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}))
93, 7, 8sylc 65 . . . . 5 ((∃𝑥 ∈ On 𝐴𝑥𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}) → 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥})
10 onelon 6203 . . . . . . . 8 (( {𝑥 ∈ On ∣ 𝐴𝑥} ∈ On ∧ 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}) → 𝑦 ∈ On)
111, 10sylanb 584 . . . . . . 7 ((∃𝑥 ∈ On 𝐴𝑥𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}) → 𝑦 ∈ On)
12 nfcv 2982 . . . . . . . . . . . . . 14 𝑥𝐴
13 nfcv 2982 . . . . . . . . . . . . . 14 𝑥
14 nfrab1 3375 . . . . . . . . . . . . . . 15 𝑥{𝑥 ∈ On ∣ 𝐴𝑥}
1514nfint 4872 . . . . . . . . . . . . . 14 𝑥 {𝑥 ∈ On ∣ 𝐴𝑥}
1612, 13, 15nfbr 5099 . . . . . . . . . . . . 13 𝑥 𝐴 {𝑥 ∈ On ∣ 𝐴𝑥}
17 breq2 5056 . . . . . . . . . . . . 13 (𝑥 = {𝑥 ∈ On ∣ 𝐴𝑥} → (𝐴𝑥𝐴 {𝑥 ∈ On ∣ 𝐴𝑥}))
1816, 17onminsb 7508 . . . . . . . . . . . 12 (∃𝑥 ∈ On 𝐴𝑥𝐴 {𝑥 ∈ On ∣ 𝐴𝑥})
19 sdomentr 8648 . . . . . . . . . . . 12 ((𝐴 {𝑥 ∈ On ∣ 𝐴𝑥} ∧ {𝑥 ∈ On ∣ 𝐴𝑥} ≈ 𝑦) → 𝐴𝑦)
2018, 19sylan 583 . . . . . . . . . . 11 ((∃𝑥 ∈ On 𝐴𝑥 {𝑥 ∈ On ∣ 𝐴𝑥} ≈ 𝑦) → 𝐴𝑦)
21 breq2 5056 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
2221elrab 3666 . . . . . . . . . . . . 13 (𝑦 ∈ {𝑥 ∈ On ∣ 𝐴𝑥} ↔ (𝑦 ∈ On ∧ 𝐴𝑦))
23 ssrab2 4042 . . . . . . . . . . . . . 14 {𝑥 ∈ On ∣ 𝐴𝑥} ⊆ On
24 onnmin 7512 . . . . . . . . . . . . . 14 (({𝑥 ∈ On ∣ 𝐴𝑥} ⊆ On ∧ 𝑦 ∈ {𝑥 ∈ On ∣ 𝐴𝑥}) → ¬ 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥})
2523, 24mpan 689 . . . . . . . . . . . . 13 (𝑦 ∈ {𝑥 ∈ On ∣ 𝐴𝑥} → ¬ 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥})
2622, 25sylbir 238 . . . . . . . . . . . 12 ((𝑦 ∈ On ∧ 𝐴𝑦) → ¬ 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥})
2726expcom 417 . . . . . . . . . . 11 (𝐴𝑦 → (𝑦 ∈ On → ¬ 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}))
2820, 27syl 17 . . . . . . . . . 10 ((∃𝑥 ∈ On 𝐴𝑥 {𝑥 ∈ On ∣ 𝐴𝑥} ≈ 𝑦) → (𝑦 ∈ On → ¬ 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}))
2928impancom 455 . . . . . . . . 9 ((∃𝑥 ∈ On 𝐴𝑥𝑦 ∈ On) → ( {𝑥 ∈ On ∣ 𝐴𝑥} ≈ 𝑦 → ¬ 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}))
3029con2d 136 . . . . . . . 8 ((∃𝑥 ∈ On 𝐴𝑥𝑦 ∈ On) → (𝑦 {𝑥 ∈ On ∣ 𝐴𝑥} → ¬ {𝑥 ∈ On ∣ 𝐴𝑥} ≈ 𝑦))
3130impancom 455 . . . . . . 7 ((∃𝑥 ∈ On 𝐴𝑥𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}) → (𝑦 ∈ On → ¬ {𝑥 ∈ On ∣ 𝐴𝑥} ≈ 𝑦))
3211, 31mpd 15 . . . . . 6 ((∃𝑥 ∈ On 𝐴𝑥𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}) → ¬ {𝑥 ∈ On ∣ 𝐴𝑥} ≈ 𝑦)
33 ensym 8554 . . . . . 6 (𝑦 {𝑥 ∈ On ∣ 𝐴𝑥} → {𝑥 ∈ On ∣ 𝐴𝑥} ≈ 𝑦)
3432, 33nsyl 142 . . . . 5 ((∃𝑥 ∈ On 𝐴𝑥𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}) → ¬ 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥})
35 brsdom 8528 . . . . 5 (𝑦 {𝑥 ∈ On ∣ 𝐴𝑥} ↔ (𝑦 {𝑥 ∈ On ∣ 𝐴𝑥} ∧ ¬ 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}))
369, 34, 35sylanbrc 586 . . . 4 ((∃𝑥 ∈ On 𝐴𝑥𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}) → 𝑦 {𝑥 ∈ On ∣ 𝐴𝑥})
3736ralrimiva 3177 . . 3 (∃𝑥 ∈ On 𝐴𝑥 → ∀𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}𝑦 {𝑥 ∈ On ∣ 𝐴𝑥})
38 iscard 9401 . . 3 ((card‘ {𝑥 ∈ On ∣ 𝐴𝑥}) = {𝑥 ∈ On ∣ 𝐴𝑥} ↔ ( {𝑥 ∈ On ∣ 𝐴𝑥} ∈ On ∧ ∀𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}𝑦 {𝑥 ∈ On ∣ 𝐴𝑥}))
392, 37, 38sylanbrc 586 . 2 (∃𝑥 ∈ On 𝐴𝑥 → (card‘ {𝑥 ∈ On ∣ 𝐴𝑥}) = {𝑥 ∈ On ∣ 𝐴𝑥})
40 vprc 5205 . . . . . 6 ¬ V ∈ V
41 inteq 4865 . . . . . . . 8 ({𝑥 ∈ On ∣ 𝐴𝑥} = ∅ → {𝑥 ∈ On ∣ 𝐴𝑥} = ∅)
42 int0 4876 . . . . . . . 8 ∅ = V
4341, 42syl6eq 2875 . . . . . . 7 ({𝑥 ∈ On ∣ 𝐴𝑥} = ∅ → {𝑥 ∈ On ∣ 𝐴𝑥} = V)
4443eleq1d 2900 . . . . . 6 ({𝑥 ∈ On ∣ 𝐴𝑥} = ∅ → ( {𝑥 ∈ On ∣ 𝐴𝑥} ∈ V ↔ V ∈ V))
4540, 44mtbiri 330 . . . . 5 ({𝑥 ∈ On ∣ 𝐴𝑥} = ∅ → ¬ {𝑥 ∈ On ∣ 𝐴𝑥} ∈ V)
46 fvex 6674 . . . . . 6 (card‘ {𝑥 ∈ On ∣ 𝐴𝑥}) ∈ V
47 eleq1 2903 . . . . . 6 ((card‘ {𝑥 ∈ On ∣ 𝐴𝑥}) = {𝑥 ∈ On ∣ 𝐴𝑥} → ((card‘ {𝑥 ∈ On ∣ 𝐴𝑥}) ∈ V ↔ {𝑥 ∈ On ∣ 𝐴𝑥} ∈ V))
4846, 47mpbii 236 . . . . 5 ((card‘ {𝑥 ∈ On ∣ 𝐴𝑥}) = {𝑥 ∈ On ∣ 𝐴𝑥} → {𝑥 ∈ On ∣ 𝐴𝑥} ∈ V)
4945, 48nsyl 142 . . . 4 ({𝑥 ∈ On ∣ 𝐴𝑥} = ∅ → ¬ (card‘ {𝑥 ∈ On ∣ 𝐴𝑥}) = {𝑥 ∈ On ∣ 𝐴𝑥})
5049necon2ai 3043 . . 3 ((card‘ {𝑥 ∈ On ∣ 𝐴𝑥}) = {𝑥 ∈ On ∣ 𝐴𝑥} → {𝑥 ∈ On ∣ 𝐴𝑥} ≠ ∅)
51 rabn0 4322 . . 3 ({𝑥 ∈ On ∣ 𝐴𝑥} ≠ ∅ ↔ ∃𝑥 ∈ On 𝐴𝑥)
5250, 51sylib 221 . 2 ((card‘ {𝑥 ∈ On ∣ 𝐴𝑥}) = {𝑥 ∈ On ∣ 𝐴𝑥} → ∃𝑥 ∈ On 𝐴𝑥)
5339, 52impbii 212 1 (∃𝑥 ∈ On 𝐴𝑥 ↔ (card‘ {𝑥 ∈ On ∣ 𝐴𝑥}) = {𝑥 ∈ On ∣ 𝐴𝑥})
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2115   ≠ wne 3014  ∀wral 3133  ∃wrex 3134  {crab 3137  Vcvv 3480   ⊆ wss 3919  ∅c0 4276  ∩ cint 4862   class class class wbr 5052  Ord word 6177  Oncon0 6178  ‘cfv 6343   ≈ cen 8502   ≼ cdom 8503   ≺ csdm 8504  cardccrd 9361 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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-ord 6181  df-on 6182  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-er 8285  df-en 8506  df-dom 8507  df-sdom 8508  df-card 9365 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator