Metamath Proof Explorer

Theorem raluz2

Description: Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005)

		Ref	Expression
	Assertion	raluz2	$⊢ \forall n \in ℤ_{\geq M} φ \leftrightarrow (M \in ℤ \to \forall n \in ℤ (M \leq n \to φ))$

Proof

Step	Hyp	Ref	Expression
1		eluz2	$⊢ n \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land n \in ℤ \land M \leq n)$
2		3anass	$⊢ (M \in ℤ \land n \in ℤ \land M \leq n) \leftrightarrow (M \in ℤ \land (n \in ℤ \land M \leq n))$
3	1 2	bitri	$⊢ n \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land (n \in ℤ \land M \leq n))$
4	3	imbi1i	$⊢ (n \in ℤ_{\geq M} \to φ) \leftrightarrow ((M \in ℤ \land (n \in ℤ \land M \leq n)) \to φ)$
5		impexp	$⊢ ((M \in ℤ \land (n \in ℤ \land M \leq n)) \to φ) \leftrightarrow (M \in ℤ \to ((n \in ℤ \land M \leq n) \to φ))$
6		impexp	$⊢ ((n \in ℤ \land M \leq n) \to φ) \leftrightarrow (n \in ℤ \to (M \leq n \to φ))$
7	6	imbi2i	$⊢ (M \in ℤ \to ((n \in ℤ \land M \leq n) \to φ)) \leftrightarrow (M \in ℤ \to (n \in ℤ \to (M \leq n \to φ)))$
8	5 7	bitri	$⊢ ((M \in ℤ \land (n \in ℤ \land M \leq n)) \to φ) \leftrightarrow (M \in ℤ \to (n \in ℤ \to (M \leq n \to φ)))$
9		bi2.04	$⊢ (M \in ℤ \to (n \in ℤ \to (M \leq n \to φ))) \leftrightarrow (n \in ℤ \to (M \in ℤ \to (M \leq n \to φ)))$
10	8 9	bitri	$⊢ ((M \in ℤ \land (n \in ℤ \land M \leq n)) \to φ) \leftrightarrow (n \in ℤ \to (M \in ℤ \to (M \leq n \to φ)))$
11	4 10	bitri	$⊢ (n \in ℤ_{\geq M} \to φ) \leftrightarrow (n \in ℤ \to (M \in ℤ \to (M \leq n \to φ)))$
12	11	ralbii2	$⊢ \forall n \in ℤ_{\geq M} φ \leftrightarrow \forall n \in ℤ (M \in ℤ \to (M \leq n \to φ))$
13		r19.21v	$⊢ \forall n \in ℤ (M \in ℤ \to (M \leq n \to φ)) \leftrightarrow (M \in ℤ \to \forall n \in ℤ (M \leq n \to φ))$
14	12 13	bitri	$⊢ \forall n \in ℤ_{\geq M} φ \leftrightarrow (M \in ℤ \to \forall n \in ℤ (M \leq n \to φ))$