Theorem rexanuz2

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

	Ref	Expression
Hypothesis	rexuz3.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	rexanuz2	⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		rexuz3.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		eluzel2	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
3	2 1	eleq2s	⊢ ( 𝑗 ∈ 𝑍 → 𝑀 ∈ ℤ )
4	3	a1d	⊢ ( 𝑗 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) → 𝑀 ∈ ℤ ) )
5	4	rexlimiv	⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) → 𝑀 ∈ ℤ )
6	3	a1d	⊢ ( 𝑗 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 → 𝑀 ∈ ℤ ) )
7	6	rexlimiv	⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 → 𝑀 ∈ ℤ )
8	7	adantr	⊢ ( ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → 𝑀 ∈ ℤ )
9	1	rexuz3	⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ) )
10		rexanuz	⊢ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) )
11	1	rexuz3	⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) )
12	1	rexuz3	⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) )
13	11 12	anbi12d	⊢ ( 𝑀 ∈ ℤ → ( ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) ↔ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) ) )
14	10 13	bitr4id	⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) ) )
15	9 14	bitrd	⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) ) )
16	5 8 15	pm5.21nii	⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) )