Theorem prfi 9283

Description: An unordered pair is finite. For a shorter proof using ax-un 7733, see prfiALT 9284. (Contributed by NM, 22-Aug-2008.) Avoid ax-11 2198, ax-un 7733. (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 4736	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
2		snfi 9040	. . 3 ⊢ {𝐵} ∈ Fin
3	1, 2	eqeltrdi 2877	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ Fin)
4		prprc2 4737	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
5		snfi 9040	. . 3 ⊢ {𝐴} ∈ Fin
6	4, 5	eqeltrdi 2877	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ Fin)
7		2onn 8628	. . . . . 6 ⊢ 2o ∈ ω
8		simp1 1152	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → 𝐴 ∈ V)
9		simp2 1153	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → 𝐵 ∈ V)
10		simp3 1154	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐴 = 𝐵)
11	8, 9, 10	enpr2d 9045	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ≈ 2o)
12		breq2 5117	. . . . . . 7 ⊢ (𝑥 = 2o → ({𝐴, 𝐵} ≈ 𝑥 ↔ {𝐴, 𝐵} ≈ 2o))
13	12	rspcev 3590	. . . . . 6 ⊢ ((2o ∈ ω ∧ {𝐴, 𝐵} ≈ 2o) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
14	7, 11, 13	sylancr 598	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
15		isfi 8972	. . . . 5 ⊢ ({𝐴, 𝐵} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
16	14, 15	sylibr 237	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ∈ Fin)
17	16	3expia 1137	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (¬ 𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin))
18		dfsn2 4607	. . . . 5 ⊢ {𝐴} = {𝐴, 𝐴}
19		preq2 4705	. . . . 5 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵})
20	18, 19	eqtr2id 2817	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴})
21	20, 5	eqeltrdi 2877	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin)
22	17, 21	pm2.61d2 183	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ Fin)
23	3, 6, 22	ecase 1047	1 ⊢ {𝐴, 𝐵} ∈ Fin

Syntax hints:  ¬ wn 3   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  ∃wrex 3095  Vcvv 3463  {csn 4594  {cpr 4596   class class class wbr 5113  ωcom 7862  2_oc2o 8447   ≈ cen 8940  Fincfn 8943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-mo 2573  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-om 7863  df-1o 8453  df-2o 8454  df-en 8944  df-fin 8947

This theorem is referenced by:  tpfi  9285  fiint  9286  inelfi  9378  tskpr  10755  hashpw  14473  hashfun  14474  pr2pwpr  14516  hashtpg  14522  hash3tpexb  14531  sumpr  15799  lcmfpr  16685  prmreclem2  16977  acsfn2  17719  isdrs2  18362  efmnd2hash  18953  symg2hash  19462  psgnprfval  19591  gsumpr  20025  znidomb  21680  m2detleib  22757  ovolioo  25696  i1f1  25818  itgioo  25944  limcun  26023  aannenlem2  26459  wilthlem2  27199  perfectlem2  27360  upgrex  29383  ex-hash  30745  prodpr  33111  linds2eq  33638  elrspunsn  33681  constrfin  34081  constrllcllem  34087  constrlccllem  34088  inelpisys  34489  coinfliplem  34814  coinflippv  34819  subfacp1lem1  35604  poimirlem9  38202  kelac2lem  43717  sumpair  45681  refsum2cnlem1  45683  climxlim2lem  46485  ibliooicc  46611  fourierdlem50  46796  fourierdlem51  46797  fourierdlem54  46800  fourierdlem70  46816  fourierdlem71  46817  fourierdlem76  46822  fourierdlem102  46848  fourierdlem103  46849  fourierdlem104  46850  fourierdlem114  46860  saluncl  46957  sge0pr  47034  meadjun  47102  omeunle  47156  perfectALTVlem2  48410  gpgorder  48747  zlmodzxzel  49054  ldepspr  49172  zlmodzxzldeplem2  49200  rrx2line  49439  2sphere  49448