ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  disjnim GIF version

Theorem disjnim 3842
Description: If a collection 𝐵(𝑖) for 𝑖𝐴 is disjoint, then pairs are disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Jim Kingdon, 6-Oct-2022.)
Hypothesis
Ref Expression
disjnim.1 (𝑖 = 𝑗𝐵 = 𝐶)
Assertion
Ref Expression
disjnim (Disj 𝑖𝐴 𝐵 → ∀𝑖𝐴𝑗𝐴 (𝑖𝑗 → (𝐵𝐶) = ∅))
Distinct variable groups:   𝑖,𝑗,𝐴   𝐵,𝑗   𝐶,𝑖
Allowed substitution hints:   𝐵(𝑖)   𝐶(𝑗)

Proof of Theorem disjnim
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 df-disj 3829 . 2 (Disj 𝑖𝐴 𝐵 ↔ ∀𝑥∃*𝑖𝐴 𝑥𝐵)
2 disjnim.1 . . . . . . 7 (𝑖 = 𝑗𝐵 = 𝐶)
32eleq2d 2158 . . . . . 6 (𝑖 = 𝑗 → (𝑥𝐵𝑥𝐶))
43rmo4 2809 . . . . 5 (∃*𝑖𝐴 𝑥𝐵 ↔ ∀𝑖𝐴𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
54albii 1405 . . . 4 (∀𝑥∃*𝑖𝐴 𝑥𝐵 ↔ ∀𝑥𝑖𝐴𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
6 ralcom4 2642 . . . 4 (∀𝑖𝐴𝑥𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗) ↔ ∀𝑥𝑖𝐴𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
75, 6bitr4i 186 . . 3 (∀𝑥∃*𝑖𝐴 𝑥𝐵 ↔ ∀𝑖𝐴𝑥𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
8 ralcom4 2642 . . . . 5 (∀𝑗𝐴𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗) ↔ ∀𝑥𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
9 19.23v 1812 . . . . . . . . 9 (∀𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗) ↔ (∃𝑥(𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
109biimpi 119 . . . . . . . 8 (∀𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗) → (∃𝑥(𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗))
1110necon3ad 2298 . . . . . . 7 (∀𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗) → (𝑖𝑗 → ¬ ∃𝑥(𝑥𝐵𝑥𝐶)))
12 notm0 3307 . . . . . . . 8 (¬ ∃𝑥 𝑥 ∈ (𝐵𝐶) ↔ (𝐵𝐶) = ∅)
13 elin 3184 . . . . . . . . . 10 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵𝑥𝐶))
1413exbii 1542 . . . . . . . . 9 (∃𝑥 𝑥 ∈ (𝐵𝐶) ↔ ∃𝑥(𝑥𝐵𝑥𝐶))
1514notbii 630 . . . . . . . 8 (¬ ∃𝑥 𝑥 ∈ (𝐵𝐶) ↔ ¬ ∃𝑥(𝑥𝐵𝑥𝐶))
1612, 15bitr3i 185 . . . . . . 7 ((𝐵𝐶) = ∅ ↔ ¬ ∃𝑥(𝑥𝐵𝑥𝐶))
1711, 16syl6ibr 161 . . . . . 6 (∀𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗) → (𝑖𝑗 → (𝐵𝐶) = ∅))
1817ralimi 2439 . . . . 5 (∀𝑗𝐴𝑥((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗) → ∀𝑗𝐴 (𝑖𝑗 → (𝐵𝐶) = ∅))
198, 18sylbir 134 . . . 4 (∀𝑥𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗) → ∀𝑗𝐴 (𝑖𝑗 → (𝐵𝐶) = ∅))
2019ralimi 2439 . . 3 (∀𝑖𝐴𝑥𝑗𝐴 ((𝑥𝐵𝑥𝐶) → 𝑖 = 𝑗) → ∀𝑖𝐴𝑗𝐴 (𝑖𝑗 → (𝐵𝐶) = ∅))
217, 20sylbi 120 . 2 (∀𝑥∃*𝑖𝐴 𝑥𝐵 → ∀𝑖𝐴𝑗𝐴 (𝑖𝑗 → (𝐵𝐶) = ∅))
221, 21sylbi 120 1 (Disj 𝑖𝐴 𝐵 → ∀𝑖𝐴𝑗𝐴 (𝑖𝑗 → (𝐵𝐶) = ∅))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wal 1288   = wceq 1290  wex 1427  wcel 1439  wne 2256  wral 2360  ∃*wrmo 2363  cin 2999  c0 3287  Disj wdisj 3828
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071
This theorem depends on definitions:  df-bi 116  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rmo 2368  df-v 2622  df-dif 3002  df-in 3006  df-nul 3288  df-disj 3829
This theorem is referenced by:  disjnims  3843
  Copyright terms: Public domain W3C validator