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

Theorem unfi 9211
Description: The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 16-Nov-2002.) Avoid ax-pow 5365. (Revised by BTernaryTau, 7-Aug-2024.)
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 uneq2 4162 . . . . 5 (𝑥 = ∅ → (𝐴𝑥) = (𝐴 ∪ ∅))
21eleq1d 2826 . . . 4 (𝑥 = ∅ → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∪ ∅) ∈ Fin))
32imbi2d 340 . . 3 (𝑥 = ∅ → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈ Fin)))
4 uneq2 4162 . . . . 5 (𝑥 = 𝑦 → (𝐴𝑥) = (𝐴𝑦))
54eleq1d 2826 . . . 4 (𝑥 = 𝑦 → ((𝐴𝑥) ∈ Fin ↔ (𝐴𝑦) ∈ Fin))
65imbi2d 340 . . 3 (𝑥 = 𝑦 → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴𝑦) ∈ Fin)))
7 uneq2 4162 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴𝑥) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
87eleq1d 2826 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
98imbi2d 340 . . 3 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
10 uneq2 4162 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑥) = (𝐴𝐵))
1110eleq1d 2826 . . . 4 (𝑥 = 𝐵 → ((𝐴𝑥) ∈ Fin ↔ (𝐴𝐵) ∈ Fin))
1211imbi2d 340 . . 3 (𝑥 = 𝐵 → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴𝐵) ∈ Fin)))
13 un0 4394 . . . . 5 (𝐴 ∪ ∅) = 𝐴
1413eleq1i 2832 . . . 4 ((𝐴 ∪ ∅) ∈ Fin ↔ 𝐴 ∈ Fin)
1514biimpri 228 . . 3 (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈ Fin)
16 snssi 4808 . . . . . . . . . . 11 (𝑧𝐴 → {𝑧} ⊆ 𝐴)
17 ssequn2 4189 . . . . . . . . . . . . . 14 ({𝑧} ⊆ 𝐴 ↔ (𝐴 ∪ {𝑧}) = 𝐴)
1817biimpi 216 . . . . . . . . . . . . 13 ({𝑧} ⊆ 𝐴 → (𝐴 ∪ {𝑧}) = 𝐴)
1918uneq2d 4168 . . . . . . . . . . . 12 ({𝑧} ⊆ 𝐴 → (𝑦 ∪ (𝐴 ∪ {𝑧})) = (𝑦𝐴))
20 un12 4173 . . . . . . . . . . . 12 (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝑦 ∪ (𝐴 ∪ {𝑧}))
21 uncom 4158 . . . . . . . . . . . 12 (𝐴𝑦) = (𝑦𝐴)
2219, 20, 213eqtr4g 2802 . . . . . . . . . . 11 ({𝑧} ⊆ 𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴𝑦))
2316, 22syl 17 . . . . . . . . . 10 (𝑧𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴𝑦))
2423eleq1d 2826 . . . . . . . . 9 (𝑧𝐴 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin ↔ (𝐴𝑦) ∈ Fin))
2524biimprd 248 . . . . . . . 8 (𝑧𝐴 → ((𝐴𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
2625adantld 490 . . . . . . 7 (𝑧𝐴 → ((¬ 𝑧𝑦 ∧ (𝐴𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
27 isfi 9016 . . . . . . . . . . 11 ((𝐴𝑦) ∈ Fin ↔ ∃𝑤 ∈ ω (𝐴𝑦) ≈ 𝑤)
2827biimpi 216 . . . . . . . . . 10 ((𝐴𝑦) ∈ Fin → ∃𝑤 ∈ ω (𝐴𝑦) ≈ 𝑤)
29 r19.41v 3189 . . . . . . . . . . 11 (∃𝑤 ∈ ω ((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) ↔ (∃𝑤 ∈ ω (𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)))
30 disjsn 4711 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑦) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝐴𝑦))
31 elun 4153 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (𝐴𝑦) ↔ (𝑧𝐴𝑧𝑦))
3231notbii 320 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ (𝐴𝑦) ↔ ¬ (𝑧𝐴𝑧𝑦))
33 pm4.56 991 . . . . . . . . . . . . . . . . . . 19 ((¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) ↔ ¬ (𝑧𝐴𝑧𝑦))
3432, 33bitr4i 278 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ (𝐴𝑦) ↔ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))
3530, 34sylbbr 236 . . . . . . . . . . . . . . . . 17 ((¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) → ((𝐴𝑦) ∩ {𝑧}) = ∅)
36 nnord 7895 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ω → Ord 𝑤)
37 orddisj 6422 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑤 → (𝑤 ∩ {𝑤}) = ∅)
3836, 37syl 17 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ω → (𝑤 ∩ {𝑤}) = ∅)
39 en2sn 9081 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ V ∧ 𝑤 ∈ V) → {𝑧} ≈ {𝑤})
4039el2v 3487 . . . . . . . . . . . . . . . . . . 19 {𝑧} ≈ {𝑤}
41 unen 9086 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑦) ≈ 𝑤 ∧ {𝑧} ≈ {𝑤}) ∧ (((𝐴𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
4240, 41mpanl2 701 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑦) ≈ 𝑤 ∧ (((𝐴𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
4338, 42sylanr2 683 . . . . . . . . . . . . . . . . 17 (((𝐴𝑦) ≈ 𝑤 ∧ (((𝐴𝑦) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ ω)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
4435, 43sylanr1 682 . . . . . . . . . . . . . . . 16 (((𝐴𝑦) ≈ 𝑤 ∧ ((¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) ∧ 𝑤 ∈ ω)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
45443impb 1115 . . . . . . . . . . . . . . 15 (((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) ∧ 𝑤 ∈ ω) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
46453comr 1126 . . . . . . . . . . . . . 14 ((𝑤 ∈ ω ∧ (𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
47463expb 1121 . . . . . . . . . . . . 13 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
48 unass 4172 . . . . . . . . . . . . . 14 ((𝐴𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧}))
49 df-suc 6390 . . . . . . . . . . . . . . . . 17 suc 𝑤 = (𝑤 ∪ {𝑤})
50 peano2 7912 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ω → suc 𝑤 ∈ ω)
5149, 50eqeltrrid 2846 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ω → (𝑤 ∪ {𝑤}) ∈ ω)
52 breq2 5147 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑤 ∪ {𝑤}) → (((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣 ↔ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})))
5352rspcev 3622 . . . . . . . . . . . . . . . 16 (((𝑤 ∪ {𝑤}) ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣)
5451, 53sylan 580 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣)
55 isfi 9016 . . . . . . . . . . . . . . 15 (((𝐴𝑦) ∪ {𝑧}) ∈ Fin ↔ ∃𝑣 ∈ ω ((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣)
5654, 55sylibr 234 . . . . . . . . . . . . . 14 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ((𝐴𝑦) ∪ {𝑧}) ∈ Fin)
5748, 56eqeltrrid 2846 . . . . . . . . . . . . 13 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
5847, 57syldan 591 . . . . . . . . . . . 12 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
5958rexlimiva 3147 . . . . . . . . . . 11 (∃𝑤 ∈ ω ((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
6029, 59sylbir 235 . . . . . . . . . 10 ((∃𝑤 ∈ ω (𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
6128, 60sylan 580 . . . . . . . . 9 (((𝐴𝑦) ∈ Fin ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
6261ancoms 458 . . . . . . . 8 (((¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) ∧ (𝐴𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
6362expl 457 . . . . . . 7 𝑧𝐴 → ((¬ 𝑧𝑦 ∧ (𝐴𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
6426, 63pm2.61i 182 . . . . . 6 ((¬ 𝑧𝑦 ∧ (𝐴𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
6564ex 412 . . . . 5 𝑧𝑦 → ((𝐴𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
6665imim2d 57 . . . 4 𝑧𝑦 → ((𝐴 ∈ Fin → (𝐴𝑦) ∈ Fin) → (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
6766adantl 481 . . 3 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((𝐴 ∈ Fin → (𝐴𝑦) ∈ Fin) → (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
683, 6, 9, 12, 15, 67findcard2s 9205 . 2 (𝐵 ∈ Fin → (𝐴 ∈ Fin → (𝐴𝐵) ∈ Fin))
6968impcom 407 1 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴𝐵) ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 848   = wceq 1540  wcel 2108  wrex 3070  Vcvv 3480  cun 3949  cin 3950  wss 3951  c0 4333  {csn 4626   class class class wbr 5143  Ord word 6383  suc csuc 6386  ωcom 7887  cen 8982  Fincfn 8985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-om 7888  df-en 8986  df-fin 8989
This theorem is referenced by:  unfid  9212  ssfi  9213  cnvfi  9216  fnfi  9218  unfib  9347  unfi2  9348  difinf  9349  imafiOLD  9354  pwfilem  9356  xpfi  9358  xpfiOLD  9359  prfiALT  9364  tpfi  9365  fodomfir  9368  iunfi  9383  fsuppun  9427  fsuppunfi  9428  ressuppfi  9435  fiin  9462  cantnfp1lem1  9718  ficardadju  10240  ficardun2  10242  ackbij1lem6  10264  ackbij1lem16  10274  fin23lem28  10380  fin23lem30  10382  isfin1-3  10426  axcclem  10497  hashun  14421  hashunlei  14464  hashmap  14474  hashbclem  14491  hashf1lem2  14495  hashf1  14496  hash7g  14525  s7f1o  15005  fsumsplitsn  15780  fsummsnunz  15790  fsumsplitsnun  15791  incexclem  15872  isumltss  15884  fprodsplitsn  16025  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  lcmfunsnlem2  16677  lcmfun  16682  ramub1lem1  17064  fpwipodrs  18585  acsfiindd  18598  mndpsuppfi  18779  symgfisg  19486  gsumzunsnd  19974  gsumunsnfd  19975  dsmmacl  21761  mplsubg  22022  mpllss  22023  fctop  23011  uncmp  23411  bwth  23418  lfinun  23533  locfincmp  23534  comppfsc  23540  1stckgenlem  23561  ptbasin  23585  cfinfil  23901  fin1aufil  23940  alexsubALTlem3  24057  tmdgsum  24103  tsmsfbas  24136  tsmsgsum  24147  tsmsres  24152  tsmsxplem1  24161  prdsmet  24380  prdsbl  24504  icccmplem2  24845  rrxmval  25439  rrxmet  25442  rrxdstprj1  25443  ovolfiniun  25536  volfiniun  25582  fta1glem2  26208  fta1lem  26349  aannenlem2  26371  aalioulem2  26375  dchrfi  27299  usgrfilem  29344  ffsrn  32740  eulerpartlemt  34373  ballotlemgun  34527  hgt750lemb  34671  hgt750leme  34673  lindsenlbs  37622  poimirlem31  37658  poimirlem32  37659  itg2addnclem2  37679  ftc1anclem7  37706  ftc1anc  37708  prdsbnd  37800  pclfinN  39902  elrfi  42705  mzpcompact2lem  42762  eldioph2  42773  lsmfgcl  43086  fiuneneq  43204  dvmptfprodlem  45959  dvnprodlem2  45962  fourierdlem50  46171  fourierdlem51  46172  fourierdlem54  46175  fourierdlem76  46197  fourierdlem80  46201  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem114  46235  sge0resplit  46421  sge0iunmptlemfi  46428  sge0xaddlem1  46448  hoiprodp1  46603  sge0hsphoire  46604  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem5  46614  hspmbllem2  46642  fsummmodsnunz  47362
  Copyright terms: Public domain W3C validator