Theorem disjor 5073

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 5059	. 2 ⊢ (Disj 𝑖 ∈ 𝐴 𝐵 ↔ ∀𝑥∃*𝑖 ∈ 𝐴 𝑥 ∈ 𝐵)
2		ralcom4 3258	. . 3 ⊢ (∀𝑖 ∈ 𝐴 ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗) ↔ ∀𝑥∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
3		orcom 870	. . . . . . 7 ⊢ ((𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ((𝐵 ∩ 𝐶) = ∅ ∨ 𝑖 = 𝑗))
4		df-or 848	. . . . . . 7 ⊢ (((𝐵 ∩ 𝐶) = ∅ ∨ 𝑖 = 𝑗) ↔ (¬ (𝐵 ∩ 𝐶) = ∅ → 𝑖 = 𝑗))
5		neq0 4302	. . . . . . . . . 10 ⊢ (¬ (𝐵 ∩ 𝐶) = ∅ ↔ ∃𝑥 𝑥 ∈ (𝐵 ∩ 𝐶))
6		elin 3918	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
7	6	exbii 1849	. . . . . . . . . 10 ⊢ (∃𝑥 𝑥 ∈ (𝐵 ∩ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
8	5, 7	bitri 275	. . . . . . . . 9 ⊢ (¬ (𝐵 ∩ 𝐶) = ∅ ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
9	8	imbi1i 349	. . . . . . . 8 ⊢ ((¬ (𝐵 ∩ 𝐶) = ∅ → 𝑖 = 𝑗) ↔ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
10		19.23v 1943	. . . . . . . 8 ⊢ (∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗) ↔ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
11	9, 10	bitr4i 278	. . . . . . 7 ⊢ ((¬ (𝐵 ∩ 𝐶) = ∅ → 𝑖 = 𝑗) ↔ ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
12	3, 4, 11	3bitri 297	. . . . . 6 ⊢ ((𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
13	12	ralbii 3078	. . . . 5 ⊢ (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑗 ∈ 𝐴 ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
14		ralcom4 3258	. . . . 5 ⊢ (∀𝑗 ∈ 𝐴 ∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗) ↔ ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
15	13, 14	bitri 275	. . . 4 ⊢ (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
16	15	ralbii 3078	. . 3 ⊢ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅) ↔ ∀𝑖 ∈ 𝐴 ∀𝑥∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
17		disjor.1	. . . . . 6 ⊢ (𝑖 = 𝑗 → 𝐵 = 𝐶)
18	17	eleq2d 2817	. . . . 5 ⊢ (𝑖 = 𝑗 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
19	18	rmo4 3689	. . . 4 ⊢ (∃*𝑖 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶) → 𝑖 = 𝑗))
20	19	albii 1820	. . 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 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2111  ∀wral 3047  ∃*wrmo 3345   ∩ cin 3901  ∅c0 4283  Disj wdisj 5058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-11 2160  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2535  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rmo 3346  df-v 3438  df-dif 3905  df-in 3909  df-nul 4284  df-disj 5059

This theorem is referenced by:  disjors  5074  disjord  5080  disjiunb  5081  disjxiun  5088  disjxun  5089  otsndisj  5459  qsdisj2  8719  s3sndisj  14871  cshwsdisj  17007  dyadmbl  25526  numedglnl  29120  clwwlknondisj  30086  2wspmdisj  30312  disjnf  32545  disjorsf  32555  poimirlem26  37685  mblfinlem2  37697  grpods  42226  ndisj2  45087  nnfoctbdjlem  46492  iundjiun  46497  otiunsndisjX  47309