This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rexanuz

Description: Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013)

Ref Expression
Assertion rexanuz ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) )

Proof

Step Hyp Ref Expression
1 r19.26 ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) )
2 1 rexbii ⊢ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑗 ∈ ℤ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) )
3 r19.40 ⊢ ( ∃ 𝑗 ∈ ℤ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) )
4 2 3 sylbi ⊢ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) )
5 uzf ⊢ ℤ≥ : ℤ ⟶ 𝒫 ℤ
6 ffn ⊢ ( ℤ≥ : ℤ ⟶ 𝒫 ℤ → ℤ≥ Fn ℤ )
7 raleq ⊢ ( 𝑥 = ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ 𝑥 𝜑 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) )
8 7 rexrn ⊢ ( ℤ≥ Fn ℤ → ( ∃ 𝑥 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑥 𝜑 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) )
9 5 6 8 mp2b ⊢ ( ∃ 𝑥 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑥 𝜑 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 )
10 raleq ⊢ ( 𝑦 = ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ 𝑦 𝜓 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) )
11 10 rexrn ⊢ ( ℤ≥ Fn ℤ → ( ∃ 𝑦 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑦 𝜓 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) )
12 5 6 11 mp2b ⊢ ( ∃ 𝑦 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑦 𝜓 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 )
13 uzin2 ⊢ ( ( 𝑥 ∈ ran ℤ≥ ∧ 𝑦 ∈ ran ℤ≥ ) → ( 𝑥 ∩ 𝑦 ) ∈ ran ℤ≥ )
14 inss1 ⊢ ( 𝑥 ∩ 𝑦 ) ⊆ 𝑥
15 ssralv ⊢ ( ( 𝑥 ∩ 𝑦 ) ⊆ 𝑥 → ( ∀ 𝑘 ∈ 𝑥 𝜑 → ∀ 𝑘 ∈ ( 𝑥 ∩ 𝑦 ) 𝜑 ) )
16 14 15 ax-mp ⊢ ( ∀ 𝑘 ∈ 𝑥 𝜑 → ∀ 𝑘 ∈ ( 𝑥 ∩ 𝑦 ) 𝜑 )
17 inss2 ⊢ ( 𝑥 ∩ 𝑦 ) ⊆ 𝑦
18 ssralv ⊢ ( ( 𝑥 ∩ 𝑦 ) ⊆ 𝑦 → ( ∀ 𝑘 ∈ 𝑦 𝜓 → ∀ 𝑘 ∈ ( 𝑥 ∩ 𝑦 ) 𝜓 ) )
19 17 18 ax-mp ⊢ ( ∀ 𝑘 ∈ 𝑦 𝜓 → ∀ 𝑘 ∈ ( 𝑥 ∩ 𝑦 ) 𝜓 )
20 16 19 anim12i ⊢ ( ( ∀ 𝑘 ∈ 𝑥 𝜑 ∧ ∀ 𝑘 ∈ 𝑦 𝜓 ) → ( ∀ 𝑘 ∈ ( 𝑥 ∩ 𝑦 ) 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑥 ∩ 𝑦 ) 𝜓 ) )
21 r19.26 ⊢ ( ∀ 𝑘 ∈ ( 𝑥 ∩ 𝑦 ) ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑘 ∈ ( 𝑥 ∩ 𝑦 ) 𝜑 ∧ ∀ 𝑘 ∈ ( 𝑥 ∩ 𝑦 ) 𝜓 ) )
22 20 21 sylibr ⊢ ( ( ∀ 𝑘 ∈ 𝑥 𝜑 ∧ ∀ 𝑘 ∈ 𝑦 𝜓 ) → ∀ 𝑘 ∈ ( 𝑥 ∩ 𝑦 ) ( 𝜑 ∧ 𝜓 ) )
23 raleq ⊢ ( 𝑧 = ( 𝑥 ∩ 𝑦 ) → ( ∀ 𝑘 ∈ 𝑧 ( 𝜑 ∧ 𝜓 ) ↔ ∀ 𝑘 ∈ ( 𝑥 ∩ 𝑦 ) ( 𝜑 ∧ 𝜓 ) ) )
24 23 rspcev ⊢ ( ( ( 𝑥 ∩ 𝑦 ) ∈ ran ℤ≥ ∧ ∀ 𝑘 ∈ ( 𝑥 ∩ 𝑦 ) ( 𝜑 ∧ 𝜓 ) ) → ∃ 𝑧 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑧 ( 𝜑 ∧ 𝜓 ) )
25 13 22 24 syl2an ⊢ ( ( ( 𝑥 ∈ ran ℤ≥ ∧ 𝑦 ∈ ran ℤ≥ ) ∧ ( ∀ 𝑘 ∈ 𝑥 𝜑 ∧ ∀ 𝑘 ∈ 𝑦 𝜓 ) ) → ∃ 𝑧 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑧 ( 𝜑 ∧ 𝜓 ) )
26 25 an4s ⊢ ( ( ( 𝑥 ∈ ran ℤ≥ ∧ ∀ 𝑘 ∈ 𝑥 𝜑 ) ∧ ( 𝑦 ∈ ran ℤ≥ ∧ ∀ 𝑘 ∈ 𝑦 𝜓 ) ) → ∃ 𝑧 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑧 ( 𝜑 ∧ 𝜓 ) )
27 26 rexlimdvaa ⊢ ( ( 𝑥 ∈ ran ℤ≥ ∧ ∀ 𝑘 ∈ 𝑥 𝜑 ) → ( ∃ 𝑦 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑦 𝜓 → ∃ 𝑧 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑧 ( 𝜑 ∧ 𝜓 ) ) )
28 27 rexlimiva ⊢ ( ∃ 𝑥 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑥 𝜑 → ( ∃ 𝑦 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑦 𝜓 → ∃ 𝑧 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑧 ( 𝜑 ∧ 𝜓 ) ) )
29 28 imp ⊢ ( ( ∃ 𝑥 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑥 𝜑 ∧ ∃ 𝑦 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑦 𝜓 ) → ∃ 𝑧 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑧 ( 𝜑 ∧ 𝜓 ) )
30 raleq ⊢ ( 𝑧 = ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ 𝑧 ( 𝜑 ∧ 𝜓 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ) )
31 30 rexrn ⊢ ( ℤ≥ Fn ℤ → ( ∃ 𝑧 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑧 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ) )
32 5 6 31 mp2b ⊢ ( ∃ 𝑧 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑧 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) )
33 29 32 sylib ⊢ ( ( ∃ 𝑥 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑥 𝜑 ∧ ∃ 𝑦 ∈ ran ℤ≥ ∀ 𝑘 ∈ 𝑦 𝜓 ) → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) )
34 9 12 33 syl2anbr ⊢ ( ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) )
35 4 34 impbii ⊢ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) )