Theorem prfi 9269

Description: An unordered pair is finite. For a shorter proof using ax-un 7719, see prfiALT 9270. (Contributed by NM, 22-Aug-2008.) Avoid ax-11 2192, ax-un 7719. (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 4725	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
2		snfi 9025	. . 3 ⊢ {𝐵} ∈ Fin
3	1, 2	eqeltrdi 2871	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ Fin)
4		prprc2 4726	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
5		snfi 9025	. . 3 ⊢ {𝐴} ∈ Fin
6	4, 5	eqeltrdi 2871	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ Fin)
7		2onn 8613	. . . . . 6 ⊢ 2o ∈ ω
8		simp1 1150	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → 𝐴 ∈ V)
9		simp2 1151	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → 𝐵 ∈ V)
10		simp3 1152	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐴 = 𝐵)
11	8, 9, 10	enpr2d 9030	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ≈ 2o)
12		breq2 5105	. . . . . . 7 ⊢ (𝑥 = 2o → ({𝐴, 𝐵} ≈ 𝑥 ↔ {𝐴, 𝐵} ≈ 2o))
13	12	rspcev 3582	. . . . . 6 ⊢ ((2o ∈ ω ∧ {𝐴, 𝐵} ≈ 2o) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
14	7, 11, 13	sylancr 596	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
15		isfi 8957	. . . . 5 ⊢ ({𝐴, 𝐵} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
16	14, 15	sylibr 236	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ∈ Fin)
17	16	3expia 1135	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (¬ 𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin))
18		dfsn2 4596	. . . . 5 ⊢ {𝐴} = {𝐴, 𝐴}
19		preq2 4694	. . . . 5 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵})
20	18, 19	eqtr2id 2811	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴})
21	20, 5	eqeltrdi 2871	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin)
22	17, 21	pm2.61d2 182	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ Fin)
23	3, 6, 22	ecase 1045	1 ⊢ {𝐴, 𝐵} ∈ Fin

Syntax hints:  ¬ wn 3   ∧ wa 399   ∧ w3a 1099   = wceq 1561   ∈ wcel 2143  ∃wrex 3087  Vcvv 3455  {csn 4583  {cpr 4585   class class class wbr 5101  ωcom 7847  2_oc2o 8432   ≈ cen 8925  Fincfn 8928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-tr 5209  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-ord 6350  df-on 6351  df-lim 6352  df-suc 6353  df-fun 6524  df-fn 6525  df-f 6526  df-f1 6527  df-fo 6528  df-f1o 6529  df-om 7848  df-1o 8438  df-2o 8439  df-en 8929  df-fin 8932

This theorem is referenced by:  tpfi  9271  fiint  9272  inelfi  9365  tskpr  10729  hashpw  14450  hashfun  14451  pr2pwpr  14493  hashtpg  14499  hash3tpexb  14508  sumpr  15776  lcmfpr  16662  prmreclem2  16954  acsfn2  17696  isdrs2  18339  efmnd2hash  18929  symg2hash  19433  psgnprfval  19562  gsumpr  19996  znidomb  21614  m2detleib  22692  ovolioo  25631  i1f1  25753  itgioo  25879  limcun  25958  aannenlem2  26394  wilthlem2  27134  perfectlem2  27295  upgrex  29294  ex-hash  30656  prodpr  33029  linds2eq  33568  elrspunsn  33616  constrfin  34044  constrllcllem  34050  constrlccllem  34051  inelpisys  34452  coinfliplem  34777  coinflippv  34782  subfacp1lem1  35530  poimirlem9  38129  kelac2lem  43642  sumpair  45616  refsum2cnlem1  45618  climxlim2lem  46420  ibliooicc  46546  fourierdlem50  46731  fourierdlem51  46732  fourierdlem54  46735  fourierdlem70  46751  fourierdlem71  46752  fourierdlem76  46757  fourierdlem102  46783  fourierdlem103  46784  fourierdlem104  46785  fourierdlem114  46795  saluncl  46892  sge0pr  46969  meadjun  47037  omeunle  47091  perfectALTVlem2  48345  gpgorder  48682  zlmodzxzel  48978  ldepspr  49096  zlmodzxzldeplem2  49124  rrx2line  49363  2sphere  49372