Metamath Proof Explorer


Theorem rexanuz3

Description: Combine two different upper integer properties into one, for a single integer. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses rexanuz3.1 j φ
rexanuz3.2 Z = M
rexanuz3.3 φ j Z k j χ
rexanuz3.4 φ j Z k j ψ
rexanuz3.5 k = j χ θ
rexanuz3.6 k = j ψ τ
Assertion rexanuz3 φ j Z θ τ

Proof

Step Hyp Ref Expression
1 rexanuz3.1 j φ
2 rexanuz3.2 Z = M
3 rexanuz3.3 φ j Z k j χ
4 rexanuz3.4 φ j Z k j ψ
5 rexanuz3.5 k = j χ θ
6 rexanuz3.6 k = j ψ τ
7 3 4 jca φ j Z k j χ j Z k j ψ
8 2 rexanuz2 j Z k j χ ψ j Z k j χ j Z k j ψ
9 7 8 sylibr φ j Z k j χ ψ
10 2 eleq2i j Z j M
11 10 biimpi j Z j M
12 eluzelz j M j
13 uzid j j j
14 11 12 13 3syl j Z j j
15 14 adantr j Z k j χ ψ j j
16 simpr j Z k j χ ψ k j χ ψ
17 5 6 anbi12d k = j χ ψ θ τ
18 17 rspcva j j k j χ ψ θ τ
19 15 16 18 syl2anc j Z k j χ ψ θ τ
20 19 adantll φ j Z k j χ ψ θ τ
21 20 ex φ j Z k j χ ψ θ τ
22 21 ex φ j Z k j χ ψ θ τ
23 1 22 reximdai φ j Z k j χ ψ j Z θ τ
24 9 23 mpd φ j Z θ τ