![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > hashen | Structured version Visualization version GIF version |
Description: Two finite sets have the same number of elements iff they are equinumerous. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.) |
Ref | Expression |
---|---|
hashen | ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) = (♯‘𝐵) ↔ 𝐴 ≈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 6668 | . . . 4 ⊢ ((♯‘𝐴) = (♯‘𝐵) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(♯‘𝐴)) = (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(♯‘𝐵))) | |
2 | eqid 2738 | . . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) | |
3 | 2 | hashginv 13779 | . . . . 5 ⊢ (𝐴 ∈ Fin → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(♯‘𝐴)) = (card‘𝐴)) |
4 | 2 | hashginv 13779 | . . . . 5 ⊢ (𝐵 ∈ Fin → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(♯‘𝐵)) = (card‘𝐵)) |
5 | 3, 4 | eqeqan12d 2755 | . . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(♯‘𝐴)) = (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(♯‘𝐵)) ↔ (card‘𝐴) = (card‘𝐵))) |
6 | 1, 5 | syl5ib 247 | . . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) = (♯‘𝐵) → (card‘𝐴) = (card‘𝐵))) |
7 | fveq2 6668 | . . . 4 ⊢ ((card‘𝐴) = (card‘𝐵) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵))) | |
8 | 2 | hashgval 13778 | . . . . 5 ⊢ (𝐴 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴)) |
9 | 2 | hashgval 13778 | . . . . 5 ⊢ (𝐵 ∈ Fin → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) = (♯‘𝐵)) |
10 | 8, 9 | eqeqan12d 2755 | . . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐴)) = ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘(card‘𝐵)) ↔ (♯‘𝐴) = (♯‘𝐵))) |
11 | 7, 10 | syl5ib 247 | . . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((card‘𝐴) = (card‘𝐵) → (♯‘𝐴) = (♯‘𝐵))) |
12 | 6, 11 | impbid 215 | . 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) = (♯‘𝐵) ↔ (card‘𝐴) = (card‘𝐵))) |
13 | finnum 9443 | . . 3 ⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card) | |
14 | finnum 9443 | . . 3 ⊢ (𝐵 ∈ Fin → 𝐵 ∈ dom card) | |
15 | carden2 9482 | . . 3 ⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) = (card‘𝐵) ↔ 𝐴 ≈ 𝐵)) | |
16 | 13, 14, 15 | syl2an 599 | . 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((card‘𝐴) = (card‘𝐵) ↔ 𝐴 ≈ 𝐵)) |
17 | 12, 16 | bitrd 282 | 1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) = (♯‘𝐵) ↔ 𝐴 ≈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1542 ∈ wcel 2113 Vcvv 3397 class class class wbr 5027 ↦ cmpt 5107 ◡ccnv 5518 dom cdm 5519 ↾ cres 5521 ‘cfv 6333 (class class class)co 7164 ωcom 7593 reccrdg 8067 ≈ cen 8545 Fincfn 8548 cardccrd 9430 0cc0 10608 1c1 10609 + caddc 10611 ♯chash 13775 |
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-pow 5229 ax-pr 5293 ax-un 7473 ax-cnex 10664 ax-resscn 10665 ax-1cn 10666 ax-icn 10667 ax-addcl 10668 ax-addrcl 10669 ax-mulcl 10670 ax-mulrcl 10671 ax-mulcom 10672 ax-addass 10673 ax-mulass 10674 ax-distr 10675 ax-i2m1 10676 ax-1ne0 10677 ax-1rid 10678 ax-rnegex 10679 ax-rrecex 10680 ax-cnre 10681 ax-pre-lttri 10682 ax-pre-lttrn 10683 ax-pre-ltadd 10684 ax-pre-mulgt0 10685 |
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-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rab 3062 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-pss 3860 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-tp 4518 df-op 4520 df-uni 4794 df-int 4834 df-iun 4880 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-pred 6123 df-ord 6169 df-on 6170 df-lim 6171 df-suc 6172 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-riota 7121 df-ov 7167 df-oprab 7168 df-mpo 7169 df-om 7594 df-wrecs 7969 df-recs 8030 df-rdg 8068 df-er 8313 df-en 8549 df-dom 8550 df-sdom 8551 df-fin 8552 df-card 9434 df-pnf 10748 df-mnf 10749 df-xr 10750 df-ltxr 10751 df-le 10752 df-sub 10943 df-neg 10944 df-nn 11710 df-n0 11970 df-z 12056 df-uz 12318 df-hash 13776 |
This theorem is referenced by: hasheni 13793 hasheqf1o 13794 isfinite4 13808 hasheq0 13809 hashsng 13815 hashen1 13816 hashsdom 13827 hash1snb 13865 hashxplem 13879 hashmap 13881 hashpw 13882 hashbclem 13895 phphashd 13911 hash2pr 13914 pr2pwpr 13924 hash3tr 13935 isercolllem2 15108 isercoll 15110 summolem3 15157 mertenslem1 15325 prodmolem3 15372 bpolylem 15487 hashdvds 16205 crth 16208 phimullem 16209 eulerth 16213 4sqlem11 16384 lagsubg2 18452 dfod2 18802 sylow1lem2 18835 sylow2alem2 18854 slwhash 18860 sylow2 18862 sylow3lem1 18863 cyggenod 19115 lt6abl 19127 ablfac1c 19305 ablfac1eu 19307 ablfaclem3 19321 fta1blem 24913 vieta1 25052 isppw 25843 clwlknon2num 28297 numclwlk1lem2 28299 fisshasheq 32636 derangen2 32699 erdsze2lem1 32728 erdsze2lem2 32729 poimirlem9 35398 poimirlem25 35414 poimirlem26 35415 poimirlem27 35416 poimirlem28 35417 eldioph2lem1 40138 frlmpwfi 40479 isnumbasgrplem3 40486 idomsubgmo 40579 |
Copyright terms: Public domain | W3C validator |