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 9447 | . . 3 ⊢ (𝐴 ∈ dom card → (card‘𝐴) = ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴}) | |
2 | ssrab2 3967 | . . . 4 ⊢ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ⊆ On | |
3 | fvex 6681 | . . . . . 6 ⊢ (card‘𝐴) ∈ V | |
4 | 1, 3 | eqeltrrdi 2842 | . . . . 5 ⊢ (𝐴 ∈ dom card → ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ∈ V) |
5 | intex 5202 | . . . . 5 ⊢ ({𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ≠ ∅ ↔ ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ∈ V) | |
6 | 4, 5 | sylibr 237 | . . . 4 ⊢ (𝐴 ∈ dom card → {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ≠ ∅) |
7 | onint 7523 | . . . 4 ⊢ (({𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ⊆ On ∧ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ≠ ∅) → ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ∈ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴}) | |
8 | 2, 6, 7 | sylancr 590 | . . 3 ⊢ (𝐴 ∈ dom card → ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ∈ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴}) |
9 | 1, 8 | eqeltrd 2833 | . 2 ⊢ (𝐴 ∈ dom card → (card‘𝐴) ∈ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴}) |
10 | breq1 5030 | . . . 4 ⊢ (𝑦 = (card‘𝐴) → (𝑦 ≈ 𝐴 ↔ (card‘𝐴) ≈ 𝐴)) | |
11 | 10 | elrab 3585 | . . 3 ⊢ ((card‘𝐴) ∈ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ↔ ((card‘𝐴) ∈ On ∧ (card‘𝐴) ≈ 𝐴)) |
12 | 11 | simprbi 500 | . 2 ⊢ ((card‘𝐴) ∈ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} → (card‘𝐴) ≈ 𝐴) |
13 | 9, 12 | syl 17 | 1 ⊢ (𝐴 ∈ dom card → (card‘𝐴) ≈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2113 ≠ wne 2934 {crab 3057 Vcvv 3397 ⊆ wss 3841 ∅c0 4209 ∩ cint 4833 class class class wbr 5027 dom cdm 5519 Oncon0 6166 ‘cfv 6333 ≈ cen 8545 cardccrd 9430 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5164 ax-nul 5171 ax-pr 5293 ax-un 7473 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3399 df-sbc 3680 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-pss 3860 df-nul 4210 df-if 4412 df-sn 4514 df-pr 4516 df-tp 4518 df-op 4520 df-uni 4794 df-int 4834 df-br 5028 df-opab 5090 df-mpt 5108 df-tr 5134 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-ord 6169 df-on 6170 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-fv 6341 df-en 8549 df-card 9434 |
This theorem is referenced by: isnum3 9449 oncardid 9451 cardidm 9454 ficardom 9456 ficardid 9457 cardnn 9458 cardnueq0 9459 carden2a 9461 carden2b 9462 carddomi2 9465 sdomsdomcardi 9466 cardsdomelir 9468 cardsdomel 9469 infxpidm2 9510 dfac8b 9524 numdom 9531 alephnbtwn2 9565 alephsucdom 9572 infenaleph 9584 dfac12r 9639 cardadju 9687 pwsdompw 9697 cff1 9751 cfflb 9752 cflim2 9756 cfss 9758 cfslb 9759 domtriomlem 9935 cardid 10040 cardidg 10041 carden 10044 sdomsdomcard 10053 hargch 10166 gch2 10168 hashkf 13777 |
Copyright terms: Public domain | W3C validator |