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

Theorem unen 9064
Description: Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes] p. 92. (Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
unen (((𝐴𝐵𝐶𝐷) ∧ ((𝐴𝐶) = ∅ ∧ (𝐵𝐷) = ∅)) → (𝐴𝐶) ≈ (𝐵𝐷))

Proof of Theorem unen
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bren 8967 . . 3 (𝐴𝐵 ↔ ∃𝑥 𝑥:𝐴1-1-onto𝐵)
2 bren 8967 . . 3 (𝐶𝐷 ↔ ∃𝑦 𝑦:𝐶1-1-onto𝐷)
3 exdistrv 1952 . . . 4 (∃𝑥𝑦(𝑥:𝐴1-1-onto𝐵𝑦:𝐶1-1-onto𝐷) ↔ (∃𝑥 𝑥:𝐴1-1-onto𝐵 ∧ ∃𝑦 𝑦:𝐶1-1-onto𝐷))
4 vex 3474 . . . . . . . 8 𝑥 ∈ V
5 vex 3474 . . . . . . . 8 𝑦 ∈ V
64, 5unex 7742 . . . . . . 7 (𝑥𝑦) ∈ V
7 f1oun 6852 . . . . . . 7 (((𝑥:𝐴1-1-onto𝐵𝑦:𝐶1-1-onto𝐷) ∧ ((𝐴𝐶) = ∅ ∧ (𝐵𝐷) = ∅)) → (𝑥𝑦):(𝐴𝐶)–1-1-onto→(𝐵𝐷))
8 f1oen3g 8980 . . . . . . 7 (((𝑥𝑦) ∈ V ∧ (𝑥𝑦):(𝐴𝐶)–1-1-onto→(𝐵𝐷)) → (𝐴𝐶) ≈ (𝐵𝐷))
96, 7, 8sylancr 586 . . . . . 6 (((𝑥:𝐴1-1-onto𝐵𝑦:𝐶1-1-onto𝐷) ∧ ((𝐴𝐶) = ∅ ∧ (𝐵𝐷) = ∅)) → (𝐴𝐶) ≈ (𝐵𝐷))
109ex 412 . . . . 5 ((𝑥:𝐴1-1-onto𝐵𝑦:𝐶1-1-onto𝐷) → (((𝐴𝐶) = ∅ ∧ (𝐵𝐷) = ∅) → (𝐴𝐶) ≈ (𝐵𝐷)))
1110exlimivv 1928 . . . 4 (∃𝑥𝑦(𝑥:𝐴1-1-onto𝐵𝑦:𝐶1-1-onto𝐷) → (((𝐴𝐶) = ∅ ∧ (𝐵𝐷) = ∅) → (𝐴𝐶) ≈ (𝐵𝐷)))
123, 11sylbir 234 . . 3 ((∃𝑥 𝑥:𝐴1-1-onto𝐵 ∧ ∃𝑦 𝑦:𝐶1-1-onto𝐷) → (((𝐴𝐶) = ∅ ∧ (𝐵𝐷) = ∅) → (𝐴𝐶) ≈ (𝐵𝐷)))
131, 2, 12syl2anb 597 . 2 ((𝐴𝐵𝐶𝐷) → (((𝐴𝐶) = ∅ ∧ (𝐵𝐷) = ∅) → (𝐴𝐶) ≈ (𝐵𝐷)))
1413imp 406 1 (((𝐴𝐵𝐶𝐷) ∧ ((𝐴𝐶) = ∅ ∧ (𝐵𝐷) = ∅)) → (𝐴𝐶) ≈ (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1534  wex 1774  wcel 2099  Vcvv 3470  cun 3943  cin 3944  c0 4318   class class class wbr 5142  1-1-ontowf1o 6541  cen 8954
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-12 2167  ax-ext 2699  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-en 8958
This theorem is referenced by:  enrefnn  9065  enpr2dOLD  9068  difsnen  9071  undomOLD  9078  limensuci  9171  infensuc  9173  pssnn  9186  unfi  9190  phplem2OLD  9236  pssnnOLD  9283  dif1ennnALT  9295  unfiOLD  9331  infdifsn  9674  pm54.43  10018  dif1card  10027  endjudisj  10185  djuen  10186  ssfin4  10327  fin23lem26  10342  unsnen  10570  fzennn  13959  mreexexlem4d  17620
  Copyright terms: Public domain W3C validator