Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > hashprg | Structured version Visualization version GIF version |
Description: The size of an unordered pair. (Contributed by Mario Carneiro, 27-Sep-2013.) (Revised by Mario Carneiro, 5-May-2016.) (Revised by AV, 18-Sep-2021.) |
Ref | Expression |
---|---|
hashprg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≠ 𝐵 ↔ (♯‘{𝐴, 𝐵}) = 2)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 485 | . . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ 𝑊) | |
2 | elsni 4601 | . . . . . . 7 ⊢ (𝐵 ∈ {𝐴} → 𝐵 = 𝐴) | |
3 | 2 | eqcomd 2743 | . . . . . 6 ⊢ (𝐵 ∈ {𝐴} → 𝐴 = 𝐵) |
4 | 3 | necon3ai 2966 | . . . . 5 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ {𝐴}) |
5 | snfi 8921 | . . . . . 6 ⊢ {𝐴} ∈ Fin | |
6 | hashunsng 14219 | . . . . . . 7 ⊢ (𝐵 ∈ 𝑊 → (({𝐴} ∈ Fin ∧ ¬ 𝐵 ∈ {𝐴}) → (♯‘({𝐴} ∪ {𝐵})) = ((♯‘{𝐴}) + 1))) | |
7 | 6 | imp 407 | . . . . . 6 ⊢ ((𝐵 ∈ 𝑊 ∧ ({𝐴} ∈ Fin ∧ ¬ 𝐵 ∈ {𝐴})) → (♯‘({𝐴} ∪ {𝐵})) = ((♯‘{𝐴}) + 1)) |
8 | 5, 7 | mpanr1 701 | . . . . 5 ⊢ ((𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ {𝐴}) → (♯‘({𝐴} ∪ {𝐵})) = ((♯‘{𝐴}) + 1)) |
9 | 1, 4, 8 | syl2an 596 | . . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → (♯‘({𝐴} ∪ {𝐵})) = ((♯‘{𝐴}) + 1)) |
10 | hashsng 14196 | . . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1) | |
11 | 10 | adantr 481 | . . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (♯‘{𝐴}) = 1) |
12 | 11 | adantr 481 | . . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → (♯‘{𝐴}) = 1) |
13 | 12 | oveq1d 7364 | . . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → ((♯‘{𝐴}) + 1) = (1 + 1)) |
14 | 9, 13 | eqtrd 2777 | . . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → (♯‘({𝐴} ∪ {𝐵})) = (1 + 1)) |
15 | df-pr 4587 | . . . 4 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) | |
16 | 15 | fveq2i 6840 | . . 3 ⊢ (♯‘{𝐴, 𝐵}) = (♯‘({𝐴} ∪ {𝐵})) |
17 | df-2 12149 | . . 3 ⊢ 2 = (1 + 1) | |
18 | 14, 16, 17 | 3eqtr4g 2802 | . 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → (♯‘{𝐴, 𝐵}) = 2) |
19 | 1ne2 12294 | . . . . . . 7 ⊢ 1 ≠ 2 | |
20 | 19 | a1i 11 | . . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 1 ≠ 2) |
21 | 11, 20 | eqnetrd 3009 | . . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (♯‘{𝐴}) ≠ 2) |
22 | dfsn2 4597 | . . . . . . . 8 ⊢ {𝐴} = {𝐴, 𝐴} | |
23 | preq2 4693 | . . . . . . . 8 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵}) | |
24 | 22, 23 | eqtr2id 2790 | . . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴}) |
25 | 24 | fveq2d 6841 | . . . . . 6 ⊢ (𝐴 = 𝐵 → (♯‘{𝐴, 𝐵}) = (♯‘{𝐴})) |
26 | 25 | neeq1d 3001 | . . . . 5 ⊢ (𝐴 = 𝐵 → ((♯‘{𝐴, 𝐵}) ≠ 2 ↔ (♯‘{𝐴}) ≠ 2)) |
27 | 21, 26 | syl5ibrcom 246 | . . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 = 𝐵 → (♯‘{𝐴, 𝐵}) ≠ 2)) |
28 | 27 | necon2d 2964 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((♯‘{𝐴, 𝐵}) = 2 → 𝐴 ≠ 𝐵)) |
29 | 28 | imp 407 | . 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (♯‘{𝐴, 𝐵}) = 2) → 𝐴 ≠ 𝐵) |
30 | 18, 29 | impbida 799 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≠ 𝐵 ↔ (♯‘{𝐴, 𝐵}) = 2)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ≠ wne 2941 ∪ cun 3906 {csn 4584 {cpr 4586 ‘cfv 6491 (class class class)co 7349 Fincfn 8816 1c1 10985 + caddc 10987 2c2 12141 ♯chash 14157 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-sep 5254 ax-nul 5261 ax-pow 5318 ax-pr 5382 ax-un 7662 ax-cnex 11040 ax-resscn 11041 ax-1cn 11042 ax-icn 11043 ax-addcl 11044 ax-addrcl 11045 ax-mulcl 11046 ax-mulrcl 11047 ax-mulcom 11048 ax-addass 11049 ax-mulass 11050 ax-distr 11051 ax-i2m1 11052 ax-1ne0 11053 ax-1rid 11054 ax-rnegex 11055 ax-rrecex 11056 ax-cnre 11057 ax-pre-lttri 11058 ax-pre-lttrn 11059 ax-pre-ltadd 11060 ax-pre-mulgt0 11061 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-reu 3352 df-rab 3406 df-v 3445 df-sbc 3738 df-csb 3854 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3927 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-int 4906 df-iun 4954 df-br 5104 df-opab 5166 df-mpt 5187 df-tr 5221 df-id 5528 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5585 df-we 5587 df-xp 5636 df-rel 5637 df-cnv 5638 df-co 5639 df-dm 5640 df-rn 5641 df-res 5642 df-ima 5643 df-pred 6249 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6443 df-fun 6493 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-fv 6499 df-riota 7305 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7793 df-1st 7911 df-2nd 7912 df-frecs 8179 df-wrecs 8210 df-recs 8284 df-rdg 8323 df-1o 8379 df-oadd 8383 df-er 8581 df-en 8817 df-dom 8818 df-sdom 8819 df-fin 8820 df-dju 9770 df-card 9808 df-pnf 11124 df-mnf 11125 df-xr 11126 df-ltxr 11127 df-le 11128 df-sub 11320 df-neg 11321 df-nn 12087 df-2 12149 df-n0 12347 df-z 12433 df-uz 12696 df-fz 13353 df-hash 14158 |
This theorem is referenced by: hashprb 14224 prhash2ex 14226 hashfun 14264 hash2exprb 14297 nehash2 14300 hashtpg 14311 elss2prb 14313 wrdlen2i 14762 isnzr2hash 20657 upgrex 27841 umgrbi 27850 usgr1e 27991 usgrexmplef 28005 cusgrexilem2 28188 cusgrfilem1 28201 umgr2v2e 28271 vdegp1bi 28283 eulerpathpr 28982 ccfldextdgrr 32139 coinflipprob 32852 cusgredgex 33488 subfacp1lem1 33546 poimirlem9 35982 fourierdlem54 44154 fourierdlem102 44202 fourierdlem103 44203 fourierdlem104 44204 fourierdlem114 44214 prpair 45442 prproropf1olem1 45444 paireqne 45452 prprspr2 45459 reuprpr 45464 |
Copyright terms: Public domain | W3C validator |