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 ( 𝑀 ∈ ℤ → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) 𝜑 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) 𝜑 ) )