Metamath Proof Explorer

Theorem orrabdioph

Description: Diophantine set builder for disjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion orrabdioph ⊢ t ∈ ℕ 0 1 … N | φ ∈ Dioph ⁡ N ∧ t ∈ ℕ 0 1 … N | ψ ∈ Dioph ⁡ N → t ∈ ℕ 0 1 … N | φ ∨ ψ ∈ Dioph ⁡ N

Proof

Step Hyp Ref Expression
1 unrab ⊢ t ∈ ℕ 0 1 … N | φ ∪ t ∈ ℕ 0 1 … N | ψ = t ∈ ℕ 0 1 … N | φ ∨ ψ
2 diophun ⊢ t ∈ ℕ 0 1 … N | φ ∈ Dioph ⁡ N ∧ t ∈ ℕ 0 1 … N | ψ ∈ Dioph ⁡ N → t ∈ ℕ 0 1 … N | φ ∪ t ∈ ℕ 0 1 … N | ψ ∈ Dioph ⁡ N
3 1 2 eqeltrrid ⊢ t ∈ ℕ 0 1 … N | φ ∈ Dioph ⁡ N ∧ t ∈ ℕ 0 1 … N | ψ ∈ Dioph ⁡ N → t ∈ ℕ 0 1 … N | φ ∨ ψ ∈ Dioph ⁡ N