Metamath Proof Explorer

Theorem disjor

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)

Ref Expression
Hypothesis disjor.1 ⊢ i = j → B = C
Assertion disjor ⊢ Disj i ∈ A B ↔ ∀ i ∈ A ∀ j ∈ A i = j ∨ B ∩ C = ∅

Proof

Step Hyp Ref Expression
1 disjor.1 ⊢ i = j → B = C
2 df-disj ⊢ Disj i ∈ A B ↔ ∀ x ∃* i ∈ A x ∈ B
3 ralcom4 ⊢ ∀ i ∈ A ∀ x ∀ j ∈ A x ∈ B ∧ x ∈ C → i = j ↔ ∀ x ∀ i ∈ A ∀ j ∈ A x ∈ B ∧ x ∈ C → i = j
4 orcom ⊢ i = j ∨ B ∩ C = ∅ ↔ B ∩ C = ∅ ∨ i = j
5 df-or ⊢ B ∩ C = ∅ ∨ i = j ↔ ¬ B ∩ C = ∅ → i = j
6 neq0 ⊢ ¬ B ∩ C = ∅ ↔ ∃ x x ∈ B ∩ C
7 elin ⊢ x ∈ B ∩ C ↔ x ∈ B ∧ x ∈ C
8 7 exbii ⊢ ∃ x x ∈ B ∩ C ↔ ∃ x x ∈ B ∧ x ∈ C
9 6 8 bitri ⊢ ¬ B ∩ C = ∅ ↔ ∃ x x ∈ B ∧ x ∈ C
10 9 imbi1i ⊢ ¬ B ∩ C = ∅ → i = j ↔ ∃ x x ∈ B ∧ x ∈ C → i = j
11 19.23v ⊢ ∀ x x ∈ B ∧ x ∈ C → i = j ↔ ∃ x x ∈ B ∧ x ∈ C → i = j
12 10 11 bitr4i ⊢ ¬ B ∩ C = ∅ → i = j ↔ ∀ x x ∈ B ∧ x ∈ C → i = j
13 4 5 12 3bitri ⊢ i = j ∨ B ∩ C = ∅ ↔ ∀ x x ∈ B ∧ x ∈ C → i = j
14 13 ralbii ⊢ ∀ j ∈ A i = j ∨ B ∩ C = ∅ ↔ ∀ j ∈ A ∀ x x ∈ B ∧ x ∈ C → i = j
15 ralcom4 ⊢ ∀ j ∈ A ∀ x x ∈ B ∧ x ∈ C → i = j ↔ ∀ x ∀ j ∈ A x ∈ B ∧ x ∈ C → i = j
16 14 15 bitri ⊢ ∀ j ∈ A i = j ∨ B ∩ C = ∅ ↔ ∀ x ∀ j ∈ A x ∈ B ∧ x ∈ C → i = j
17 16 ralbii ⊢ ∀ i ∈ A ∀ j ∈ A i = j ∨ B ∩ C = ∅ ↔ ∀ i ∈ A ∀ x ∀ j ∈ A x ∈ B ∧ x ∈ C → i = j
18 1 eleq2d ⊢ i = j → x ∈ B ↔ x ∈ C
19 18 rmo4 ⊢ ∃* i ∈ A x ∈ B ↔ ∀ i ∈ A ∀ j ∈ A x ∈ B ∧ x ∈ C → i = j
20 19 albii ⊢ ∀ x ∃* i ∈ A x ∈ B ↔ ∀ x ∀ i ∈ A ∀ j ∈ A x ∈ B ∧ x ∈ C → i = j
21 3 17 20 3bitr4i ⊢ ∀ i ∈ A ∀ j ∈ A i = j ∨ B ∩ C = ∅ ↔ ∀ x ∃* i ∈ A x ∈ B
22 2 21 bitr4i ⊢ Disj i ∈ A B ↔ ∀ i ∈ A ∀ j ∈ A i = j ∨ B ∩ C = ∅