Theorem 3orrabdioph

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

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

Proof

Step	Hyp	Ref	Expression
1		df-3or	⊢ ( ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) )
2	1	rabbii	⊢ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) }
3		orrabdioph	⊢ ( ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑁 ) ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜓 } ∈ ( Dioph ‘ 𝑁 ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝜑 ∨ 𝜓 ) } ∈ ( Dioph ‘ 𝑁 ) )
4		orrabdioph	⊢ ( ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝜑 ∨ 𝜓 ) } ∈ ( Dioph ‘ 𝑁 ) ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜒 } ∈ ( Dioph ‘ 𝑁 ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) } ∈ ( Dioph ‘ 𝑁 ) )
5	3 4	sylan	⊢ ( ( ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑁 ) ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜓 } ∈ ( Dioph ‘ 𝑁 ) ) ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜒 } ∈ ( Dioph ‘ 𝑁 ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) } ∈ ( Dioph ‘ 𝑁 ) )
6	2 5	eqeltrid	⊢ ( ( ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑁 ) ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜓 } ∈ ( Dioph ‘ 𝑁 ) ) ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜒 } ∈ ( Dioph ‘ 𝑁 ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) } ∈ ( Dioph ‘ 𝑁 ) )
7	6	3impa	⊢ ( ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑁 ) ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜓 } ∈ ( Dioph ‘ 𝑁 ) ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜒 } ∈ ( Dioph ‘ 𝑁 ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) } ∈ ( Dioph ‘ 𝑁 ) )