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

Theorem karden 8614
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 9225). 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 8613 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.)
Hypotheses
Ref Expression
karden.1 𝐴 ∈ V
karden.2 𝐵 ∈ V
karden.3 𝐶 = {𝑥 ∣ (𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
karden.4 𝐷 = {𝑥 ∣ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (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.1 . . . . . . . 8 𝐴 ∈ V
21enref 7847 . . . . . . 7 𝐴𝐴
3 breq1 4576 . . . . . . . 8 (𝑤 = 𝐴 → (𝑤𝐴𝐴𝐴))
41, 3spcev 3268 . . . . . . 7 (𝐴𝐴 → ∃𝑤 𝑤𝐴)
52, 4ax-mp 5 . . . . . 6 𝑤 𝑤𝐴
6 abn0 3903 . . . . . 6 ({𝑤𝑤𝐴} ≠ ∅ ↔ ∃𝑤 𝑤𝐴)
75, 6mpbir 219 . . . . 5 {𝑤𝑤𝐴} ≠ ∅
8 scott0 8605 . . . . . 6 ({𝑤𝑤𝐴} = ∅ ↔ {𝑧 ∈ {𝑤𝑤𝐴} ∣ ∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)} = ∅)
98necon3bii 2829 . . . . 5 ({𝑤𝑤𝐴} ≠ ∅ ↔ {𝑧 ∈ {𝑤𝑤𝐴} ∣ ∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)} ≠ ∅)
107, 9mpbi 218 . . . 4 {𝑧 ∈ {𝑤𝑤𝐴} ∣ ∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)} ≠ ∅
11 rabn0 3907 . . . 4 ({𝑧 ∈ {𝑤𝑤𝐴} ∣ ∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)} ≠ ∅ ↔ ∃𝑧 ∈ {𝑤𝑤𝐴}∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦))
1210, 11mpbi 218 . . 3 𝑧 ∈ {𝑤𝑤𝐴}∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)
13 vex 3171 . . . . . . . 8 𝑧 ∈ V
14 breq1 4576 . . . . . . . 8 (𝑤 = 𝑧 → (𝑤𝐴𝑧𝐴))
1513, 14elab 3314 . . . . . . 7 (𝑧 ∈ {𝑤𝑤𝐴} ↔ 𝑧𝐴)
16 breq1 4576 . . . . . . . 8 (𝑤 = 𝑦 → (𝑤𝐴𝑦𝐴))
1716ralab 3329 . . . . . . 7 (∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦) ↔ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦)))
1815, 17anbi12i 728 . . . . . 6 ((𝑧 ∈ {𝑤𝑤𝐴} ∧ ∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)) ↔ (𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))))
19 simpl 471 . . . . . . . . 9 ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) → 𝑧𝐴)
2019a1i 11 . . . . . . . 8 (𝐶 = 𝐷 → ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) → 𝑧𝐴))
21 karden.3 . . . . . . . . . . . 12 𝐶 = {𝑥 ∣ (𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
22 karden.4 . . . . . . . . . . . 12 𝐷 = {𝑥 ∣ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
2321, 22eqeq12i 2619 . . . . . . . . . . 11 (𝐶 = 𝐷 ↔ {𝑥 ∣ (𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))} = {𝑥 ∣ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))})
24 abbi 2719 . . . . . . . . . . 11 (∀𝑥((𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))) ↔ {𝑥 ∣ (𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))} = {𝑥 ∣ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))})
2523, 24bitr4i 265 . . . . . . . . . 10 (𝐶 = 𝐷 ↔ ∀𝑥((𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))))
26 breq1 4576 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
27 fveq2 6084 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (rank‘𝑥) = (rank‘𝑧))
2827sseq1d 3590 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → ((rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑧) ⊆ (rank‘𝑦)))
2928imbi2d 328 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → ((𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ (𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))))
3029albidv 1834 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))))
3126, 30anbi12d 742 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦)))))
32 breq1 4576 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑥𝐵𝑧𝐵))
3328imbi2d 328 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → ((𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ (𝑦𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦))))
3433albidv 1834 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑦(𝑦𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦))))
3532, 34anbi12d 742 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑧𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦)))))
3631, 35bibi12d 333 . . . . . . . . . . 11 (𝑥 = 𝑧 → (((𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))) ↔ ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) ↔ (𝑧𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦))))))
3736spv 2242 . . . . . . . . . 10 (∀𝑥((𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))) → ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) ↔ (𝑧𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦)))))
3825, 37sylbi 205 . . . . . . . . 9 (𝐶 = 𝐷 → ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) ↔ (𝑧𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦)))))
39 simpl 471 . . . . . . . . 9 ((𝑧𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦))) → 𝑧𝐵)
4038, 39syl6bi 241 . . . . . . . 8 (𝐶 = 𝐷 → ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) → 𝑧𝐵))
4120, 40jcad 553 . . . . . . 7 (𝐶 = 𝐷 → ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) → (𝑧𝐴𝑧𝐵)))
42 ensym 7864 . . . . . . . 8 (𝑧𝐴𝐴𝑧)
43 entr 7867 . . . . . . . 8 ((𝐴𝑧𝑧𝐵) → 𝐴𝐵)
4442, 43sylan 486 . . . . . . 7 ((𝑧𝐴𝑧𝐵) → 𝐴𝐵)
4541, 44syl6 34 . . . . . 6 (𝐶 = 𝐷 → ((𝑧𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) → 𝐴𝐵))
4618, 45syl5bi 230 . . . . 5 (𝐶 = 𝐷 → ((𝑧 ∈ {𝑤𝑤𝐴} ∧ ∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)) → 𝐴𝐵))
4746expd 450 . . . 4 (𝐶 = 𝐷 → (𝑧 ∈ {𝑤𝑤𝐴} → (∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦) → 𝐴𝐵)))
4847rexlimdv 3007 . . 3 (𝐶 = 𝐷 → (∃𝑧 ∈ {𝑤𝑤𝐴}∀𝑦 ∈ {𝑤𝑤𝐴} (rank‘𝑧) ⊆ (rank‘𝑦) → 𝐴𝐵))
4912, 48mpi 20 . 2 (𝐶 = 𝐷𝐴𝐵)
50 enen2 7959 . . . . 5 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
51 enen2 7959 . . . . . . 7 (𝐴𝐵 → (𝑦𝐴𝑦𝐵))
5251imbi1d 329 . . . . . 6 (𝐴𝐵 → ((𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ (𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦))))
5352albidv 1834 . . . . 5 (𝐴𝐵 → (∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦))))
5450, 53anbi12d 742 . . . 4 (𝐴𝐵 → ((𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))))
5554abbidv 2723 . . 3 (𝐴𝐵 → {𝑥 ∣ (𝑥𝐴 ∧ ∀𝑦(𝑦𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))} = {𝑥 ∣ (𝑥𝐵 ∧ ∀𝑦(𝑦𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))})
5655, 21, 223eqtr4g 2664 . 2 (𝐴𝐵𝐶 = 𝐷)
5749, 56impbii 197 1 (𝐶 = 𝐷𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  wal 1472   = wceq 1474  wex 1694  wcel 1975  {cab 2591  wne 2775  wral 2891  wrex 2892  {crab 2895  Vcvv 3168  wss 3535  c0 3869   class class class wbr 4573  cfv 5786  cen 7811  rankcrnk 8482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-ral 2896  df-rex 2897  df-reu 2898  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-int 4401  df-iun 4447  df-iin 4448  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-om 6931  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-er 7602  df-en 7815  df-r1 8483  df-rank 8484
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator