![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cardid2 | Structured version Visualization version GIF version |
Description: Any numerable set is equinumerous to its cardinal number. Proposition 10.5 of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.) |
Ref | Expression |
---|---|
cardid2 | ⊢ (𝐴 ∈ dom card → (card‘𝐴) ≈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cardval3 9092 | . . 3 ⊢ (𝐴 ∈ dom card → (card‘𝐴) = ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴}) | |
2 | ssrab2 3913 | . . . 4 ⊢ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ⊆ On | |
3 | fvex 6447 | . . . . . 6 ⊢ (card‘𝐴) ∈ V | |
4 | 1, 3 | syl6eqelr 2916 | . . . . 5 ⊢ (𝐴 ∈ dom card → ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ∈ V) |
5 | intex 5043 | . . . . 5 ⊢ ({𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ≠ ∅ ↔ ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ∈ V) | |
6 | 4, 5 | sylibr 226 | . . . 4 ⊢ (𝐴 ∈ dom card → {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ≠ ∅) |
7 | onint 7257 | . . . 4 ⊢ (({𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ⊆ On ∧ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ≠ ∅) → ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ∈ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴}) | |
8 | 2, 6, 7 | sylancr 583 | . . 3 ⊢ (𝐴 ∈ dom card → ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ∈ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴}) |
9 | 1, 8 | eqeltrd 2907 | . 2 ⊢ (𝐴 ∈ dom card → (card‘𝐴) ∈ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴}) |
10 | breq1 4877 | . . . 4 ⊢ (𝑦 = (card‘𝐴) → (𝑦 ≈ 𝐴 ↔ (card‘𝐴) ≈ 𝐴)) | |
11 | 10 | elrab 3586 | . . 3 ⊢ ((card‘𝐴) ∈ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ↔ ((card‘𝐴) ∈ On ∧ (card‘𝐴) ≈ 𝐴)) |
12 | 11 | simprbi 492 | . 2 ⊢ ((card‘𝐴) ∈ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} → (card‘𝐴) ≈ 𝐴) |
13 | 9, 12 | syl 17 | 1 ⊢ (𝐴 ∈ dom card → (card‘𝐴) ≈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2166 ≠ wne 3000 {crab 3122 Vcvv 3415 ⊆ wss 3799 ∅c0 4145 ∩ cint 4698 class class class wbr 4874 dom cdm 5343 Oncon0 5964 ‘cfv 6124 ≈ cen 8220 cardccrd 9075 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-sep 5006 ax-nul 5014 ax-pr 5128 ax-un 7210 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3or 1114 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ne 3001 df-ral 3123 df-rex 3124 df-rab 3127 df-v 3417 df-sbc 3664 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-pss 3815 df-nul 4146 df-if 4308 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4660 df-int 4699 df-br 4875 df-opab 4937 df-mpt 4954 df-tr 4977 df-id 5251 df-eprel 5256 df-po 5264 df-so 5265 df-fr 5302 df-we 5304 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-rn 5354 df-res 5355 df-ima 5356 df-ord 5967 df-on 5968 df-iota 6087 df-fun 6126 df-fn 6127 df-f 6128 df-fv 6132 df-en 8224 df-card 9079 |
This theorem is referenced by: isnum3 9094 oncardid 9096 cardidm 9099 ficardom 9101 ficardid 9102 cardnn 9103 cardnueq0 9104 carden2a 9106 carden2b 9107 carddomi2 9110 sdomsdomcardi 9111 cardsdomelir 9113 cardsdomel 9114 infxpidm2 9154 dfac8b 9168 numdom 9175 alephnbtwn2 9209 alephsucdom 9216 infenaleph 9228 dfac12r 9284 cardacda 9336 pwsdompw 9342 cff1 9396 cfflb 9397 cflim2 9401 cfss 9403 cfslb 9404 domtriomlem 9580 cardid 9685 cardidg 9686 carden 9689 sdomsdomcard 9698 hargch 9811 gch2 9813 hashkf 13413 |
Copyright terms: Public domain | W3C validator |