rexanuz

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

		Ref	Expression
	Assertion	rexanuz	$⊢ \exists j \in ℤ \forall k \in ℤ_{\geq j} (φ \land ψ) \leftrightarrow (\exists j \in ℤ \forall k \in ℤ_{\geq j} φ \land \exists j \in ℤ \forall k \in ℤ_{\geq j} ψ)$

Proof

Step	Hyp	Ref	Expression
1		r19.26	$⊢ \forall k \in ℤ_{\geq j} (φ \land ψ) \leftrightarrow (\forall k \in ℤ_{\geq j} φ \land \forall k \in ℤ_{\geq j} ψ)$
2	1	rexbii	$⊢ \exists j \in ℤ \forall k \in ℤ_{\geq j} (φ \land ψ) \leftrightarrow \exists j \in ℤ (\forall k \in ℤ_{\geq j} φ \land \forall k \in ℤ_{\geq j} ψ)$
3		r19.40	$⊢ \exists j \in ℤ (\forall k \in ℤ_{\geq j} φ \land \forall k \in ℤ_{\geq j} ψ) \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} φ \land \exists j \in ℤ \forall k \in ℤ_{\geq j} ψ)$
4	2 3	sylbi	$⊢ \exists j \in ℤ \forall k \in ℤ_{\geq j} (φ \land ψ) \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} φ \land \exists j \in ℤ \forall k \in ℤ_{\geq j} ψ)$
5		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
6		ffn	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ \to ℤ_{\geq} Fn ℤ$
7		raleq	$⊢ x = ℤ_{\geq j} \to (\forall k \in x φ \leftrightarrow \forall k \in ℤ_{\geq j} φ)$
8	7	rexrn	$⊢ ℤ_{\geq} Fn ℤ \to (\exists x \in ran ℤ_{\geq} \forall k \in x φ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} φ)$
9	5 6 8	mp2b	$⊢ \exists x \in ran ℤ_{\geq} \forall k \in x φ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} φ$
10		raleq	$⊢ y = ℤ_{\geq j} \to (\forall k \in y ψ \leftrightarrow \forall k \in ℤ_{\geq j} ψ)$
11	10	rexrn	$⊢ ℤ_{\geq} Fn ℤ \to (\exists y \in ran ℤ_{\geq} \forall k \in y ψ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} ψ)$
12	5 6 11	mp2b	$⊢ \exists y \in ran ℤ_{\geq} \forall k \in y ψ \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} ψ$
13		uzin2	$⊢ (x \in ran ℤ_{\geq} \land y \in ran ℤ_{\geq}) \to x \cap y \in ran ℤ_{\geq}$
14		inss1	$⊢ x \cap y \subseteq x$
15		ssralv	$⊢ x \cap y \subseteq x \to (\forall k \in x φ \to \forall k \in (x \cap y) φ)$
16	14 15	ax-mp	$⊢ \forall k \in x φ \to \forall k \in (x \cap y) φ$
17		inss2	$⊢ x \cap y \subseteq y$
18		ssralv	$⊢ x \cap y \subseteq y \to (\forall k \in y ψ \to \forall k \in (x \cap y) ψ)$
19	17 18	ax-mp	$⊢ \forall k \in y ψ \to \forall k \in (x \cap y) ψ$
20	16 19	anim12i	$⊢ (\forall k \in x φ \land \forall k \in y ψ) \to (\forall k \in (x \cap y) φ \land \forall k \in (x \cap y) ψ)$
21		r19.26	$⊢ \forall k \in (x \cap y) (φ \land ψ) \leftrightarrow (\forall k \in (x \cap y) φ \land \forall k \in (x \cap y) ψ)$
22	20 21	sylibr	$⊢ (\forall k \in x φ \land \forall k \in y ψ) \to \forall k \in (x \cap y) (φ \land ψ)$
23		raleq	$⊢ z = x \cap y \to (\forall k \in z (φ \land ψ) \leftrightarrow \forall k \in (x \cap y) (φ \land ψ))$
24	23	rspcev	$⊢ (x \cap y \in ran ℤ_{\geq} \land \forall k \in (x \cap y) (φ \land ψ)) \to \exists z \in ran ℤ_{\geq} \forall k \in z (φ \land ψ)$
25	13 22 24	syl2an	$⊢ ((x \in ran ℤ_{\geq} \land y \in ran ℤ_{\geq}) \land (\forall k \in x φ \land \forall k \in y ψ)) \to \exists z \in ran ℤ_{\geq} \forall k \in z (φ \land ψ)$
26	25	an4s	$⊢ ((x \in ran ℤ_{\geq} \land \forall k \in x φ) \land (y \in ran ℤ_{\geq} \land \forall k \in y ψ)) \to \exists z \in ran ℤ_{\geq} \forall k \in z (φ \land ψ)$
27	26	rexlimdvaa	$⊢ (x \in ran ℤ_{\geq} \land \forall k \in x φ) \to (\exists y \in ran ℤ_{\geq} \forall k \in y ψ \to \exists z \in ran ℤ_{\geq} \forall k \in z (φ \land ψ))$
28	27	rexlimiva	$⊢ \exists x \in ran ℤ_{\geq} \forall k \in x φ \to (\exists y \in ran ℤ_{\geq} \forall k \in y ψ \to \exists z \in ran ℤ_{\geq} \forall k \in z (φ \land ψ))$
29	28	imp	$⊢ (\exists x \in ran ℤ_{\geq} \forall k \in x φ \land \exists y \in ran ℤ_{\geq} \forall k \in y ψ) \to \exists z \in ran ℤ_{\geq} \forall k \in z (φ \land ψ)$
30		raleq	$⊢ z = ℤ_{\geq j} \to (\forall k \in z (φ \land ψ) \leftrightarrow \forall k \in ℤ_{\geq j} (φ \land ψ))$
31	30	rexrn	$⊢ ℤ_{\geq} Fn ℤ \to (\exists z \in ran ℤ_{\geq} \forall k \in z (φ \land ψ) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (φ \land ψ))$
32	5 6 31	mp2b	$⊢ \exists z \in ran ℤ_{\geq} \forall k \in z (φ \land ψ) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (φ \land ψ)$
33	29 32	sylib	$⊢ (\exists x \in ran ℤ_{\geq} \forall k \in x φ \land \exists y \in ran ℤ_{\geq} \forall k \in y ψ) \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (φ \land ψ)$
34	9 12 33	syl2anbr	$⊢ (\exists j \in ℤ \forall k \in ℤ_{\geq j} φ \land \exists j \in ℤ \forall k \in ℤ_{\geq j} ψ) \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (φ \land ψ)$
35	4 34	impbii	$⊢ \exists j \in ℤ \forall k \in ℤ_{\geq j} (φ \land ψ) \leftrightarrow (\exists j \in ℤ \forall k \in ℤ_{\geq j} φ \land \exists j \in ℤ \forall k \in ℤ_{\geq j} ψ)$

Metamath Proof Explorer

Theorem rexanuz

Proof