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

Proof

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