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

Theorem karden 9118
Description: If we allow the Axiom of Regularity, we can avoid the Axiom of Choice by defining the cardinal number of a set as the set of all sets equinumerous to it and having the least possible rank. This theorem proves the equinumerosity relationship for this definition (compare carden 9771). The hypotheses correspond to the definition of kard of [Enderton] p. 222 (which we don't define separately since currently we do not use it elsewhere). This theorem along with kardex 9117 justify the definition of kard. The restriction to the least rank prevents the proper class that would result from {𝑥𝑥𝐴}. (Contributed by NM, 18-Dec-2003.) (Revised by AV, 12-Jul-2022.)
Hypotheses
Ref Expression
karden.a 𝐴 ∈ V
karden.c 𝐶 = {𝑥 ∣ (𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
karden.d 𝐷 = {𝑥 ∣ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Assertion
Ref Expression
karden (𝐶 = 𝐷𝐴𝐵)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦
Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)

Proof of Theorem karden
Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 karden.a . . . . . . 7 𝐴 ∈ V
2 breq1 4932 . . . . . . 7 (𝑤 = 𝐴 → (𝑤𝐴𝐴𝐴))
31enref 8339 . . . . . . 7 𝐴𝐴
41, 2, 3ceqsexv2d 3463 . . . . . 6 𝑤 𝑤𝐴
5 abn0 4222 . . . . . 6 ({𝑤𝑤𝐴} ≠ ∅ ↔ ∃𝑤 𝑤𝐴)
64, 5mpbir 223 . . . . 5 {𝑤𝑤𝐴} ≠ ∅
7 scott0 9109 . . . . . 6 ({𝑤𝑤𝐴} = ∅ ↔ {𝑧 ∈ {𝑤𝑤𝐴} ∣ ∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)} = ∅)
87necon3bii 3019 . . . . 5 ({𝑤𝑤𝐴} ≠ ∅ ↔ {𝑧 ∈ {𝑤𝑤𝐴} ∣ ∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)} ≠ ∅)
96, 8mpbi 222 . . . 4 {𝑧 ∈ {𝑤𝑤𝐴} ∣ ∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)} ≠ ∅
10 rabn0 4225 . . . 4 ({𝑧 ∈ {𝑤𝑤𝐴} ∣ ∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)} ≠ ∅ ↔ ∃𝑧 ∈ {𝑤𝑤𝐴}∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦))
119, 10mpbi 222 . . 3 𝑧 ∈ {𝑤𝑤𝐴}∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)
12 vex 3418 . . . . . . . 8 𝑧 ∈ V
13 breq1 4932 . . . . . . . 8 (𝑤 = 𝑧 → (𝑤𝐴𝑧𝐴))
1412, 13elab 3582 . . . . . . 7 (𝑧 ∈ {𝑤𝑤𝐴} ↔ 𝑧𝐴)
15 breq1 4932 . . . . . . . 8 (𝑤 = 𝑦 → (𝑤𝐴𝑦𝐴))
1615ralab 3600 . . . . . . 7 (∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦) ↔ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦)))
1714, 16anbi12i 617 . . . . . 6 ((𝑧 ∈ {𝑤𝑤𝐴} ∧ ∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)) ↔ (𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))))
18 simpl 475 . . . . . . . . 9 ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) → 𝑧𝐴)
1918a1i 11 . . . . . . . 8 (𝐶 = 𝐷 → ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) → 𝑧𝐴))
20 karden.c . . . . . . . . . . . 12 𝐶 = {𝑥 ∣ (𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
21 karden.d . . . . . . . . . . . 12 𝐷 = {𝑥 ∣ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
2220, 21eqeq12i 2792 . . . . . . . . . . 11 (𝐶 = 𝐷 ↔ {𝑥 ∣ (𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))} = {𝑥 ∣ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))})
23 abbi 2907 . . . . . . . . . . 11 (∀𝑥((𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))) ↔ {𝑥 ∣ (𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))} = {𝑥 ∣ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))})
2422, 23bitr4i 270 . . . . . . . . . 10 (𝐶 = 𝐷 ↔ ∀𝑥((𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))))
25 breq1 4932 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
26 fveq2 6499 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (rank‘𝑥) = (rank‘𝑧))
2726sseq1d 3888 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → ((rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑧) ⊆ (rank‘𝑦)))
2827imbi2d 333 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → ((𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ (𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))))
2928albidv 1879 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))))
3025, 29anbi12d 621 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦)))))
31 breq1 4932 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑥𝐵𝑧𝐵))
3227imbi2d 333 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → ((𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ (𝑦𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦))))
3332albidv 1879 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑦(𝑦𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦))))
3431, 33anbi12d 621 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑧𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦)))))
3530, 34bibi12d 338 . . . . . . . . . . 11 (𝑥 = 𝑧 → (((𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))) ↔ ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) ↔ (𝑧𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦))))))
3635spv 2324 . . . . . . . . . 10 (∀𝑥((𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))) → ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) ↔ (𝑧𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦)))))
3724, 36sylbi 209 . . . . . . . . 9 (𝐶 = 𝐷 → ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) ↔ (𝑧𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦)))))
38 simpl 475 . . . . . . . . 9 ((𝑧𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦))) → 𝑧𝐵)
3937, 38syl6bi 245 . . . . . . . 8 (𝐶 = 𝐷 → ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) → 𝑧𝐵))
4019, 39jcad 505 . . . . . . 7 (𝐶 = 𝐷 → ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) → (𝑧𝐴𝑧𝐵)))
41 ensym 8355 . . . . . . . 8 (𝑧𝐴𝐴𝑧)
42 entr 8358 . . . . . . . 8 ((𝐴𝑧𝑧𝐵) → 𝐴𝐵)
4341, 42sylan 572 . . . . . . 7 ((𝑧𝐴𝑧𝐵) → 𝐴𝐵)
4440, 43syl6 35 . . . . . 6 (𝐶 = 𝐷 → ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) → 𝐴𝐵))
4517, 44syl5bi 234 . . . . 5 (𝐶 = 𝐷 → ((𝑧 ∈ {𝑤𝑤𝐴} ∧ ∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)) → 𝐴𝐵))
4645expd 408 . . . 4 (𝐶 = 𝐷 → (𝑧 ∈ {𝑤𝑤𝐴} → (∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦) → 𝐴𝐵)))
4746rexlimdv 3228 . . 3 (𝐶 = 𝐷 → (∃𝑧 ∈ {𝑤𝑤𝐴}∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦) → 𝐴𝐵))
4811, 47mpi 20 . 2 (𝐶 = 𝐷𝐴𝐵)
49 enen2 8454 . . . . 5 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
50 enen2 8454 . . . . . . 7 (𝐴𝐵 → (𝑦𝐴𝑦𝐵))
5150imbi1d 334 . . . . . 6 (𝐴𝐵 → ((𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ (𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦))))
5251albidv 1879 . . . . 5 (𝐴𝐵 → (∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦))))
5349, 52anbi12d 621 . . . 4 (𝐴𝐵 → ((𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))))
5453abbidv 2843 . . 3 (𝐴𝐵 → {𝑥 ∣ (𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))} = {𝑥 ∣ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))})
5554, 20, 213eqtr4g 2839 . 2 (𝐴𝐵𝐶 = 𝐷)
5648, 55impbii 201 1 (𝐶 = 𝐷𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  wal 1505   = wceq 1507  wex 1742  wcel 2050  {cab 2758  wne 2967  wral 3088  wrex 3089  {crab 3092  Vcvv 3415  wss 3829  c0 4178   class class class wbr 4929  cfv 6188  cen 8303  rankcrnk 8986
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-int 4750  df-iun 4794  df-iin 4795  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-om 7397  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-er 8089  df-en 8307  df-r1 8987  df-rank 8988
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator