Metamath Proof Explorer

Theorem disjorf

Description: Two ways to say that a collection B ( i ) for i e. A is disjoint. (Contributed by Thierry Arnoux, 8-Mar-2017)

Ref Expression
Hypotheses disjorf.1 ⊢ Ⅎ _ i A
disjorf.2 ⊢ Ⅎ _ j A
disjorf.3 ⊢ i = j → B = C
Assertion disjorf ⊢ Disj i ∈ A B ↔ ∀ i ∈ A ∀ j ∈ A i = j ∨ B ∩ C = ∅

Proof

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