Theorem disjor 5087

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 5073	. 2 ⊢ (Disj 𝑖 ∈ 𝐴 𝐵 ↔ ∀𝑥∃*𝑖 ∈ 𝐴 𝑥 ∈ 𝐵)
2		ralcom4 3291	. . 3 ⊢ (∀𝑖 ∈ 𝐴 ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗) ↔ ∀𝑥∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
3		orcom 883	. . . . . . 7 ⊢ ((𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ((𝐵 ∩ 𝐶) = ∅ ∨ 𝑖 = 𝑗))
4		df-or 861	. . . . . . 7 ⊢ (((𝐵 ∩ 𝐶) = ∅ ∨ 𝑖 = 𝑗) ↔ (¬ (𝐵 ∩ 𝐶) = ∅ → 𝑖 = 𝑗))
5		neq0 4307	. . . . . . . . . 10 ⊢ (¬ (𝐵 ∩ 𝐶) = ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵 ∩ 𝐶))
6		elin 3923	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
7	6	exbii 1871	. . . . . . . . . 10 ⊢ (∃𝑥 𝑥 ∈ (𝐵 ∩ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
8	5, 7	bitri 278	. . . . . . . . 9 ⊢ (¬ (𝐵 ∩ 𝐶) = ∅ ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
9	8	imbi1i 352	. . . . . . . 8 ⊢ ((¬ (𝐵 ∩ 𝐶) = ∅ → 𝑖 = 𝑗) ↔ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
10		19.23v 1965	. . . . . . . 8 ⊢ (∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗) ↔ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
11	9, 10	bitr4i 281	. . . . . . 7 ⊢ ((¬ (𝐵 ∩ 𝐶) = ∅ → 𝑖 = 𝑗) ↔ ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
12	3, 4, 11	3bitri 300	. . . . . 6 ⊢ ((𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
13	12	ralbii 3111	. . . . 5 ⊢ (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑗 ∈ 𝐴 ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
14		ralcom4 3291	. . . . 5 ⊢ (∀𝑗 ∈ 𝐴 ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗) ↔ ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
15	13, 14	bitri 278	. . . 4 ⊢ (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
16	15	ralbii 3111	. . 3 ⊢ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑖 ∈ 𝐴 ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
17		disjor.1	. . . . . 6 ⊢ (𝑖 = 𝑗 → 𝐵 = 𝐶)
18	17	eleq2d 2851	. . . . 5 ⊢ (𝑖 = 𝑗 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
19	18	rmo4 3696	. . . 4 ⊢ (∃*𝑖 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
20	19	albii 1842	. . 3 ⊢ (∀𝑥∃*𝑖 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑥∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
21	2, 16, 20	3bitr4i 306	. 2 ⊢ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑥∃*𝑖 ∈ 𝐴 𝑥 ∈ 𝐵)
22	1, 21	bitr4i 281	1 ⊢ (Disj 𝑖 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860  ∀wal 1561   = wceq 1563  ∃wex 1802   ∈ wcel 2145  ∀wral 3079  ∃*wrmo 3369   ∩ cin 3906  ∅c0 4288  Disj wdisj 5072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-11 2194  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-mo 2569  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rmo 3370  df-v 3459  df-dif 3910  df-in 3914  df-nul 4289  df-disj 5073

This theorem is referenced by:  disjors  5088  disjord  5094  disjiunb  5095  disjxiun  5102  disjxun  5103  otsndisj  5493  qsdisj2  8781  s3sndisj  14994  cshwsdisj  17148  dyadmbl  25720  numedglnl  29403  clwwlknondisj  30371  2wspmdisj  30597  disjnf  32825  disjorsf  32835  poimirlem26  38157  mblfinlem2  38169  grpods  42823  ndisj2  45629  nnfoctbdjlem  47027  iundjiun  47032  otiunsndisjX  47871