Theorem prfi 9281

Description: An unordered pair is finite. For a shorter proof using ax-un 7714, see prfiALT 9282. (Contributed by NM, 22-Aug-2008.) Avoid ax-11 2158, ax-un 7714. (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 4732	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
2		snfi 9017	. . 3 ⊢ {𝐵} ∈ Fin
3	1, 2	eqeltrdi 2837	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ Fin)
4		prprc2 4733	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
5		snfi 9017	. . 3 ⊢ {𝐴} ∈ Fin
6	4, 5	eqeltrdi 2837	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ Fin)
7		2onn 8609	. . . . . 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 9023	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ≈ 2o)
12		breq2 5114	. . . . . . 7 ⊢ (𝑥 = 2o → ({𝐴, 𝐵} ≈ 𝑥 ↔ {𝐴, 𝐵} ≈ 2o))
13	12	rspcev 3591	. . . . . 6 ⊢ ((2o ∈ ω ∧ {𝐴, 𝐵} ≈ 2o) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
14	7, 11, 13	sylancr 587	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
15		isfi 8950	. . . . 5 ⊢ ({𝐴, 𝐵} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
16	14, 15	sylibr 234	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ∈ Fin)
17	16	3expia 1121	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (¬ 𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin))
18		dfsn2 4605	. . . . 5 ⊢ {𝐴} = {𝐴, 𝐴}
19		preq2 4701	. . . . 5 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵})
20	18, 19	eqtr2id 2778	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴})
21	20, 5	eqeltrdi 2837	. . 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 1540   ∈ wcel 2109  ∃wrex 3054  Vcvv 3450  {csn 4592  {cpr 4594   class class class wbr 5110  ωcom 7845  2_oc2o 8431   ≈ cen 8918  Fincfn 8921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-om 7846  df-1o 8437  df-2o 8438  df-en 8922  df-fin 8925

This theorem is referenced by:  tpfi  9283  fiint  9284  fiintOLD  9285  inelfi  9376  tskpr  10730  hashpw  14408  hashfun  14409  pr2pwpr  14451  hashtpg  14457  hash3tpexb  14466  sumpr  15721  lcmfpr  16604  prmreclem2  16895  acsfn2  17631  isdrs2  18274  efmnd2hash  18828  symg2hash  19329  psgnprfval  19458  gsumpr  19892  znidomb  21478  m2detleib  22525  ovolioo  25476  i1f1  25598  itgioo  25724  limcun  25803  aannenlem2  26244  wilthlem2  26986  perfectlem2  27148  upgrex  29026  ex-hash  30389  prodpr  32758  linds2eq  33359  elrspunsn  33407  constrfin  33743  constrllcllem  33749  constrlccllem  33750  inelpisys  34151  coinfliplem  34477  coinflippv  34482  subfacp1lem1  35173  poimirlem9  37630  kelac2lem  43060  sumpair  45036  refsum2cnlem1  45038  climxlim2lem  45850  ibliooicc  45976  fourierdlem50  46161  fourierdlem51  46162  fourierdlem54  46165  fourierdlem70  46181  fourierdlem71  46182  fourierdlem76  46187  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem114  46225  saluncl  46322  sge0pr  46399  meadjun  46467  omeunle  46521  perfectALTVlem2  47727  gpgorder  48054  zlmodzxzel  48347  ldepspr  48466  zlmodzxzldeplem2  48494  rrx2line  48733  2sphere  48742