Theorem rexanuz2

Description: Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013)

	Ref	Expression
Hypothesis	rexuz3.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
Assertion	rexanuz2	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \wedge \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		rexuz3.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		eluzel2	$$⊢j\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
3	2 1	eleq2s	$$⊢j\in Z\to M\in \mathbb{Z}$$
4	3	a1d	$$⊢j\in Z\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\to M\in \mathbb{Z}\right)$$
5	4	rexlimiv	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\to M\in \mathbb{Z}$$
6	3	a1d	$$⊢j\in Z\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\phi \to M\in \mathbb{Z}\right)$$
7	6	rexlimiv	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \to M\in \mathbb{Z}$$
8	7	adantr	$$⊢\left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \wedge \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)\to M\in \mathbb{Z}$$
9	1	rexuz3	$$⊢M\in \mathbb{Z}\to \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\leftrightarrow \exists j\in \mathbb{Z}\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\right)$$
10		rexanuz	$$⊢\exists j\in \mathbb{Z}\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists j\in \mathbb{Z}\forall k\in {\mathbb{Z}}_{\ge j}\phi \wedge \exists j\in \mathbb{Z}\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)$$
11	1	rexuz3	$$⊢M\in \mathbb{Z}\to \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \leftrightarrow \exists j\in \mathbb{Z}\forall k\in {\mathbb{Z}}_{\ge j}\phi \right)$$
12	1	rexuz3	$$⊢M\in \mathbb{Z}\to \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi \leftrightarrow \exists j\in \mathbb{Z}\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)$$
13	11 12	anbi12d	$$⊢M\in \mathbb{Z}\to \left(\left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \wedge \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)\leftrightarrow \left(\exists j\in \mathbb{Z}\forall k\in {\mathbb{Z}}_{\ge j}\phi \wedge \exists j\in \mathbb{Z}\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)\right)$$
14	10 13	bitr4id	$$⊢M\in \mathbb{Z}\to \left(\exists j\in \mathbb{Z}\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \wedge \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)\right)$$
15	9 14	bitrd	$$⊢M\in \mathbb{Z}\to \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \wedge \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)\right)$$
16	5 8 15	pm5.21nii	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \wedge \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)$$