Theorem disjor 5106

Description: Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 14-Nov-2016.)

Hypothesis

Ref	Expression
disjor.1	⊢ (𝑖 = 𝑗 → 𝐵 = 𝐶)

Assertion

Ref	Expression
disjor	⊢ (Disj 𝑖 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅))

Distinct variable groups:   𝑖,𝑗,𝐴   𝐵,𝑗   𝐶,𝑖

Allowed substitution hints:   𝐵(𝑖)   𝐶(𝑗)

Proof of Theorem disjor

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-disj 5092	. 2 ⊢ (Disj 𝑖 ∈ 𝐴 𝐵 ↔ ∀𝑥∃*𝑖 ∈ 𝐴 𝑥 ∈ 𝐵)
2		ralcom4 3272	. . 3 ⊢ (∀𝑖 ∈ 𝐴 ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗) ↔ ∀𝑥∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
3		orcom 870	. . . . . . 7 ⊢ ((𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ((𝐵 ∩ 𝐶) = ∅ ∨ 𝑖 = 𝑗))
4		df-or 848	. . . . . . 7 ⊢ (((𝐵 ∩ 𝐶) = ∅ ∨ 𝑖 = 𝑗) ↔ (¬ (𝐵 ∩ 𝐶) = ∅ → 𝑖 = 𝑗))
5		neq0 4332	. . . . . . . . . 10 ⊢ (¬ (𝐵 ∩ 𝐶) = ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵 ∩ 𝐶))
6		elin 3947	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
7	6	exbii 1848	. . . . . . . . . 10 ⊢ (∃𝑥 𝑥 ∈ (𝐵 ∩ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
8	5, 7	bitri 275	. . . . . . . . 9 ⊢ (¬ (𝐵 ∩ 𝐶) = ∅ ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
9	8	imbi1i 349	. . . . . . . 8 ⊢ ((¬ (𝐵 ∩ 𝐶) = ∅ → 𝑖 = 𝑗) ↔ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
10		19.23v 1942	. . . . . . . 8 ⊢ (∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗) ↔ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
11	9, 10	bitr4i 278	. . . . . . 7 ⊢ ((¬ (𝐵 ∩ 𝐶) = ∅ → 𝑖 = 𝑗) ↔ ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
12	3, 4, 11	3bitri 297	. . . . . 6 ⊢ ((𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
13	12	ralbii 3083	. . . . 5 ⊢ (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑗 ∈ 𝐴 ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
14		ralcom4 3272	. . . . 5 ⊢ (∀𝑗 ∈ 𝐴 ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗) ↔ ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
15	13, 14	bitri 275	. . . 4 ⊢ (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
16	15	ralbii 3083	. . 3 ⊢ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑖 ∈ 𝐴 ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
17		disjor.1	. . . . . 6 ⊢ (𝑖 = 𝑗 → 𝐵 = 𝐶)
18	17	eleq2d 2821	. . . . 5 ⊢ (𝑖 = 𝑗 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
19	18	rmo4 3718	. . . 4 ⊢ (∃*𝑖 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
20	19	albii 1819	. . 3 ⊢ (∀𝑥∃*𝑖 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑥∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
21	2, 16, 20	3bitr4i 303	. 2 ⊢ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑥∃*𝑖 ∈ 𝐴 𝑥 ∈ 𝐵)
22	1, 21	bitr4i 278	1 ⊢ (Disj 𝑖 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∀wral 3052  ∃*wrmo 3363   ∩ cin 3930  ∅c0 4313  Disj wdisj 5091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-mo 2540  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rmo 3364  df-v 3466  df-dif 3934  df-in 3938  df-nul 4314  df-disj 5092

This theorem is referenced by:  disjors  5107  disjord  5113  disjiunb  5114  disjxiun  5121  disjxun  5122  otsndisj  5499  qsdisj2  8814  s3sndisj  14991  cshwsdisj  17123  dyadmbl  25558  numedglnl  29128  clwwlknondisj  30097  2wspmdisj  30323  disjnf  32556  disjorsf  32566  poimirlem26  37675  mblfinlem2  37687  grpods  42212  ndisj2  45042  nnfoctbdjlem  46451  iundjiun  46456  otiunsndisjX  47275