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

Theorem disjor 4666
Description: Two ways to say that a collection 𝐵(𝑖) for 𝑖𝐴 is disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 14-Nov-2016.)
Hypothesis
Ref Expression
disjor.1 (𝑖 = 𝑗𝐵 = 𝐶)
Assertion
Ref Expression
disjor (Disj 𝑖𝐴 𝐵 ↔ ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝐵𝐶) = ∅))
Distinct variable groups:   𝑖,𝑗,𝐴   𝐵,𝑗   𝐶,𝑖
Allowed substitution hints:   𝐵(𝑖)   𝐶(𝑗)

Proof of Theorem disjor
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 df-disj 4653 . 2 (Disj 𝑖𝐴 𝐵 ↔ ∀𝑥∃*𝑖𝐴 𝑥𝐵)
2 ralcom4 3255 . . 3 (∀𝑖𝐴𝑥𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗) ↔ ∀𝑥𝑖𝐴𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
3 orcom 401 . . . . . . 7 ((𝑖 = 𝑗 ∨ (𝐵𝐶) = ∅) ↔ ((𝐵𝐶) = ∅ ∨ 𝑖 = 𝑗))
4 df-or 384 . . . . . . 7 (((𝐵𝐶) = ∅ ∨ 𝑖 = 𝑗) ↔ (¬ (𝐵𝐶) = ∅ → 𝑖 = 𝑗))
5 neq0 3963 . . . . . . . . . 10 (¬ (𝐵𝐶) = ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵𝐶))
6 elin 3829 . . . . . . . . . . 11 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
76exbii 1814 . . . . . . . . . 10 (∃𝑥 𝑥 ∈ (𝐵𝐶) ↔ ∃𝑥(𝑥𝐵𝑥𝐶))
85, 7bitri 264 . . . . . . . . 9 (¬ (𝐵𝐶) = ∅ ↔ ∃𝑥(𝑥𝐵𝑥𝐶))
98imbi1i 338 . . . . . . . 8 ((¬ (𝐵𝐶) = ∅ → 𝑖 = 𝑗) ↔ (∃𝑥(𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
10 19.23v 1911 . . . . . . . 8 (∀𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗) ↔ (∃𝑥(𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
119, 10bitr4i 267 . . . . . . 7 ((¬ (𝐵𝐶) = ∅ → 𝑖 = 𝑗) ↔ ∀𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
123, 4, 113bitri 286 . . . . . 6 ((𝑖 = 𝑗 ∨ (𝐵𝐶) = ∅) ↔ ∀𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
1312ralbii 3009 . . . . 5 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝐵𝐶) = ∅) ↔ ∀𝑗𝐴𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
14 ralcom4 3255 . . . . 5 (∀𝑗𝐴𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗) ↔ ∀𝑥𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
1513, 14bitri 264 . . . 4 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝐵𝐶) = ∅) ↔ ∀𝑥𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
1615ralbii 3009 . . 3 (∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝐵𝐶) = ∅) ↔ ∀𝑖𝐴𝑥𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
17 disjor.1 . . . . . 6 (𝑖 = 𝑗𝐵 = 𝐶)
1817eleq2d 2716 . . . . 5 (𝑖 = 𝑗 → (𝑥𝐵𝑥𝐶))
1918rmo4 3432 . . . 4 (∃*𝑖𝐴 𝑥𝐵 ↔ ∀𝑖𝐴𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
2019albii 1787 . . 3 (∀𝑥∃*𝑖𝐴 𝑥𝐵 ↔ ∀𝑥𝑖𝐴𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
212, 16, 203bitr4i 292 . 2 (∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝐵𝐶) = ∅) ↔ ∀𝑥∃*𝑖𝐴 𝑥𝐵)
221, 21bitr4i 267 1 (Disj 𝑖𝐴 𝐵 ↔ ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝐵𝐶) = ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  wal 1521   = wceq 1523  wex 1744  wcel 2030  wral 2941  ∃*wrmo 2944  cin 3606  c0 3948  Disj wdisj 4652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rmo 2949  df-v 3233  df-dif 3610  df-in 3614  df-nul 3949  df-disj 4653
This theorem is referenced by:  disjors  4667  disjord  4673  disjiunb  4674  disjxiun  4681  disjxiunOLD  4682  disjxun  4683  otsndisj  5008  otiunsndisj  5009  qsdisj2  7868  s3sndisj  13752  s3iunsndisj  13753  cshwsdisj  15852  dyadmbl  23414  numedglnl  26084  clwwlknondisj  27086  clwwlknondisjOLD  27090  2wspmdisj  27317  disjnf  29510  disjorsf  29519  poimirlem26  33565  mblfinlem2  33577  ndisj2  39532  nnfoctbdjlem  40990  iundjiun  40995  otiunsndisjX  41621
  Copyright terms: Public domain W3C validator