Theorem prfi 9315

Description: An unordered pair is finite. For a shorter proof using ax-un 7751, see prfiALT 9316. (Contributed by NM, 22-Aug-2008.) Avoid ax-11 2194, ax-un 7751. (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 9071	. . 3 ⊢ {𝐵} ∈ Fin
3	1, 2	eqeltrdi 2869	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ Fin)
4		prprc2 4727	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
5		snfi 9071	. . 3 ⊢ {𝐴} ∈ Fin
6	4, 5	eqeltrdi 2869	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ Fin)
7		2onn 8651	. . . . . 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 9076	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ≈ 2o)
12		breq2 5107	. . . . . . 7 ⊢ (𝑥 = 2o → ({𝐴, 𝐵} ≈ 𝑥 ↔ {𝐴, 𝐵} ≈ 2o))
13	12	rspcev 3577	. . . . . 6 ⊢ ((2o ∈ ω ∧ {𝐴, 𝐵} ≈ 2o) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
14	7, 11, 13	sylancr 599	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
15		isfi 9002	. . . . 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 2809	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴})
21	20, 5	eqeltrdi 2869	. . 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 3087  Vcvv 3451  {csn 4584  {cpr 4586   class class class wbr 5103  ωcom 7877  2_oc2o 8470   ≈ cen 8970  Fincfn 8973

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 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-om 7878  df-1o 8476  df-2o 8477  df-en 8974  df-fin 8977

This theorem is used by:  tpfi  9317  fiint  9318  inelfi  9410  tskpr  10855  hashpw  14581  hashfun  14582  pr2pwpr  14624  hashtpg  14630  hash3tpexb  14639  sumpr  15914  lcmfpr  16802  prmreclem2  17095  acsfn2  17837  isdrs2  18480  efmnd2hash  19090  symg2hash  19606  psgnprfval  19735  gsumpr  20169  znidomb  21867  m2detleib  22946  ovolioo  25889  i1f1  26011  itgioo  26136  limcun  26215  aannenlem2  26656  wilthlem2  27396  perfectlem2  27557  upgrex  29670  ex-hash  31054  prodpr  33417  linds2eq  33936  elrspunsn  33979  constrfin  34378  constrllcllem  34384  constrlccllem  34385  inelpisys  34787  coinfliplem  35111  coinflippv  35116  subfacp1lem1  35944  poimirlem9  38547  kelac2lem  44065  sumpair  46051  refsum2cnlem1  46053  climxlim2lem  46854  ibliooicc  46980  fourierdlem50  47165  fourierdlem51  47166  fourierdlem54  47169  fourierdlem70  47185  fourierdlem71  47186  fourierdlem76  47191  fourierdlem102  47217  fourierdlem103  47218  fourierdlem104  47219  fourierdlem114  47229  saluncl  47326  sge0pr  47403  meadjun  47471  omeunle  47525  perfectALTVlem2  48819  gpgorder  49156  zlmodzxzel  49466  ldepspr  49584  zlmodzxzldeplem2  49612  rrx2line  49851  2sphere  49860