rexuz3

Description: Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013)

		Ref	Expression
	Hypothesis	rexuz3.1	$⊢ Z = ℤ_{\geq M}$
	Assertion	rexuz3	$⊢ M \in ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} φ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} φ)$

Proof

Step	Hyp	Ref	Expression
1		rexuz3.1	$⊢ Z = ℤ_{\geq M}$
2		ralel	$⊢ \forall k \in Z k \in Z$
3		fveq2	$⊢ j = M \to ℤ_{\geq j} = ℤ_{\geq M}$
4	3 1	eqtr4di	$⊢ j = M \to ℤ_{\geq j} = Z$
5	4	raleqdv	$⊢ j = M \to (\forall k \in ℤ_{\geq j} k \in Z \leftrightarrow \forall k \in Z k \in Z)$
6	5	rspcev	$⊢ (M \in ℤ \land \forall k \in Z k \in Z) \to \exists j \in ℤ \forall k \in ℤ_{\geq j} k \in Z$
7	2 6	mpan2	$⊢ M \in ℤ \to \exists j \in ℤ \forall k \in ℤ_{\geq j} k \in Z$
8	7	biantrurd	$⊢ M \in ℤ \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} φ \leftrightarrow (\exists j \in ℤ \forall k \in ℤ_{\geq j} k \in Z \land \exists j \in ℤ \forall k \in ℤ_{\geq j} φ))$
9	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
10	9	a1d	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to (φ \to k \in Z)$
11	10	ancrd	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to (φ \to (k \in Z \land φ))$
12	11	ralimdva	$⊢ j \in Z \to (\forall k \in ℤ_{\geq j} φ \to \forall k \in ℤ_{\geq j} (k \in Z \land φ))$
13		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
14	13 1	eleq2s	$⊢ j \in Z \to j \in ℤ$
15	12 14	jctild	$⊢ j \in Z \to (\forall k \in ℤ_{\geq j} φ \to (j \in ℤ \land \forall k \in ℤ_{\geq j} (k \in Z \land φ)))$
16	15	imp	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} φ) \to (j \in ℤ \land \forall k \in ℤ_{\geq j} (k \in Z \land φ))$
17		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
18		simpl	$⊢ (k \in Z \land φ) \to k \in Z$
19	18	ralimi	$⊢ \forall k \in ℤ_{\geq j} (k \in Z \land φ) \to \forall k \in ℤ_{\geq j} k \in Z$
20		eleq1w	$⊢ k = j \to (k \in Z \leftrightarrow j \in Z)$
21	20	rspcva	$⊢ (j \in ℤ_{\geq j} \land \forall k \in ℤ_{\geq j} k \in Z) \to j \in Z$
22	17 19 21	syl2an	$⊢ (j \in ℤ \land \forall k \in ℤ_{\geq j} (k \in Z \land φ)) \to j \in Z$
23		simpr	$⊢ (k \in Z \land φ) \to φ$
24	23	ralimi	$⊢ \forall k \in ℤ_{\geq j} (k \in Z \land φ) \to \forall k \in ℤ_{\geq j} φ$
25	24	adantl	$⊢ (j \in ℤ \land \forall k \in ℤ_{\geq j} (k \in Z \land φ)) \to \forall k \in ℤ_{\geq j} φ$
26	22 25	jca	$⊢ (j \in ℤ \land \forall k \in ℤ_{\geq j} (k \in Z \land φ)) \to (j \in Z \land \forall k \in ℤ_{\geq j} φ)$
27	16 26	impbii	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} φ) \leftrightarrow (j \in ℤ \land \forall k \in ℤ_{\geq j} (k \in Z \land φ))$
28	27	rexbii2	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} φ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in Z \land φ)$
29		rexanuz	$⊢ \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in Z \land φ) \leftrightarrow (\exists j \in ℤ \forall k \in ℤ_{\geq j} k \in Z \land \exists j \in ℤ \forall k \in ℤ_{\geq j} φ)$
30	28 29	bitr2i	$⊢ (\exists j \in ℤ \forall k \in ℤ_{\geq j} k \in Z \land \exists j \in ℤ \forall k \in ℤ_{\geq j} φ) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} φ$
31	8 30	bitr2di	$⊢ M \in ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} φ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} φ)$

Metamath Proof Explorer

Theorem rexuz3

Proof