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

Theorem disjor 4198
Description: Two ways to say that a collection  B ( i ) for  i  e.  A is disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 14-Nov-2016.)
Hypothesis
Ref Expression
disjmo.1  |-  ( i  =  j  ->  B  =  C )
Assertion
Ref Expression
disjor  |-  (Disj  i  e.  A B  <->  A. i  e.  A  A. j  e.  A  ( i  =  j  \/  ( B  i^i  C )  =  (/) ) )
Distinct variable groups:    i, j, A    B, j    C, i
Allowed substitution hints:    B( i)    C( j)

Proof of Theorem disjor
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 df-disj 4185 . 2  |-  (Disj  i  e.  A B  <->  A. x E* i  e.  A x  e.  B )
2 ralcom4 2976 . . 3  |-  ( A. i  e.  A  A. x A. j  e.  A  ( ( x  e.  B  /\  x  e.  C )  ->  i  =  j )  <->  A. x A. i  e.  A  A. j  e.  A  ( ( x  e.  B  /\  x  e.  C )  ->  i  =  j ) )
3 orcom 378 . . . . . . 7  |-  ( ( i  =  j  \/  ( B  i^i  C
)  =  (/) )  <->  ( ( B  i^i  C )  =  (/)  \/  i  =  j ) )
4 df-or 361 . . . . . . 7  |-  ( ( ( B  i^i  C
)  =  (/)  \/  i  =  j )  <->  ( -.  ( B  i^i  C )  =  (/)  ->  i  =  j ) )
5 neq0 3640 . . . . . . . . . 10  |-  ( -.  ( B  i^i  C
)  =  (/)  <->  E. x  x  e.  ( B  i^i  C ) )
6 elin 3532 . . . . . . . . . . 11  |-  ( x  e.  ( B  i^i  C )  <->  ( x  e.  B  /\  x  e.  C ) )
76exbii 1593 . . . . . . . . . 10  |-  ( E. x  x  e.  ( B  i^i  C )  <->  E. x ( x  e.  B  /\  x  e.  C ) )
85, 7bitri 242 . . . . . . . . 9  |-  ( -.  ( B  i^i  C
)  =  (/)  <->  E. x
( x  e.  B  /\  x  e.  C
) )
98imbi1i 317 . . . . . . . 8  |-  ( ( -.  ( B  i^i  C )  =  (/)  ->  i  =  j )  <->  ( E. x ( x  e.  B  /\  x  e.  C )  ->  i  =  j ) )
10 19.23v 1915 . . . . . . . 8  |-  ( A. x ( ( x  e.  B  /\  x  e.  C )  ->  i  =  j )  <->  ( E. x ( x  e.  B  /\  x  e.  C )  ->  i  =  j ) )
119, 10bitr4i 245 . . . . . . 7  |-  ( ( -.  ( B  i^i  C )  =  (/)  ->  i  =  j )  <->  A. x
( ( x  e.  B  /\  x  e.  C )  ->  i  =  j ) )
123, 4, 113bitri 264 . . . . . 6  |-  ( ( i  =  j  \/  ( B  i^i  C
)  =  (/) )  <->  A. x
( ( x  e.  B  /\  x  e.  C )  ->  i  =  j ) )
1312ralbii 2731 . . . . 5  |-  ( A. j  e.  A  (
i  =  j  \/  ( B  i^i  C
)  =  (/) )  <->  A. j  e.  A  A. x
( ( x  e.  B  /\  x  e.  C )  ->  i  =  j ) )
14 ralcom4 2976 . . . . 5  |-  ( A. j  e.  A  A. x ( ( x  e.  B  /\  x  e.  C )  ->  i  =  j )  <->  A. x A. j  e.  A  ( ( x  e.  B  /\  x  e.  C )  ->  i  =  j ) )
1513, 14bitri 242 . . . 4  |-  ( A. j  e.  A  (
i  =  j  \/  ( B  i^i  C
)  =  (/) )  <->  A. x A. j  e.  A  ( ( x  e.  B  /\  x  e.  C )  ->  i  =  j ) )
1615ralbii 2731 . . 3  |-  ( A. i  e.  A  A. j  e.  A  (
i  =  j  \/  ( B  i^i  C
)  =  (/) )  <->  A. i  e.  A  A. x A. j  e.  A  ( ( x  e.  B  /\  x  e.  C )  ->  i  =  j ) )
17 disjmo.1 . . . . . 6  |-  ( i  =  j  ->  B  =  C )
1817eleq2d 2505 . . . . 5  |-  ( i  =  j  ->  (
x  e.  B  <->  x  e.  C ) )
1918rmo4 3129 . . . 4  |-  ( E* i  e.  A x  e.  B  <->  A. i  e.  A  A. j  e.  A  ( (
x  e.  B  /\  x  e.  C )  ->  i  =  j ) )
2019albii 1576 . . 3  |-  ( A. x E* i  e.  A x  e.  B  <->  A. x A. i  e.  A  A. j  e.  A  ( ( x  e.  B  /\  x  e.  C )  ->  i  =  j ) )
212, 16, 203bitr4i 270 . 2  |-  ( A. i  e.  A  A. j  e.  A  (
i  =  j  \/  ( B  i^i  C
)  =  (/) )  <->  A. x E* i  e.  A x  e.  B )
221, 21bitr4i 245 1  |-  (Disj  i  e.  A B  <->  A. i  e.  A  A. j  e.  A  ( i  =  j  \/  ( B  i^i  C )  =  (/) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    \/ wo 359    /\ wa 360   A.wal 1550   E.wex 1551    = wceq 1653    e. wcel 1726   A.wral 2707   E*wrmo 2710    i^i cin 3321   (/)c0 3630  Disj wdisj 4184
This theorem is referenced by:  disjmoOLD  4199  disjors  4200  disjxiun  4211  disjxun  4212  qsdisj2  6984  dyadmbl  19494  disjorsf  24024  mblfinlem2  26246  otsndisj  28068  otiunsndisj  28069  otiunsndisjX  28070  cshwsdisj  28307  2spotdisj  28512  2spotiundisj  28513  2spotmdisj  28519
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rmo 2715  df-v 2960  df-dif 3325  df-in 3329  df-nul 3631  df-disj 4185
  Copyright terms: Public domain W3C validator