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

Metamath Proof Explorer

Theorem axdc4uz

Description: A version of axdc4 that works on an upper set of integers instead of _om . (Contributed by Mario Carneiro, 8-Jan-2014)

Ref Expression
Hypotheses axdc4uz.1 ⊢ 𝑀 ∈ ℤ
axdc4uz.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion axdc4uz ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝐴 ∧ 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 axdc4uz.1 ⊢ 𝑀 ∈ ℤ
2 axdc4uz.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 eleq2 ⊢ ( 𝑓 = 𝐴 → ( 𝐶 ∈ 𝑓 ↔ 𝐶 ∈ 𝐴 ) )
4 xpeq2 ⊢ ( 𝑓 = 𝐴 → ( 𝑍 × 𝑓 ) = ( 𝑍 × 𝐴 ) )
5 pweq ⊢ ( 𝑓 = 𝐴 → 𝒫 𝑓 = 𝒫 𝐴 )
6 5 difeq1d ⊢ ( 𝑓 = 𝐴 → ( 𝒫 𝑓 ∖ { ∅ } ) = ( 𝒫 𝐴 ∖ { ∅ } ) )
7 4 6 feq23d ⊢ ( 𝑓 = 𝐴 → ( 𝐹 : ( 𝑍 × 𝑓 ) ⟶ ( 𝒫 𝑓 ∖ { ∅ } ) ↔ 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) )
8 3 7 anbi12d ⊢ ( 𝑓 = 𝐴 → ( ( 𝐶 ∈ 𝑓 ∧ 𝐹 : ( 𝑍 × 𝑓 ) ⟶ ( 𝒫 𝑓 ∖ { ∅ } ) ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) ) )
9 feq3 ⊢ ( 𝑓 = 𝐴 → ( 𝑔 : 𝑍 ⟶ 𝑓 ↔ 𝑔 : 𝑍 ⟶ 𝐴 ) )
10 9 3anbi1d ⊢ ( 𝑓 = 𝐴 → ( ( 𝑔 : 𝑍 ⟶ 𝑓 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ↔ ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ) )
11 10 exbidv ⊢ ( 𝑓 = 𝐴 → ( ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝑓 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ↔ ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ) )
12 8 11 imbi12d ⊢ ( 𝑓 = 𝐴 → ( ( ( 𝐶 ∈ 𝑓 ∧ 𝐹 : ( 𝑍 × 𝑓 ) ⟶ ( 𝒫 𝑓 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝑓 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ) ↔ ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ) ) )
13 vex ⊢ 𝑓 ∈ V
14 eqid ⊢ ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 + 1 ) ) , 𝑀 ) ↾ ω ) = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 + 1 ) ) , 𝑀 ) ↾ ω )
15 eqid ⊢ ( 𝑛 ∈ ω , 𝑥 ∈ 𝑓 ↦ ( ( ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 + 1 ) ) , 𝑀 ) ↾ ω ) ‘ 𝑛 ) 𝐹 𝑥 ) ) = ( 𝑛 ∈ ω , 𝑥 ∈ 𝑓 ↦ ( ( ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 + 1 ) ) , 𝑀 ) ↾ ω ) ‘ 𝑛 ) 𝐹 𝑥 ) )
16 1 2 13 14 15 axdc4uzlem ⊢ ( ( 𝐶 ∈ 𝑓 ∧ 𝐹 : ( 𝑍 × 𝑓 ) ⟶ ( 𝒫 𝑓 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝑓 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) )
17 12 16 vtoclg ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐶 ∈ 𝐴 ∧ 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) ) )
18 17 3impib ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝐴 ∧ 𝐹 : ( 𝑍 × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ 𝑔 ( 𝑔 : 𝑍 ⟶ 𝐴 ∧ ( 𝑔 ‘ 𝑀 ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑔 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝑘 𝐹 ( 𝑔 ‘ 𝑘 ) ) ) )