rexanuz3

Description: Combine two different upper integer properties into one, for a single integer. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	rexanuz3.1	$⊢ Ⅎ j φ$
	rexanuz3.2	$⊢ Z = ℤ_{\geq M}$
	rexanuz3.3	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} χ$
	rexanuz3.4	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} ψ$
	rexanuz3.5	$⊢ k = j \to (χ \leftrightarrow θ)$
	rexanuz3.6	$⊢ k = j \to (ψ \leftrightarrow τ)$
Assertion	rexanuz3	$⊢ φ \to \exists j \in Z (θ \land τ)$

Proof

Step	Hyp	Ref	Expression
1		rexanuz3.1	$⊢ Ⅎ j φ$
2		rexanuz3.2	$⊢ Z = ℤ_{\geq M}$
3		rexanuz3.3	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} χ$
4		rexanuz3.4	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} ψ$
5		rexanuz3.5	$⊢ k = j \to (χ \leftrightarrow θ)$
6		rexanuz3.6	$⊢ k = j \to (ψ \leftrightarrow τ)$
7	3 4	jca	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} χ \land \exists j \in Z \forall k \in ℤ_{\geq j} ψ)$
8	2	rexanuz2	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} (χ \land ψ) \leftrightarrow (\exists j \in Z \forall k \in ℤ_{\geq j} χ \land \exists j \in Z \forall k \in ℤ_{\geq j} ψ)$
9	7 8	sylibr	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} (χ \land ψ)$
10	2	eleq2i	$⊢ j \in Z \leftrightarrow j \in ℤ_{\geq M}$
11	10	biimpi	$⊢ j \in Z \to j \in ℤ_{\geq M}$
12		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
13		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
14	11 12 13	3syl	$⊢ j \in Z \to j \in ℤ_{\geq j}$
15	14	adantr	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} (χ \land ψ)) \to j \in ℤ_{\geq j}$
16		simpr	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} (χ \land ψ)) \to \forall k \in ℤ_{\geq j} (χ \land ψ)$
17	5 6	anbi12d	$⊢ k = j \to ((χ \land ψ) \leftrightarrow (θ \land τ))$
18	17	rspcva	$⊢ (j \in ℤ_{\geq j} \land \forall k \in ℤ_{\geq j} (χ \land ψ)) \to (θ \land τ)$
19	15 16 18	syl2anc	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} (χ \land ψ)) \to (θ \land τ)$
20	19	adantll	$⊢ ((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} (χ \land ψ)) \to (θ \land τ)$
21	20	ex	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} (χ \land ψ) \to (θ \land τ))$
22	21	ex	$⊢ φ \to (j \in Z \to (\forall k \in ℤ_{\geq j} (χ \land ψ) \to (θ \land τ)))$
23	1 22	reximdai	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (χ \land ψ) \to \exists j \in Z (θ \land τ))$
24	9 23	mpd	$⊢ φ \to \exists j \in Z (θ \land τ)$

Metamath Proof Explorer

Theorem rexanuz3

Proof