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

Theorem dcun 3604
Description: The union of two decidable classes is decidable. (Contributed by Jim Kingdon, 5-Oct-2022.) (Revised by Jim Kingdon, 13-Oct-2025.)
Hypotheses
Ref Expression
dcun.a (𝜑DECID 𝐶𝐴)
dcun.b (𝜑DECID 𝐶𝐵)
Assertion
Ref Expression
dcun (𝜑DECID 𝐶 ∈ (𝐴𝐵))

Proof of Theorem dcun
StepHypRef Expression
1 elun1 3374 . . . . 5 (𝐶𝐴𝐶 ∈ (𝐴𝐵))
21adantl 277 . . . 4 ((𝜑𝐶𝐴) → 𝐶 ∈ (𝐴𝐵))
32orcd 740 . . 3 ((𝜑𝐶𝐴) → (𝐶 ∈ (𝐴𝐵) ∨ ¬ 𝐶 ∈ (𝐴𝐵)))
4 df-dc 842 . . 3 (DECID 𝐶 ∈ (𝐴𝐵) ↔ (𝐶 ∈ (𝐴𝐵) ∨ ¬ 𝐶 ∈ (𝐴𝐵)))
53, 4sylibr 134 . 2 ((𝜑𝐶𝐴) → DECID 𝐶 ∈ (𝐴𝐵))
6 elun2 3375 . . . . . 6 (𝐶𝐵𝐶 ∈ (𝐴𝐵))
76adantl 277 . . . . 5 (((𝜑 ∧ ¬ 𝐶𝐴) ∧ 𝐶𝐵) → 𝐶 ∈ (𝐴𝐵))
87orcd 740 . . . 4 (((𝜑 ∧ ¬ 𝐶𝐴) ∧ 𝐶𝐵) → (𝐶 ∈ (𝐴𝐵) ∨ ¬ 𝐶 ∈ (𝐴𝐵)))
98, 4sylibr 134 . . 3 (((𝜑 ∧ ¬ 𝐶𝐴) ∧ 𝐶𝐵) → DECID 𝐶 ∈ (𝐴𝐵))
10 simplr 529 . . . . . . 7 (((𝜑 ∧ ¬ 𝐶𝐴) ∧ ¬ 𝐶𝐵) → ¬ 𝐶𝐴)
11 simpr 110 . . . . . . 7 (((𝜑 ∧ ¬ 𝐶𝐴) ∧ ¬ 𝐶𝐵) → ¬ 𝐶𝐵)
12 ioran 759 . . . . . . 7 (¬ (𝐶𝐴𝐶𝐵) ↔ (¬ 𝐶𝐴 ∧ ¬ 𝐶𝐵))
1310, 11, 12sylanbrc 417 . . . . . 6 (((𝜑 ∧ ¬ 𝐶𝐴) ∧ ¬ 𝐶𝐵) → ¬ (𝐶𝐴𝐶𝐵))
14 elun 3348 . . . . . 6 (𝐶 ∈ (𝐴𝐵) ↔ (𝐶𝐴𝐶𝐵))
1513, 14sylnibr 683 . . . . 5 (((𝜑 ∧ ¬ 𝐶𝐴) ∧ ¬ 𝐶𝐵) → ¬ 𝐶 ∈ (𝐴𝐵))
1615olcd 741 . . . 4 (((𝜑 ∧ ¬ 𝐶𝐴) ∧ ¬ 𝐶𝐵) → (𝐶 ∈ (𝐴𝐵) ∨ ¬ 𝐶 ∈ (𝐴𝐵)))
1716, 4sylibr 134 . . 3 (((𝜑 ∧ ¬ 𝐶𝐴) ∧ ¬ 𝐶𝐵) → DECID 𝐶 ∈ (𝐴𝐵))
18 dcun.b . . . . 5 (𝜑DECID 𝐶𝐵)
19 exmiddc 843 . . . . 5 (DECID 𝐶𝐵 → (𝐶𝐵 ∨ ¬ 𝐶𝐵))
2018, 19syl 14 . . . 4 (𝜑 → (𝐶𝐵 ∨ ¬ 𝐶𝐵))
2120adantr 276 . . 3 ((𝜑 ∧ ¬ 𝐶𝐴) → (𝐶𝐵 ∨ ¬ 𝐶𝐵))
229, 17, 21mpjaodan 805 . 2 ((𝜑 ∧ ¬ 𝐶𝐴) → DECID 𝐶 ∈ (𝐴𝐵))
23 dcun.a . . 3 (𝜑DECID 𝐶𝐴)
24 exmiddc 843 . . 3 (DECID 𝐶𝐴 → (𝐶𝐴 ∨ ¬ 𝐶𝐴))
2523, 24syl 14 . 2 (𝜑 → (𝐶𝐴 ∨ ¬ 𝐶𝐴))
265, 22, 25mpjaodan 805 1 (𝜑DECID 𝐶 ∈ (𝐴𝐵))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wo 715  DECID wdc 841  wcel 2202  cun 3198
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213
This theorem depends on definitions:  df-bi 117  df-dc 842  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-in 3206  df-ss 3213
This theorem is referenced by:  tpfidceq  7122  sumsplitdc  11995
  Copyright terms: Public domain W3C validator