Theorem 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	⊢ Ⅎ 𝑗 𝜑
	rexanuz3.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	rexanuz3.3	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜒 )
	rexanuz3.4	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 )
	rexanuz3.5	⊢ ( 𝑘 = 𝑗 → ( 𝜒 ↔ 𝜃 ) )
	rexanuz3.6	⊢ ( 𝑘 = 𝑗 → ( 𝜓 ↔ 𝜏 ) )
Assertion	rexanuz3	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ( 𝜃 ∧ 𝜏 ) )

Proof

Step	Hyp	Ref	Expression
1		rexanuz3.1	⊢ Ⅎ 𝑗 𝜑
2		rexanuz3.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		rexanuz3.3	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜒 )
4		rexanuz3.4	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 )
5		rexanuz3.5	⊢ ( 𝑘 = 𝑗 → ( 𝜒 ↔ 𝜃 ) )
6		rexanuz3.6	⊢ ( 𝑘 = 𝑗 → ( 𝜓 ↔ 𝜏 ) )
7	3 4	jca	⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜒 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) )
8	2	rexanuz2	⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜒 ∧ 𝜓 ) ↔ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜒 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) )
9	7 8	sylibr	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜒 ∧ 𝜓 ) )
10	2	eleq2i	⊢ ( 𝑗 ∈ 𝑍 ↔ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
11	10	biimpi	⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
12		eluzelz	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℤ )
13		uzid	⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
14	11 12 13	3syl	⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
15	14	adantr	⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜒 ∧ 𝜓 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
16		simpr	⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜒 ∧ 𝜓 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜒 ∧ 𝜓 ) )
17	5 6	anbi12d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜒 ∧ 𝜓 ) ↔ ( 𝜃 ∧ 𝜏 ) ) )
18	17	rspcva	⊢ ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜒 ∧ 𝜓 ) ) → ( 𝜃 ∧ 𝜏 ) )
19	15 16 18	syl2anc	⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜒 ∧ 𝜓 ) ) → ( 𝜃 ∧ 𝜏 ) )
20	19	adantll	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜒 ∧ 𝜓 ) ) → ( 𝜃 ∧ 𝜏 ) )
21	20	ex	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜒 ∧ 𝜓 ) → ( 𝜃 ∧ 𝜏 ) ) )
22	21	ex	⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜒 ∧ 𝜓 ) → ( 𝜃 ∧ 𝜏 ) ) ) )
23	1 22	reximdai	⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜒 ∧ 𝜓 ) → ∃ 𝑗 ∈ 𝑍 ( 𝜃 ∧ 𝜏 ) ) )
24	9 23	mpd	⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ( 𝜃 ∧ 𝜏 ) )