Theorem prfi 9222

Description: An unordered pair is finite. For a shorter proof using ax-un 7678, see prfiALT 9223. (Contributed by NM, 22-Aug-2008.) Avoid ax-11 2162, ax-un 7678. (Revised by BTernaryTau, 13-Jan-2025.)

Assertion

Ref	Expression
prfi	⊢ {𝐴, 𝐵} ∈ Fin

Proof of Theorem prfi

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		prprc1 4720	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
2		snfi 8978	. . 3 ⊢ {𝐵} ∈ Fin
3	1, 2	eqeltrdi 2842	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ Fin)
4		prprc2 4721	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
5		snfi 8978	. . 3 ⊢ {𝐴} ∈ Fin
6	4, 5	eqeltrdi 2842	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ Fin)
7		2onn 8568	. . . . . 6 ⊢ 2o ∈ ω
8		simp1 1136	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → 𝐴 ∈ V)
9		simp2 1137	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → 𝐵 ∈ V)
10		simp3 1138	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐴 = 𝐵)
11	8, 9, 10	enpr2d 8983	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ≈ 2o)
12		breq2 5100	. . . . . . 7 ⊢ (𝑥 = 2o → ({𝐴, 𝐵} ≈ 𝑥 ↔ {𝐴, 𝐵} ≈ 2o))
13	12	rspcev 3574	. . . . . 6 ⊢ ((2o ∈ ω ∧ {𝐴, 𝐵} ≈ 2o) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
14	7, 11, 13	sylancr 587	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
15		isfi 8910	. . . . 5 ⊢ ({𝐴, 𝐵} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
16	14, 15	sylibr 234	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ∈ Fin)
17	16	3expia 1121	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (¬ 𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin))
18		dfsn2 4591	. . . . 5 ⊢ {𝐴} = {𝐴, 𝐴}
19		preq2 4689	. . . . 5 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵})
20	18, 19	eqtr2id 2782	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴})
21	20, 5	eqeltrdi 2842	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin)
22	17, 21	pm2.61d2 181	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ Fin)
23	3, 6, 22	ecase 1033	1 ⊢ {𝐴, 𝐵} ∈ Fin

Syntax hints:  ¬ wn 3   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ∃wrex 3058  Vcvv 3438  {csn 4578  {cpr 4580   class class class wbr 5096  ωcom 7806  2_oc2o 8389   ≈ cen 8878  Fincfn 8881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2537  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-om 7807  df-1o 8395  df-2o 8396  df-en 8882  df-fin 8885

This theorem is referenced by:  tpfi  9224  fiint  9225  inelfi  9319  tskpr  10679  hashpw  14357  hashfun  14358  pr2pwpr  14400  hashtpg  14406  hash3tpexb  14415  sumpr  15669  lcmfpr  16552  prmreclem2  16843  acsfn2  17584  isdrs2  18227  efmnd2hash  18817  symg2hash  19319  psgnprfval  19448  gsumpr  19882  znidomb  21514  m2detleib  22573  ovolioo  25523  i1f1  25645  itgioo  25771  limcun  25850  aannenlem2  26291  wilthlem2  27033  perfectlem2  27195  upgrex  29114  ex-hash  30477  prodpr  32856  linds2eq  33411  elrspunsn  33459  constrfin  33852  constrllcllem  33858  constrlccllem  33859  inelpisys  34260  coinfliplem  34585  coinflippv  34590  subfacp1lem1  35322  poimirlem9  37769  kelac2lem  43248  sumpair  45222  refsum2cnlem1  45224  climxlim2lem  46031  ibliooicc  46157  fourierdlem50  46342  fourierdlem51  46343  fourierdlem54  46346  fourierdlem70  46362  fourierdlem71  46363  fourierdlem76  46368  fourierdlem102  46394  fourierdlem103  46395  fourierdlem104  46396  fourierdlem114  46406  saluncl  46503  sge0pr  46580  meadjun  46648  omeunle  46702  perfectALTVlem2  47910  gpgorder  48247  zlmodzxzel  48543  ldepspr  48661  zlmodzxzldeplem2  48689  rrx2line  48928  2sphere  48937