Metamath Proof Explorer


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 ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝜑𝜓 ) ↔ ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) 𝜑 ∧ ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) 𝜓 ) )