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

Theorem unfi 9116
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 5320. (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 4117 . . . . 5 (𝑥 = ∅ → (𝐴𝑥) = (𝐴 ∪ ∅))
21eleq1d 2822 . . . 4 (𝑥 = ∅ → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∪ ∅) ∈ Fin))
32imbi2d 340 . . 3 (𝑥 = ∅ → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈ Fin)))
4 uneq2 4117 . . . . 5 (𝑥 = 𝑦 → (𝐴𝑥) = (𝐴𝑦))
54eleq1d 2822 . . . 4 (𝑥 = 𝑦 → ((𝐴𝑥) ∈ Fin ↔ (𝐴𝑦) ∈ Fin))
65imbi2d 340 . . 3 (𝑥 = 𝑦 → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴𝑦) ∈ Fin)))
7 uneq2 4117 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴𝑥) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
87eleq1d 2822 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
98imbi2d 340 . . 3 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
10 uneq2 4117 . . . . 5 (𝑥 = 𝐵 → (𝐴𝑥) = (𝐴𝐵))
1110eleq1d 2822 . . . 4 (𝑥 = 𝐵 → ((𝐴𝑥) ∈ Fin ↔ (𝐴𝐵) ∈ Fin))
1211imbi2d 340 . . 3 (𝑥 = 𝐵 → ((𝐴 ∈ Fin → (𝐴𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴𝐵) ∈ Fin)))
13 un0 4350 . . . . 5 (𝐴 ∪ ∅) = 𝐴
1413eleq1i 2828 . . . 4 ((𝐴 ∪ ∅) ∈ Fin ↔ 𝐴 ∈ Fin)
1514biimpri 227 . . 3 (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈ Fin)
16 snssi 4768 . . . . . . . . . . 11 (𝑧𝐴 → {𝑧} ⊆ 𝐴)
17 ssequn2 4143 . . . . . . . . . . . . . 14 ({𝑧} ⊆ 𝐴 ↔ (𝐴 ∪ {𝑧}) = 𝐴)
1817biimpi 215 . . . . . . . . . . . . 13 ({𝑧} ⊆ 𝐴 → (𝐴 ∪ {𝑧}) = 𝐴)
1918uneq2d 4123 . . . . . . . . . . . 12 ({𝑧} ⊆ 𝐴 → (𝑦 ∪ (𝐴 ∪ {𝑧})) = (𝑦𝐴))
20 un12 4127 . . . . . . . . . . . 12 (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝑦 ∪ (𝐴 ∪ {𝑧}))
21 uncom 4113 . . . . . . . . . . . 12 (𝐴𝑦) = (𝑦𝐴)
2219, 20, 213eqtr4g 2801 . . . . . . . . . . 11 ({𝑧} ⊆ 𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴𝑦))
2316, 22syl 17 . . . . . . . . . 10 (𝑧𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴𝑦))
2423eleq1d 2822 . . . . . . . . 9 (𝑧𝐴 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin ↔ (𝐴𝑦) ∈ Fin))
2524biimprd 247 . . . . . . . 8 (𝑧𝐴 → ((𝐴𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
2625adantld 491 . . . . . . 7 (𝑧𝐴 → ((¬ 𝑧𝑦 ∧ (𝐴𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
27 isfi 8916 . . . . . . . . . . 11 ((𝐴𝑦) ∈ Fin ↔ ∃𝑤 ∈ ω (𝐴𝑦) ≈ 𝑤)
2827biimpi 215 . . . . . . . . . 10 ((𝐴𝑦) ∈ Fin → ∃𝑤 ∈ ω (𝐴𝑦) ≈ 𝑤)
29 r19.41v 3185 . . . . . . . . . . 11 (∃𝑤 ∈ ω ((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) ↔ (∃𝑤 ∈ ω (𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)))
30 disjsn 4672 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑦) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝐴𝑦))
31 elun 4108 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ (𝐴𝑦) ↔ (𝑧𝐴𝑧𝑦))
3231notbii 319 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ (𝐴𝑦) ↔ ¬ (𝑧𝐴𝑧𝑦))
33 pm4.56 987 . . . . . . . . . . . . . . . . . . 19 ((¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) ↔ ¬ (𝑧𝐴𝑧𝑦))
3432, 33bitr4i 277 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ (𝐴𝑦) ↔ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))
3530, 34sylbbr 235 . . . . . . . . . . . . . . . . 17 ((¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) → ((𝐴𝑦) ∩ {𝑧}) = ∅)
36 nnord 7810 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ ω → Ord 𝑤)
37 orddisj 6355 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑤 → (𝑤 ∩ {𝑤}) = ∅)
3836, 37syl 17 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ ω → (𝑤 ∩ {𝑤}) = ∅)
39 en2sn 8985 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ V ∧ 𝑤 ∈ V) → {𝑧} ≈ {𝑤})
4039el2v 3453 . . . . . . . . . . . . . . . . . . 19 {𝑧} ≈ {𝑤}
41 unen 8990 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑦) ≈ 𝑤 ∧ {𝑧} ≈ {𝑤}) ∧ (((𝐴𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
4240, 41mpanl2 699 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑦) ≈ 𝑤 ∧ (((𝐴𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
4338, 42sylanr2 681 . . . . . . . . . . . . . . . . 17 (((𝐴𝑦) ≈ 𝑤 ∧ (((𝐴𝑦) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ ω)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
4435, 43sylanr1 680 . . . . . . . . . . . . . . . 16 (((𝐴𝑦) ≈ 𝑤 ∧ ((¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) ∧ 𝑤 ∈ ω)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
45443impb 1115 . . . . . . . . . . . . . . 15 (((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) ∧ 𝑤 ∈ ω) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
46453comr 1125 . . . . . . . . . . . . . 14 ((𝑤 ∈ ω ∧ (𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
47463expb 1120 . . . . . . . . . . . . 13 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))) → ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
48 unass 4126 . . . . . . . . . . . . . 14 ((𝐴𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧}))
49 df-suc 6323 . . . . . . . . . . . . . . . . 17 suc 𝑤 = (𝑤 ∪ {𝑤})
50 peano2 7827 . . . . . . . . . . . . . . . . 17 (𝑤 ∈ ω → suc 𝑤 ∈ ω)
5149, 50eqeltrrid 2843 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ω → (𝑤 ∪ {𝑤}) ∈ ω)
52 breq2 5109 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑤 ∪ {𝑤}) → (((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣 ↔ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})))
5352rspcev 3581 . . . . . . . . . . . . . . . 16 (((𝑤 ∪ {𝑤}) ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣)
5451, 53sylan 580 . . . . . . . . . . . . . . 15 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣)
55 isfi 8916 . . . . . . . . . . . . . . 15 (((𝐴𝑦) ∪ {𝑧}) ∈ Fin ↔ ∃𝑣 ∈ ω ((𝐴𝑦) ∪ {𝑧}) ≈ 𝑣)
5654, 55sylibr 233 . . . . . . . . . . . . . 14 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ((𝐴𝑦) ∪ {𝑧}) ∈ Fin)
5748, 56eqeltrrid 2843 . . . . . . . . . . . . 13 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
5847, 57syldan 591 . . . . . . . . . . . 12 ((𝑤 ∈ ω ∧ ((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
5958rexlimiva 3144 . . . . . . . . . . 11 (∃𝑤 ∈ ω ((𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
6029, 59sylbir 234 . . . . . . . . . 10 ((∃𝑤 ∈ ω (𝐴𝑦) ≈ 𝑤 ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
6128, 60sylan 580 . . . . . . . . 9 (((𝐴𝑦) ∈ Fin ∧ (¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
6261ancoms 459 . . . . . . . 8 (((¬ 𝑧𝐴 ∧ ¬ 𝑧𝑦) ∧ (𝐴𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
6362expl 458 . . . . . . 7 𝑧𝐴 → ((¬ 𝑧𝑦 ∧ (𝐴𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
6426, 63pm2.61i 182 . . . . . 6 ((¬ 𝑧𝑦 ∧ (𝐴𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
6564ex 413 . . . . 5 𝑧𝑦 → ((𝐴𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
6665imim2d 57 . . . 4 𝑧𝑦 → ((𝐴 ∈ Fin → (𝐴𝑦) ∈ Fin) → (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
6766adantl 482 . . 3 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((𝐴 ∈ Fin → (𝐴𝑦) ∈ Fin) → (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
683, 6, 9, 12, 15, 67findcard2s 9109 . 2 (𝐵 ∈ Fin → (𝐴 ∈ Fin → (𝐴𝐵) ∈ Fin))
6968impcom 408 1 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴𝐵) ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 845   = wceq 1541  wcel 2106  wrex 3073  Vcvv 3445  cun 3908  cin 3909  wss 3910  c0 4282  {csn 4586   class class class wbr 5105  Ord word 6316  suc csuc 6319  ωcom 7802  cen 8880  Fincfn 8883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-om 7803  df-en 8884  df-fin 8887
This theorem is referenced by:  ssfi  9117  imafi  9119  pwfilem  9121  cnvfi  9124  fnfi  9125  unfi2  9259  difinf  9260  xpfi  9261  xpfiOLD  9262  prfi  9266  tpfi  9267  iunfi  9284  pwfilemOLD  9290  fsuppun  9324  fsuppunfi  9325  ressuppfi  9331  fiin  9358  cantnfp1lem1  9614  ficardadju  10135  ficardun2  10138  ficardun2OLD  10139  ackbij1lem6  10161  ackbij1lem16  10171  fin23lem28  10276  fin23lem30  10278  isfin1-3  10322  axcclem  10393  hashun  14282  hashunlei  14325  hashmap  14335  hashbclem  14349  hashf1lem1OLD  14354  hashf1lem2  14355  hashf1  14356  fsumsplitsn  15629  fsummsnunz  15639  fsumsplitsnun  15640  incexclem  15721  isumltss  15733  fprodsplitsn  15872  lcmfunsnlem2lem1  16514  lcmfunsnlem2lem2  16515  lcmfunsnlem2  16516  lcmfun  16521  ramub1lem1  16898  fpwipodrs  18429  acsfiindd  18442  symgfisg  19250  gsumzunsnd  19733  gsumunsnfd  19734  dsmmacl  21147  psrbagaddclOLD  21331  mplsubg  21408  mpllss  21409  fctop  22354  uncmp  22754  bwth  22761  lfinun  22876  locfincmp  22877  comppfsc  22883  1stckgenlem  22904  ptbasin  22928  cfinfil  23244  fin1aufil  23283  alexsubALTlem3  23400  tmdgsum  23446  tsmsfbas  23479  tsmsgsum  23490  tsmsres  23495  tsmsxplem1  23504  prdsmet  23723  prdsbl  23847  icccmplem2  24186  rrxmval  24769  rrxmet  24772  rrxdstprj1  24773  ovolfiniun  24865  volfiniun  24911  fta1glem2  25531  fta1lem  25667  aannenlem2  25689  aalioulem2  25693  dchrfi  26603  usgrfilem  28275  ffsrn  31646  eulerpartlemt  32971  ballotlemgun  33124  hgt750lemb  33269  hgt750leme  33271  lindsenlbs  36073  poimirlem31  36109  poimirlem32  36110  itg2addnclem2  36130  ftc1anclem7  36157  ftc1anc  36159  prdsbnd  36252  pclfinN  38363  elrfi  41003  mzpcompact2lem  41060  eldioph2  41071  lsmfgcl  41387  fiuneneq  41510  unfid  43353  dvmptfprodlem  44175  dvnprodlem2  44178  fourierdlem50  44387  fourierdlem51  44388  fourierdlem54  44391  fourierdlem76  44413  fourierdlem80  44417  fourierdlem102  44439  fourierdlem103  44440  fourierdlem104  44441  fourierdlem114  44451  sge0resplit  44637  sge0iunmptlemfi  44644  sge0xaddlem1  44664  hoiprodp1  44819  sge0hsphoire  44820  hoidmvlelem1  44826  hoidmvlelem2  44827  hoidmvlelem5  44830  hspmbllem2  44858  fsummmodsnunz  45557  mndpsuppfi  46441
  Copyright terms: Public domain W3C validator