Theorem prfi 9208

Description: An unordered pair is finite. For a shorter proof using ax-un 7668, see prfiALT 9209. (Contributed by NM, 22-Aug-2008.) Avoid ax-11 2160, ax-un 7668. (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 4715	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
2		snfi 8965	. . 3 ⊢ {𝐵} ∈ Fin
3	1, 2	eqeltrdi 2839	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ Fin)
4		prprc2 4716	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
5		snfi 8965	. . 3 ⊢ {𝐴} ∈ Fin
6	4, 5	eqeltrdi 2839	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ Fin)
7		2onn 8557	. . . . . 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 8970	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ≈ 2o)
12		breq2 5093	. . . . . . 7 ⊢ (𝑥 = 2o → ({𝐴, 𝐵} ≈ 𝑥 ↔ {𝐴, 𝐵} ≈ 2o))
13	12	rspcev 3572	. . . . . 6 ⊢ ((2o ∈ ω ∧ {𝐴, 𝐵} ≈ 2o) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
14	7, 11, 13	sylancr 587	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
15		isfi 8898	. . . . 5 ⊢ ({𝐴, 𝐵} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
16	14, 15	sylibr 234	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ∈ Fin)
17	16	3expia 1121	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (¬ 𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin))
18		dfsn2 4586	. . . . 5 ⊢ {𝐴} = {𝐴, 𝐴}
19		preq2 4684	. . . . 5 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵})
20	18, 19	eqtr2id 2779	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴})
21	20, 5	eqeltrdi 2839	. . 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 2111  ∃wrex 3056  Vcvv 3436  {csn 4573  {cpr 4575   class class class wbr 5089  ωcom 7796  2_oc2o 8379   ≈ cen 8866  Fincfn 8869

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 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

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-nf 1785  df-sb 2068  df-mo 2535  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-om 7797  df-1o 8385  df-2o 8386  df-en 8870  df-fin 8873

This theorem is referenced by:  tpfi  9210  fiint  9211  inelfi  9302  tskpr  10661  hashpw  14343  hashfun  14344  pr2pwpr  14386  hashtpg  14392  hash3tpexb  14401  sumpr  15655  lcmfpr  16538  prmreclem2  16829  acsfn2  17569  isdrs2  18212  efmnd2hash  18802  symg2hash  19304  psgnprfval  19433  gsumpr  19867  znidomb  21498  m2detleib  22546  ovolioo  25496  i1f1  25618  itgioo  25744  limcun  25823  aannenlem2  26264  wilthlem2  27006  perfectlem2  27168  upgrex  29070  ex-hash  30433  prodpr  32809  linds2eq  33346  elrspunsn  33394  constrfin  33759  constrllcllem  33765  constrlccllem  33766  inelpisys  34167  coinfliplem  34492  coinflippv  34497  subfacp1lem1  35223  poimirlem9  37679  kelac2lem  43167  sumpair  45142  refsum2cnlem1  45144  climxlim2lem  45953  ibliooicc  46079  fourierdlem50  46264  fourierdlem51  46265  fourierdlem54  46268  fourierdlem70  46284  fourierdlem71  46285  fourierdlem76  46290  fourierdlem102  46316  fourierdlem103  46317  fourierdlem104  46318  fourierdlem114  46328  saluncl  46425  sge0pr  46502  meadjun  46570  omeunle  46624  perfectALTVlem2  47832  gpgorder  48169  zlmodzxzel  48465  ldepspr  48584  zlmodzxzldeplem2  48612  rrx2line  48851  2sphere  48860