Theorem prfi 9296

Description: An unordered pair is finite. For a shorter proof using ax-un 7737, see prfiALT 9297. (Contributed by NM, 22-Aug-2008.) Avoid ax-11 2194, ax-un 7737. (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 4726	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
2		snfi 9053	. . 3 ⊢ {𝐵} ∈ Fin
3	1, 2	eqeltrdi 2868	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ Fin)
4		prprc2 4727	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
5		snfi 9053	. . 3 ⊢ {𝐴} ∈ Fin
6	4, 5	eqeltrdi 2868	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ Fin)
7		2onn 8633	. . . . . 6 ⊢ 2o ∈ ω
8		simp1 1154	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → 𝐴 ∈ V)
9		simp2 1155	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → 𝐵 ∈ V)
10		simp3 1156	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐴 = 𝐵)
11	8, 9, 10	enpr2d 9058	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ≈ 2o)
12		breq2 5107	. . . . . . 7 ⊢ (𝑥 = 2o → ({𝐴, 𝐵} ≈ 𝑥 ↔ {𝐴, 𝐵} ≈ 2o))
13	12	rspcev 3576	. . . . . 6 ⊢ ((2o ∈ ω ∧ {𝐴, 𝐵} ≈ 2o) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
14	7, 11, 13	sylancr 599	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
15		isfi 8984	. . . . 5 ⊢ ({𝐴, 𝐵} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
16	14, 15	sylibr 237	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ∈ Fin)
17	16	3expia 1139	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (¬ 𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin))
18		dfsn2 4597	. . . . 5 ⊢ {𝐴} = {𝐴, 𝐴}
19		preq2 4695	. . . . 5 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵})
20	18, 19	eqtr2id 2808	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴})
21	20, 5	eqeltrdi 2868	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin)
22	17, 21	pm2.61d2 183	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ Fin)
23	3, 6, 22	ecase 1049	1 ⊢ {𝐴, 𝐵} ∈ Fin

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∃wrex 3086  Vcvv 3450  {csn 4584  {cpr 4586   class class class wbr 5103  ωcom 7863  2_oc2o 8452   ≈ cen 8952  Fincfn 8955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-om 7864  df-1o 8458  df-2o 8459  df-en 8956  df-fin 8959

This theorem is used by:  tpfi  9298  fiint  9299  inelfi  9391  tskpr  10782  hashpw  14504  hashfun  14505  pr2pwpr  14547  hashtpg  14553  hash3tpexb  14562  sumpr  15837  lcmfpr  16720  prmreclem2  17012  acsfn2  17754  isdrs2  18397  efmnd2hash  19006  symg2hash  19522  psgnprfval  19651  gsumpr  20085  znidomb  21777  m2detleib  22856  ovolioo  25799  i1f1  25921  itgioo  26046  limcun  26125  aannenlem2  26568  wilthlem2  27308  perfectlem2  27469  upgrex  29552  ex-hash  30936  prodpr  33299  linds2eq  33817  elrspunsn  33860  constrfin  34259  constrllcllem  34265  constrlccllem  34266  inelpisys  34668  coinfliplem  34993  coinflippv  34998  subfacp1lem1  35761  poimirlem9  38381  kelac2lem  43908  sumpair  45872  refsum2cnlem1  45874  climxlim2lem  46676  ibliooicc  46802  fourierdlem50  46987  fourierdlem51  46988  fourierdlem54  46991  fourierdlem70  47007  fourierdlem71  47008  fourierdlem76  47013  fourierdlem102  47039  fourierdlem103  47040  fourierdlem104  47041  fourierdlem114  47051  saluncl  47148  sge0pr  47225  meadjun  47293  omeunle  47347  perfectALTVlem2  48641  gpgorder  48978  zlmodzxzel  49288  ldepspr  49406  zlmodzxzldeplem2  49434  rrx2line  49673  2sphere  49682