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 ⊢Disji∈AB↔∀i∈A∀j∈Ai=j∨B∩C=∅

Proof

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