Theorem prfi 9224

Description: An unordered pair is finite. For a shorter proof using ax-un 7678, see prfiALT 9225. (Contributed by NM, 22-Aug-2008.) Avoid ax-11 2168, 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 4697	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
2		snfi 8980	. . 3 ⊢ {𝐵} ∈ Fin
3	1, 2	eqeltrdi 2847	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ Fin)
4		prprc2 4698	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
5		snfi 8980	. . 3 ⊢ {𝐴} ∈ Fin
6	4, 5	eqeltrdi 2847	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ Fin)
7		2onn 8568	. . . . . 6 ⊢ 2o ∈ ω
8		simp1 1142	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → 𝐴 ∈ V)
9		simp2 1143	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → 𝐵 ∈ V)
10		simp3 1144	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐴 = 𝐵)
11	8, 9, 10	enpr2d 8985	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ≈ 2o)
12		breq2 5076	. . . . . . 7 ⊢ (𝑥 = 2o → ({𝐴, 𝐵} ≈ 𝑥 ↔ {𝐴, 𝐵} ≈ 2o))
13	12	rspcev 3560	. . . . . 6 ⊢ ((2o ∈ ω ∧ {𝐴, 𝐵} ≈ 2o) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
14	7, 11, 13	sylancr 593	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
15		isfi 8912	. . . . 5 ⊢ ({𝐴, 𝐵} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
16	14, 15	sylibr 235	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ∈ Fin)
17	16	3expia 1127	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (¬ 𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin))
18		dfsn2 4568	. . . . 5 ⊢ {𝐴} = {𝐴, 𝐴}
19		preq2 4666	. . . . 5 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵})
20	18, 19	eqtr2id 2787	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴})
21	20, 5	eqeltrdi 2847	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin)
22	17, 21	pm2.61d2 182	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ Fin)
23	3, 6, 22	ecase 1039	1 ⊢ {𝐴, 𝐵} ∈ Fin

Syntax hints:  ¬ wn 3   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ∃wrex 3063  Vcvv 3431  {csn 4555  {cpr 4557   class class class wbr 5072  ωcom 7806  2_oc2o 8389   ≈ cen 8880  Fincfn 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-mo 2543  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-om 7807  df-1o 8395  df-2o 8396  df-en 8884  df-fin 8887

This theorem is referenced by:  tpfi  9226  fiint  9227  inelfi  9321  tskpr  10684  hashpw  14389  hashfun  14390  pr2pwpr  14432  hashtpg  14438  hash3tpexb  14447  sumpr  15701  lcmfpr  16587  prmreclem2  16879  acsfn2  17620  isdrs2  18263  efmnd2hash  18853  symg2hash  19358  psgnprfval  19487  gsumpr  19921  znidomb  21536  m2detleib  22614  ovolioo  25553  i1f1  25675  itgioo  25801  limcun  25880  aannenlem2  26313  wilthlem2  27050  perfectlem2  27211  upgrex  29179  ex-hash  30541  prodpr  32918  linds2eq  33464  elrspunsn  33512  constrfin  33930  constrllcllem  33936  constrlccllem  33937  inelpisys  34338  coinfliplem  34663  coinflippv  34668  subfacp1lem1  35407  poimirlem9  37996  kelac2lem  43509  sumpair  45483  refsum2cnlem1  45485  climxlim2lem  46288  ibliooicc  46414  fourierdlem50  46599  fourierdlem51  46600  fourierdlem54  46603  fourierdlem70  46619  fourierdlem71  46620  fourierdlem76  46625  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem114  46663  saluncl  46760  sge0pr  46837  meadjun  46905  omeunle  46959  perfectALTVlem2  48213  gpgorder  48550  zlmodzxzel  48846  ldepspr  48964  zlmodzxzldeplem2  48992  rrx2line  49231  2sphere  49240