Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > enfi | Structured version Visualization version GIF version |
Description: Equinumerous sets have the same finiteness. For a shorter proof using ax-pow 5255, see enfiALT 8863. (Contributed by NM, 22-Aug-2008.) Avoid ax-pow 5255. (Revised by BTernaryTau, 23-Sep-2024.) |
Ref | Expression |
---|---|
enfi | ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ensymfib 8859 | . . . . 5 ⊢ (𝐴 ∈ Fin → (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴)) | |
2 | 1 | pm5.32i 578 | . . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) ↔ (𝐴 ∈ Fin ∧ 𝐵 ≈ 𝐴)) |
3 | enfii 8861 | . . . 4 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ≈ 𝐴) → 𝐵 ∈ Fin) | |
4 | 2, 3 | sylbi 220 | . . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ Fin) |
5 | 4 | expcom 417 | . 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin → 𝐵 ∈ Fin)) |
6 | enfii 8861 | . . 3 ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵) → 𝐴 ∈ Fin) | |
7 | 6 | expcom 417 | . 2 ⊢ (𝐴 ≈ 𝐵 → (𝐵 ∈ Fin → 𝐴 ∈ Fin)) |
8 | 5, 7 | impbid 215 | 1 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Fin ↔ 𝐵 ∈ Fin)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∈ wcel 2110 class class class wbr 5050 ≈ cen 8620 Fincfn 8623 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5189 ax-nul 5196 ax-pr 5319 ax-un 7520 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2940 df-ral 3063 df-rex 3064 df-reu 3065 df-rab 3067 df-v 3407 df-sbc 3692 df-dif 3866 df-un 3868 df-in 3870 df-ss 3880 df-pss 3882 df-nul 4235 df-if 4437 df-pw 4512 df-sn 4539 df-pr 4541 df-tp 4543 df-op 4545 df-uni 4817 df-br 5051 df-opab 5113 df-tr 5159 df-id 5452 df-eprel 5457 df-po 5465 df-so 5466 df-fr 5506 df-we 5508 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-ord 6213 df-on 6214 df-lim 6215 df-suc 6216 df-iota 6335 df-fun 6379 df-fn 6380 df-f 6381 df-f1 6382 df-fo 6383 df-f1o 6384 df-fv 6385 df-om 7642 df-1o 8199 df-en 8624 df-fin 8627 |
This theorem is referenced by: enfiiOLD 8891 wofib 9158 en2eleq 9619 sdom2en01 9913 fin23lem21 9950 enfin1ai 9995 fin17 10005 isfin7-2 10007 engch 10239 uzinf 13535 hasheni 13911 isfinite4 13926 symggen 18859 psgnunilem1 18882 dfod2 18952 odhash 18960 gsumval3lem2 19288 gsumval3 19289 cyggic 20534 cusgrfilem3 27542 unidifsnel 30599 unidifsnne 30600 derangen 32844 erdsze2lem1 32875 phpreu 35496 lindsdom 35506 poimirlem30 35542 diophin 40295 diophren 40336 fiphp3d 40342 fiuneneq 40723 |
Copyright terms: Public domain | W3C validator |