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 ⊢ Ⅎ 𝑖 𝐴
disjorf.2 ⊢ Ⅎ 𝑗 𝐴
disjorf.3 ⊢ ( 𝑖 = 𝑗 → 𝐵 = 𝐶 )
Assertion disjorf ( Disj 𝑖 ∈ 𝐴 𝐵 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) )

Proof

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