3orrabdioph

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

		Ref	Expression
	Assertion	3orrabdioph	$⊢ (\{t \in ({ℕ_{0}}^{(1 \dots N)}) \| φ\} \in Dioph (N) \land \{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)}) \| (φ \lor ψ \lor χ)\} \in Dioph (N)$

Step	Hyp	Ref	Expression
1		df-3or	$⊢ (φ \lor ψ \lor χ) \leftrightarrow ((φ \lor ψ) \lor χ)$
2	1	rabbii	$⊢ \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (φ \lor ψ \lor χ)\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| ((φ \lor ψ) \lor χ)\}$
3		orrabdioph	$⊢ (\{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)}) \| (φ \lor ψ)\} \in Dioph (N)$
4		orrabdioph	$⊢ (\{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (φ \lor ψ)\} \in Dioph (N) \land \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| χ\} \in Dioph (N)) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| ((φ \lor ψ) \lor χ)\} \in Dioph (N)$
5	3 4	sylan	$⊢ ((\{t \in ({ℕ_{0}}^{(1 \dots N)}) \| φ\} \in Dioph (N) \land \{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)}) \| ((φ \lor ψ) \lor χ)\} \in Dioph (N)$
6	2 5	eqeltrid	$⊢ ((\{t \in ({ℕ_{0}}^{(1 \dots N)}) \| φ\} \in Dioph (N) \land \{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)}) \| (φ \lor ψ \lor χ)\} \in Dioph (N)$
7	6	3impa	$⊢ (\{t \in ({ℕ_{0}}^{(1 \dots N)}) \| φ\} \in Dioph (N) \land \{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)}) \| (φ \lor ψ \lor χ)\} \in Dioph (N)$

Metamath Proof Explorer