Theorem prfi 9329

Description: An unordered pair is finite. For a shorter proof using ax-un 7761, see prfiALT 9330. (Contributed by NM, 22-Aug-2008.) Avoid ax-11 2196, ax-un 7761. (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 9085	. . 3 ⊢ {𝐵} ∈ Fin
3	1, 2	eqeltrdi 2872	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ Fin)
4		prprc2 4727	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
5		snfi 9085	. . 3 ⊢ {𝐴} ∈ Fin
6	4, 5	eqeltrdi 2872	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ Fin)
7		2onn 8665	. . . . . 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 9090	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ≈ 2o)
12		breq2 5110	. . . . . . 7 ⊢ (𝑥 = 2o → ({𝐴, 𝐵} ≈ 𝑥 ↔ {𝐴, 𝐵} ≈ 2o))
13	12	rspcev 3580	. . . . . 6 ⊢ ((2o ∈ ω ∧ {𝐴, 𝐵} ≈ 2o) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
14	7, 11, 13	sylancr 599	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
15		isfi 9016	. . . . 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 2811	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴})
21	20, 5	eqeltrdi 2872	. . 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 1569   ∈ wcel 2146  ∃wrex 3090  Vcvv 3454  {csn 4588  {cpr 4590   class class class wbr 5106  ωcom 7887  2_oc2o 8484   ≈ cen 8984  Fincfn 8987

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-tr 5216  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 6372  df-on 6373  df-lim 6374  df-suc 6375  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-om 7888  df-1o 8490  df-2o 8491  df-en 8988  df-fin 8991

This theorem is used by:  tpfi  9331  fiint  9332  inelfi  9423  tskpr  10868  hashpw  14594  hashfun  14595  pr2pwpr  14637  hashtpg  14643  hash3tpexb  14652  sumpr  15929  lcmfpr  16817  prmreclem2  17110  acsfn2  17852  isdrs2  18495  efmnd2hash  19105  symg2hash  19621  psgnprfval  19750  gsumpr  20184  znidomb  21882  m2detleib  22961  ovolioo  25904  i1f1  26026  itgioo  26151  limcun  26230  aannenlem2  26671  wilthlem2  27411  perfectlem2  27572  upgrex  29685  ex-hash  31069  prodpr  33473  linds2eq  33992  elrspunsn  34035  constrfin  34434  constrllcllem  34440  constrlccllem  34441  inelpisys  34843  coinfliplem  35167  coinflippv  35172  subfacp1lem1  36068  poimirlem9  38690  kelac2lem  44209  sumpair  46194  refsum2cnlem1  46196  climxlim2lem  46997  ibliooicc  47123  fourierdlem50  47308  fourierdlem51  47309  fourierdlem54  47312  fourierdlem70  47328  fourierdlem71  47329  fourierdlem76  47334  fourierdlem102  47360  fourierdlem103  47361  fourierdlem104  47362  fourierdlem114  47372  saluncl  47469  sge0pr  47546  meadjun  47614  omeunle  47668  perfectALTVlem2  48962  gpgorder  49299  zlmodzxzel  49609  ldepspr  49727  zlmodzxzldeplem2  49755