MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unfi Structured version   Visualization version   GIF version

Theorem unfi 8462
Description: The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 16-Nov-2002.)
Assertion
Ref Expression
unfi ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴𝐵) ∈ Fin)

Proof of Theorem unfi
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 diffi 8427 . 2 (𝐵 ∈ Fin → (𝐵𝐴) ∈ Fin)
2 reeanv 3295 . . . 4 (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴𝑥 ∧ (𝐵𝐴) ≈ 𝑦) ↔ (∃𝑥 ∈ ω 𝐴𝑥 ∧ ∃𝑦 ∈ ω (𝐵𝐴) ≈ 𝑦))
3 isfi 8212 . . . . 5 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
4 isfi 8212 . . . . 5 ((𝐵𝐴) ∈ Fin ↔ ∃𝑦 ∈ ω (𝐵𝐴) ≈ 𝑦)
53, 4anbi12i 614 . . . 4 ((𝐴 ∈ Fin ∧ (𝐵𝐴) ∈ Fin) ↔ (∃𝑥 ∈ ω 𝐴𝑥 ∧ ∃𝑦 ∈ ω (𝐵𝐴) ≈ 𝑦))
62, 5bitr4i 269 . . 3 (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴𝑥 ∧ (𝐵𝐴) ≈ 𝑦) ↔ (𝐴 ∈ Fin ∧ (𝐵𝐴) ∈ Fin))
7 nnacl 7924 . . . . 5 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 +𝑜 𝑦) ∈ ω)
8 unfilem3 8461 . . . . . . 7 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑦 ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥))
9 entr 8240 . . . . . . . 8 (((𝐵𝐴) ≈ 𝑦𝑦 ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) → (𝐵𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥))
109expcom 400 . . . . . . 7 (𝑦 ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥) → ((𝐵𝐴) ≈ 𝑦 → (𝐵𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)))
118, 10syl 17 . . . . . 6 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐵𝐴) ≈ 𝑦 → (𝐵𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)))
12 disjdif 4236 . . . . . . . 8 (𝐴 ∩ (𝐵𝐴)) = ∅
13 disjdif 4236 . . . . . . . 8 (𝑥 ∩ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) = ∅
14 unen 8275 . . . . . . . 8 (((𝐴𝑥 ∧ (𝐵𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) ∧ ((𝐴 ∩ (𝐵𝐴)) = ∅ ∧ (𝑥 ∩ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) = ∅)) → (𝐴 ∪ (𝐵𝐴)) ≈ (𝑥 ∪ ((𝑥 +𝑜 𝑦) ∖ 𝑥)))
1512, 13, 14mpanr12 688 . . . . . . 7 ((𝐴𝑥 ∧ (𝐵𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) → (𝐴 ∪ (𝐵𝐴)) ≈ (𝑥 ∪ ((𝑥 +𝑜 𝑦) ∖ 𝑥)))
16 undif2 4240 . . . . . . . . 9 (𝐴 ∪ (𝐵𝐴)) = (𝐴𝐵)
1716a1i 11 . . . . . . . 8 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ∪ (𝐵𝐴)) = (𝐴𝐵))
18 nnaword1 7942 . . . . . . . . 9 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑥 ⊆ (𝑥 +𝑜 𝑦))
19 undif 4245 . . . . . . . . 9 (𝑥 ⊆ (𝑥 +𝑜 𝑦) ↔ (𝑥 ∪ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) = (𝑥 +𝑜 𝑦))
2018, 19sylib 209 . . . . . . . 8 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ∪ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) = (𝑥 +𝑜 𝑦))
2117, 20breq12d 4857 . . . . . . 7 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ∪ (𝐵𝐴)) ≈ (𝑥 ∪ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) ↔ (𝐴𝐵) ≈ (𝑥 +𝑜 𝑦)))
2215, 21syl5ib 235 . . . . . 6 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴𝑥 ∧ (𝐵𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) → (𝐴𝐵) ≈ (𝑥 +𝑜 𝑦)))
2311, 22sylan2d 594 . . . . 5 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴𝑥 ∧ (𝐵𝐴) ≈ 𝑦) → (𝐴𝐵) ≈ (𝑥 +𝑜 𝑦)))
24 breq2 4848 . . . . . . 7 (𝑧 = (𝑥 +𝑜 𝑦) → ((𝐴𝐵) ≈ 𝑧 ↔ (𝐴𝐵) ≈ (𝑥 +𝑜 𝑦)))
2524rspcev 3502 . . . . . 6 (((𝑥 +𝑜 𝑦) ∈ ω ∧ (𝐴𝐵) ≈ (𝑥 +𝑜 𝑦)) → ∃𝑧 ∈ ω (𝐴𝐵) ≈ 𝑧)
26 isfi 8212 . . . . . 6 ((𝐴𝐵) ∈ Fin ↔ ∃𝑧 ∈ ω (𝐴𝐵) ≈ 𝑧)
2725, 26sylibr 225 . . . . 5 (((𝑥 +𝑜 𝑦) ∈ ω ∧ (𝐴𝐵) ≈ (𝑥 +𝑜 𝑦)) → (𝐴𝐵) ∈ Fin)
287, 23, 27syl6an 666 . . . 4 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴𝑥 ∧ (𝐵𝐴) ≈ 𝑦) → (𝐴𝐵) ∈ Fin))
2928rexlimivv 3224 . . 3 (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴𝑥 ∧ (𝐵𝐴) ≈ 𝑦) → (𝐴𝐵) ∈ Fin)
306, 29sylbir 226 . 2 ((𝐴 ∈ Fin ∧ (𝐵𝐴) ∈ Fin) → (𝐴𝐵) ∈ Fin)
311, 30sylan2 582 1 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴𝐵) ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wcel 2156  wrex 3097  cdif 3766  cun 3767  cin 3768  wss 3769  c0 4116   class class class wbr 4844  (class class class)co 6870  ωcom 7291   +𝑜 coa 7789  cen 8185  Fincfn 8188
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-oadd 7796  df-er 7975  df-en 8189  df-fin 8192
This theorem is referenced by:  unfi2  8464  difinf  8465  xpfi  8466  prfi  8470  tpfi  8471  fnfi  8473  iunfi  8489  pwfilem  8495  fsuppun  8529  fsuppunfi  8530  ressuppfi  8536  fiin  8563  cantnfp1lem1  8818  ficardun2  9306  ackbij1lem6  9328  ackbij1lem16  9338  fin23lem28  9443  fin23lem30  9445  isfin1-3  9489  axcclem  9560  hashun  13385  hashunlei  13425  hashmap  13435  hashbclem  13449  hashf1lem1  13452  hashf1lem2  13453  hashf1  13454  fsumsplitsn  14693  fsummsnunz  14702  fsumsplitsnun  14703  fsummsnunzOLD  14704  fsumsplitsnunOLD  14705  incexclem  14786  isumltss  14798  fprodsplitsn  14936  lcmfunsnlem2lem1  15566  lcmfunsnlem2lem2  15567  lcmfunsnlem2  15568  lcmfun  15573  ramub1lem1  15943  fpwipodrs  17365  acsfiindd  17378  symgfisg  18085  gsumzunsnd  18552  gsumunsnfd  18553  psrbagaddcl  19575  mplsubg  19642  mpllss  19643  dsmmacl  20292  fctop  21019  uncmp  21417  bwth  21424  lfinun  21539  locfincmp  21540  comppfsc  21546  1stckgenlem  21567  ptbasin  21591  cfinfil  21907  fin1aufil  21946  alexsubALTlem3  22063  tmdgsum  22109  tsmsfbas  22141  tsmsgsum  22152  tsmsres  22157  tsmsxplem1  22166  prdsmet  22385  prdsbl  22506  icccmplem2  22836  rrxmval  23399  rrxmet  23402  rrxdstprj1  23403  ovolfiniun  23481  volfiniun  23527  fta1glem2  24139  fta1lem  24275  aannenlem2  24297  aalioulem2  24301  dchrfi  25193  usgrfilem  26434  ffsrn  29830  eulerpartlemt  30757  ballotlemgun  30910  hgt750lemb  31058  hgt750leme  31060  lindsenlbs  33715  poimirlem31  33751  poimirlem32  33752  itg2addnclem2  33772  ftc1anclem7  33801  ftc1anc  33803  prdsbnd  33901  pclfinN  35678  elrfi  37756  mzpcompact2lem  37813  eldioph2  37824  lsmfgcl  38142  fiuneneq  38273  unfid  39831  dvmptfprodlem  40636  dvnprodlem2  40639  fourierdlem50  40849  fourierdlem51  40850  fourierdlem54  40853  fourierdlem76  40875  fourierdlem80  40879  fourierdlem102  40901  fourierdlem103  40902  fourierdlem104  40903  fourierdlem114  40913  sge0resplit  41099  sge0iunmptlemfi  41106  sge0xaddlem1  41126  hoiprodp1  41281  sge0hsphoire  41282  hoidmvlelem1  41288  hoidmvlelem2  41289  hoidmvlelem5  41292  hspmbllem2  41320  fsummmodsnunz  41917  mndpsuppfi  42721
  Copyright terms: Public domain W3C validator