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

Theorem disjor 5125
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 5111 . 2 (Disj 𝑖𝐴 𝐵 ↔ ∀𝑥∃*𝑖𝐴 𝑥𝐵)
2 ralcom4 3286 . . 3 (∀𝑖𝐴𝑥𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗) ↔ ∀𝑥𝑖𝐴𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
3 orcom 871 . . . . . . 7 ((𝑖 = 𝑗 ∨ (𝐵𝐶) = ∅) ↔ ((𝐵𝐶) = ∅ ∨ 𝑖 = 𝑗))
4 df-or 849 . . . . . . 7 (((𝐵𝐶) = ∅ ∨ 𝑖 = 𝑗) ↔ (¬ (𝐵𝐶) = ∅ → 𝑖 = 𝑗))
5 neq0 4352 . . . . . . . . . 10 (¬ (𝐵𝐶) = ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵𝐶))
6 elin 3967 . . . . . . . . . . 11 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
76exbii 1848 . . . . . . . . . 10 (∃𝑥 𝑥 ∈ (𝐵𝐶) ↔ ∃𝑥(𝑥𝐵𝑥𝐶))
85, 7bitri 275 . . . . . . . . 9 (¬ (𝐵𝐶) = ∅ ↔ ∃𝑥(𝑥𝐵𝑥𝐶))
98imbi1i 349 . . . . . . . 8 ((¬ (𝐵𝐶) = ∅ → 𝑖 = 𝑗) ↔ (∃𝑥(𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
10 19.23v 1942 . . . . . . . 8 (∀𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗) ↔ (∃𝑥(𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
119, 10bitr4i 278 . . . . . . 7 ((¬ (𝐵𝐶) = ∅ → 𝑖 = 𝑗) ↔ ∀𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
123, 4, 113bitri 297 . . . . . 6 ((𝑖 = 𝑗 ∨ (𝐵𝐶) = ∅) ↔ ∀𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
1312ralbii 3093 . . . . 5 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝐵𝐶) = ∅) ↔ ∀𝑗𝐴𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
14 ralcom4 3286 . . . . 5 (∀𝑗𝐴𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗) ↔ ∀𝑥𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
1513, 14bitri 275 . . . 4 (∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝐵𝐶) = ∅) ↔ ∀𝑥𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
1615ralbii 3093 . . 3 (∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝐵𝐶) = ∅) ↔ ∀𝑖𝐴𝑥𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
17 disjor.1 . . . . . 6 (𝑖 = 𝑗𝐵 = 𝐶)
1817eleq2d 2827 . . . . 5 (𝑖 = 𝑗 → (𝑥𝐵𝑥𝐶))
1918rmo4 3736 . . . 4 (∃*𝑖𝐴 𝑥𝐵 ↔ ∀𝑖𝐴𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
2019albii 1819 . . 3 (∀𝑥∃*𝑖𝐴 𝑥𝐵 ↔ ∀𝑥𝑖𝐴𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
212, 16, 203bitr4i 303 . 2 (∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝐵𝐶) = ∅) ↔ ∀𝑥∃*𝑖𝐴 𝑥𝐵)
221, 21bitr4i 278 1 (Disj 𝑖𝐴 𝐵 ↔ ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝐵𝐶) = ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  wal 1538   = wceq 1540  wex 1779  wcel 2108  wral 3061  ∃*wrmo 3379  cin 3950  c0 4333  Disj wdisj 5110
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-11 2157  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-mo 2540  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rmo 3380  df-v 3482  df-dif 3954  df-in 3958  df-nul 4334  df-disj 5111
This theorem is referenced by:  disjors  5126  disjord  5132  disjiunb  5133  disjxiun  5140  disjxun  5141  otsndisj  5524  qsdisj2  8835  s3sndisj  15006  cshwsdisj  17136  dyadmbl  25635  numedglnl  29161  clwwlknondisj  30130  2wspmdisj  30356  disjnf  32583  disjorsf  32593  poimirlem26  37653  mblfinlem2  37665  grpods  42195  ndisj2  45056  nnfoctbdjlem  46470  iundjiun  46475  otiunsndisjX  47291
  Copyright terms: Public domain W3C validator