MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prfi Structured version   Visualization version   GIF version

Theorem prfi 9360
Description: An unordered pair is finite. For a shorter proof using ax-un 7753, see prfiALT 9361. (Contributed by NM, 22-Aug-2008.) Avoid ax-11 2154, ax-un 7753. (Revised by BTernaryTau, 13-Jan-2025.)
Assertion
Ref Expression
prfi {𝐴, 𝐵} ∈ Fin

Proof of Theorem prfi
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 prprc1 4769 . . 3 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
2 snfi 9081 . . 3 {𝐵} ∈ Fin
31, 2eqeltrdi 2846 . 2 𝐴 ∈ V → {𝐴, 𝐵} ∈ Fin)
4 prprc2 4770 . . 3 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
5 snfi 9081 . . 3 {𝐴} ∈ Fin
64, 5eqeltrdi 2846 . 2 𝐵 ∈ V → {𝐴, 𝐵} ∈ Fin)
7 2onn 8678 . . . . . 6 2o ∈ ω
8 simp1 1135 . . . . . . 7 ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → 𝐴 ∈ V)
9 simp2 1136 . . . . . . 7 ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → 𝐵 ∈ V)
10 simp3 1137 . . . . . . 7 ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐴 = 𝐵)
118, 9, 10enpr2d 9087 . . . . . 6 ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ≈ 2o)
12 breq2 5151 . . . . . . 7 (𝑥 = 2o → ({𝐴, 𝐵} ≈ 𝑥 ↔ {𝐴, 𝐵} ≈ 2o))
1312rspcev 3621 . . . . . 6 ((2o ∈ ω ∧ {𝐴, 𝐵} ≈ 2o) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
147, 11, 13sylancr 587 . . . . 5 ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
15 isfi 9014 . . . . 5 ({𝐴, 𝐵} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
1614, 15sylibr 234 . . . 4 ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ∈ Fin)
17163expia 1120 . . 3 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (¬ 𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin))
18 dfsn2 4643 . . . . 5 {𝐴} = {𝐴, 𝐴}
19 preq2 4738 . . . . 5 (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵})
2018, 19eqtr2id 2787 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴})
2120, 5eqeltrdi 2846 . . 3 (𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin)
2217, 21pm2.61d2 181 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ Fin)
233, 6, 22ecase 1033 1 {𝐴, 𝐵} ∈ Fin
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 395  w3a 1086   = wceq 1536  wcel 2105  wrex 3067  Vcvv 3477  {csn 4630  {cpr 4632   class class class wbr 5147  ωcom 7886  2oc2o 8498  cen 8980  Fincfn 8983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-om 7887  df-1o 8504  df-2o 8505  df-en 8984  df-fin 8987
This theorem is referenced by:  tpfi  9362  fiint  9363  fiintOLD  9364  inelfi  9455  tskpr  10807  hashpw  14471  hashfun  14472  pr2pwpr  14514  hashtpg  14520  hash3tpexb  14529  sumpr  15780  lcmfpr  16660  prmreclem2  16950  acsfn2  17707  isdrs2  18363  efmnd2hash  18919  symg2hash  19423  psgnprfval  19553  gsumpr  19987  znidomb  21597  m2detleib  22652  ovolioo  25616  i1f1  25738  itgioo  25865  limcun  25944  aannenlem2  26385  wilthlem2  27126  perfectlem2  27288  upgrex  29123  ex-hash  30481  prodpr  32832  linds2eq  33388  elrspunsn  33436  constrfin  33750  inelpisys  34134  coinfliplem  34459  coinflippv  34464  subfacp1lem1  35163  poimirlem9  37615  kelac2lem  43052  sumpair  44972  refsum2cnlem1  44974  climxlim2lem  45800  ibliooicc  45926  fourierdlem50  46111  fourierdlem51  46112  fourierdlem54  46115  fourierdlem70  46131  fourierdlem71  46132  fourierdlem76  46137  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem114  46175  saluncl  46272  sge0pr  46349  meadjun  46417  omeunle  46471  perfectALTVlem2  47646  gpgorder  47947  zlmodzxzel  48199  ldepspr  48318  zlmodzxzldeplem2  48346  rrx2line  48589  2sphere  48598
  Copyright terms: Public domain W3C validator