Theorem orrabdioph

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

	Ref	Expression
Assertion	orrabdioph	⊢ ( ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑁 ) ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜓 } ∈ ( Dioph ‘ 𝑁 ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝜑 ∨ 𝜓 ) } ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		unrab	⊢ ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜑 } ∪ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜓 } ) = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝜑 ∨ 𝜓 ) }
2		diophun	⊢ ( ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑁 ) ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜓 } ∈ ( Dioph ‘ 𝑁 ) ) → ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜑 } ∪ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜓 } ) ∈ ( Dioph ‘ 𝑁 ) )
3	1 2	eqeltrrid	⊢ ( ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑁 ) ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜓 } ∈ ( Dioph ‘ 𝑁 ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝜑 ∨ 𝜓 ) } ∈ ( Dioph ‘ 𝑁 ) )