Proof of Theorem dcun
| Step | Hyp | Ref
 | Expression | 
| 1 |   | elun1 3330 | 
. . . . 5
⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ (𝐴 ∪ 𝐵)) | 
| 2 | 1 | adantl 277 | 
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ (𝐴 ∪ 𝐵)) | 
| 3 | 2 | orcd 734 | 
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐶 ∈ (𝐴 ∪ 𝐵) ∨ ¬ 𝐶 ∈ (𝐴 ∪ 𝐵))) | 
| 4 |   | df-dc 836 | 
. . 3
⊢
(DECID 𝐶 ∈ (𝐴 ∪ 𝐵) ↔ (𝐶 ∈ (𝐴 ∪ 𝐵) ∨ ¬ 𝐶 ∈ (𝐴 ∪ 𝐵))) | 
| 5 | 3, 4 | sylibr 134 | 
. 2
⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → DECID 𝐶 ∈ (𝐴 ∪ 𝐵)) | 
| 6 |   | elun2 3331 | 
. . . . . 6
⊢ (𝐶 ∈ 𝐵 → 𝐶 ∈ (𝐴 ∪ 𝐵)) | 
| 7 | 6 | adantl 277 | 
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ 𝐴) ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ (𝐴 ∪ 𝐵)) | 
| 8 | 7 | orcd 734 | 
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ 𝐴) ∧ 𝐶 ∈ 𝐵) → (𝐶 ∈ (𝐴 ∪ 𝐵) ∨ ¬ 𝐶 ∈ (𝐴 ∪ 𝐵))) | 
| 9 | 8, 4 | sylibr 134 | 
. . 3
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ 𝐴) ∧ 𝐶 ∈ 𝐵) → DECID 𝐶 ∈ (𝐴 ∪ 𝐵)) | 
| 10 |   | simplr 528 | 
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ 𝐴) ∧ ¬ 𝐶 ∈ 𝐵) → ¬ 𝐶 ∈ 𝐴) | 
| 11 |   | simpr 110 | 
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ 𝐴) ∧ ¬ 𝐶 ∈ 𝐵) → ¬ 𝐶 ∈ 𝐵) | 
| 12 |   | ioran 753 | 
. . . . . . 7
⊢ (¬
(𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵) ↔ (¬ 𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐵)) | 
| 13 | 10, 11, 12 | sylanbrc 417 | 
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ 𝐴) ∧ ¬ 𝐶 ∈ 𝐵) → ¬ (𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵)) | 
| 14 |   | elun 3304 | 
. . . . . 6
⊢ (𝐶 ∈ (𝐴 ∪ 𝐵) ↔ (𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵)) | 
| 15 | 13, 14 | sylnibr 678 | 
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ 𝐴) ∧ ¬ 𝐶 ∈ 𝐵) → ¬ 𝐶 ∈ (𝐴 ∪ 𝐵)) | 
| 16 | 15 | olcd 735 | 
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ 𝐴) ∧ ¬ 𝐶 ∈ 𝐵) → (𝐶 ∈ (𝐴 ∪ 𝐵) ∨ ¬ 𝐶 ∈ (𝐴 ∪ 𝐵))) | 
| 17 | 16, 4 | sylibr 134 | 
. . 3
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ 𝐴) ∧ ¬ 𝐶 ∈ 𝐵) → DECID 𝐶 ∈ (𝐴 ∪ 𝐵)) | 
| 18 |   | dcun.b | 
. . . . 5
⊢ (𝜑 → DECID 𝐶 ∈ 𝐵) | 
| 19 |   | exmiddc 837 | 
. . . . 5
⊢
(DECID 𝐶 ∈ 𝐵 → (𝐶 ∈ 𝐵 ∨ ¬ 𝐶 ∈ 𝐵)) | 
| 20 | 18, 19 | syl 14 | 
. . . 4
⊢ (𝜑 → (𝐶 ∈ 𝐵 ∨ ¬ 𝐶 ∈ 𝐵)) | 
| 21 | 20 | adantr 276 | 
. . 3
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ 𝐴) → (𝐶 ∈ 𝐵 ∨ ¬ 𝐶 ∈ 𝐵)) | 
| 22 | 9, 17, 21 | mpjaodan 799 | 
. 2
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ 𝐴) → DECID 𝐶 ∈ (𝐴 ∪ 𝐵)) | 
| 23 |   | dcun.a | 
. . 3
⊢ (𝜑 → DECID 𝐶 ∈ 𝐴) | 
| 24 |   | exmiddc 837 | 
. . 3
⊢
(DECID 𝐶 ∈ 𝐴 → (𝐶 ∈ 𝐴 ∨ ¬ 𝐶 ∈ 𝐴)) | 
| 25 | 23, 24 | syl 14 | 
. 2
⊢ (𝜑 → (𝐶 ∈ 𝐴 ∨ ¬ 𝐶 ∈ 𝐴)) | 
| 26 | 5, 22, 25 | mpjaodan 799 | 
1
⊢ (𝜑 → DECID 𝐶 ∈ (𝐴 ∪ 𝐵)) |