Metamath Proof Explorer

Theorem rexuz3

Description: Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013)

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

Proof

Step Hyp Ref Expression
1 rexuz3.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ralel ⊢ ∀ 𝑘 ∈ 𝑍 𝑘 ∈ 𝑍
3 fveq2 ⊢ ( 𝑗 = 𝑀 → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ 𝑀 ) )
4 3 1 eqtr4di ⊢ ( 𝑗 = 𝑀 → ( ℤ≥ ‘ 𝑗 ) = 𝑍 )
5 4 raleqdv ⊢ ( 𝑗 = 𝑀 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ 𝑍 ↔ ∀ 𝑘 ∈ 𝑍 𝑘 ∈ 𝑍 ) )
6 5 rspcev ⊢ ( ( 𝑀 ∈ ℤ ∧ ∀ 𝑘 ∈ 𝑍 𝑘 ∈ 𝑍 ) → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ 𝑍 )
7 2 6 mpan2 ⊢ ( 𝑀 ∈ ℤ → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ 𝑍 )
8 7 biantrurd ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ 𝑍 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ) )
9 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
10 9 a1d ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝜑 → 𝑘 ∈ 𝑍 ) )
11 10 ancrd ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝜑 → ( 𝑘 ∈ 𝑍 ∧ 𝜑 ) ) )
12 11 ralimdva ⊢ ( 𝑗 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ 𝑍 ∧ 𝜑 ) ) )
13 eluzelz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℤ )
14 13 1 eleq2s ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ )
15 12 14 jctild ⊢ ( 𝑗 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 → ( 𝑗 ∈ ℤ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ 𝑍 ∧ 𝜑 ) ) ) )
16 15 imp ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) → ( 𝑗 ∈ ℤ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ 𝑍 ∧ 𝜑 ) ) )
17 uzid ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
18 simpl ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝜑 ) → 𝑘 ∈ 𝑍 )
19 18 ralimi ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ 𝑍 ∧ 𝜑 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ 𝑍 )
20 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
21 20 rspcva ⊢ ( ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
22 17 19 21 syl2an ⊢ ( ( 𝑗 ∈ ℤ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ 𝑍 ∧ 𝜑 ) ) → 𝑗 ∈ 𝑍 )
23 simpr ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝜑 ) → 𝜑 )
24 23 ralimi ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ 𝑍 ∧ 𝜑 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 )
25 24 adantl ⊢ ( ( 𝑗 ∈ ℤ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ 𝑍 ∧ 𝜑 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 )
26 22 25 jca ⊢ ( ( 𝑗 ∈ ℤ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ 𝑍 ∧ 𝜑 ) ) → ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) )
27 16 26 impbii ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ↔ ( 𝑗 ∈ ℤ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ 𝑍 ∧ 𝜑 ) ) )
28 27 rexbii2 ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ 𝑍 ∧ 𝜑 ) )
29 rexanuz ⊢ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ 𝑍 ∧ 𝜑 ) ↔ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ 𝑍 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) )
30 28 29 bitr2i ⊢ ( ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑘 ∈ 𝑍 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 )
31 8 30 bitr2di ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) )