anrabdioph

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

		Ref	Expression
	Assertion	anrabdioph	$⊢ (\{t \in ({ℕ_{0}}^{(1 \dots N)}) \| φ\} \in Dioph (N) \land \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| ψ\} \in Dioph (N)) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (φ \land ψ)\} \in Dioph (N)$

Step	Hyp	Ref	Expression
1		inrab	$⊢ \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| φ\} \cap \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| ψ\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (φ \land ψ)\}$
2		diophin	$⊢ (\{t \in ({ℕ_{0}}^{(1 \dots N)}) \| φ\} \in Dioph (N) \land \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| ψ\} \in Dioph (N)) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| φ\} \cap \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| ψ\} \in Dioph (N)$
3	1 2	eqeltrrid	$⊢ (\{t \in ({ℕ_{0}}^{(1 \dots N)}) \| φ\} \in Dioph (N) \land \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| ψ\} \in Dioph (N)) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (φ \land ψ)\} \in Dioph (N)$

Metamath Proof Explorer