Theorem disjor 5068

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 5054	. 2 ⊢ (Disj 𝑖 ∈ 𝐴 𝐵 ↔ ∀𝑥∃*𝑖 ∈ 𝐴 𝑥 ∈ 𝐵)
2		ralcom4 3264	. . 3 ⊢ (∀𝑖 ∈ 𝐴 ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗) ↔ ∀𝑥∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
3		orcom 871	. . . . . . 7 ⊢ ((𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ((𝐵 ∩ 𝐶) = ∅ ∨ 𝑖 = 𝑗))
4		df-or 849	. . . . . . 7 ⊢ (((𝐵 ∩ 𝐶) = ∅ ∨ 𝑖 = 𝑗) ↔ (¬ (𝐵 ∩ 𝐶) = ∅ → 𝑖 = 𝑗))
5		neq0 4293	. . . . . . . . . 10 ⊢ (¬ (𝐵 ∩ 𝐶) = ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵 ∩ 𝐶))
6		elin 3906	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
7	6	exbii 1850	. . . . . . . . . 10 ⊢ (∃𝑥 𝑥 ∈ (𝐵 ∩ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
8	5, 7	bitri 275	. . . . . . . . 9 ⊢ (¬ (𝐵 ∩ 𝐶) = ∅ ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
9	8	imbi1i 349	. . . . . . . 8 ⊢ ((¬ (𝐵 ∩ 𝐶) = ∅ → 𝑖 = 𝑗) ↔ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
10		19.23v 1944	. . . . . . . 8 ⊢ (∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗) ↔ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
11	9, 10	bitr4i 278	. . . . . . 7 ⊢ ((¬ (𝐵 ∩ 𝐶) = ∅ → 𝑖 = 𝑗) ↔ ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
12	3, 4, 11	3bitri 297	. . . . . 6 ⊢ ((𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
13	12	ralbii 3084	. . . . 5 ⊢ (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑗 ∈ 𝐴 ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
14		ralcom4 3264	. . . . 5 ⊢ (∀𝑗 ∈ 𝐴 ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗) ↔ ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
15	13, 14	bitri 275	. . . 4 ⊢ (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
16	15	ralbii 3084	. . 3 ⊢ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑖 ∈ 𝐴 ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
17		disjor.1	. . . . . 6 ⊢ (𝑖 = 𝑗 → 𝐵 = 𝐶)
18	17	eleq2d 2823	. . . . 5 ⊢ (𝑖 = 𝑗 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
19	18	rmo4 3677	. . . 4 ⊢ (∃*𝑖 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
20	19	albii 1821	. . 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 848  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∀wral 3052  ∃*wrmo 3342   ∩ cin 3889  ∅c0 4274  Disj wdisj 5053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-11 2163  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rmo 3343  df-v 3432  df-dif 3893  df-in 3897  df-nul 4275  df-disj 5054

This theorem is referenced by:  disjors  5069  disjord  5075  disjiunb  5076  disjxiun  5083  disjxun  5084  otsndisj  5467  qsdisj2  8735  s3sndisj  14920  cshwsdisj  17060  dyadmbl  25577  numedglnl  29227  clwwlknondisj  30196  2wspmdisj  30422  disjnf  32655  disjorsf  32665  poimirlem26  37981  mblfinlem2  37993  grpods  42647  ndisj2  45500  nnfoctbdjlem  46901  iundjiun  46906  otiunsndisjX  47739