Theorem 3anrabdioph

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

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

Proof

Step	Hyp	Ref	Expression
1		df-3an	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) )
2	1	rabbii	⊢ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) } = { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) }
3		anrabdioph	⊢ ( ( { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 𝑁 ) ∧ { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜓 } ∈ ( Dioph ‘ 𝑁 ) ) → { 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ ( 𝜑 ∧ 𝜓 ) } ∈ ( Dioph ‘ 𝑁 ) )
4		anrabdioph	⊢ ( ( { 𝑡 ∈ ( ℕ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 ‘ 𝑁 ) )