Theorem prfi 9329

Description: An unordered pair is finite. For a shorter proof using ax-un 7723, see prfiALT 9330. (Contributed by NM, 22-Aug-2008.) Avoid ax-11 2156, ax-un 7723. (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 4738	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
2		snfi 9051	. . 3 ⊢ {𝐵} ∈ Fin
3	1, 2	eqeltrdi 2841	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ Fin)
4		prprc2 4739	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
5		snfi 9051	. . 3 ⊢ {𝐴} ∈ Fin
6	4, 5	eqeltrdi 2841	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ Fin)
7		2onn 8648	. . . . . 6 ⊢ 2o ∈ ω
8		simp1 1136	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → 𝐴 ∈ V)
9		simp2 1137	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → 𝐵 ∈ V)
10		simp3 1138	. . . . . . 7 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ¬ 𝐴 = 𝐵)
11	8, 9, 10	enpr2d 9057	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ≈ 2o)
12		breq2 5120	. . . . . . 7 ⊢ (𝑥 = 2o → ({𝐴, 𝐵} ≈ 𝑥 ↔ {𝐴, 𝐵} ≈ 2o))
13	12	rspcev 3599	. . . . . 6 ⊢ ((2o ∈ ω ∧ {𝐴, 𝐵} ≈ 2o) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
14	7, 11, 13	sylancr 587	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
15		isfi 8984	. . . . 5 ⊢ ({𝐴, 𝐵} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴, 𝐵} ≈ 𝑥)
16	14, 15	sylibr 234	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵) → {𝐴, 𝐵} ∈ Fin)
17	16	3expia 1121	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (¬ 𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin))
18		dfsn2 4612	. . . . 5 ⊢ {𝐴} = {𝐴, 𝐴}
19		preq2 4707	. . . . 5 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵})
20	18, 19	eqtr2id 2782	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} = {𝐴})
21	20, 5	eqeltrdi 2841	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐵} ∈ Fin)
22	17, 21	pm2.61d2 181	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ Fin)
23	3, 6, 22	ecase 1033	1 ⊢ {𝐴, 𝐵} ∈ Fin

Syntax hints:  ¬ wn 3   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  ∃wrex 3059  Vcvv 3457  {csn 4599  {cpr 4601   class class class wbr 5116  ωcom 7855  2_oc2o 8468   ≈ cen 8950  Fincfn 8953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-12 2176  ax-ext 2706  ax-sep 5263  ax-nul 5273  ax-pr 5399

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-pss 3944  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-br 5117  df-opab 5179  df-tr 5227  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-om 7856  df-1o 8474  df-2o 8475  df-en 8954  df-fin 8957

This theorem is referenced by:  tpfi  9331  fiint  9332  fiintOLD  9333  inelfi  9424  tskpr  10776  hashpw  14442  hashfun  14443  pr2pwpr  14485  hashtpg  14491  hash3tpexb  14500  sumpr  15751  lcmfpr  16631  prmreclem2  16922  acsfn2  17660  isdrs2  18303  efmnd2hash  18857  symg2hash  19358  psgnprfval  19487  gsumpr  19921  znidomb  21507  m2detleib  22554  ovolioo  25506  i1f1  25628  itgioo  25754  limcun  25833  aannenlem2  26274  wilthlem2  27015  perfectlem2  27177  upgrex  29003  ex-hash  30366  prodpr  32738  linds2eq  33314  elrspunsn  33362  constrfin  33696  constrllcllem  33702  constrlccllem  33703  inelpisys  34093  coinfliplem  34419  coinflippv  34424  subfacp1lem1  35122  poimirlem9  37574  kelac2lem  43013  sumpair  44986  refsum2cnlem1  44988  climxlim2lem  45804  ibliooicc  45930  fourierdlem50  46115  fourierdlem51  46116  fourierdlem54  46119  fourierdlem70  46135  fourierdlem71  46136  fourierdlem76  46141  fourierdlem102  46167  fourierdlem103  46168  fourierdlem104  46169  fourierdlem114  46179  saluncl  46276  sge0pr  46353  meadjun  46421  omeunle  46475  perfectALTVlem2  47654  gpgorder  47958  zlmodzxzel  48216  ldepspr  48335  zlmodzxzldeplem2  48363  rrx2line  48606  2sphere  48615