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

Theorem unfi 8394
 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 8359 . 2 (𝐵 ∈ Fin → (𝐵𝐴) ∈ Fin)
2 reeanv 3245 . . . 4 (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴𝑥 ∧ (𝐵𝐴) ≈ 𝑦) ↔ (∃𝑥 ∈ ω 𝐴𝑥 ∧ ∃𝑦 ∈ ω (𝐵𝐴) ≈ 𝑦))
3 isfi 8147 . . . . 5 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
4 isfi 8147 . . . . 5 ((𝐵𝐴) ∈ Fin ↔ ∃𝑦 ∈ ω (𝐵𝐴) ≈ 𝑦)
53, 4anbi12i 735 . . . 4 ((𝐴 ∈ Fin ∧ (𝐵𝐴) ∈ Fin) ↔ (∃𝑥 ∈ ω 𝐴𝑥 ∧ ∃𝑦 ∈ ω (𝐵𝐴) ≈ 𝑦))
62, 5bitr4i 267 . . 3 (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴𝑥 ∧ (𝐵𝐴) ≈ 𝑦) ↔ (𝐴 ∈ Fin ∧ (𝐵𝐴) ∈ Fin))
7 nnacl 7862 . . . . 5 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 +𝑜 𝑦) ∈ ω)
8 unfilem3 8393 . . . . . . 7 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑦 ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥))
9 entr 8175 . . . . . . . 8 (((𝐵𝐴) ≈ 𝑦𝑦 ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) → (𝐵𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥))
109expcom 450 . . . . . . 7 (𝑦 ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥) → ((𝐵𝐴) ≈ 𝑦 → (𝐵𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)))
118, 10syl 17 . . . . . 6 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐵𝐴) ≈ 𝑦 → (𝐵𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)))
12 disjdif 4184 . . . . . . . 8 (𝐴 ∩ (𝐵𝐴)) = ∅
13 disjdif 4184 . . . . . . . 8 (𝑥 ∩ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) = ∅
14 unen 8207 . . . . . . . 8 (((𝐴𝑥 ∧ (𝐵𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) ∧ ((𝐴 ∩ (𝐵𝐴)) = ∅ ∧ (𝑥 ∩ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) = ∅)) → (𝐴 ∪ (𝐵𝐴)) ≈ (𝑥 ∪ ((𝑥 +𝑜 𝑦) ∖ 𝑥)))
1512, 13, 14mpanr12 723 . . . . . . 7 ((𝐴𝑥 ∧ (𝐵𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) → (𝐴 ∪ (𝐵𝐴)) ≈ (𝑥 ∪ ((𝑥 +𝑜 𝑦) ∖ 𝑥)))
16 undif2 4188 . . . . . . . . 9 (𝐴 ∪ (𝐵𝐴)) = (𝐴𝐵)
1716a1i 11 . . . . . . . 8 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ∪ (𝐵𝐴)) = (𝐴𝐵))
18 nnaword1 7880 . . . . . . . . 9 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑥 ⊆ (𝑥 +𝑜 𝑦))
19 undif 4193 . . . . . . . . 9 (𝑥 ⊆ (𝑥 +𝑜 𝑦) ↔ (𝑥 ∪ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) = (𝑥 +𝑜 𝑦))
2018, 19sylib 208 . . . . . . . 8 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ∪ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) = (𝑥 +𝑜 𝑦))
2117, 20breq12d 4817 . . . . . . 7 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ∪ (𝐵𝐴)) ≈ (𝑥 ∪ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) ↔ (𝐴𝐵) ≈ (𝑥 +𝑜 𝑦)))
2215, 21syl5ib 234 . . . . . 6 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴𝑥 ∧ (𝐵𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) → (𝐴𝐵) ≈ (𝑥 +𝑜 𝑦)))
2311, 22sylan2d 500 . . . . 5 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴𝑥 ∧ (𝐵𝐴) ≈ 𝑦) → (𝐴𝐵) ≈ (𝑥 +𝑜 𝑦)))
24 breq2 4808 . . . . . . 7 (𝑧 = (𝑥 +𝑜 𝑦) → ((𝐴𝐵) ≈ 𝑧 ↔ (𝐴𝐵) ≈ (𝑥 +𝑜 𝑦)))
2524rspcev 3449 . . . . . 6 (((𝑥 +𝑜 𝑦) ∈ ω ∧ (𝐴𝐵) ≈ (𝑥 +𝑜 𝑦)) → ∃𝑧 ∈ ω (𝐴𝐵) ≈ 𝑧)
26 isfi 8147 . . . . . 6 ((𝐴𝐵) ∈ Fin ↔ ∃𝑧 ∈ ω (𝐴𝐵) ≈ 𝑧)
2725, 26sylibr 224 . . . . 5 (((𝑥 +𝑜 𝑦) ∈ ω ∧ (𝐴𝐵) ≈ (𝑥 +𝑜 𝑦)) → (𝐴𝐵) ∈ Fin)
287, 23, 27syl6an 569 . . . 4 ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴𝑥 ∧ (𝐵𝐴) ≈ 𝑦) → (𝐴𝐵) ∈ Fin))
2928rexlimivv 3174 . . 3 (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴𝑥 ∧ (𝐵𝐴) ≈ 𝑦) → (𝐴𝐵) ∈ Fin)
306, 29sylbir 225 . 2 ((𝐴 ∈ Fin ∧ (𝐵𝐴) ∈ Fin) → (𝐴𝐵) ∈ Fin)
311, 30sylan2 492 1 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴𝐵) ∈ Fin)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632   ∈ wcel 2139  ∃wrex 3051   ∖ cdif 3712   ∪ cun 3713   ∩ cin 3714   ⊆ wss 3715  ∅c0 4058   class class class wbr 4804  (class class class)co 6814  ωcom 7231   +𝑜 coa 7727   ≈ cen 8120  Fincfn 8123 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-oadd 7734  df-er 7913  df-en 8124  df-fin 8127 This theorem is referenced by:  unfi2  8396  difinf  8397  xpfi  8398  prfi  8402  tpfi  8403  fnfi  8405  iunfi  8421  pwfilem  8427  fsuppun  8461  fsuppunfi  8462  ressuppfi  8468  fiin  8495  cantnfp1lem1  8750  ficardun2  9237  ackbij1lem6  9259  ackbij1lem16  9269  fin23lem28  9374  fin23lem30  9376  isfin1-3  9420  axcclem  9491  hashun  13383  hashunlei  13424  hashmap  13434  hashbclem  13448  hashf1lem1  13451  hashf1lem2  13452  hashf1  13453  fsumsplitsn  14693  fsummsnunz  14702  fsumsplitsnun  14703  fsummsnunzOLD  14704  fsumsplitsnunOLD  14705  incexclem  14787  isumltss  14799  fprodsplitsn  14939  lcmfunsnlem2lem1  15573  lcmfunsnlem2lem2  15574  lcmfunsnlem2  15575  lcmfun  15580  ramub1lem1  15952  fpwipodrs  17385  acsfiindd  17398  symgfisg  18108  gsumzunsnd  18575  gsumunsnfd  18576  psrbagaddcl  19592  mplsubg  19659  mpllss  19660  dsmmacl  20307  fctop  21030  uncmp  21428  bwth  21435  lfinun  21550  locfincmp  21551  comppfsc  21557  1stckgenlem  21578  ptbasin  21602  cfinfil  21918  fin1aufil  21957  alexsubALTlem3  22074  tmdgsum  22120  tsmsfbas  22152  tsmsgsum  22163  tsmsres  22168  tsmsxplem1  22177  prdsmet  22396  prdsbl  22517  icccmplem2  22847  rrxmval  23408  rrxmet  23411  rrxdstprj1  23412  ovolfiniun  23489  volfiniun  23535  fta1glem2  24145  fta1lem  24281  aannenlem2  24303  aalioulem2  24307  dchrfi  25200  usgrfilem  26439  ffsrn  29834  eulerpartlemt  30763  ballotlemgun  30916  hgt750lemb  31064  hgt750leme  31066  lindsenlbs  33735  poimirlem31  33771  poimirlem32  33772  itg2addnclem2  33793  ftc1anclem7  33822  ftc1anc  33824  prdsbnd  33923  pclfinN  35707  elrfi  37777  mzpcompact2lem  37834  eldioph2  37845  lsmfgcl  38164  fiuneneq  38295  unfid  39862  dvmptfprodlem  40680  dvnprodlem2  40683  fourierdlem50  40894  fourierdlem51  40895  fourierdlem54  40898  fourierdlem76  40920  fourierdlem80  40924  fourierdlem102  40946  fourierdlem103  40947  fourierdlem104  40948  fourierdlem114  40958  sge0resplit  41144  sge0iunmptlemfi  41151  sge0xaddlem1  41171  hoiprodp1  41326  sge0hsphoire  41327  hoidmvlelem1  41333  hoidmvlelem2  41334  hoidmvlelem5  41337  hspmbllem2  41365  fsummmodsnunz  41873  mndpsuppfi  42684
 Copyright terms: Public domain W3C validator