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 ⊢Ⅎ_iA
disjorf.2 ⊢Ⅎ_jA
disjorf.3 ⊢i=j→B=C
Assertion disjorf ⊢Disji∈AB↔∀i∈A∀j∈Ai=j∨B∩C=∅

Proof

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