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 Z = M
Assertion rexuz3 M j Z k j φ j k j φ

Proof

Step Hyp Ref Expression
1 rexuz3.1 Z = M
2 ralel k Z k Z
3 fveq2 j = M j = M
4 3 1 eqtr4di j = M j = Z
5 4 raleqdv j = M k j k Z k Z k Z
6 5 rspcev M k Z k Z j k j k Z
7 2 6 mpan2 M j k j k Z
8 7 biantrurd M j k j φ j k j k Z j k j φ
9 1 uztrn2 j Z k j k Z
10 9 a1d j Z k j φ k Z
11 10 ancrd j Z k j φ k Z φ
12 11 ralimdva j Z k j φ k j k Z φ
13 eluzelz j M j
14 13 1 eleq2s j Z j
15 12 14 jctild j Z k j φ j k j k Z φ
16 15 imp j Z k j φ j k j k Z φ
17 uzid j j j
18 simpl k Z φ k Z
19 18 ralimi k j k Z φ k j k Z
20 eleq1w k = j k Z j Z
21 20 rspcva j j k j k Z j Z
22 17 19 21 syl2an j k j k Z φ j Z
23 simpr k Z φ φ
24 23 ralimi k j k Z φ k j φ
25 24 adantl j k j k Z φ k j φ
26 22 25 jca j k j k Z φ j Z k j φ
27 16 26 impbii j Z k j φ j k j k Z φ
28 27 rexbii2 j Z k j φ j k j k Z φ
29 rexanuz j k j k Z φ j k j k Z j k j φ
30 28 29 bitr2i j k j k Z j k j φ j Z k j φ
31 8 30 bitr2di M j Z k j φ j k j φ